Devirtualization with proper addresses (#944)

* Devirtualization now uses proper MemoryObjects to represent function addresses
ExprSimplifier can simplify comparisons on simple MemoryObjects

Author: ThomasHaas

dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java

@@ -12,6 +12,7 @@
 import com.dat3m.dartagnan.expression.integers.*;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
 import com.dat3m.dartagnan.expression.utils.IntegerHelper;
+import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.google.common.base.VerifyException;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Iterables;
@@ -165,6 +166,24 @@ public Expression visitIntCmpExpression(IntCmpExpr cmp) {
             return expressions.makeValue(cmpResult);
         }
 
+        // ------- Operations on memory objects -------
+        if (left instanceof MemoryObject lMem && right instanceof MemoryObject rMem) {
+            final boolean sameObj = lMem.equals(rMem);
+
+            final Boolean cmpResult = switch (op) {
+                case EQ -> sameObj;
+                case NEQ -> !sameObj;
+                case LT, ULT -> sameObj ? false : null;
+                case LTE, ULTE -> sameObj ? true : null;
+                default ->
+                    throw new VerifyException(String.format("Unexpected comparison operator '%s'. Missing normalization?", op));
+            };
+
+            if (cmpResult != null) {
+                return expressions.makeValue(cmpResult);
+            }
+        }
+
         return expressions.makeIntCmp(left, op, right);
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java

@@ -3,11 +3,8 @@
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.ExpressionVisitor;
-import com.dat3m.dartagnan.expression.integers.IntLiteral;
 import com.dat3m.dartagnan.expression.processing.ExprTransformer;
 import com.dat3m.dartagnan.expression.processing.ExpressionInspector;
-import com.dat3m.dartagnan.expression.type.IntegerType;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.IRHelper;
 import com.dat3m.dartagnan.program.Program;
@@ -40,8 +37,6 @@ public class NaiveDevirtualisation implements ProgramProcessor {
 
     private static final Logger logger = LogManager.getLogger(NaiveDevirtualisation.class);
 
-    private int nextAvailableFuncAddress = 8; // We use 8-aligned addresses
-
     private NaiveDevirtualisation() {
     }
 
@@ -97,16 +92,16 @@ private void findAndTransformAddressTakenFunctions(
         }
     }
 
-    private boolean assignAddressToFunction(Function func, Map<Function, IntLiteral> func2AddressMap) {
-        final IntegerType ptrType = TypeFactory.getInstance().getArchType();
-        final ExpressionFactory expressions = ExpressionFactory.getInstance();
-        if (!func2AddressMap.containsKey(func)) {
-            logger.debug("Assigned address \"{}\" to function \"{}\"", nextAvailableFuncAddress, func);
-            func2AddressMap.put(func, expressions.makeValue(nextAvailableFuncAddress, ptrType));
-            nextAvailableFuncAddress += 8;
-            return true;
+    private boolean assignAddressToFunction(Function func, Map<Function, MemoryObject> func2AddressMap) {
+        if (func2AddressMap.containsKey(func)) {
+            return false;
         }
-        return false;
+
+        final MemoryObject funcAddr = func.getProgram().getMemory().allocate(1);
+        funcAddr.setName(String.format("__funcAddr_%s", func.getName()));
+        func2AddressMap.put(func, funcAddr);
+        logger.debug("Assigned address to function \"{}\"", func);
+        return true;
     }
 
     private void applyTransformerToEvent(Event e, ExpressionVisitor<Expression> transformer) {
@@ -119,7 +114,7 @@ private void applyTransformerToEvent(Event e, ExpressionVisitor<Expression> tran
         }
     }
 
-    private void devirtualise(Function function, Map<Function, IntLiteral> func2AddressMap) {
+    private void devirtualise(Function function, Map<Function, MemoryObject> func2AddressMap) {
         final ExpressionFactory expressions = ExpressionFactory.getInstance();
 
         int devirtCounter = 0;
@@ -147,8 +142,8 @@ private void devirtualise(Function function, Map<Function, IntLiteral> func2Addr
             final Expression funcPtr = call.getCallTarget();
             // Construct call table
             for (Function possibleTarget : possibleTargets) {
-                final IntLiteral targetAddress = func2AddressMap.get(possibleTarget);
-                final Label caseLabel = EventFactory.newLabel(String.format("__Ldevirt_%s#%s", targetAddress.getValue(), devirtCounter));
+                final MemoryObject targetAddress = func2AddressMap.get(possibleTarget);
+                final Label caseLabel = EventFactory.newLabel(String.format("__Ldevirt_%s#%s", possibleTarget.getName(), devirtCounter));
                 final CondJump caseJump = EventFactory.newJump(expressions.makeEQ(funcPtr, targetAddress), caseLabel);
                 caseLabels.add(caseLabel);
                 caseJumps.add(caseJump);
@@ -178,7 +173,7 @@ private boolean needsDevirtualization(CallEvent call) {
         return !call.isDirectCall();
     }
 
-    private List<Function> getPossibleTargets(CallEvent call, Map<Function, IntLiteral> func2AddressMap) {
+    private List<Function> getPossibleTargets(CallEvent call, Map<Function, MemoryObject> func2AddressMap) {
         Preconditions.checkArgument(needsDevirtualization(call));
         return func2AddressMap.keySet().stream()
                 .filter(f -> f.getFunctionType() == call.getCallType())
@@ -210,7 +205,7 @@ public Expression visitFunction(Function function) {
 
     private static class FunctionToAddressTransformer extends ExprTransformer {
 
-        private final Map<Function, IntLiteral> func2AddressMap = new HashMap<>();
+        private final Map<Function, MemoryObject> func2AddressMap = new HashMap<>();
 
         @Override
         public Expression visitFunction(Function function) {