New Pointer Analysis

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;

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";
 

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java

@@ -265,7 +265,7 @@ public BooleanFormula encodeFinalRegisterValues() {
         for(Map.Entry<Register,Dependency.State> e : dep.finalWriters().entrySet()) {
             final Formula value = context.encodeFinalExpression(e.getKey());
             final Dependency.State state = e.getValue();
-            final List<Event> writers = state.may;
+            final List<RegWriter> writers = state.may;
             if(initializeRegisters && !state.initialized) {
                 List<BooleanFormula> 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<BooleanFormula> 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)) {

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

@@ -142,7 +142,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) {
@@ -166,18 +166,18 @@ private void process(Thread thread, ExecutionAnalysis exec) {
     }
 
     private static State process(Event reader, Set<Writer> state, Register register, ExecutionAnalysis exec) {
-        List<Event> candidates = state.stream()
+        List<RegWriter> candidates = state.stream()
                 .filter(e -> e.register.equals(register))
                 .map(e -> e.event)
                 .filter(e -> reader == null || !exec.areMutuallyExclusive(reader, e))
                 .collect(toList());
         //NOTE if candidates is empty, the reader is unreachable
-        List<Event> mays = candidates.stream()
+        List<RegWriter> mays = candidates.stream()
                 .filter(Objects::nonNull)
                 .sorted(Comparator.comparingInt(Event::getGlobalId))
                 .collect(Collectors.toCollection(ArrayList::new));
         int end = mays.size();
-        List<Event> musts = range(0, end)
+        List<RegWriter> 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());
@@ -186,9 +186,9 @@ private static State process(Event reader, Set<Writer> 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;
         }
@@ -222,15 +222,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<Event> may;
+        public final List<RegWriter> 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<Event> must;
+        public final List<RegWriter> must;
 
-        private State(boolean initialized, List<Event> may, List<Event> must) {
+        private State(boolean initialized, List<RegWriter> may, List<RegWriter> 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;

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

@@ -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('.'));