diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Alias.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Alias.java index ef41f71f62..50793f9614 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Alias.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Alias.java @@ -4,15 +4,15 @@ public enum Alias implements OptionInterface { // For comparison reasons, we might want to add a NONE method with may = true, must = false - FIELD_SENSITIVE, FIELD_INSENSITIVE; + FIELD_SENSITIVE, FIELD_INSENSITIVE, FULL; public static Alias getDefault() { - return FIELD_SENSITIVE; + return FULL; } // Used to decide the order shown by the selector in the UI public static Alias[] orderedValues() { - Alias[] order = { FIELD_SENSITIVE, FIELD_INSENSITIVE }; + Alias[] order = { FIELD_SENSITIVE, FIELD_INSENSITIVE, FULL }; // Be sure no element is missing assert(Arrays.asList(order).containsAll(Arrays.asList(values()))); return order; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index cdede24330..ab6b222fce 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -47,6 +47,7 @@ public class OptionNames { public static final String ALIAS_GRAPHVIZ = "program.analysis.generateAliasGraph"; public static final String ALIAS_GRAPHVIZ_SPLIT_BY_THREAD = "program.analysis.generateAliasGraph.splitByThread"; public static final String ALIAS_GRAPHVIZ_SHOW_ALL = "program.analysis.generateAliasGraph.showAllEvents"; + public static final String ALIAS_GRAPHVIZ_INTERNAL = "program.analysis.generateAliasGraph.internal"; public static final String ALWAYS_SPLIT_ON_JUMPS = "program.analysis.cf.alwaysSplitOnJump"; public static final String MERGE_BRANCHES = "program.analysis.cf.mergeBranches"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 397d69712c..5bd4b88e7d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -265,7 +265,7 @@ public BooleanFormula encodeFinalRegisterValues() { for(Map.Entry e : dep.finalWriters().entrySet()) { final Formula value = context.encodeFinalExpression(e.getKey()); final Dependency.State state = e.getValue(); - final List writers = state.may; + final List writers = state.may; if(initializeRegisters && !state.initialized) { List clause = new ArrayList<>(); clause.add(context.equalZero(value)); @@ -275,9 +275,9 @@ public BooleanFormula encodeFinalRegisterValues() { enc.add(bmgr.or(clause)); } for(int i = 0; i < writers.size(); i++) { - final Event writer = writers.get(i); + final RegWriter writer = writers.get(i); List clause = new ArrayList<>(); - clause.add(context.equal(value, context.result((RegWriter) writer))); + clause.add(context.equal(value, context.result(writer))); clause.add(bmgr.not(context.execution(writer))); for(Event w : writers.subList(i + 1, writers.size())) { if(!exec.areMutuallyExclusive(writer, w)) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java index ca52b02483..5faa5a7c2b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java @@ -146,7 +146,7 @@ private void process(Thread thread, ExecutionAnalysis exec) { if (event.cfImpliesExec()) { state.removeIf(e -> e.register.equals(register)); } - state.add(new Writer(register, event)); + state.add(new Writer(register, rw)); } //copy state, if branching if (event instanceof CondJump jump) { @@ -170,18 +170,18 @@ private void process(Thread thread, ExecutionAnalysis exec) { } private static State process(Event reader, Set state, Register register, ExecutionAnalysis exec) { - List candidates = state.stream() + List candidates = state.stream() .filter(e -> e.register.equals(register)) .map(e -> e.event) .filter(e -> reader == null || !exec.areMutuallyExclusive(reader, e)) .toList(); //NOTE if candidates is empty, the reader is unreachable - List mays = candidates.stream() + List mays = candidates.stream() .filter(Objects::nonNull) .sorted(Comparator.comparingInt(Event::getGlobalId)) .collect(Collectors.toCollection(ArrayList::new)); int end = mays.size(); - List musts = range(0, end) + List musts = range(0, end) .filter(i -> mays.subList(i + 1, end).stream().allMatch(j -> exec.areMutuallyExclusive(mays.get(i), j))) .mapToObj(mays::get) .collect(toList()); @@ -190,9 +190,9 @@ private static State process(Event reader, Set state, Register register, private static final class Writer { final Register register; - final Event event; + final RegWriter event; - Writer(Register r, Event e) { + Writer(Register r, RegWriter e) { register = checkNotNull(r); event = e; } @@ -226,15 +226,15 @@ public static final class State { * Complete, but unsound, program-ordered list of direct providers for the register: * If there is a program execution where an event of the program was the latest writer, that event is contained in this list. */ - public final List may; + public final List may; /** * Sound, but incomplete, program-ordered list of direct providers with no overwriting event in between: * Each event in this list will be the latest writer in any execution that contains that event. */ - public final List must; + public final List must; - private State(boolean initialized, List may, List must) { + private State(boolean initialized, List may, List must) { verify(new HashSet<>(may).containsAll(must), "Each must-writer must also be a may-writer."); verify(may.isEmpty() || must.contains(may.get(may.size() - 1)), "The last may-writer must also be a must-writer."); this.initialized = initialized; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java index 41db29a1b8..b9f46fc6da 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java @@ -9,6 +9,7 @@ import com.dat3m.dartagnan.program.event.metadata.SourceLocation; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.utils.visualization.Graphviz; +import com.dat3m.dartagnan.verification.Context; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; @@ -32,21 +33,15 @@ public interface AliasAnalysis { boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b); - static AliasAnalysis fromConfig(Program program, Configuration config) throws InvalidConfigurationException { + static AliasAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException { Config c = new Config(config); - logger.info("Selected alias analysis: " + c.method); - AliasAnalysis a; + logger.info("Selected alias analysis: {}", c.method); long t0 = System.currentTimeMillis(); - switch (c.method) { - case FIELD_SENSITIVE: - a = FieldSensitiveAndersen.fromConfig(program, config); - break; - case FIELD_INSENSITIVE: - a = AndersenAliasAnalysis.fromConfig(program, config); - break; - default: - throw new UnsupportedOperationException("Alias method not recognized"); - } + AliasAnalysis a = switch (c.method) { + case FIELD_SENSITIVE -> FieldSensitiveAndersen.fromConfig(program, config); + case FIELD_INSENSITIVE -> AndersenAliasAnalysis.fromConfig(program, config); + case FULL -> InclusionBasedPointerAnalysis.fromConfig(program, analysisContext, c); + }; a = new CombinedAliasAnalysis(a, EqualityAliasAnalysis.fromConfig(program, config)); if (Arch.supportsVirtualAddressing(program.getArch())) { a = VirtualAliasAnalysis.wrap(a); @@ -64,7 +59,7 @@ static AliasAnalysis fromConfig(Program program, Configuration config) throws In final class Config { @Option(name = ALIAS_METHOD, description = "General type of analysis that approximates the 'loc' relationship between memory events.") - private Alias method = Alias.FIELD_SENSITIVE; + private Alias method = Alias.getDefault(); @Option(name = ALIAS_GRAPHVIZ, description = "If 'true', stores the results of the alias analysis as a PNG image." + @@ -74,15 +69,23 @@ final class Config { @Option(name = ALIAS_GRAPHVIZ_SPLIT_BY_THREAD, description = "Controls which event sets are represented by nodes in the graph output." + " If 'true', nodes represent events of the same thread and source location." + - " If 'false', nodes represent events of just the same source location." + " Requires '" + - ALIAS_GRAPHVIZ + "=true'." + " Defaults to 'false'.", secure = true) + " If 'false', nodes represent events of just the same source location." + + " Requires '" + ALIAS_GRAPHVIZ + "=true'." + + " Defaults to 'false'.", secure = true) private boolean graphvizSplitByThread; @Option(name = ALIAS_GRAPHVIZ_SHOW_ALL, - description = "If 'true', the graph representation contains even initializations." + " Requires '" + - ALIAS_GRAPHVIZ + "=true'." + " Defaults to 'false'.", secure = true) + description = "If 'true', the graph representation contains even initializations." + + " Requires '" + ALIAS_GRAPHVIZ + "=true'." + + " Defaults to 'false'.", secure = true) private boolean graphvizShowAll; + @Option(name = ALIAS_GRAPHVIZ_INTERNAL, + description = "If 'true' and supported, the graph shows an internal representation." + + " Requires '" + ALIAS_GRAPHVIZ + "=true'." + + " Defaults to 'false'.", secure = true) + boolean graphvizInternal; + private Config(Configuration config) throws InvalidConfigurationException { config.inject(this); } @@ -107,9 +110,19 @@ public boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b) { public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) { return a1.mayAlias(a, b) && a2.mayAlias(a, b); } + + @Override + public Graphviz getGraphVisualization() { + return a1.getGraphVisualization(); + } } - private void generateGraph(Program program, Config configuration) { + //this should be protected + default Graphviz getGraphVisualization() { + return null; + } + + private Graphviz defaultGraph(Program program, Config configuration) { // Nodes represent sets of events. // A solid line marks the existence of events that must alias. // A dashed line marks the existence of events that may alias. @@ -144,7 +157,12 @@ private void generateGraph(Program program, Config configuration) { graphviz.addEdges(mustGraph); graphviz.end(); graphviz.end(); + return graphviz; + } + private void generateGraph(Program program, Config configuration) { + final Graphviz internalGraph = configuration.graphvizInternal ? getGraphVisualization() : null; + final Graphviz graphviz = internalGraph != null ? internalGraph : defaultGraph(program, configuration); // Generates the .dot file and convert into the .png file. String programName = program.getName(); String programBase = programName.substring(0, programName.lastIndexOf('.')); 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 new file mode 100644 index 0000000000..975355638c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java @@ -0,0 +1,976 @@ +package com.dat3m.dartagnan.program.analysis.alias; + +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionVisitor; +import com.dat3m.dartagnan.expression.integers.*; +import com.dat3m.dartagnan.expression.misc.ITEExpr; +import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.analysis.Dependency; +import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument; +import com.dat3m.dartagnan.program.memory.MemoryObject; +import com.dat3m.dartagnan.utils.visualization.Graphviz; +import com.dat3m.dartagnan.verification.Context; +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; + +import java.math.BigInteger; +import java.util.*; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Verify.verify; + +/** + * Offset- and alignment-enhanced inclusion-based pointer analysis based on Andersen's. + * This implementation is insensitive to control-flow, but field-sensitive. + */ +/* + The analysis constructs a directed inclusion graph over expressions of the program. + The nodes abstractly represent the values an expression (at a program location) could take over all executions. + There is a node (also called variable in the code) for each memory object (addr), two for each Local (result and rhs), Load (result and addr), and Store (addr and value). + These nodes are not just per expression but also per program location to achieve an SSA-like form (*). + + Edges between two nodes A and B describe one of three relationships: + (1) An edge "A -f_includes-> B" means that "f(A) \subseteq B" holds (where A/B are understood as sets of values). + Rather than arbitrary functions "f", we use multi-linear expressions "f(A) = A + k1*x1 + k2*x2 + ... kn*xn + o" where ki and o are constants. + For simplicity, we write "k*x + o" where k=(k1,...,kn) and x=(x1,...,xn) are understood as vectors, and drop the _includes suffix (i.e. write A -f-> B). + The (sub)expression "k*x + o" describes the set of values {k*x + o | x \in Z^n} that can be obtained by varying x freely (**). + (2) An edge "A -stores-> B" means that there exists a store that stores at address-expression A the value-expression B. + (3) An edge "A -loads-> R" means that there exists a load that loads from address-expression A and puts its result into R (R is the node of a register). + + Initially, the graph has the following edges + - For every "store(A, V)" event, it has a "A -stores-> V" edge + - For every "R = load(A)" event, it has a "A -loads-> R" edge. + - For every assignment "R := B + k*x + o", we have a "B -(k*x+o)-> R" edge + For too complex assignments that do not match the structure, say "R := h(B1, B2, .., Bn)" where h is complex, we introduce edges "Bi -1x+0-> R". + + On this initial graph, two rules are applied until saturation + (1) Transitivity: A -f_includes-> B AND B -g_includes-> C IMPLIES A -fg_includes-> C (notice that we need to compose the labels as well). + (2) Communication: if A -loads-> R and B -stores-> V and A and B can overlap (i.e. the corresponding Load/Store events can alias), then V -0x+0-> R (all values in V are included in R) + + It can happen that these rules generate an edge A -f-> B although another edge A -g-> B already exists. + In this case, the edges get merged by a join operation. + To guarantee termination, the saturation of cyclic inclusion relationships get accelerated: + E.g. if A includes B (B -0x+0-> A) and B includes A+2 (A -0x+2-> B) + then A includes A+2x, B includes A+2x+2 and both include B+2x. + + (*) We also generate special phi nodes that can improve precision on code that is not in SSA form. + (**) In the implementation we make an unsound assumption that x is non-negative. + This disallows negative (dynamic) indexing into arrays/pointers but gives additional precision in other cases. + Note that "o" can be negative which is sufficient to support "containerof" functionality. +*/ +public class InclusionBasedPointerAnalysis implements AliasAnalysis { + + private static final Logger logger = LogManager.getLogger(InclusionBasedPointerAnalysis.class); + + // This analysis depends on the results of a Dependency analysis, mapping used registers to a list of possible writers. + private final Dependency dependency; + + // For providing helpful error messages, this analysis prints call-stack and loop information for events. + private final Supplier synContext; + + // When a variable gains an includes-edge, it is added to this queue for later processing. + private final LinkedHashMap> queue = new LinkedHashMap<>(); + + // Maps memory events to variables representing their pointer set. + private final Map addressVariables = new HashMap<>(); + + // Maps memory objects to variables representing their base address. + // These Variables should always have empty includes-sets. + private final Map objectVariables = new HashMap<>(); + + // Maps a set of same-register writers to a variable representing their combined result sets (~phi node). + // Non-trivial modifiers may only appear for singleton Locals. + private final Map, DerivedVariable> registerVariables = new HashMap<>(); + + // If enabled, the algorithm describes its internal graph to be written into a file. + private Graphviz graphviz; + + // ================================ Debugging ================================ + + private record IntPair(int x, int y) { + @Override public String toString() {return x + "," + y;} + } + + // Count inclusion tests grouped by complexity. + private final Map totalAlignmentSizes = logger.isDebugEnabled() ? new HashMap<>() : null; + // Count created variables. + private int totalVariables = 0; + // Count variable substitutions. + private int totalReplacements = 0; + // Count new edges already covered by existing ones. + private int failedAddInto = 0; + // Count times a piece of new information was added to the graph. + private int succeededAddInto = 0; + + // ================================ Construction ================================ + + public static InclusionBasedPointerAnalysis fromConfig(Program program, Context analysisContext, AliasAnalysis.Config config) { + final var analysis = new InclusionBasedPointerAnalysis(program, analysisContext.requires(Dependency.class)); + analysis.run(program, config); + logger.debug("variable count: {}", analysis.totalVariables); + logger.debug("replacement count: {}", analysis.totalReplacements); + logger.debug("alignment sizes: {}", analysis.totalAlignmentSizes); + logger.debug("addIncludeEdge: {} successes vs {} fails", analysis.succeededAddInto, analysis.failedAddInto); + return analysis; + } + + private InclusionBasedPointerAnalysis(Program p, Dependency d) { + dependency = d; + synContext = Suppliers.memoize(() -> SyntacticContextAnalysis.newInstance(p)); + } + + // ================================ API ================================ + + @Override + public boolean mayAlias(MemoryCoreEvent x, MemoryCoreEvent y) { + final DerivedVariable vx = addressVariables.get(x); + final DerivedVariable vy = addressVariables.get(y); + if (vx == null || vy == null) { + return true; + } + if (vx.base == vy.base && isConstant(vx.modifier) && isConstant(vy.modifier)) { + return vx.modifier.offset == vy.modifier.offset; + } + final List ox = new ArrayList<>(vx.base.includes); + ox.add(new IncludeEdge(vx.base, TRIVIAL_MODIFIER)); + final List oy = new ArrayList<>(vy.base.includes); + oy.add(new IncludeEdge(vy.base, TRIVIAL_MODIFIER)); + for (final IncludeEdge ax : ox) { + for (final IncludeEdge ay : oy) { + if (ax.source == ay.source && overlaps(compose(ax.modifier, vx.modifier), compose(ay.modifier, vy.modifier))) { + return true; + } + } + } + return false; + } + + @Override + public boolean mustAlias(MemoryCoreEvent x, MemoryCoreEvent y) { + final DerivedVariable vx = addressVariables.get(x); + final DerivedVariable vy = addressVariables.get(y); + return vx != null && vy != null && vx.base == vy.base && vx.modifier.offset == vy.modifier.offset && + isConstant(vx.modifier) && isConstant(vy.modifier); + } + + @Override + public Graphviz getGraphVisualization() { + return graphviz; + } + + // ================================ Processing ================================ + + private void run(Program program, AliasAnalysis.Config configuration) { + checkArgument(program.isCompiled(), "The program must be compiled first."); + // Pre-processing: + // Each memory object gets a variable representing its base address value. + for (final MemoryObject object : program.getMemory().getObjects()) { + totalVariables++; + objectVariables.put(object, new Variable(object, object.toString())); + } + // Each expression gets a "res" variable representing its result value set. + // Each register writer gets an "out" variable ("ld" for loads) representing its return value set. + // If needed, a register gets a "phi" variable representing its phi-node's value set. + // Variables may fulfill multiple roles, e.g. the "out" of a Local is the "res" of its expression, etc. + for (final RegWriter writer : program.getThreadEvents(RegWriter.class)) { + processWriter(writer); + } + for (final MemoryCoreEvent memoryEvent : program.getThreadEvents(MemoryCoreEvent.class)) { + processMemoryEvent(memoryEvent); + } + // Fixed-point computation: + while (!queue.isEmpty()) { + //TODO replace with removeFirst() when using java 21 or newer + final Variable variable = queue.keySet().iterator().next(); + final List edges = queue.remove(variable); + logger.trace("dequeue {}", variable); + algorithm(variable, edges); + } + if (configuration.graphvizInternal) { + generateGraph(); + } + for (final Map.Entry entry : addressVariables.entrySet()) { + postProcess(entry); + } + objectVariables.clear(); + registerVariables.clear(); + } + + // Declares the "out" variable of 'event' and inserts initial 'includes' and 'loads' edges. + // Also declares "res" and "phi" variables, if needed. + private void processWriter(RegWriter event) { + logger.trace("{}", event); + final Expression expr = event instanceof Local local ? local.getExpr() : + event instanceof ThreadArgument arg ? arg.getCreator().getArguments().get(arg.getIndex()) : + event instanceof Alloc alloc ? alloc.getAllocatedObject() : null; + final DerivedVariable value; + if (expr != null) { + final RegReader reader = event instanceof ThreadArgument arg ? arg.getCreator() : (RegReader) event; + value = getResultVariable(expr, reader); + if (value == null) { + return; + } + } else if (event instanceof Load load) { + final DerivedVariable address = getResultVariable(load.getAddress(), load); + if (address == null) { + logger.warn("null pointer address for {}", synContext.get().getContextInfo(event)); + return; + } + addressVariables.put(load, address); + final Variable result = newVariable("ld" + load.getGlobalId() + "(" + load.getResultRegister().getName() + ")"); + address.base.loads.add(new LoadEdge(result, address.modifier)); + result.seeAlso.add(address.base); + value = derive(result); + } else { + return; + } + final DerivedVariable old = registerVariables.put(List.of(event), value); + if (old != null) { + // this might happen if events are iterated out of order + assert isTrivial(old.modifier); + replace(old.base, value); + } + } + + // Declares the "res" variables of the address of 'event', if needed, and inserts 'stores' relationships. + // Also propagates communications to loads, if both directly access the same variable. + private void processMemoryEvent(MemoryCoreEvent event) { + logger.trace("{}", event); + if (event instanceof Load) { + // event was already processed in processWriter(RegWriter) + return; + } + final DerivedVariable address = getResultVariable(event.getAddress(), event); + if (address == null) { + logger.warn("null pointer address for {}", synContext.get().getContextInfo(event)); + return; + } + addressVariables.put(event, address); + if (event instanceof Store store) { + final DerivedVariable value = getResultVariable(store.getMemValue(), store); + if (value != null) { + final StoreEdge edge = new StoreEdge(value, address.modifier); + address.base.stores.add(edge); + value.base.seeAlso.add(address.base); + final List loads = new ArrayList<>(address.base.loads); + for (final Variable includer : address.base.seeAlso) { + if (includer.loads.isEmpty()) { + continue; + } + for (final IncludeEdge includeEdge : includer.includes) { + if (includeEdge.source == address.base) { + for (final LoadEdge load : includer.loads) { + loads.add(compose(load, includeEdge.modifier)); + } + } + } + } + processCommunication(List.of(edge), loads); + } + } + } + + // Closes the "includes" relation transitively and tests for new communications. + private void algorithm(Variable variable, List edges) { + logger.trace("{} includes {}", variable, edges); + // 'A -> variable -> B' implies 'A -> B'. + for (final Variable user : List.copyOf(variable.seeAlso)) { + for (final IncludeEdge edgeAfter : user.includes.stream().filter(e -> e.source == variable).toList()) { + for (final IncludeEdge edge : edges) { + addInclude(user, compose(edge, edgeAfter.modifier)); + } + } + } + // memory communication + // X B -loads> Y ==> X -> Y (if overlapping modifiers) + // Note that variable -> variable can be implied here + final boolean hasLoads = !variable.loads.isEmpty(); + final boolean hasStores = !variable.stores.isEmpty(); + if (hasLoads || hasStores) { + for (final IncludeEdge edge : edges) { + if (edge.source.object == null) { + continue; + } + final List loads = new ArrayList<>(edge.source.loads); + final List stores = new ArrayList<>(edge.source.stores); + for (final Variable out : edge.source.seeAlso) { + for (final IncludeEdge edge1 : out.includes) { + if (hasStores && edge1.source == edge.source) { + for (final LoadEdge load : out.loads) { + loads.add(compose(load, edge1.modifier)); + } + } + if (hasLoads && edge1.source == edge.source) { + for (final StoreEdge store : out.stores) { + stores.add(compose(store, edge1.modifier)); + } + } + } + } + final boolean isTrivial = isTrivial(edge.modifier); + final List variableLoads = isTrivial ? variable.loads : new ArrayList<>(variable.loads.size()); + final List variableStores = isTrivial ? variable.stores : new ArrayList<>(variable.stores.size()); + if (!isTrivial) { + for (final LoadEdge load : variable.loads) { + variableLoads.add(new LoadEdge(load.result, compose(load.addressModifier, edge.modifier))); + } + for (final StoreEdge store : variable.stores) { + variableStores.add(new StoreEdge(store.value, compose(store.addressModifier, edge.modifier))); + } + } + processCommunication(variableStores, loads); + processCommunication(stores, variableLoads); + } + } + } + + // Removes information from the internal graph, which are no longer needed after the algorithm has finished. + // This simplifies alias queries and releases memory resources. + private void postProcess(Map.Entry entry) { + logger.trace("{}", entry); + final DerivedVariable address = entry.getValue(); + if (address == null) { + // should have already warned about this event + return; + } + // Remove all obsolete inclusion relationships between register states. + address.base.includes.removeIf(i -> i.source.object == null); + address.base.loads.clear(); + address.base.stores.clear(); + address.base.seeAlso.clear(); + // In a well-structured program, all address expressions refer to at least one memory object. + if (logger.isWarnEnabled() && address.base.object == null && + address.base.includes.stream().allMatch(i -> i.source.object == null)) { + logger.warn("empty pointer set for {}", synContext.get().getContextInfo(entry.getKey())); + } + if (address.base.includes.size() != 1) { + return; + } + final IncludeEdge includeEdge = address.base.includes.get(0); + final Modifier modifier = compose(includeEdge.modifier, address.modifier); + assert includeEdge.source.object != null; + // If the only included address refers to the last element, treat it as a direct static offset instead. + final int remainingSize = includeEdge.source.object.size() - modifier.offset; + for (final Integer a : modifier.alignment) { + if (a < remainingSize) { + return; + } + } + entry.setValue(derive(includeEdge.source, modifier.offset, List.of())); + } + + // ================================ Internals ================================ + + private static final class Variable { + // Any value contained in the referred variables is also contained (+ modifier). + // Visualized as ingoing edges. + private final List includes = new ArrayList<>(); + // There is some load event using this (+ address modifier) as pointer set and the referred variable as result set. + // Visualized as outgoing edges. + private final List loads = new ArrayList<>(); + // There is some store event using this (+ address modifier) as pointer set and the derived variable as value set. + // 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<>(); + // If nonnull, this variable represents that object's base address. + private final MemoryObject object; + // For visualization. + private final String name; + private Variable(MemoryObject o, String n) { + object = o; + name = n; + } + @Override public String toString() { return name; } + } + + private record IncludeEdge(Variable source, Modifier modifier) {} + + private record LoadEdge(Variable result, Modifier addressModifier) {} + + private record StoreEdge(DerivedVariable value, Modifier addressModifier) {} + + private record Modifier(int offset, List alignment) {} + + private record DerivedVariable(Variable base, Modifier modifier) {} + + private static boolean isConstant(Modifier modifier) { + return modifier.alignment.isEmpty(); + } + + private static boolean isTrivial(Modifier modifier) { + return modifier.offset == 0 && isConstant(modifier); + } + + private static final List TOP = List.of(1); + + private static final Modifier RELAXED_MODIFIER = new Modifier(0, TOP); + + private static final Modifier TRIVIAL_MODIFIER = new Modifier(0, List.of()); + + 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)); + } + + private static IncludeEdge includeEdge(DerivedVariable variable) { + return new IncludeEdge(variable.base, variable.modifier); + } + + private Variable newVariable(String name) { + totalVariables++; + return new Variable(null, name); + } + + // Inserts a single inclusion relationship into the graph. + // Also detects and eliminates cycles, assuming that the graph was already closed transitively. + // Also closes the inclusion relation transitively on the left. + private void addInclude(Variable variable, IncludeEdge includeEdge) { + final IncludeEdge edge = tryInsertIncludeEdge(variable, includeEdge); + if (edge == null) { + return; + } + final List edges = queue.computeIfAbsent(variable, k -> new ArrayList<>()); + if (edges.isEmpty()) { + logger.trace("enqueue {}", variable); + } + edges.add(edge); + // 'variable includes edge.source' and 'edge.source includes v' implies 'variable includes v'. + // Cases of 'v == variable' or 'v == edge.source' require recursion. + final var stack = new Stack(); + stack.push(edge); + while (!stack.empty()) { + final IncludeEdge e = stack.pop(); + for (final IncludeEdge edgeBefore : List.copyOf(e.source.includes)) { + final IncludeEdge joinedEdge = tryInsertIncludeEdge(variable, compose(edgeBefore, e.modifier)); + if (joinedEdge != null) { + edges.add(joinedEdge); + if (edgeBefore.source == edge.source || edgeBefore.source == variable) { + stack.push(joinedEdge); + } + } + } + } + } + + // Tries to insert an element into a set of edges. + // If the edge is already covered by the set, this operation has no effect and returns false. + // If the edge is inserted, any existing elements that are covered by it are removed to form a set of minimal elements. + private IncludeEdge tryInsertIncludeEdge(Variable variable, IncludeEdge edge) { + // Try to accelerate edge. + // Negative offsets get passed as-is, as to disable the assumption of non-negative indexes. + final IncludeEdge element = variable != edge.source ? edge : + new IncludeEdge(variable, new Modifier(0, compose(edge.modifier.alignment, edge.modifier.offset))); + //NOTE The Stream API is too costly here + for (final IncludeEdge o : variable.includes) { + if (element.source.equals(o.source) && includes(o.modifier, element.modifier)) { + failedAddInto++; + return null; + } + } + variable.includes.removeIf(o -> element.source.equals(o.source) && includes(element.modifier, o.modifier)); + variable.includes.add(element); + element.source.seeAlso.add(variable); + succeededAddInto++; + return element; + } + + // Called when a placeholder variable for a register writer is to be replaced by the proper variable. + // A variable cannot be removed, if some event maps to it and there are multiple replacements. + // In this case, the mapping stays but all outgoing edges are removed from that variable. + private void replace(Variable old, DerivedVariable replacement) { + assert old != replacement.base; + assert !objectVariables.containsValue(old); + totalReplacements++; + logger.trace("{} -> {}", old, replacement); + // likely / most frequent case + addressVariables.replaceAll((k, v) -> v.base != old ? v : compose(replacement, v.modifier)); + registerVariables.replaceAll((k, v) -> v.base != old ? v : compose(replacement, v.modifier)); + for (final Variable out : old.seeAlso) { + out.includes.replaceAll(e -> e.source != old ? e : includeEdge(compose(replacement, e.modifier))); + assert out.loads.stream().noneMatch(e -> e.result == old); + out.stores.replaceAll(e -> e.value.base != old ? e : + new StoreEdge(compose(replacement, e.value.modifier), e.addressModifier)); + } + replacement.base.seeAlso.addAll(old.seeAlso); + for (final IncludeEdge edge : old.includes) { + edge.source.seeAlso.remove(old); + edge.source.seeAlso.add(replacement.base); + } + // Redirect load and store relationships. + // This could enable more communications, but replacement. + for (final LoadEdge load : old.loads) { + replacement.base.loads.add(compose(load, replacement.modifier)); + load.result.seeAlso.add(replacement.base); + } + for (final StoreEdge store : old.stores) { + replacement.base.stores.add(compose(store, replacement.modifier)); + store.value.base.seeAlso.add(replacement.base); + } + old.seeAlso.clear(); + old.includes.clear(); + old.loads.clear(); + old.stores.clear(); + } + + // Find "may read from" relationships and deduce new 'includes' edges for the internal graph. + private void processCommunication(List stores, List loads) { + logger.trace("{} vs {}", stores, loads); + if (loads.isEmpty()) { + return; + } + for (final StoreEdge store : stores) { + for (final LoadEdge load : loads) { + if (overlaps(store.addressModifier, load.addressModifier)) { + addInclude(load.result, includeEdge(store.value)); + } + } + } + } + + // Checks if leftAlignment contains all linear combinations of offset + rightAlignment. + // Is allowed to have false negatives, as such only lead to more memory usage of the analysis. + private boolean includes(Modifier left, Modifier right) { + int offset = right.offset - left.offset; + // DEBUG: Count this test. + if (totalAlignmentSizes != null) { + totalAlignmentSizes.merge(new IntPair(left.alignment.size(), right.alignment.size()), 1, Integer::sum); + } + 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; + } + } + // 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. + if (left.alignment.size() == 1) { + final int alignment = Math.abs(left.alignment.get(0)); + for (final Integer a : right.alignment) { + if (a % alignment != 0) { + return false; + } + } + return offset % alignment == 0; + } + // Case of multiple dynamic indexes with pairwise indivisible alignments. + final int gcd = IntMath.gcd(reduceGCD(right.alignment), Math.abs(offset)); + if (gcd == 0) { + return true; + } + int max = Math.abs(offset); + for (final Integer i : right.alignment) { + max = Math.max(max, i); + } + final var mem = new boolean[max / gcd + 1]; + mem[0] = true; + for (int j = 1; j < mem.length; j++) { + for (final Integer i : left.alignment) { + if (j - i/gcd >= 0 && mem[j - i/gcd]) { + mem[j] = true; + break; + } + } + } + for (final Integer j : right.alignment) { + if (!mem[j/gcd]) { + return false; + } + } + return mem[Math.abs(offset)/gcd]; + } + + // Checks if there may be some common value in both sets. + // Allowed to have false positives. + 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); + 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; + } + + // 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)); + } + + // Computes the greatest common divisor of the operands. + private static int reduceGCD(List alignment) { + if (alignment.isEmpty()) { + return 0; + } + int result = alignment.get(0); + for (final Integer a : alignment.subList(1, alignment.size())) { + result = IntMath.gcd(result, a); + } + return result; + } + + // Merges two sets of pairwise-indivisible dynamic offsets. + private static List compose(List left, List right) { + if (left.isEmpty() || right.isEmpty()) { + return right.isEmpty() ? left : right; + } + if (left == TOP || right == TOP) { + return TOP; + } + // assert left and right each consist of pairwise indivisible positives + final List result = new ArrayList<>(); + for (final Integer i : left) { + if (hasNoDivisorsInList(i, right, true)) { + result.add(i); + } + } + for (final Integer j : right) { + if (hasNoDivisorsInList(j, left, false)) { + result.add(j); + } + } + return result; + } + + // 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) { + if ((strict || value < candidate) && value % candidate == 0) { + return false; + } + } + return true; + } + + private static Modifier compose(Modifier left, Modifier right) { + return new Modifier(left.offset + right.offset, compose(left.alignment, right.alignment)); + } + + // Adds a single value to a set of dynamic offsets. + private static List compose(List left, int right) { + return right == 0 ? left : compose(left, List.of(right)); + } + + // Adds an optional register to a set of dynamic offsets. + // If the register is present, it may contain any value. + private static List compose(List left, Register right) { + return right == null ? left : TOP; + } + + // Applies another offset to an existing labeled edge. + private static DerivedVariable compose(DerivedVariable other, Modifier modifier) { + return isTrivial(modifier) ? other : new DerivedVariable(other.base, compose(other.modifier, modifier)); + } + + private static IncludeEdge compose(IncludeEdge other, Modifier modifier) { + return isTrivial(modifier) ? other : new IncludeEdge(other.source, compose(other.modifier, modifier)); + } + + private static LoadEdge compose(LoadEdge other, Modifier modifier) { + return isTrivial(modifier) ? other : new LoadEdge(other.result, compose(other.addressModifier, modifier)); + } + + private static StoreEdge compose(StoreEdge other, Modifier modifier) { + return isTrivial(modifier) ? other : new StoreEdge(other.value, compose(other.addressModifier, modifier)); + } + + // Multiplies all dynamic offsets with another factor. + private static List mul(List a, int factor) { + return factor == 0 ? List.of() : a.stream().map(i -> i * factor).toList(); + } + + // Describes (constant address or register or zero) + offset + alignment * (variable) + private record Result(MemoryObject address, Register register, BigInteger offset, List alignment) { + private boolean isConstant() { + return address == null && register == null && alignment.isEmpty(); + } + @Override + public String toString() { + return String.format("%s+%s+%sx", address != null ? address : register, offset, alignment); + } + } + + // Interprets an expression. + // The result refers to an existing variable, + // if the expression has a static base, or if the expression has a dynamic base with exactly one writer. + // Otherwise, it refers to a new variable with proper incoming edges. + private DerivedVariable getResultVariable(Expression expression, RegReader reader) { + final var collector = new Collector(); + final Result result = expression.accept(collector); + final DerivedVariable main; + 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)); + } else { + main = null; + } + if (main != null && + collector.address.stream().allMatch(a -> a == result.address) && + collector.register.stream().allMatch(r -> r == result.register)) { + return main; + } + if (main == null && collector.address.isEmpty() && collector.register.isEmpty()) { + return null; + } + final Variable variable = newVariable("res" + reader.getGlobalId() + "(" + expression + ")"); + if (main != null) { + addInclude(variable, includeEdge(main)); + } + for (final MemoryObject object : collector.address) { + if (result == null || object != result.address) { + addInclude(variable, new IncludeEdge(objectVariables.get(object), RELAXED_MODIFIER)); + } + } + for (final Register register : collector.register) { + if (result == null || register != result.register) { + final DerivedVariable registerVariable = getPhiNodeVariable(register, reader); + addInclude(variable, new IncludeEdge(registerVariable.base, RELAXED_MODIFIER)); + } + } + return derive(variable); + } + + // Fetches the node for address values that can be read from a register at a specific program point. + // Constructs a new node, if there are multiple writers. + private DerivedVariable getPhiNodeVariable(Register register, RegReader reader) { + // We assume here that uninitialized values carry no meaningful address to any memory object. + final List writers = dependency.of(reader, register).may; + final DerivedVariable find = registerVariables.get(writers); + if (find != null) { + return find; + } + final Variable result = newVariable("phi" + reader.getGlobalId() + "(" + register.getName() + ")"); + // If writers is a singleton here, its "phi" node will be replaced later. Otherwise, the "out" nodes. + for (final RegWriter writer : writers.size() == 1 ? List.of() : writers) { + // The variables created here will be replaced later, if the events are out of order. + final DerivedVariable writerVariable = registerVariables.computeIfAbsent(List.of(writer), + k -> derive(newVariable("out" + writer.getGlobalId()))); + addInclude(result, includeEdge(writerVariable)); + } + return registerVariables.compute(writers, (k, v) -> derive(result)); + } + + private static final class Collector implements ExpressionVisitor { + + final Set address = new HashSet<>(); + final Set register = new HashSet<>(); + + @Override + public Result visitExpression(Expression expr) { + register.addAll(expr.getRegs()); + return null; + } + + @Override + public Result visitIntBinaryExpression(IntBinaryExpr x) { + final Result left = x.getLeft().accept(this); + final Result right = x.getRight().accept(this); + final IntBinaryOp kind = x.getKind(); + if (left != null && left.isConstant() && right != null && right.isConstant()) { + // TODO: Make sure that the type of normalization does not break this code. + // Maybe always do signed normalization? + final BigInteger result = kind.apply(left.offset, right.offset, x.getType().getBitWidth()); + return new Result(null, null, result, List.of()); + } + return switch (kind) { + case MUL -> { + if (left == null && right == null || + left != null && left.address != null || + right != null && right.address != null) { + yield null; + } + if (left == null || right == null) { + final Result factor = left == null ? right : left; + if (factor.register != null) { + yield null; + } + final List alignment = compose(factor.alignment, factor.offset.intValue()); + yield new Result(null, null, BigInteger.ZERO, alignment); + } + final List leftAlignment = mul(compose(left.alignment, left.register), right.offset.intValue()); + final List rightAlignment = mul(compose(right.alignment, right.register), left.offset.intValue()); + yield new Result(null, null, left.offset.multiply(right.offset), compose(leftAlignment, rightAlignment)); + } + case ADD, SUB -> { + if (left == null || right == null || left.address != null && right.address != null) { + yield null; + } + final MemoryObject base = left.address != null ? left.address : right.address; + final BigInteger offset = kind.apply(left.offset, right.offset, x.getType().getBitWidth()); + if (base != null) { + final List leftAlignment = compose(left.alignment, left.register); + final List rightAlignment = compose(right.alignment, right.register); + yield new Result(base, null, offset, compose(leftAlignment, rightAlignment)); + } + if (left.register != null && right.register != null) { + yield null; + } + final Register register = left.register != null ? left.register : right.register; + final List alignment = compose(left.alignment, right.alignment); + yield new Result(null, register, offset, alignment); + } + default -> null; + }; + } + + @Override + public Result visitIntUnaryExpression(IntUnaryExpr x) { + if (x.getKind() != IntUnaryOp.MINUS) { + return null; + } + final Result result = x.getOperand().accept(this); + if (result.address != null || result.register != null) { + return null; + } + final var alignment = new ArrayList(); + for (final Integer a : result.alignment) { + alignment.add(-Math.abs(a)); + } + return new Result(null, null, result.offset.negate(), alignment); + } + + @Override + public Result visitIntSizeCastExpression(IntSizeCast expr) { + // We assume type casts do not affect the value of pointers. + final Result result = expr.getOperand().accept(this); + return expr.isExtension() && !expr.preservesSign() ? result : null; + } + + @Override + public Result visitITEExpression(ITEExpr x) { + x.getTrueCase().accept(this); + x.getFalseCase().accept(this); + return null; + } + + @Override + public Result visitMemoryObject(MemoryObject a) { + address.add(a); + return new Result(a, null, BigInteger.ZERO, List.of()); + } + + @Override + public Result visitRegister(Register r) { + register.add(r); + return new Result(null, r, BigInteger.ZERO, List.of()); + } + + @Override + public Result visitIntLiteral(IntLiteral v) { + return new Result(null, null, v.getValue(), List.of()); + } + } + + // Projects the internal representation of this analysis: + // Nodes are variables, grey edges are inclusions. + // Blue edges connect address variables to register variables. + // Red edges connect address variables to stored value variables. + // Green-labeled nodes represent memory objects. + // Red-labeled nodes are address variables that do not include any memory objects (probably a bug). + // Blue-labeled nodes are variables where transitivity is broken (certainly a bug). + private void generateGraph() { + final Set seen = new HashSet<>(objectVariables.values()); + for (Set news = seen; !news.isEmpty();) { + final var next = new HashSet(); + for (final Variable v : news) { + next.addAll(v.seeAlso); + v.includes.forEach(o -> next.add(o.source)); + v.loads.forEach(o -> next.add(o.result)); + v.stores.forEach(o -> next.add(o.value.base)); + } + next.removeAll(seen); + seen.addAll(next); + news = next; + } + final Map> map = new HashMap<>(); + final Map> loads = new HashMap<>(); + final Map> stores = new HashMap<>(); + for (Variable v : seen) { + if (v == null) { + continue; + } + for (final IncludeEdge i : v.includes) { + verify(i.source.seeAlso.contains(v)); + map.computeIfAbsent("\"" + i.source.name + "\"", k -> new HashSet<>()).add("\"" + v.name + "\""); + } + for (final LoadEdge i : v.loads) { + verify(i.result.seeAlso.contains(v)); + loads.computeIfAbsent("\"" + v.name + "\"", k -> new HashSet<>()).add("\"" + i.result.name + "\""); + } + for (final StoreEdge i : v.stores) { + verify(i.value.base.seeAlso.contains(v)); + stores.computeIfAbsent("\"" + v.name + "\"", k -> new HashSet<>()).add("\"" + i.value.base.name + "\""); + } + } + final Set problematic = new HashSet<>(); + for (final DerivedVariable a : addressVariables.values()) { + if (!objectVariables.containsValue(a.base) && + a.base.includes.stream().noneMatch(i -> objectVariables.containsValue(i.source))) { + problematic.add("\"" + a.base.name + "\""); + } + } + final Set transitionBlocker = new HashSet<>(); + for (final Set outSet : map.values()) { + for (final String v2 : outSet) { + if (!outSet.containsAll(map.getOrDefault(v2, Set.of()))) { + transitionBlocker.add(v2); + } + } + } + problematic.removeAll(transitionBlocker); + graphviz = new Graphviz(); + graphviz.beginDigraph("internal alias"); + for (final Variable v : objectVariables.values()) { + graphviz.addNode("\"" + v.name + "\"", "fontcolor=mediumseagreen"); + } + for (final String v : problematic) { + graphviz.addNode(v, "fontcolor=red"); + } + for (final String v : transitionBlocker) { + graphviz.addNode(v, "fontcolor=blue"); + } + graphviz.beginSubgraph("inclusion"); + graphviz.setEdgeAttributes("color=grey"); + graphviz.addEdges(map); + graphviz.end(); + graphviz.beginSubgraph("loads"); + graphviz.setEdgeAttributes("color=mediumslateblue"); + graphviz.addEdges(loads); + graphviz.end(); + graphviz.beginSubgraph("stores"); + graphviz.setEdgeAttributes("color=orangered3"); + graphviz.addEdges(stores); + graphviz.end(); + graphviz.end(); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/Graphviz.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/Graphviz.java index 844a0a511e..bd9f32954d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/Graphviz.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/Graphviz.java @@ -60,6 +60,11 @@ public Graphviz appendLine(String text) { return this; } + public Graphviz addNode(String name, String... attributes) { + text.append(String.format("%s [%s]\n", name, String.join(", ", attributes))); + return this; + } + public Graphviz addEdge(String node1, String node2, String... options) { String edge = directed ? "->" : "--"; if (options == null) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index bb90a722c9..644be1d63c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -95,7 +95,7 @@ public static void performStaticProgramAnalyses(VerificationTask task, Context a analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, config)); analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(Dependency.class, Dependency.fromConfig(program, analysisContext, config)); - analysisContext.register(AliasAnalysis.class, AliasAnalysis.fromConfig(program, config)); + analysisContext.register(AliasAnalysis.class, AliasAnalysis.fromConfig(program, analysisContext, config)); analysisContext.register(ThreadSymmetry.class, ThreadSymmetry.fromConfig(program, config)); for(Thread thread : program.getThreads()) { for(Event e : thread.getEvents()) { 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 af5b0edebc..78a4bd0b85 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -20,6 +20,7 @@ import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.processing.LoopUnrolling; import com.dat3m.dartagnan.program.processing.MemoryAllocation; +import com.dat3m.dartagnan.program.processing.ProcessingManager; import com.dat3m.dartagnan.program.processing.compilation.Compilation; import com.dat3m.dartagnan.verification.Context; import org.junit.Test; @@ -28,8 +29,7 @@ import java.util.List; -import static com.dat3m.dartagnan.configuration.Alias.FIELD_INSENSITIVE; -import static com.dat3m.dartagnan.configuration.Alias.FIELD_SENSITIVE; +import static com.dat3m.dartagnan.configuration.Alias.*; import static com.dat3m.dartagnan.configuration.OptionNames.ALIAS_METHOD; import static com.dat3m.dartagnan.program.event.EventFactory.*; import static org.junit.Assert.*; @@ -110,6 +110,11 @@ public void fieldinsensitive0() throws InvalidConfigurationException { program0(FIELD_INSENSITIVE, MAY, NONE, MAY, NONE, MAY, NONE); } + @Test + public void full0() throws InvalidConfigurationException { + program0(FULL, MAY, MAY, NONE, NONE, NONE, NONE); + } + private void program0(Alias method, Result... expect) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); @@ -131,9 +136,6 @@ private void program0(Alias method, Result... expect) throws InvalidConfiguratio b.addChild(0, e3); Program program = b.build(); - Compilation.newInstance().run(program); - LoopUnrolling.newInstance().run(program); - MemoryAllocation.newInstance().run(program); AliasAnalysis a = analyze(program, method); MemoryCoreEvent me0 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e0); MemoryCoreEvent me1 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e1); @@ -158,6 +160,11 @@ public void fieldinsensitive1() throws InvalidConfigurationException { program1(FIELD_INSENSITIVE, NONE, NONE, MUST, MAY, MAY, MAY); } + @Test + public void full1() throws InvalidConfigurationException { + program1(FULL, NONE, NONE, MUST, MUST, NONE, NONE); + } + private void program1(Alias method, Result... expect) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); MemoryObject x = b.newMemoryObject("x", 3); @@ -175,9 +182,6 @@ private void program1(Alias method, Result... expect) throws InvalidConfiguratio b.addChild(0, e3); Program program = b.build(); - Compilation.newInstance().run(program); - LoopUnrolling.newInstance().run(program); - MemoryAllocation.newInstance().run(program); AliasAnalysis a = analyze(program, method); MemoryCoreEvent me0 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e0); MemoryCoreEvent me1 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e1); @@ -202,6 +206,11 @@ public void fieldinsensitive2() throws InvalidConfigurationException { program2(FIELD_INSENSITIVE, NONE, NONE, NONE, MAY, MAY, MAY); } + @Test + public void full2() throws InvalidConfigurationException { + program2(FULL, NONE, NONE, NONE, MAY, NONE, MAY); + } + private void program2(Alias method, Result... expect) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); IntegerType type = types.getArchType(); @@ -229,9 +238,6 @@ private void program2(Alias method, Result... expect) throws InvalidConfiguratio b.addChild(0, l0); Program program = b.build(); - Compilation.newInstance().run(program); - LoopUnrolling.newInstance().run(program); - MemoryAllocation.newInstance().run(program); AliasAnalysis a = analyze(program, method); MemoryCoreEvent me0 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e0); MemoryCoreEvent me1 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e1); @@ -256,6 +262,11 @@ public void fieldinsensitive3() throws InvalidConfigurationException { program3(FIELD_INSENSITIVE, MUST, NONE, NONE, MAY, MAY, MAY); } + @Test + public void full3() throws InvalidConfigurationException { + program3(FULL, MUST, NONE, NONE, MAY, MAY, MAY); + } + private void program3(Alias method, Result... expect) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); MemoryObject x = b.newMemoryObject("x", 3); @@ -273,9 +284,6 @@ private void program3(Alias method, Result... expect) throws InvalidConfiguratio b.addChild(0, e3); Program program = b.build(); - Compilation.newInstance().run(program); - LoopUnrolling.newInstance().run(program); - MemoryAllocation.newInstance().run(program); AliasAnalysis a = analyze(program, method); MemoryCoreEvent me0 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e0); MemoryCoreEvent me1 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e1); @@ -300,6 +308,11 @@ public void fieldinsensitive4() throws InvalidConfigurationException { program4(FIELD_INSENSITIVE, NONE, MUST, NONE, NONE, NONE, NONE); } + @Test + public void full4() throws InvalidConfigurationException { + program4(FULL, NONE, MUST, NONE, NONE, NONE, NONE); + } + private void program4(Alias method, Result... expect) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); MemoryObject x = b.newMemoryObject("x", 1); @@ -344,6 +357,11 @@ public void fieldinsensitive5() throws InvalidConfigurationException { program5(FIELD_INSENSITIVE, MUST, NONE, NONE, NONE, NONE, NONE); } + @Test + public void full5() throws InvalidConfigurationException { + program5(FULL, NONE, MUST, NONE, NONE, NONE, NONE); + } + private void program5(Alias method, Result... expect) throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); MemoryObject x = b.newMemoryObject("x", 1); @@ -378,6 +396,91 @@ private void program5(Alias method, Result... expect) throws InvalidConfiguratio assertAlias(expect[5], a, me2, me3); } + @Test + public void fullPropagation0() throws InvalidConfigurationException { + ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); + MemoryObject x = b.newMemoryObject("x", 1); + MemoryObject y = b.newMemoryObject("y", 1); + x.setInitialValue(0, y); + y.setInitialValue(0, x); + + b.newThread(0); + Register r0 = b.getOrNewRegister(0, "r0"); + Register r1 = b.getOrNewRegister(0, "r1"); + Register r2 = b.getOrNewRegister(0, "r2"); + Register r3 = b.getOrNewRegister(0, "r3"); + Load e0 = newLoad(r0, y); // reads x + b.addChild(0, e0); + Load e1 = newLoad(r1, r0); // reads y + b.addChild(0, e1); + Load e2 = newLoad(r2, r1); // reads x + b.addChild(0, e2); + Load e3 = newLoad(r3, r2); // reads y + b.addChild(0, e3); + Store e4 = newStore(y, r3); // stores y + b.addChild(0, e4); + + Program program = b.build(); + AliasAnalysis a = analyze(program, FULL); + MemoryCoreEvent me0 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e0); + MemoryCoreEvent me1 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e1); + MemoryCoreEvent me2 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e2); + MemoryCoreEvent me3 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e3); + + assertAlias(MAY, a, me0, me1); + assertAlias(MAY, a, me0, me2); + assertAlias(MAY, a, me1, me2); + assertAlias(MAY, a, me0, me3); + assertAlias(MAY, a, me1, me3); + assertAlias(MAY, a, me2, me3); + } + + @Test + public void fullPropagation1() throws InvalidConfigurationException { + ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); + MemoryObject x = b.newMemoryObject("x", 1); + MemoryObject y = b.newMemoryObject("y", 1); + x.setInitialValue(0, y); + y.setInitialValue(0, x); + + b.newThread(0); + Register r0 = b.getOrNewRegister(0, "r0"); + Register r1 = b.getOrNewRegister(0, "r1"); + Register r2 = b.getOrNewRegister(0, "r2"); + Load e0 = newLoad(r0, y); // reads x + b.addChild(0, e0); + Label l0 = newLabel("l0"); + b.addChild(0, newJump(expressions.makeEQ(r0, x), l0)); + Load e1 = newLoad(r0, x); // reads y + b.addChild(0, e1); + b.addChild(0, l0); + Load e2 = newLoad(r1, r0); // reads x + b.addChild(0, e2); + Load e3 = newLoad(r2, r1); // reads y + b.addChild(0, e3); + Store e4 = newStore(r0, r2); // stores y + b.addChild(0, e4); + + Program program = b.build(); + AliasAnalysis a = analyze(program, FULL); + MemoryCoreEvent me0 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e0); + MemoryCoreEvent me1 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e1); + MemoryCoreEvent me2 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e2); + MemoryCoreEvent me3 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e3); + MemoryCoreEvent me4 = (MemoryCoreEvent) findMatchingEventAfterProcessing(program, e4); + + assertAlias(NONE, a, me0, me1); + assertAlias(MAY, a, me0, me2); + assertAlias(MAY, a, me1, me2); + assertAlias(MAY, a, me0, me3); + assertAlias(MAY, a, me1, me3); + assertAlias(MAY, a, me2, me3); + assertAlias(MAY, a, me0, me4); + assertAlias(MAY, a, me1, me4); + assertAlias(MUST, a, me2, me4); + assertAlias(MAY, a, me3, me4); + } + private Load newLoad(Register value, Expression address) { return EventFactory.newLoad(value, address); } @@ -403,9 +506,15 @@ private Expression mult(Expression lhs, long rhs) { } private AliasAnalysis analyze(Program program, Alias method) throws InvalidConfigurationException { - Compilation.newInstance().run(program); - LoopUnrolling.newInstance().run(program); - return AliasAnalysis.fromConfig(program, Configuration.builder().setOption(ALIAS_METHOD, method.asStringOption()).build()); + Configuration configuration = Configuration.builder() + .setOption(ALIAS_METHOD, method.asStringOption()) + .build(); + ProcessingManager.fromConfig(configuration).run(program); + Context analysisContext = Context.create(); + analysisContext.register(BranchEquivalence.class, BranchEquivalence.fromConfig(program, configuration)); + analysisContext.register(ExecutionAnalysis.class, ExecutionAnalysis.fromConfig(program, analysisContext, configuration)); + analysisContext.register(Dependency.class, Dependency.fromConfig(program, analysisContext, configuration)); + return AliasAnalysis.fromConfig(program, analysisContext, configuration); } private void assertAlias(Result expect, AliasAnalysis a, MemoryCoreEvent x, MemoryCoreEvent y) {