diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java index 73c626da7d..8a13f70d7c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java @@ -17,7 +17,6 @@ import com.dat3m.dartagnan.witness.graphviz.Graphviz; import com.google.common.base.Supplier; import com.google.common.base.Suppliers; -import com.google.common.collect.Lists; import com.google.common.math.IntMath; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -422,7 +421,7 @@ private static final class Variable { // Visualized as outgoing edges. private final List stores = new ArrayList<>(); // All variables that have a direct (includes/loads/stores) link to this. - private final Set seeAlso = new HashSet<>(); + private final Set seeAlso = new LinkedHashSet<>(); // If nonnull, this variable represents that object's base address. private final MemoryObject object; // For visualization. @@ -458,12 +457,17 @@ private static boolean isTrivial(Modifier modifier) { private static final Modifier TRIVIAL_MODIFIER = new Modifier(0, List.of()); + private static Modifier modifier(int offset, List alignment) { + int a = singleAlignment(alignment); + return new Modifier(a >= 0 ? offset : offset % -a, alignment); + } + private static DerivedVariable derive(Variable base) { return new DerivedVariable(base, TRIVIAL_MODIFIER); } private static DerivedVariable derive(Variable base, int offset, List alignment) { - return new DerivedVariable(base, new Modifier(offset, alignment)); + return new DerivedVariable(base, modifier(offset, alignment)); } private static IncludeEdge includeEdge(DerivedVariable variable) { @@ -683,30 +687,22 @@ private boolean includes(Modifier left, Modifier right) { if (left.alignment.isEmpty()) { return right.alignment.isEmpty() && offset == 0; } - for (final Integer a : left.alignment) { - if (a < 0) { - final int l = reduceAbsGCD(left.alignment); - final int r = reduceAbsGCD(right.alignment); - return offset % l == 0 && r % l == 0; - } - } - for (final Integer a : right.alignment) { - if (a < 0) { - final int l = reduceAbsGCD(left.alignment); - final int r = reduceAbsGCD(right.alignment); - return offset % l == 0 && r % l == 0; - } + // Case of unbounded dynamic indexes. + int leftAlignment = singleAlignment(left.alignment); + int rightAlignment = singleAlignment(right.alignment); + if (leftAlignment < 0 || rightAlignment < 0) { + int l = leftAlignment < 0 ? -leftAlignment : reduceGCD(left.alignment); + int r = rightAlignment < 0 ? -rightAlignment : reduceGCD(right.alignment); + return offset % l == 0 && r % l == 0; } - // FIXME assumes that dynamic indexes used here only have non-negative values. - // This cannot be used when a negative alignment occurs, because the analysis would not terminate. + // Case of a single non-negative dynamic index. if (left.alignment.size() == 1) { - final int alignment = Math.abs(left.alignment.get(0)); for (final Integer a : right.alignment) { - if (a % alignment != 0) { + if (a % leftAlignment != 0) { return false; } } - return offset % alignment == 0 && offset >= 0; + return offset % leftAlignment == 0 && offset >= 0; } // Case of multiple dynamic indexes with pairwise indivisible alignments. final int gcd = IntMath.gcd(reduceGCD(right.alignment), Math.abs(offset)); @@ -740,22 +736,21 @@ private boolean includes(Modifier left, Modifier right) { private static boolean overlaps(Modifier l, Modifier r) { // exists non-negative integers x, y with l.offset + x * l.alignment == r.offset + y * r.alignment final int offset = r.offset - l.offset; - final int left = reduceAbsGCD(l.alignment); - final int right = reduceAbsGCD(r.alignment); + final int leftAlignment = singleAlignment(l.alignment); + final int rightAlignment = singleAlignment(r.alignment); + final int left = leftAlignment < 0 ? -leftAlignment : reduceGCD(l.alignment); + final int right = rightAlignment < 0 ? -rightAlignment : reduceGCD(r.alignment); if (left == 0 && right == 0) { return offset == 0; } final int divisor = left == 0 ? right : right == 0 ? left : IntMath.gcd(left, right); - final boolean nonNegativeIndexes = left == 0 ? offset <= 0 : right != 0 || offset >= 0; - return nonNegativeIndexes && offset % divisor == 0; + final boolean leftDirectedTowardsRight = right != 0 || leftAlignment < 0 || offset >= 0; + final boolean rightDirectedTowardsLeft = left != 0 || rightAlignment < 0 || offset <= 0; + return leftDirectedTowardsRight && rightDirectedTowardsLeft && offset % divisor == 0; } - // Computes the greatest common divisor of the absolute values of the operands. - // This gets called only if there is at least one negative dynamic offset. - // Positive values assume non-negative multipliers and thus enable the precision of the previous analysis. - // Negative values indicate that the multiplier can also be negative. - private static int reduceAbsGCD(List alignment) { - return reduceGCD(Lists.transform(alignment, Math::abs)); + private static int singleAlignment(List alignment) { + return alignment.size() != 1 ? 0 : alignment.get(0); } // Computes the greatest common divisor of the operands. @@ -778,6 +773,17 @@ private static List compose(List left, List right) { if (left == TOP || right == TOP) { return TOP; } + // Negative values are unrestricted and compose always. + // Therefore, each list shall either contain a single negative value, or only positive values. + int leftAlignment = singleAlignment(left); + int rightAlignment = singleAlignment(right); + if (leftAlignment < 0 || rightAlignment < 0) { + int alignment = leftAlignment < 0 ? -leftAlignment : -rightAlignment; + for (Integer other : leftAlignment < 0 ? right : left) { + alignment = IntMath.gcd(alignment, Math.abs(other)); + } + return List.of(-alignment); + } // assert left and right each consist of pairwise indivisible positives final List result = new ArrayList<>(); for (final Integer i : left) { @@ -790,9 +796,16 @@ private static List compose(List left, List right) { result.add(j); } } + sort(result); return result; } + private static void sort(List alignment) { + if (alignment.size() > 1) { + Collections.sort(alignment); + } + } + // Checks if value is no multiple of any element in the list. private static boolean hasNoDivisorsInList(int value, List candidates, boolean strict) { for (final Integer candidate : candidates) { @@ -804,7 +817,7 @@ private static boolean hasNoDivisorsInList(int value, List candidates, } private static Modifier compose(Modifier left, Modifier right) { - return new Modifier(left.offset + right.offset, compose(left.alignment, right.alignment)); + return modifier(left.offset + right.offset, compose(left.alignment, right.alignment)); } // Adds a single value to a set of dynamic offsets. @@ -862,7 +875,8 @@ private DerivedVariable getResultVariable(Expression expression, RegReader reade if (result != null && (result.address != null || result.register != null)) { final DerivedVariable base = result.address != null ? derive(objectVariables.get(result.address)) : getPhiNodeVariable(result.register, reader); - main = compose(base, new Modifier(result.offset.intValue(), result.alignment)); + sort(result.alignment); + main = compose(base, modifier(result.offset.intValue(), result.alignment)); } else { main = null; } @@ -914,8 +928,8 @@ private DerivedVariable getPhiNodeVariable(Register register, RegReader reader) private static final class Collector implements ExpressionVisitor { - final Set address = new HashSet<>(); - final Set register = new HashSet<>(); + final Set address = new LinkedHashSet<>(); + final Set register = new LinkedHashSet<>(); @Override public Result visitExpression(Expression expr) { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index fea312ebc5..36c3fdb8c8 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -1,11 +1,14 @@ package com.dat3m.dartagnan.miscellaneous; import com.dat3m.dartagnan.configuration.Alias; +import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.parsers.cat.ParserCat; +import com.dat3m.dartagnan.parsers.program.ProgramParser; import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Program.SourceLanguage; @@ -26,16 +29,27 @@ import com.dat3m.dartagnan.program.processing.ProcessingManager; import com.dat3m.dartagnan.program.processing.compilation.Compilation; import com.dat3m.dartagnan.verification.Context; +import com.dat3m.dartagnan.verification.VerificationTask; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.Wmm; +import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import org.junit.Test; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; +import java.io.File; +import java.util.EnumSet; +import java.util.LinkedList; import java.util.List; import static com.dat3m.dartagnan.configuration.Alias.*; -import static com.dat3m.dartagnan.configuration.OptionNames.ALIAS_METHOD; -import static com.dat3m.dartagnan.configuration.OptionNames.REACHING_DEFINITIONS_METHOD; +import static com.dat3m.dartagnan.configuration.OptionNames.*; +import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; import static com.dat3m.dartagnan.program.event.EventFactory.*; +import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; +import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; +import static com.dat3m.dartagnan.verification.solving.ModelChecker.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.LOC; import static org.junit.Assert.*; public class AnalysisTest { @@ -237,7 +251,7 @@ public void fieldinsensitive0() throws InvalidConfigurationException { @Test public void full0() throws InvalidConfigurationException { - program0(FULL, NONE, MAY, NONE, NONE, NONE, NONE); + program0(FULL, NONE, MAY, MAY, NONE, NONE, NONE); } private void program0(Alias method, Result... expect) throws InvalidConfigurationException { @@ -659,6 +673,41 @@ private void assertAlias(Result expect, AliasAnalysis a, MemoryCoreEvent x, Memo } } + /* + * This test may fail to show the presence of an error immediately. + * When it fails during a merge, consider repeating it on the head of the target branch. + */ + @Test + public void aliasAnalysisDeterminism() throws Exception { + final String programPath = getTestResourcePath("libvsync/bounded_mpmc_check_empty-opt.ll"); + final String modelPath = "cat/c11.cat"; + final int ITERATIONS = 10; + final Program program = new ProgramParser().parse(new File(programPath)); + final Wmm wmm = new ParserCat().parse(new File(getRootPath(modelPath))); + final Configuration config = Configuration.builder() + .setOption(ENABLE_EXTENDED_RELATION_ANALYSIS, "false") + .build(); + final VerificationTask task = VerificationTask.builder() + .withConfig(config) + .withBound(1) + .withTarget(Arch.C11) + .build(program, wmm, EnumSet.of(PROGRAM_SPEC)); + wmm.configureAll(task.getConfig()); + preprocessProgram(task, task.getConfig()); + final Relation loc = wmm.getRelation(LOC); + final List sizes = new LinkedList<>(); + for (int i = 0; i < ITERATIONS; i++) { + final Context context = Context.create(); + performStaticProgramAnalyses(task, context, config); + performStaticWmmAnalyses(task, context, config); + final RelationAnalysis relationAnalysis = context.get(RelationAnalysis.class); + sizes.add(relationAnalysis.getKnowledge(loc).getMaySet().size()); + } + for (int i = 1; i < ITERATIONS; i++) { + assertEquals(sizes.get(i - 1), sizes.get(i)); + } + } + private void assertList(List results, Object... expected) { assertArrayEquals(expected, results.toArray()); }