Add support alloc-free

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

@@ -209,10 +209,6 @@ public BooleanFormula sameValue(MemoryCoreEvent first, MemoryCoreEvent second) {
         return addresses.get(event);
     }
 
-    public TypedFormula<?, ?> address(MemFree free) {
-        return addresses.get(free);
-    }
-
     public TypedFormula<?, ?> address(MemoryObject memoryObject) { return objAddress.get(memoryObject); }
 
     public TypedFormula<IntegerType, ?> size(MemoryObject memoryObject) {
@@ -332,9 +328,6 @@ private void initialize() {
                     values.put(e, exprEncoder.encodeAt(store.getMemValue(), e));
                 }
             }
-            if (e instanceof MemFree free) {
-                addresses.put(e, exprEncoder.encodeAt(free.getAddress(), free));
-            }
         }
     }
 }

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

@@ -13,7 +13,6 @@
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.Assert;
 import com.dat3m.dartagnan.program.event.core.CondJump;
-import com.dat3m.dartagnan.program.event.core.MemFree;
 import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.smt.ModelExt;
@@ -97,10 +96,6 @@ public boolean isAllocated(MemoryObject memObj) {
         return evaluateAt(ctx.address(e), e);
     }
 
-    public TypedValue<?, ?> address(MemFree e) {
-        return evaluateAt(ctx.address(e), e);
-    }
-
     public TypedValue<?, ?> address(MemoryObject e) {
         return evaluate(ctx.address(e));
     }

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

@@ -5,7 +5,6 @@
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
-import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 import com.dat3m.dartagnan.utils.Utils;
@@ -23,6 +22,7 @@
 import java.io.FileWriter;
 import java.io.IOException;
 import java.util.*;
+import java.util.stream.Collectors;
 
 import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory;
 import static com.dat3m.dartagnan.configuration.OptionNames.*;
@@ -31,13 +31,13 @@ public interface AliasAnalysis {
 
     Logger logger = LogManager.getLogger(AliasAnalysis.class);
 
-    boolean mustAlias(Event a, Event b);
+    boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b);
 
-    boolean mayAlias(Event a, Event b);
+    boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b);
 
-    boolean mustObjectAlias(Event a, Event b);
+    boolean mustObjectAlias(MemoryCoreEvent a, MemoryCoreEvent b);
 
