Pointer expressions

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

@@ -11,6 +11,7 @@
 import com.dat3m.dartagnan.expression.booleans.BoolUnaryOp;
 import com.dat3m.dartagnan.expression.integers.*;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
+import com.dat3m.dartagnan.expression.pointer.*;
 import com.dat3m.dartagnan.expression.type.*;
 import com.dat3m.dartagnan.expression.utils.ExpressionHelper;
 import com.dat3m.dartagnan.program.Register;
@@ -92,6 +93,10 @@ public TypedFormula<BooleanType, BooleanFormula> encodeBooleanFinal(Expression e
             variable = context.useIntegers
                     ? integerFormulaManager().makeVariable(name)
                     : bitvectorFormulaManager().makeVariable(integerType.getBitWidth(), name);
+        }else if (type instanceof PointerType) {
+            variable = context.useIntegers
+                    ? integerFormulaManager().makeVariable(name)
+                    : bitvectorFormulaManager().makeVariable(types.getArchType().getBitWidth(), name);
         } else if (type instanceof AggregateType aggType) {
             final List<Formula> fields = new ArrayList<>(aggType.getFields().size());
             for (TypeOffset field : aggType.getFields()) {
@@ -178,6 +183,15 @@ public void setEvent(Event e) {
             return (TypedFormula<IntegerType, ?>) typedFormula;
         }
 
+        @SuppressWarnings("unchecked")
+        public TypedFormula<PointerType, ?> encodePointerExpr(Expression expression) {
+            checkArgument(expression.getType() instanceof PointerType);
+            final TypedFormula<?, ?> typedFormula = encode(expression);
+            assert typedFormula.type() == expression.getType();
+            assert typedFormula.formula() instanceof IntegerFormula || typedFormula.formula() instanceof BitvectorFormula;
+            return (TypedFormula<PointerType, ?>) typedFormula;
+        }
+
         @SuppressWarnings("unchecked")
         public TypedFormula<BooleanType, BooleanFormula> encodeBooleanExpr(Expression expression) {
             Preconditions.checkArgument(expression.getType() instanceof BooleanType);
@@ -331,7 +345,6 @@ public TypedFormula<BooleanType, BooleanFormula> visitBoolUnaryExpression(BoolUn
         public TypedFormula<IntegerType, ?> visitIntSizeCastExpression(IntSizeCast expr) {
             final TypedFormula<IntegerType, ?> inner = encodeIntegerExpr(expr.getOperand());
             final Formula enc;
-
             if (expr.isNoop()) {
                 return inner;
             } else if (context.useIntegers) {
@@ -344,7 +357,6 @@ public TypedFormula<BooleanType, BooleanFormula> visitBoolUnaryExpression(BoolUn
                 }
             } else {
                 assert inner.formula() instanceof BitvectorFormula;
-
                 final BitvectorFormulaManager bvmgr = bitvectorFormulaManager();
                 final BitvectorFormula innerBv = (BitvectorFormula) inner.formula();
                 final int targetBitWidth = expr.getTargetType().getBitWidth();
@@ -492,6 +504,110 @@ public TypedFormula<BooleanType, BooleanFormula> visitIntCmpExpression(IntCmpExp
             return new TypedFormula<>(expr.getType(), enc);
         }
 
+
+        // ====================================================================================
+        // 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) {
+            final TypedFormula<PointerType, ?> base = encodePointerExpr(expr.getBase());
+            final TypedFormula<IntegerType, ?> offset = encodeIntegerExpr(expr.getOffset());
+
+            if (context.useIntegers) {
+                final IntegerFormula baseForm = (IntegerFormula) base.formula();
+                final IntegerFormula offsetForm = (IntegerFormula) offset.formula();
+
+                return new TypedFormula<>(base.getType(), integerFormulaManager().add(baseForm, offsetForm));
+            } else {
+                final BitvectorFormula baseForm = (BitvectorFormula) base.formula();
+                final BitvectorFormula offsetForm = (BitvectorFormula) offset.formula();
+
+                return new TypedFormula<>(base.getType(), bitvectorFormulaManager().add(baseForm, offsetForm));
+            }
+
+        }
+
+        @Override
+        public TypedFormula<IntegerType, ?> visitPtrToIntCastExpression(PtrToIntCast expr) {
+            // Todo: add support for extension
+            final TypedFormula<PointerType, ?> inner = encodePointerExpr(expr.getOperand());
+            final Formula enc;
+            if (context.useIntegers) {
+                final BigInteger highValue = BigInteger.TWO.pow(expr.getType().getBitWidth());
+                final IntegerFormulaManager imgr = integerFormulaManager();
+                enc = imgr.modulo((IntegerFormula) inner.formula(), imgr.makeNumber(highValue));
+            } else {
+                assert inner.formula() instanceof BitvectorFormula;
+                final BitvectorFormulaManager bvmgr = bitvectorFormulaManager();
+                final BitvectorFormula innerBv = (BitvectorFormula) inner.formula();
+                final int targetBitWidth = expr.getTargetType().getBitWidth();
+                final int sourceBitWidth = types.getArchType().getBitWidth();
+                assert (sourceBitWidth == bvmgr.getLength(innerBv));
+                enc = bvmgr.extract(innerBv, targetBitWidth - 1, 0);
+            }
+            return new TypedFormula<>(expr.getType(), enc);
+
+        }
+
+        @Override
+        public TypedFormula<PointerType, ?> visitIntToPtrCastExpression(IntToPtrCast expr) {
+
+            final TypedFormula<IntegerType, ?> address = encodeIntegerExpr(expr.getOperand());
+            return new TypedFormula<>(expr.getType(), address.formula());
+        }
+
+        @Override
+        public TypedFormula<BooleanType, BooleanFormula> visitPtrCmpExpression(PtrCmpExpr expr) {
+            if (context.useIntegers) {
+                final var left = (TypedFormula<PointerType, IntegerFormula>) encodePointerExpr(expr.getLeft());
+                final var right = (TypedFormula<PointerType, IntegerFormula>) encodePointerExpr(expr.getRight());
+
+                final IntegerFormulaManager imgr = integerFormulaManager();
+                final BooleanFormula result = switch (expr.getKind()) {
+                    case EQ -> imgr.equal(left.formula(), right.formula());
+                    case NEQ -> bmgr.not(fmgr.equal(left.formula(), right.formula()));
+                    case LT -> imgr.lessThan(left.formula(), right.formula());
+                    case LTE -> imgr.lessOrEquals(left.formula(), right.formula());
+                    case GT -> imgr.greaterThan(left.formula(), right.formula());
+                    case GTE -> imgr.greaterOrEquals(left.formula(), right.formula());
+                };
+                return new TypedFormula<>(types.getBooleanType(), result);
+            }else{
+                final var left = (TypedFormula<PointerType, BitvectorFormula>) encodePointerExpr(expr.getLeft());
+                final var right = (TypedFormula<PointerType, BitvectorFormula>) encodePointerExpr(expr.getRight());
+                final BitvectorFormulaManager bvgr = bitvectorFormulaManager();
+                final BooleanFormula result = switch (expr.getKind()) {
+                    case EQ -> bvgr.equal(left.formula(), right.formula());
+                    case NEQ -> bmgr.not(fmgr.equal(left.formula(), right.formula()));
+                    case LT -> bvgr.lessThan(left.formula(), right.formula(),false);
+                    case LTE -> bvgr.lessOrEquals(left.formula(), right.formula(),false);
+                    case GT -> bvgr.greaterThan(left.formula(), right.formula(),false);
+                    case GTE -> bvgr.greaterOrEquals(left.formula(), right.formula(),false);
+                };
+                return new TypedFormula<>(types.getBooleanType(), result);
+        }
+            }
+
+        @Override
+        public TypedFormula<PointerType, ?> visitNullLiteral(NullLiteral lit) {
+            final Formula zero = context.useIntegers
+                    ? integerFormulaManager().makeNumber(0)
+                    : bitvectorFormulaManager().makeBitvector(types.getArchType().getBitWidth(), 0);
+
+            return new TypedFormula<>(lit.getType(), zero);
+        }
+
+
+
+
+
         // ====================================================================================
         // Aggregates
 
@@ -562,7 +678,8 @@ public TypedFormula<?, TupleFormula> visitInsertExpression(InsertExpr insert) {
 
         @Override
         public TypedFormula<?, ?> visitMemoryObject(MemoryObject memObj) {
-            return makeVariable(String.format("addrof(%s)", memObj), memObj.getType());
+            Formula result = makeVariable(String.format("addrof(%s)", memObj), memObj.getType()).formula();
+            return new TypedFormula<>(memObj.getType(), result);
         }
 
         @Override

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

@@ -426,7 +426,7 @@ private BooleanFormula encodeMemoryLayout(Memory memory) {
         final List<MemoryObject> memoryObjects = ImmutableList.copyOf(memory.getObjects());
         for (int i = 0; i < memoryObjects.size(); i++) {
             final MemoryObject cur = memoryObjects.get(i);
-            final Expression addrVar = context.address(cur);
+            final Expression addrVar = exprs.makePtrToIntCast(context.address(cur));
             final Expression sizeVar = context.size(cur);
 
             final Expression size;
@@ -459,7 +459,10 @@ private BooleanFormula encodeMemoryLayout(Memory memory) {
                 // First object is placed at alignment
                 enc.add(equate.apply(addrVar, alignment));
             } else {
-                final Expression nextAvailableAddr = exprs.makeAdd(context.address(prev), context.size(prev));
+                final Expression nextAvailableAddr = exprs.makeAdd(
+                        exprs.makePtrToIntCast(context.address(prev)),
+                        context.size(prev)
+                );
                 final Expression nextAlignedAddr = exprs.makeAdd(nextAvailableAddr,
                         exprs.makeSub(alignment, exprs.makeRem(nextAvailableAddr, alignment,  true))
                 );

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

@@ -6,6 +6,7 @@
 import com.dat3m.dartagnan.expression.integers.*;
 import com.dat3m.dartagnan.expression.misc.GEPExpr;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
+import com.dat3m.dartagnan.expression.pointer.*;
 import com.dat3m.dartagnan.expression.type.*;
 import com.dat3m.dartagnan.expression.utils.ExpressionHelper;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
@@ -201,6 +202,8 @@ public Expression makeIntegerCast(Expression operand, IntegerType targetType, bo
             return sourceType.equals(targetType) ? operand : new IntSizeCast(targetType, operand, signed);
         } else if (sourceType instanceof FloatType) {
             return new FloatToIntCast(targetType, operand, signed);
+        }else if (sourceType instanceof PointerType) {
+            return new PtrToIntCast(targetType, operand);
         }
 
         throw new UnsupportedOperationException(String.format("Cannot cast %s to %s.", sourceType, targetType));
@@ -314,21 +317,28 @@ 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) {
-        return makeGetElementPointer(indexingType, base, offsets, null);
+        Preconditions.checkArgument(base.getType().equals(types.getPointerType()),
+                "Applying offsets to non-pointer expression.");
+        return new GEPExpr(indexingType, base, offsets,null);
     }
 
     public Expression makeGetElementPointer(Type indexingType, Expression base, List<Expression> offsets, Integer stride) {
         // TODO: Stride should be a property of the pointer, not of a GEPExpr.
         //  Refactor GEPExpr to only accept a (new) PointerType and a list of offsets.
         //  A PointerType should have the referred type and the stride in its attributes.
-        Preconditions.checkArgument(base.getType().equals(types.getArchType()),
+        Preconditions.checkArgument(base.getType().equals(types.getPointerType()),
                 "Applying offsets to non-pointer expression.");
         Preconditions.checkArgument(stride == null || stride >= types.getMemorySizeInBytes(indexingType),
         "Stride cannot be smaller than indexing type");
         return new GEPExpr(indexingType, base, offsets, stride);
     }
 
+
     public ScopedPointer makeScopedPointer(String id, ScopedPointerType type, Expression value) {
         return new ScopedPointer(id, type, value);
     }
@@ -337,6 +347,36 @@ public ScopedPointerVariable makeScopedPointerVariable(String id, ScopedPointerT
         return new ScopedPointerVariable(id, type, memObj);
     }
 
+    public Expression makePtrAdd(Expression base, Expression offset) {
+        return new PointerAddExpr(base, offset);
+    }
+
+
+    public Expression makePtrToIntCast(Expression pointer) {
+        return new PtrToIntCast(types.getArchType(), pointer);
+    }
+
+    public Expression makeIntToPtrCast(Expression operand, PointerType pointerType) {
+        return new IntToPtrCast(pointerType, operand);
+    }
+
+    public Expression makeIntToPtrCast(Expression operand) {
+        return new IntToPtrCast(types.getPointerType(), operand);
+    }
+
+
+    public Expression makeNullLiteral(PointerType pointerType) {
+        return new NullLiteral(pointerType);
+    }
+
+    public Expression makeNullLiteral() {
+        return makeNullLiteral(types.getPointerType());
+    }
+
+    public Expression makePtrCmp(Expression left, PointerCmpOp op, Expression right) {
+        return new PtrCmpExpr(types.getBooleanType(), left, op, right);
+    }
+
     // -----------------------------------------------------------------------------------------------------------------
     // Misc
 
@@ -360,7 +400,9 @@ public Expression makeGeneralZero(Type type) {
             return makeFalse();
         } else if (type instanceof FloatType floatType) {
             return makeZero(floatType);
-        } else {
+        } else if (type instanceof PointerType pointerType) {
+            return makeNullLiteral(pointerType);
+        }else{
             throw new UnsupportedOperationException("Cannot create zero of type " + type);
         }
     }
@@ -376,6 +418,8 @@ public Expression makeCast(Expression expression, Type type, boolean signed) {
             return makeIntegerCast(expression, integerType, signed);
         } else if (type instanceof FloatType floatType) {
             return makeFloatCast(expression, floatType, signed);
+        }else if (type instanceof PointerType) {
+            return makeIntToPtrCast(makeCast(expression, types.getArchType()));
         }
         throw new UnsupportedOperationException(String.format("Cast %s into %s unsupported.", expression, type));
     }
@@ -394,7 +438,9 @@ public Expression makeEQ(Expression leftOperand, Expression rightOperand) {
             return makeBoolBinary(leftOperand, BoolBinaryOp.IFF, rightOperand);
         } else if (type instanceof IntegerType) {
             return makeIntCmp(leftOperand, IntCmpOp.EQ, rightOperand);
-        } else if (type instanceof FloatType) {
+        } if (type instanceof PointerType) {
+            return makePtrCmp(leftOperand, PointerCmpOp.EQ, rightOperand);
+        }else if (type instanceof FloatType) {
             // TODO: Decide on a default semantics for float equality?
             return makeFloatCmp(leftOperand, FloatCmpOp.OEQ, rightOperand);
         } else if (ExpressionHelper.isAggregateLike(type)) {
@@ -409,7 +455,9 @@ public Expression makeNEQ(Expression leftOperand, Expression rightOperand) {
             return makeNot(makeBoolBinary(leftOperand, BoolBinaryOp.IFF, rightOperand));
         } else if (type instanceof IntegerType) {
             return makeIntCmp(leftOperand, IntCmpOp.NEQ, rightOperand);
-        } else if (type instanceof FloatType) {
+        } if (type instanceof PointerType) {
+            return makePtrCmp(leftOperand, PointerCmpOp.NEQ, rightOperand);
+        }else if (type instanceof FloatType) {
             // TODO: Decide on a default semantics for float equality?
             return makeFloatCmp(leftOperand, FloatCmpOp.ONEQ, rightOperand);
         } else if (type instanceof AggregateType) {
@@ -438,6 +486,8 @@ public Expression makeBinary(Expression x, ExpressionKind op, Expression y) {
             return makeFloatBinary(x, floatOp, y);
         } else if (op instanceof IntCmpOp cmpOp) {
             return makeCompare(x, cmpOp, y);
+        }else if (op instanceof PointerCmpOp cmpOp) {
+            return makeCompare(x, cmpOp, y);
         }
         throw new UnsupportedOperationException(String.format("Expression kind %s is no binary operator.", op));
     }
@@ -449,7 +499,9 @@ public Expression makeCompare(Expression x, ExpressionKind cmpOp, Expression y)
             return makeFloatCmp(x, floatOp, y);
         } else if (cmpOp instanceof AggregateCmpOp aggrCmpOp) {
             return makeAggregateCmp(x, aggrCmpOp, y);
+        }else if (cmpOp instanceof PointerCmpOp ptrCmpOp) {
+            return makePtrCmp(x, ptrCmpOp, y);
         }
         throw new UnsupportedOperationException(String.format("Expression kind %s is no comparison operator.", cmpOp));
     }
-}
+}

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

@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.expression.booleans.BoolUnaryOp;
 import com.dat3m.dartagnan.expression.floats.FloatSizeCast;
 import com.dat3m.dartagnan.expression.floats.IntToFloatCast;
+import com.dat3m.dartagnan.expression.pointer.*;
 import com.dat3m.dartagnan.expression.integers.*;
 import com.dat3m.dartagnan.expression.misc.GEPExpr;
 import com.dat3m.dartagnan.expression.misc.ITEExpr;
@@ -124,6 +125,22 @@ public String visitGEPExpression(GEPExpr expr) {
         return expr.getOperands().stream().map(this::visit).collect(Collectors.joining(", ", "GEP(", ")"));
     }
 
+    @Override
+    public String visitIntToPtrCastExpression(IntToPtrCast expr) {
+        return String.format("%s to %s", visit(expr.getOperand()), expr.getTargetType());
+    }
+
+    @Override
+    public String visitPtrToIntCastExpression(PtrToIntCast expr) {
+        return String.format("%s to %s", visit(expr.getOperand()), expr.getTargetType());
+    }
+
+    @Override
+    public String visitPointerAddExpression(PointerAddExpr expr) {
+        return String.format("%s + %s", visit(expr.getBase()), visit(expr.getOffset()));
+    }
+
+
     @Override
     public String visitITEExpression(ITEExpr expr) {
         return visit(expr.getCondition()) + " ? " + visit(expr.getTrueCase()) + " : " + visit(expr.getFalseCase());