Pointer expressions

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

@@ -507,6 +507,13 @@ public TypedFormula<BooleanType, BooleanFormula> visitIntCmpExpression(IntCmpExp
 
         // ====================================================================================
         // Pointers
+        @Override
+        public TypedFormula<PointerType, ?> visitPtrLiteral(PointerLiteral literal) {
+            final Formula result = context.useIntegers
+                    ? integerFormulaManager().makeNumber(literal.getValue())
+                    : bitvectorFormulaManager().makeBitvector(types.getArchType().getBitWidth(), literal.getValue());
+            return new TypedFormula<>(literal.getType(), result);
+        }
 
         @Override
         public TypedFormula<PointerType, ?> visitPointerAddExpression(PointerAddExpr expr) {

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java

@@ -317,6 +317,10 @@ public Expression makeAggregateCmp(Expression x, AggregateCmpOp op, Expression y
     // -----------------------------------------------------------------------------------------------------------------
     // Pointers
 
+    public PointerLiteral makeValue(BigInteger value, PointerType type) {
+        return new PointerLiteral(type, value);
+    }
+
     public Expression makeGetElementPointer(Type indexingType, Expression base, List<Expression> offsets) {
         Preconditions.checkArgument(base.getType().equals(types.getPointerType()),
                 "Applying offsets to non-pointer expression.");
@@ -360,6 +364,7 @@ public Expression makeIntToPtrCast(Expression operand) {
         return new IntToPtrCast(types.getPointerType(), operand);
     }
 
+
     public Expression makeNullLiteral(PointerType pointerType) {
         return new NullLiteral(pointerType);
     }

dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionVisitor.java

@@ -63,6 +63,7 @@ public interface ExpressionVisitor<TRet> {
     default TRet visitPtrToIntCastExpression(PtrToIntCast expr) { return visitCastExpression(expr); }
     default TRet visitPtrCmpExpression(PtrCmpExpr expr) { return visitBinaryExpression(expr); }
     default TRet visitNullLiteral(NullLiteral lit) { return visitLeafExpression(lit); }
+    default TRet visitPtrLiteral(PointerLiteral lit) {return visitLeafExpression(lit);}
 
     // =================================== Generic ===================================
     default TRet visitITEExpression(ITEExpr expr) { return visitExpression(expr); }
@@ -80,5 +81,4 @@ private static UnsupportedOperationException unsupported(Expression expr, Class<
                 expr.getClass().getSimpleName(), clazz.getSimpleName());
         return new UnsupportedOperationException(error);
     }
-
 }

dartagnan/src/main/java/com/dat3m/dartagnan/expression/pointer/PointerLiteral.java

@@ -0,0 +1,39 @@
+package com.dat3m.dartagnan.expression.pointer;
+
+import com.dat3m.dartagnan.expression.ExpressionVisitor;
+import com.dat3m.dartagnan.expression.base.LiteralExpressionBase;
+import com.dat3m.dartagnan.expression.type.IntegerType;
+import com.dat3m.dartagnan.expression.type.PointerType;
+import com.google.common.base.Preconditions;
+
+import java.math.BigInteger;
+
+public final class PointerLiteral extends LiteralExpressionBase<PointerType> {
+
+    private final BigInteger value;
+
+    public PointerLiteral(PointerType type, BigInteger value) {
+        super(type);
+        this.value = value;
+    }
+
+    public BigInteger getValue() {
+        return value;
+    }
+
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) {
+        return visitor.visitPtrLiteral(this);
+    }
+
+
+    @Override
+    public boolean equals(Object o) {
+        return this == o || o instanceof PointerLiteral val && getType().equals(val.getType()) && value.equals(val.value);
+    }
+
+    @Override
+    public String toString() {
+        return String.format("%s(%s)", getType(), value);
+    }
+}

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

@@ -42,8 +42,7 @@ public class MemToReg implements FunctionProcessor {
     private static final TypeFactory types = TypeFactory.getInstance();
     private static final ExpressionFactory expressions = ExpressionFactory.getInstance();
 
-    private MemToReg() {
-    }
+    private MemToReg() {}
 
     public static MemToReg fromConfig(Configuration config) throws InvalidConfigurationException {
         return new MemToReg();

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

@@ -4,9 +4,11 @@
 import com.dat3m.dartagnan.expression.ExpressionFactory;
 import com.dat3m.dartagnan.expression.ExpressionVisitor;
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
+import com.dat3m.dartagnan.expression.pointer.PointerLiteral;
 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.PointerType;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Function;
 import com.dat3m.dartagnan.program.IRHelper;
@@ -24,6 +26,7 @@
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
+import java.math.BigInteger;
 import java.util.*;
 import java.util.stream.Collectors;
 
@@ -97,12 +100,12 @@ private void findAndTransformAddressTakenFunctions(
         }
     }
 
-    private boolean assignAddressToFunction(Function func, Map<Function, IntLiteral> func2AddressMap) {
-        final IntegerType ptrType = TypeFactory.getInstance().getArchType();
+    private boolean assignAddressToFunction(Function func, Map<Function, PointerLiteral> func2AddressMap) {
+        final PointerType ptrType = TypeFactory.getInstance().getPointerType();
         final ExpressionFactory expressions = ExpressionFactory.getInstance();
         if (!func2AddressMap.containsKey(func)) {
             logger.debug("Assigned address \"{}\" to function \"{}\"", nextAvailableFuncAddress, func);
-            func2AddressMap.put(func, expressions.makeValue(nextAvailableFuncAddress, ptrType));
+            func2AddressMap.put(func, expressions.makeValue(BigInteger.valueOf(nextAvailableFuncAddress), ptrType));
             nextAvailableFuncAddress += 8;
             return true;
         }
@@ -119,7 +122,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, PointerLiteral> func2AddressMap) {
         final ExpressionFactory expressions = ExpressionFactory.getInstance();
 
         int devirtCounter = 0;
@@ -147,7 +150,7 @@ 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 PointerLiteral targetAddress = func2AddressMap.get(possibleTarget);
                 final Label caseLabel = EventFactory.newLabel(String.format("__Ldevirt_%s#%s", targetAddress.getValue(), devirtCounter));
                 final CondJump caseJump = EventFactory.newJump(expressions.makeEQ(funcPtr, targetAddress), caseLabel);
                 caseLabels.add(caseLabel);
@@ -178,7 +181,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, PointerLiteral> func2AddressMap) {
         Preconditions.checkArgument(needsDevirtualization(call));
         return func2AddressMap.keySet().stream()
                 .filter(f -> f.getFunctionType() == call.getCallType())
@@ -210,7 +213,7 @@ public Expression visitFunction(Function function) {
 
     private static class FunctionToAddressTransformer extends ExprTransformer {
 
-        private final Map<Function, IntLiteral> func2AddressMap = new HashMap<>();
+        private final Map<Function, PointerLiteral> func2AddressMap = new HashMap<>();
 
         @Override
         public Expression visitFunction(Function function) {

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

@@ -7,10 +7,7 @@
 import com.dat3m.dartagnan.expression.integers.IntBinaryOp;
 import com.dat3m.dartagnan.expression.integers.IntLiteral;
 import com.dat3m.dartagnan.expression.processing.ExprTransformer;
-import com.dat3m.dartagnan.expression.type.AggregateType;
-import com.dat3m.dartagnan.expression.type.FunctionType;
-import com.dat3m.dartagnan.expression.type.IntegerType;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.expression.type.*;
 import com.dat3m.dartagnan.program.*;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.*;
@@ -85,6 +82,7 @@ public class ThreadCreation implements ProgramProcessor {
     private final IntegerType archType = types.getArchType();
     // The thread state consists of two flags: ALIVE and JOINABLE.
     private final IntegerType threadStateType = types.getIntegerType(2);
+    private final PointerType pointerType = types.getPointerType();
 
     private ThreadCreation(Configuration config) throws InvalidConfigurationException {
         config.inject(this);
@@ -186,7 +184,12 @@ private void resolveDynamicThreadJoin(Program program, List<ThreadData> threadDa
 
         for (DynamicThreadJoin join : program.getThreadEvents(DynamicThreadJoin.class)) {
             final Thread caller = join.getThread();
-            final Expression tidExpr = join.getTid();
+            final Expression tidExpr_ = join.getTid();
+            final Expression tidExpr = tidExpr_.getType() instanceof PointerType ? expressions.makePtrToIntCast(tidExpr_) : tidExpr_;
+
+
+
+
 
             final Register joinRegister = join.getResultRegister();
             final IntegerType statusType = (IntegerType) ((AggregateType)joinRegister.getType()).getFields().get(0).type();
@@ -462,7 +465,7 @@ private void replaceThreadLocalsWithStackalloc(Memory memory, Thread thread) {
             final List<Event> initialization = new ArrayList<>();
             for (Integer initOffset : memoryObject.getInitializedFields()) {
                 initialization.add(EventFactory.newStore(
-                        exprs.makeAdd(reg, exprs.makeValue(initOffset, types.getArchType())),
+                        exprs.makePtrAdd(reg, exprs.makeValue(initOffset, types.getArchType())),
                         memoryObject.getInitialValue(initOffset)
                 ));
             }