-    boolean mayObjectAlias(Event a, Event b);
+    boolean mayObjectAlias(MemoryCoreEvent a, MemoryCoreEvent b);
 
     /**
      * Returns an overapproximation of the MSA points in the byte range of the specified event.
@@ -135,22 +135,22 @@ private CombinedAliasAnalysis(AliasAnalysis a1, AliasAnalysis a2) {
         }
 
         @Override
-        public boolean mustAlias(Event a, Event b) {
+        public boolean mustAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
             return a1.mustAlias(a, b) || a2.mustAlias(a, b);
         }
 
         @Override
-        public boolean mayAlias(Event a, Event b) {
+        public boolean mayAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
             return a1.mayAlias(a, b) && a2.mayAlias(a, b);
         }
 
         @Override
-        public boolean mustObjectAlias(Event a, Event b) {
+        public boolean mustObjectAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
             return a1.mustObjectAlias(a, b) || a2.mustObjectAlias(a, b);
         }
 
         @Override
-        public boolean mayObjectAlias(Event a, Event b) {
+        public boolean mayObjectAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
             return a1.mayObjectAlias(a, b) && a2.mayObjectAlias(a, b);
         }
 
@@ -178,17 +178,18 @@ default Graphviz getGraphVisualization() {
     }
 
     private void populateAddressGraph(Map<String, Set<String>> may, Map<String, Set<String>> must,
-            List<? extends Event> list1, List<? extends Event> list2, Config configuration) {
-        for (final Event event1 : list1) {
+            List<? extends MemoryCoreEvent> list1, List<? extends MemoryCoreEvent> list2,
+            Config configuration) {
+        for (final MemoryCoreEvent event1 : list1) {
             final String node1 = repr(event1, configuration);
             if (node1 == null) {
                 continue;
             }
             final Set<String> maySet = may.computeIfAbsent(node1, k -> new HashSet<>());
             final Set<String> mustSet = must.computeIfAbsent(node1, k -> new HashSet<>());
-            for (final Event event2 : list2) {
+            for (final MemoryCoreEvent event2 : list2) {
                 final String node2 = repr(event2, configuration);
-                if ((event1 instanceof MemoryCoreEvent && event2 instanceof MemoryCoreEvent)
+                if ((!(event1 instanceof MemFree) && !(event2 instanceof MemFree))
                         || (event1 instanceof MemFree && event2 instanceof MemFree)) {
                     if (event1.getGlobalId() - event2.getGlobalId() >= 0) {
                         continue;
@@ -229,7 +230,9 @@ private Graphviz defaultGraph(Program program, Config configuration) {
         // A dashed orange line marks the existence of events that may object-alias.
         final Map<String, Set<String>> mayObjectGraph = new HashMap<>();
 
-        final List<MemoryCoreEvent> events = program.getThreadEvents(MemoryCoreEvent.class);
+        final List<MemoryCoreEvent> events = program.getThreadEvents(MemoryCoreEvent.class)
+                .stream().filter(e -> !(e instanceof MemFree) && !(e instanceof MemAlloc))
+                .collect(Collectors.toList());
         final List<MemAlloc> allocs = program.getThreadEvents(MemAlloc.class);
         final List<MemFree> frees = program.getThreadEvents(MemFree.class);
 
@@ -242,22 +245,16 @@ private Graphviz defaultGraph(Program program, Config configuration) {
         // Generates the graphs
         final var graphviz = new Graphviz();
         graphviz.beginGraph("alias");
-        // Group events
         for (final Thread thread : program.getThreads()) {
             graphviz.beginSubgraph("Thread" + thread.getId());
             graphviz.setEdgeAttributes("weight=100", "style=invis");
-            final List<Event> grouped = new ArrayList<>();
-            for (final Event event : thread.getEvents()) {
-                if (event instanceof MemoryCoreEvent || event instanceof MemAlloc || event instanceof MemFree) {
-                    if (!configuration.graphvizShowAll && event instanceof Init) {
-                        continue;
-                    }
-                    grouped.add(event);
+            final List<MemoryCoreEvent> memEvents = thread.getEvents(MemoryCoreEvent.class);
+            for (int i = 1; i < memEvents.size(); i++) {
+                final String node1 = repr(memEvents.get(i - 1), configuration);
+                final String node2 = repr(memEvents.get(i), configuration);
+                if (node1 == null || node2 == null) {
+                    continue;
                 }
-            }
-            for (int i = 1; i < grouped.size(); i++) {
-                final String node1 = repr(grouped.get(i - 1), configuration);
-                final String node2 = repr(grouped.get(i), configuration);
                 graphviz.addEdge(node1, node2);
             }
             graphviz.end();
@@ -301,7 +298,7 @@ private void generateGraph(Program program, Config configuration) {
         }
     }
 
-    private static String repr(Event event, Config configuration) {
+    private static String repr(MemoryCoreEvent event, Config configuration) {
         if (!configuration.graphvizShowAll && event instanceof Init) {
             return null;
         }

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

@@ -7,7 +7,6 @@
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis;
-import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.MemoryEvent;
 import com.dat3m.dartagnan.program.event.RegWriter;
 import com.dat3m.dartagnan.program.event.core.*;
@@ -54,7 +53,7 @@ public class AndersenAliasAnalysis implements AliasAnalysis {
     private final Map<Object, Set<Location>> addresses = new HashMap<>();
     private final Map<Register, Set<MemoryEvent>> events = new HashMap<>();
     private final Map<Register, Set<Location>> targets = new HashMap<>();
-    private final Map<Event, ImmutableSet<Location>> eventAddressSpaceMap = new HashMap<>();
+    private final Map<MemoryCoreEvent, ImmutableSet<Location>> eventAddressSpaceMap = new HashMap<>();
     // Maps memory events to additional offsets inside their byte range, which may match other accesses' bounds.
     private final Map<MemoryCoreEvent, List<Integer>> mixedAccesses = new HashMap<>();
 
@@ -86,23 +85,23 @@ public static AndersenAliasAnalysis fromConfig(Program program, Config config) {
     // ================================ API ================================
 
     @Override
-    public boolean mayAlias(Event x, Event y) {
+    public boolean mayAlias(MemoryCoreEvent x, MemoryCoreEvent y) {
         return !Sets.intersection(getMaxAddressSet(x), getMaxAddressSet(y)).isEmpty();
     }
 
     @Override
-    public boolean mustAlias(Event x, Event y) {
+    public boolean mustAlias(MemoryCoreEvent x, MemoryCoreEvent y) {
         Set<Location> lx = getMaxAddressSet(x);
         return lx.size() == 1 && lx.equals(getMaxAddressSet(y));
     }
 
     @Override
-    public boolean mayObjectAlias(Event a, Event b) {
+    public boolean mayObjectAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
         return !Sets.intersection(getAccessibleObjects(a), getAccessibleObjects(b)).isEmpty();
     }
 
     @Override
-    public boolean mustObjectAlias(Event a, Event b) {
+    public boolean mustObjectAlias(MemoryCoreEvent a, MemoryCoreEvent b) {
         Set<MemoryObject> objsA = getAccessibleObjects(a);
         return objsA.size() == 1 && objsA.equals(getAccessibleObjects(b));
     }
@@ -117,11 +116,11 @@ public List<Integer> mayMixedSizeAccesses(MemoryCoreEvent event) {
         return IntStream.range(1, bytes).boxed().toList();
     }
 
-    private ImmutableSet<Location> getMaxAddressSet(Event e) {
+    private ImmutableSet<Location> getMaxAddressSet(MemoryCoreEvent e) {
         return eventAddressSpaceMap.get(e);
     }
 
-    private Set<MemoryObject> getAccessibleObjects(Event e) {
+    private Set<MemoryObject> getAccessibleObjects(MemoryCoreEvent e) {
         Set<MemoryObject> objs = new HashSet<>();
         Set<Location> locs = getMaxAddressSet(e);
         if (locs != null) {
@@ -137,8 +136,8 @@ private void detectMixedSizeAccesses() {
             return;
         }
         final List<MemoryCoreEvent> events = eventAddressSpaceMap.keySet().stream()
-                .filter(e -> e instanceof MemoryCoreEvent)
-                .map(e -> (MemoryCoreEvent) e).collect(Collectors.toList());
+                .filter(e -> !(e instanceof MemAlloc) && !(e instanceof MemFree))
+                .collect(Collectors.toList());
         final List<Set<Integer>> offsets = new ArrayList<>();
         for (int i = 0; i < events.size(); i++) {
             final var set0 = new HashSet<Integer>();
@@ -176,9 +175,6 @@ private void fetchMixedOffsets(Set<Integer> setX, Set<Location> addressesX, int
     private void run(Program program) {
         List<MemoryCoreEvent> memEvents = program.getThreadEvents(MemoryCoreEvent.class);
         List<Local> locals = program.getThreadEvents(Local.class);
-        for (MemAlloc a : program.getThreadEvents(MemAlloc.class)) {
-            processAllocs(a);
-        }
         for (MemoryCoreEvent e : memEvents) {
             processLocs(e);
         }
@@ -191,22 +187,22 @@ private void run(Program program) {
             processResults(e);
         }
         for (MemoryCoreEvent e : memEvents) {
-            eventAddressSpaceMap.put(e, ImmutableSet.copyOf(getAddressSpace(e)));
-        }
-        for (MemFree f : program.getThreadEvents(MemFree.class)) {
-            eventAddressSpaceMap.put(f, ImmutableSet.copyOf(getAddressSpace(f)));
+            processResults(e);
         }
     }
 
-    private void processAllocs(MemAlloc a) {
-        Register r = a.getResultRegister();
-        Location base = new Location(a.getAllocatedObject(), 0);
-        eventAddressSpaceMap.put(a, ImmutableSet.of(base));
-        addAddress(r, base);
-        variables.add(r);
-    }
-
     private void processLocs(MemoryCoreEvent e) {
+        if (e instanceof MemFree) {
+            return;
+        }
+        if (e instanceof MemAlloc a) {
+            Register r = a.getResultRegister();
+            Location base = new Location(a.getAllocatedObject(), 0);
+            eventAddressSpaceMap.put(a, ImmutableSet.of(base));
+            addAddress(r, base);
+            variables.add(r);
+            return;
+        }
         Expression address = e.getAddress();
         // Collect for each v events of form: p = *v, *v = q
         if (address instanceof Register register) {
@@ -341,32 +337,29 @@ private void processResults(Local e) {
         }
     }
 
-    private Set<Location> getAddressSpace(Event e) {
-        Expression addrExpr;
-        if (e instanceof MemoryCoreEvent mce) {
-            addrExpr = mce.getAddress();
-        } else {
-            assert e instanceof MemFree;
-            addrExpr = ((MemFree) e).getAddress();
+    private void processResults(MemoryCoreEvent e) {
+        if (e instanceof MemAlloc) {
+            return;
         }
+        Expression address = e.getAddress();
         Set<Location> addresses;
-        if (addrExpr instanceof Register) {
-            Set<Location> target = targets.get(addrExpr);
-            addresses = target != null ? target : getAddresses(addrExpr);
+        if (address instanceof Register) {
+            Set<Location> target = targets.get(address);
+            addresses = target != null ? target : getAddresses(address);
         } else {
-            Constant addressConstant = new Constant(addrExpr);
+            Constant addressConstant = new Constant(address);
             if (addressConstant.failed) {
                 addresses = maxAddressSet;
             } else {
-                Verify.verify(addressConstant.location != null, "accessing a pure constant address");
+                Verify.verify(addressConstant.location != null, "memory event accessing a pure constant address");
                 addresses = ImmutableSet.of(addressConstant.location);
             }
         }
         if (addresses.isEmpty()) {
             logger.warn("Empty pointer set for {}", synContext.get().getContextInfo(e));
             addresses = maxAddressSet;
         }
-        return addresses;
+        eventAddressSpaceMap.put(e, ImmutableSet.copyOf(addresses));
     }
 
     private static final class Constant {