New Pointer Analysis

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java

@@ -10,7 +10,6 @@
 import com.google.common.collect.Iterables;
 
 import java.util.HashMap;
-import java.util.List;
 import java.util.Map;
 import java.util.Stack;
 import java.util.function.Predicate;
@@ -100,9 +99,6 @@ public String toString() {
         }
     }
 
-    // We use this enum to track loop nesting
-    private enum LoopMarkerTypes {START, INC, END}
-
     // ============================================================================
 
     private final Map<Event, Info> infoMap = new HashMap<>();
@@ -138,7 +134,7 @@ private void run(Program program) {
     }
 
     private void run(Thread thread, LoopAnalysis loops) {
-        final Map<Event, LoopMarkerTypes> loopMarkerTypesMap = getLoopMarkerTypesMap(thread, loops);
+        final Map<Event, LoopAnalysis.LoopIterationInfo> loopMarkerTypesMap = getLoopMarkerTypesMap(thread, loops);
 
         Stack<Context> curContextStack = new Stack<>();
         curContextStack.push(new ThreadContext(thread));
@@ -161,32 +157,31 @@ private void run(Thread thread, LoopAnalysis loops) {
                 } while (!topCallCtx.funCallMarker.getFunctionName().equals(retMarker.getFunctionName()));
             }
 
-            if (loopMarkerTypesMap.containsKey(ev)) {
-                switch (loopMarkerTypesMap.get(ev)) {
-                    case START -> curContextStack.push(new LoopContext(ev, 1));
-                    case INC -> {
-                        assert curContextStack.peek() instanceof LoopContext;
-                        int iterNum = ((LoopContext) curContextStack.pop()).iterationNumber;
-                        curContextStack.push(new LoopContext(ev, iterNum + 1));
-                    }
-                    case END -> {
-                        assert curContextStack.peek() instanceof LoopContext;
-                        curContextStack.pop();
-                    }
+            final LoopAnalysis.LoopIterationInfo iteration = loopMarkerTypesMap.get(ev);
+            if (iteration != null) {
+                final boolean start = ev == iteration.getIterationStart();
+                final boolean end = ev == iteration.getIterationEnd();
+                assert start || end;
+                if (start) {
+                    curContextStack.push(new LoopContext(ev, iteration.getIterationNumber()));
+                }
+                if (end) {
+                    assert curContextStack.peek() instanceof LoopContext c &&
+                            c.loopMarker == iteration.getIterationStart() &&
+                            c.iterationNumber == iteration.getIterationNumber();
+                    curContextStack.pop();
                 }
             }
         }
     }
 
