hernanponcedeleon · xeren · Nov 15, 2023
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java
@@ -98,11 +98,15 @@ public IValue makeValue(BigInteger value, IntegerType type) {
     }
 
     public Expression makeCast(Expression expression, Type type) {
+        return makeCast(expression, type, false);
+    }
+
+    public Expression makeCast(Expression expression, Type type, boolean signed) {
         if (type instanceof BooleanType) {
             return makeBooleanCast(expression);
         }
         if (type instanceof IntegerType integerType) {
-            return makeIntegerCast(expression, integerType, false);
+            return makeIntegerCast(expression, integerType, signed);
         }
         throw new UnsupportedOperationException(String.format("Cast %s into %s.", expression, type));
     }
@@ -242,9 +246,8 @@ public Expression makeExtract(int fieldIndex, Expression object) {
     // Pointers
 
     public Expression makeGetElementPointer(Type indexingType, Expression base, List<Expression> offsets) {
-        //TODO getPointerType()
-        Preconditions.checkArgument(base.getType().equals(types.getArchType()),
+        Preconditions.checkArgument(base.getType() instanceof IntegerType t && t.isPointer(),
                 "Applying offsets to non-pointer expression.");
-        return new GEPExpression(types.getArchType(), indexingType, base, offsets);
+        return new GEPExpression(base.getType(), indexingType, base, offsets);
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprBin.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprBin.java
@@ -17,7 +17,10 @@ public class IExprBin extends IExpr {
 
     public IExprBin(IntegerType type, Expression lhs, IOpBin op, Expression rhs) {
         super(type);
-    	Preconditions.checkArgument(lhs.getType().equals(rhs.getType()),
+    	Preconditions.checkArgument(lhs.getType().equals(rhs.getType()) ||
+                        op.equals(IOpBin.ADD) &&
+                                lhs.getType() instanceof IntegerType leftType && leftType.isPointer() &&
+                                rhs.getType() instanceof IntegerType rightType && !rightType.isPointer(),
                 "The types of %s and %s do not match.", lhs, rhs);
         this.lhs = lhs;
         this.rhs = rhs;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/IntegerType.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/IntegerType.java
@@ -9,15 +9,21 @@ public final class IntegerType implements Type {
     final static int MATHEMATICAL = -1;
 
     private final int bitWidth;
+    private final boolean isPointer;
 
-    IntegerType(int bitWidth) {
+    IntegerType(int bitWidth, boolean isPointer) {
         this.bitWidth = bitWidth;
+        this.isPointer = isPointer;
     }
 
     public boolean isMathematical() {
         return bitWidth == MATHEMATICAL;
     }
 
+    public boolean isPointer() {
+        return isPointer;
+    }
+
     public int getBitWidth() {
         checkState(bitWidth > 0, "Invalid integer bound %s", bitWidth);
         return bitWidth;
@@ -59,16 +65,16 @@ public boolean equals(Object obj) {
         if (obj == this) {
             return true;
         }
-        return obj instanceof IntegerType other && other.bitWidth == this.bitWidth;
+        return obj instanceof IntegerType other && isPointer == other.isPointer && bitWidth == other.bitWidth;
     }
 
     @Override
     public int hashCode() {
-        return 31 * bitWidth;
+        return (isPointer ? 1 : 0) + 31 * bitWidth;
     }
 
     @Override
     public String toString() {
-        return isMathematical() ? "int" : "bv" + bitWidth;
+        return isPointer ? "ptr" : isMathematical() ? "int" : "bv" + bitWidth;
     }
 }
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/TypeFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/type/TypeFactory.java
@@ -15,8 +15,9 @@ public final class TypeFactory {
 
     private final VoidType voidType = new VoidType();
     private final BooleanType booleanType = new BooleanType();
+    private final IntegerType pointerType = new IntegerType(64, true);
     private final IntegerType pointerDifferenceType;
-    private final IntegerType mathematicalIntegerType = new IntegerType(IntegerType.MATHEMATICAL);
+    private final IntegerType mathematicalIntegerType = new IntegerType(IntegerType.MATHEMATICAL, false);
 
     private final Normalizer typeNormalizer = new Normalizer();
 
@@ -35,8 +36,8 @@ public BooleanType getBooleanType() {
 
     public VoidType getVoidType() { return voidType; }
 
-    public Type getPointerType() {
-        return pointerDifferenceType;
+    public IntegerType getPointerType() {
+        return pointerType;
     }
 
     public IntegerType getIntegerType() {
@@ -45,7 +46,7 @@ public IntegerType getIntegerType() {
 
     public IntegerType getIntegerType(int bitWidth) {
         checkArgument(bitWidth > 0, "Non-positive bit width %s.", bitWidth);
-        return typeNormalizer.normalize(new IntegerType(bitWidth));
+        return typeNormalizer.normalize(new IntegerType(bitWidth, false));
     }
 
     public FunctionType getFunctionType(Type returnType, List<? extends Type> parameterTypes) {

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
@@ -215,7 +215,7 @@ public void initLocEqConst(String locName, Expression iValue){
     public void initRegEqLocPtr(int regThread, String regName, String locName, Type type) {
         MemoryObject object = getOrNewMemoryObject(locName);
         Register reg = getOrNewRegister(regThread, regName, type);
-        addChild(regThread, EventFactory.newLocal(reg, object));
+        addChild(regThread, EventFactory.newLocal(reg, expressions.makeCast(object, type)));
     }
 
     public void initRegEqLocVal(int regThread, String regName, String locName, Type type) {

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java
@@ -194,7 +194,7 @@ public Object visitThreadArguments(LitmusCParser.ThreadArgumentsContext ctx){
                         }
                     }
                 }
-                Register register = programBuilder.getOrNewRegister(scope, name, archType);
+                Register register = programBuilder.getOrNewRegister(scope, name, object.getType());
                 programBuilder.addChild(currentThread, EventFactory.newLocal(register, object));
                 id++;
             }
@@ -499,15 +499,18 @@ public Object visitNreAssignment(LitmusCParser.NreAssignmentContext ctx){
     @Override
     public Object visitNreRegDeclaration(LitmusCParser.NreRegDeclarationContext ctx){
         Register register = programBuilder.getRegister(scope, ctx.varName().getText());
-        if(register == null){
-            register = programBuilder.getOrNewRegister(scope, ctx.varName().getText(), archType);
-            if(ctx.re() != null){
-                returnRegister = register;
-                ctx.re().accept(this);
-            }
-            return null;
+        if (register != null) {
+            throw new ParsingException("Register " + ctx.varName().getText() + " is already initialised");
+        }
+        // More types are possible
+        final IntegerType type = ctx.typeSpecifier().Ast().isEmpty() ? archType :
+                programBuilder.getTypeFactory().getPointerType();
+        register = programBuilder.getOrNewRegister(scope, ctx.varName().getText(), type);
+        if (ctx.re() != null) {
+            returnRegister = register;
+            ctx.re().accept(this);
         }
-        throw new ParsingException("Register " + ctx.varName().getText() + " is already initialised");
+        return null;
     }
 
     @Override

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java
@@ -44,7 +44,7 @@ public class VisitorLlvm extends LLVMIRBaseVisitor<Expression> {
     private final Program program = new Program(new Memory(), Program.SourceLanguage.LLVM);
     private final TypeFactory types = TypeFactory.getInstance();
     private final ExpressionFactory expressions = ExpressionFactory.getInstance();
-    private final Type pointerType = types.getPointerType();
+    private final IntegerType pointerType = types.getPointerType();
     private final IntegerType integerType = types.getArchType();
     private final Map<String, Expression> constantMap = new HashMap<>();
     private final Map<String, TypeDefContext> typeDefinitionMap = new HashMap<>();
@@ -818,7 +818,7 @@ public Expression visitConstant(ConstantContext ctx) {
 
     @Override
     public Expression visitNullConst(NullConstContext ctx) {
-        return expressions.makeZero((IntegerType) pointerType);
+        return expressions.makeZero(pointerType);
     }
 
     @Override

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java
@@ -1,7 +1,7 @@
 package com.dat3m.dartagnan.program;
 
 import com.dat3m.dartagnan.exception.MalformedProgramException;
-import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.IExpr;
 import com.dat3m.dartagnan.expression.IConst;
 import com.dat3m.dartagnan.expression.processing.ExpressionVisitor;
 import com.dat3m.dartagnan.expression.type.FunctionType;
@@ -17,7 +17,7 @@
 import java.util.*;
 import java.util.stream.Collectors;
 
-public class Function implements Expression {
+public class Function extends IExpr {
 
     protected String name;
     protected Event entry; // Can be null for intrinsics
@@ -34,6 +34,7 @@ public class Function implements Expression {
     protected int dummyCount = 0;
 
     public Function(String name, FunctionType type, List<String> parameterNames, int id, Event entry) {
+        super(TypeFactory.getInstance().getPointerType());
         Preconditions.checkArgument(type.getParameterTypes().size() == parameterNames.size());
         Preconditions.checkArgument(entry == null || entry.getPredecessor() == null,
                 "The entry event of a function is not allowed to have predecessors.");
@@ -57,11 +58,6 @@ public Function(String name, FunctionType type, List<String> parameterNames, int
         }
     }
 
-    @Override
-    public Type getType() {
-        return TypeFactory.getInstance().getArchType();
-    }
-
     public String getName() { return this.name; }
     public void setName(String name) { this.name = name; }
 

diff --git a/...agnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java b/...agnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java
@@ -3,6 +3,10 @@
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.IConst;
 import com.dat3m.dartagnan.expression.IExprBin;
+import com.dat3m.dartagnan.expression.IExprUn;
+import com.dat3m.dartagnan.expression.op.IOpUn;
+import com.dat3m.dartagnan.expression.type.IntegerType;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.core.Local;
@@ -37,6 +41,7 @@
  */
 public class AndersenAliasAnalysis implements AliasAnalysis {
 
+    private final IntegerType pointerType = TypeFactory.getInstance().getPointerType();
     ///When a pointer set gains new content, it is added to this queue
     private final Queue<Object> variables = new ArrayDeque<>();
     ///Super set of all pointer sets in this analysis
@@ -150,11 +155,11 @@ private void processLocs(MemoryCoreEvent e) {
 
     private void processRegs(Local e) {
         Register register = e.getResultRegister();
-        Expression expr = e.getExpr();
+        Expression expr = ignoreCasts(e.getExpr());
         if (expr instanceof Register) {
             // r1 = r2 -> add edge r2 --> r1
             addEdge(expr, register);
-        } else if (expr instanceof IExprBin iBin && iBin.getLHS() instanceof Register) {
+        } else if (expr instanceof IExprBin iBin && ignoreCasts(iBin.getLHS()) instanceof Register) {
             addAllAddresses(register, maxAddressSet);
             variables.add(register);
         } else if (expr instanceof MemoryObject mem) {
@@ -179,7 +184,7 @@ private void algorithm() {
                                 // Add location to variables if edge is new.
                                 variables.add(address);
                             }
-                        } else if (e instanceof Store store && store.getMemValue() instanceof Register register) {
+                        } else if (e instanceof Store store && ignoreCasts(store.getMemValue()) instanceof Register register) {
                             // *variable = register
                             // Add edge from register to location
                             if (addEdge(register, address)) {
@@ -200,7 +205,7 @@ private void algorithm() {
     }
 
     private void processResults(Local e) {
-        Expression exp = e.getExpr();
+        Expression exp = ignoreCasts(e.getExpr());
         Register reg = e.getResultRegister();
         if (exp instanceof MemoryObject mem) {
             addTarget(reg, new Location(mem, 0));
@@ -209,9 +214,9 @@ private void processResults(Local e) {
         if (!(exp instanceof IExprBin iBin)) {
             return;
         }
-        Expression base = iBin.getLHS();
+        Expression base = ignoreCasts(iBin.getLHS());
         if (base instanceof MemoryObject mem) {
-            Expression rhs = iBin.getRHS();
+            Expression rhs = ignoreCasts(iBin.getRHS());
             //FIXME Address extends IConst
             if (rhs instanceof IConst ic) {
                 addTarget(reg, new Location(mem, ic.getValueAsInt()));
@@ -320,6 +325,14 @@ public String toString() {
         }
     }
 
+    private Expression ignoreCasts(Expression expression) {
+        return expression instanceof IExprUn unary &&
+                (unary.getOp() == IOpUn.CAST_SIGNED || unary.getOp() == IOpUn.CAST_UNSIGNED) &&
+                (unary.getType().isMathematical() ||
+                        !pointerType.isMathematical() && unary.getType().getBitWidth() >= pointerType.getBitWidth()) ?
+                ignoreCasts(unary.getInner()) : expression;
+    }
+
     private boolean addEdge(Object v1, Object v2) {
         return edges.computeIfAbsent(v1, key -> new HashSet<>()).add(v2);
     }

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java
@@ -33,8 +33,8 @@ public class Alloc extends AbstractEvent implements RegReader, RegWriter {
     private boolean isHeapAllocation;
 
     public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation) {
-        Preconditions.checkArgument(resultRegister.getType() == TypeFactory.getInstance().getArchType());
-        Preconditions.checkArgument(arraySize.getType() instanceof IntegerType);
+        Preconditions.checkArgument(resultRegister.getType() instanceof IntegerType t && t.isPointer());
+        Preconditions.checkArgument(arraySize.getType() instanceof IntegerType t && !t.isPointer());
         this.resultRegister = resultRegister;
         this.arraySize = arraySize;
         this.allocationType = allocType;

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java
@@ -35,7 +35,7 @@ public class MemoryObject extends IConst {
     private final HashMap<Integer, Expression> initialValues = new HashMap<>();
 
     MemoryObject(int index, int size, boolean isStaticallyAllocated) {
-        super(TypeFactory.getInstance().getArchType());
+        super(TypeFactory.getInstance().getPointerType());
         this.index = index;
         this.size = size;
         this.isStatic = isStaticallyAllocated;

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java
@@ -121,7 +121,7 @@ private void program0(Alias method, Result... expect) throws InvalidConfiguratio
         Register r0 = b.getOrNewRegister(0, "r0");
         //this is undefined behavior in C11
         //the expression does not match a sum, but x occurs in it
-        b.addChild(0, newLocal(r0, mult(x, 1)));
+        b.addChild(0, newLocal(r0, mult(expressions.makeIntegerCast(x, types.getArchType(), false), 1)));
         Store e0 = newStore(r0);
         b.addChild(0, e0);
         Store e1 = newStore(plus(r0, 1));
@@ -309,8 +309,8 @@ private void program4(Alias method, Result... expect) throws InvalidConfiguratio
 
         b.newThread(0);
         Register r0 = b.getOrNewRegister(0, "r0");
-        b.addChild(0, newLocal(r0, mult(x, 0)));
-        b.addChild(0, newLocal(r0, y));
+        b.addChild(0, newLocal(r0, mult(expressions.makeCast(x, types.getArchType(), false), 0)));
+        b.addChild(0, newLocal(r0, expressions.makeCast(y, types.getArchType(), false)));
         Store e0 = newStore(r0);
         b.addChild(0, e0);
         Store e1 = newStore(x);
@@ -353,10 +353,10 @@ private void program5(Alias method, Result... expect) throws InvalidConfiguratio
 
         b.newThread(0);
         Register r0 = b.getOrNewRegister(0, "r0");
-        b.addChild(0, newLocal(r0, y));
+        b.addChild(0, newLocal(r0, expressions.makeCast(y, types.getArchType(), false)));
         Store e0 = newStore(r0);
         b.addChild(0, e0);
-        b.addChild(0, newLocal(r0, mult(x, 0)));
+        b.addChild(0, newLocal(r0, mult(expressions.makeCast(x, types.getArchType(), false), 0)));
         Store e1 = newStore(x);
         b.addChild(0, e1);
         Store e2 = newStore(y);