Skip to content

Commit

Permalink
Fix overlap queries in Alias Analysis (#753)
Browse files Browse the repository at this point in the history
  • Loading branch information
@xeren
xeren authored Oct 15, 2024
1 parent 253a119 commit c738679
Show file tree
Hide file tree
Showing 2 changed files with 101 additions and 38 deletions.
84 changes: 49 additions & 35 deletions ...c/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -422,7 +421,7 @@ private static final class Variable {
// Visualized as outgoing edges.
private final List<StoreEdge> stores = new ArrayList<>();
// All variables that have a direct (includes/loads/stores) link to this.
private final Set<Variable> seeAlso = new HashSet<>();
private final Set<Variable> seeAlso = new LinkedHashSet<>();
// If nonnull, this variable represents that object's base address.
private final MemoryObject object;
// For visualization.
Expand Down Expand Up @@ -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<Integer> 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<Integer> alignment) {
return new DerivedVariable(base, new Modifier(offset, alignment));
return new DerivedVariable(base, modifier(offset, alignment));
}

private static IncludeEdge includeEdge(DerivedVariable variable) {
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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<Integer> alignment) {
return reduceGCD(Lists.transform(alignment, Math::abs));
private static int singleAlignment(List<Integer> alignment) {
return alignment.size() != 1 ? 0 : alignment.get(0);
}

// Computes the greatest common divisor of the operands.
Expand All @@ -778,6 +773,17 @@ private static List<Integer> compose(List<Integer> left, List<Integer> 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<Integer> result = new ArrayList<>();
for (final Integer i : left) {
Expand All @@ -790,9 +796,16 @@ private static List<Integer> compose(List<Integer> left, List<Integer> right) {
result.add(j);
}
}
sort(result);
return result;
}

private static void sort(List<Integer> 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<Integer> candidates, boolean strict) {
for (final Integer candidate : candidates) {
Expand All @@ -804,7 +817,7 @@ private static boolean hasNoDivisorsInList(int value, List<Integer> 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.
Expand Down Expand Up @@ -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;
}
Expand Down Expand Up @@ -914,8 +928,8 @@ private DerivedVariable getPhiNodeVariable(Register register, RegReader reader)

private static final class Collector implements ExpressionVisitor<Result> {

final Set<MemoryObject> address = new HashSet<>();
final Set<Register> register = new HashSet<>();
final Set<MemoryObject> address = new LinkedHashSet<>();
final Set<Register> register = new LinkedHashSet<>();

@Override
public Result visitExpression(Expression expr) {
Expand Down
55 changes: 52 additions & 3 deletions dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java
View file
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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<Integer> 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());
}
Expand Down

0 comments on commit c738679

Please sign in to comment.