-    private Map<Event, LoopMarkerTypes> getLoopMarkerTypesMap(Thread thread, LoopAnalysis loopAnalysis) {
-        final Map<Event, LoopMarkerTypes> loopMarkerTypesMap = new HashMap<>();
+    private Map<Event, LoopAnalysis.LoopIterationInfo> getLoopMarkerTypesMap(Thread thread, LoopAnalysis loopAnalysis) {
+        final Map<Event, LoopAnalysis.LoopIterationInfo> loopMarkerTypesMap = new HashMap<>();
         for (LoopAnalysis.LoopInfo loop : loopAnalysis.getLoopsOfFunction(thread)) {
-            final List<LoopAnalysis.LoopIterationInfo> iterations = loop.iterations();
-
-            loopMarkerTypesMap.put(iterations.get(0).getIterationStart(), LoopMarkerTypes.START);
-            iterations.subList(1, iterations.size())
-                    .forEach(iter -> loopMarkerTypesMap.put(iter.getIterationStart(), LoopMarkerTypes.INC));
-            loopMarkerTypesMap.put(iterations.get(iterations.size() - 1).getIterationEnd(), LoopMarkerTypes.END);
+            for (LoopAnalysis.LoopIterationInfo iteration : loop.iterations()) {
+                loopMarkerTypesMap.put(iteration.getIterationStart(), iteration);
+                loopMarkerTypesMap.put(iteration.getIterationEnd(), iteration);
+            }
         }
         return loopMarkerTypesMap;
     }

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java

@@ -59,7 +59,7 @@ static AliasAnalysis fromConfig(Program program, Context analysisContext, Config
     final class Config {
         @Option(name = ALIAS_METHOD,
                 description = "General type of analysis that approximates the 'loc' relationship between memory events.")
-        private Alias method = Alias.FULL;
+        private Alias method = Alias.getDefault();
 
         @Option(name = ALIAS_GRAPHVIZ,
                 description = "If 'true', stores the results of the alias analysis as a PNG image." +

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java

@@ -6,16 +6,19 @@
 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.Event;
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.Load;
 import com.dat3m.dartagnan.program.event.core.Local;
 import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
 import com.dat3m.dartagnan.program.event.core.Store;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument;
+import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.utils.visualization.Graphviz;
 import com.dat3m.dartagnan.verification.Context;
+import com.google.common.math.IntMath;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.sosy_lab.common.configuration.Configuration;
@@ -155,11 +158,13 @@ private void run(Program program) {
             //TODO replace with removeFirst() when using java 21 or newer
             final Variable variable = queue.keySet().iterator().next();
             final List<Offset<Variable>> edges = queue.remove(variable);
+            logger.trace("dequeue {}", variable);
             algorithm(variable, edges);
         }
-        //printGraph();
+        printGraph();
+        final SyntacticContextAnalysis synContext = SyntacticContextAnalysis.newInstance(program);
         for (final Map.Entry<MemoryCoreEvent, Offset<Variable>> entry : eventAddressSpaceMap.entrySet()) {
-            postProcess(entry);
+            postProcess(entry, synContext);
         }
         constantMap.clear();
         variableMap.clear();
@@ -179,7 +184,7 @@ private void processWriter(RegWriter event) {
         } else if (event instanceof Load load) {
             final Offset<Variable> address = getResultVariable(load.getAddress(), load);
             if (address == null) {
-                logger.warn("null pointer address for {}", event);
+                logger.warn("null pointer address for {}: {}", event.getMetadata(SourceLocation.class), event);
                 return;
             }
             eventAddressSpaceMap.put(load, address);
@@ -273,7 +278,7 @@ private void algorithm(Variable variable, List<Offset<Variable>> edges) {
         }
     }
 
-    private void postProcess(Map.Entry<MemoryCoreEvent, Offset<Variable>> entry) {
+    private void postProcess(Map.Entry<MemoryCoreEvent, Offset<Variable>> entry, SyntacticContextAnalysis synContext) {
         logger.trace("{}", entry);
         final Offset<Variable> address = entry.getValue();
         if (address == null) {
@@ -288,7 +293,7 @@ private void postProcess(Map.Entry<MemoryCoreEvent, Offset<Variable>> entry) {
         // 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.base.object == null)) {
-            logger.warn("empty pointer set for {}", entry.getKey());
+            logger.warn("empty pointer set for {}", synContext.getContextInfo(entry.getKey()));
         }
         if (address.base.includes.size() != 1) {
             return;
@@ -307,7 +312,7 @@ private void postProcess(Map.Entry<MemoryCoreEvent, Offset<Variable>> entry) {
 
     // 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 and propagates the load and store relations.
+    // Also closes the inclusion relation transitively on the left.
     private void addEdge(Variable v1, Variable v2, int o, List<Integer> a) {
         // When adding a self-loop, try to accelerate it immediately: 'v -+1> v' means 'v -+1x> v'.
         final var edge = tryAccelerateEdge(new Offset<>(v1, o, a), v2);
@@ -316,6 +321,9 @@ private void addEdge(Variable v1, Variable v2, int o, List<Integer> a) {
         }
         v1.seeAlso.add(v2);
         final List<Offset<Variable>> edges = queue.computeIfAbsent(v2, k -> new ArrayList<>());
+        if (edges.isEmpty()) {
+            logger.trace("enqueue {}", v2);
+        }
         edges.add(edge);
         // 'v0 -> v1 -> v2' implies 'v0 -> v2'.
         // Cases of 'v0 == v2' or 'v0 == v1' require recursion.
@@ -344,7 +352,6 @@ private static Offset<Variable> tryAccelerateEdge(Offset<Variable> edge, Variabl
     }
 
     // Called when a placeholder variable for a register writer is to be replaced by the proper variable.
-    // Also called during unification, where a cycle of variables is merged into one 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, Offset<Variable> replacement) {
@@ -434,7 +441,7 @@ private boolean includes(int offset, List<Integer> leftAlignment, List<Integer>
             return offset % alignment == 0;
         }
         // Case of multiple dynamic indexes with pairwise indivisible alignments.
-        final int gcd = gcd(gcd(rightAlignment), Math.abs(offset));
+        final int gcd = IntMath.gcd(gcd(rightAlignment), Math.abs(offset));
         if (gcd == 0) {
             return true;
         }
@@ -468,7 +475,7 @@ private static boolean overlaps(int offset, List<Integer> leftAlignment, List<In
         if (left == 0 && right == 0) {
             return offset == 0;
         }
-        final int divisor = left == 0 ? right : right == 0 ? left : gcd(left, right);
+        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;
     }
@@ -494,31 +501,18 @@ private static int absGcd(List<Integer> alignment) {
         }
         int result = Math.abs(alignment.get(0));
         for (final Integer a : alignment.subList(1, alignment.size())) {
-            result = gcd(result, Math.abs(a));
+            result = IntMath.gcd(result, Math.abs(a));
         }
         return result;
     }
 
-    private static int gcd(int left, int right) {
-        // Euclidean algorithm.  I cannot believe this is not part of the standard library.
-        assert left >= 0 && right >= 0;
-        int a = Math.min(left, right);
-        int b = Math.max(left, right);
-        while (a != 0) {
-            final int temp = b % a;
-            b = a;
-            a = temp;
-        }
-        return b;
-    }
-
     private static int gcd(List<Integer> alignment) {
         if (alignment.isEmpty()) {
             return 0;
         }
         int result = alignment.get(0);
         for (final Integer a : alignment.subList(1, alignment.size())) {
-            result = gcd(result, a);
+            result = IntMath.gcd(result, a);
         }
         return result;
     }
@@ -803,7 +797,6 @@ private void printGraph() {
         for (final String v : transitionBlocker) {
             graphviz.addNode(v, "fontcolor=blue");
         }
-        logger.debug("{}", problematic);
         graphviz.beginSubgraph("inclusion");
         graphviz.setEdgeAttributes("color=grey");
         graphviz.addEdges(map);
@@ -823,6 +816,7 @@ private void printGraph() {
                 graphviz.generateOutput(writer);
             }
             Graphviz.convert(file);
+            logger.info("generated graph at \"{}\"", file.getAbsolutePath());
         } catch (IOException | InterruptedException x) {
             logger.error("Could not create alias graph", x);
         }