Memory Datatype and Pointer type

benchmarks/c/miscellaneous/mixedtype.c

@@ -0,0 +1,35 @@
+#include <assert.h>
+#include <stdlib.h>
+int __VERIFIER_nondet_int(void);
+typedef unsigned short u16;
+typedef unsigned int u32;
+
+u16 get_mistyped(u16* array)
+{
+    return array[0];
+}
+
+u16 get_offset(u16* array)
+{
+    return array[1];
+}
+
+u32 get_misaligned(u16* array)
+{
+    u32* interpreted = (u32*)((void*)(array + 1));
+    return *interpreted;
+}
+
+int main()
+{
+    u32* array = (u32*) malloc(2 * sizeof(u32));
+    u32 value = __VERIFIER_nondet_int();
+    array[1] = array[0] = value;
+    u16 easy = get_mistyped((u16*)((void*)array));
+    assert(easy == (value & 0xffff));
+    u16 medium = get_offset((u16*)((void*)array));
+    assert(medium == (value >> 16));
+    u32 hard = get_misaligned((u16*)((void*)array));
+    assert(hard == ((value << 16) | (value >> 16)));
+    return 0;
+}

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

@@ -4,6 +4,7 @@
 import com.dat3m.dartagnan.expression.op.COpBin;
 import com.dat3m.dartagnan.expression.type.BooleanType;
 import com.dat3m.dartagnan.expression.type.IntegerType;
+import com.dat3m.dartagnan.expression.type.PointerType;
 import com.dat3m.dartagnan.expression.type.Type;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.analysis.BranchEquivalence;
@@ -204,7 +205,7 @@ public BooleanFormula dependency(Event first, Event second) {
     }
 
     public Formula lastValue(MemoryObject base, int offset) {
-        checkArgument(0 <= offset && offset < base.size(), "array index out of bounds");
+        checkArgument(0 <= offset && offset < base.getSizeInBytes(), "array index out of bounds");
         final String name = String.format("last_val_at_%s_%d", base, offset);
         if (useIntegers) {
             return formulaManager.getIntegerFormulaManager().makeVariable(name);
@@ -360,6 +361,13 @@ public Formula makeLiteral(Type type, BigInteger value) {
             int bitWidth = integerType.getBitWidth();
             return formulaManager.getBitvectorFormulaManager().makeBitvector(bitWidth, value);
         }
+        if (type instanceof PointerType pointerType) {
+            if (useIntegers) {
+                return formulaManager.getIntegerFormulaManager().makeNumber(value);
+            }
+            int bitWidth = pointerType.getBitWidth();
+            return formulaManager.getBitvectorFormulaManager().makeBitvector(bitWidth, value);
+        }
         throw new UnsupportedOperationException(String.format("Encoding variable of type %s.", type));
     }
 
@@ -414,6 +422,13 @@ Formula makeVariable(String name, Type type) {
             int bitWidth = integerType.getBitWidth();
             return formulaManager.getBitvectorFormulaManager().makeVariable(bitWidth, name);
         }
+        if (type instanceof PointerType pointerType) {
+            if (useIntegers) {
+                return formulaManager.getIntegerFormulaManager().makeVariable(name);
+            }
+            int bitWidth = pointerType.getBitWidth();
+            return formulaManager.getBitvectorFormulaManager().makeVariable(bitWidth, name);
+        }
         throw new UnsupportedOperationException(String.format("Encoding variable of type %s.", type));
     }
 }

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

@@ -3,7 +3,10 @@
 import com.dat3m.dartagnan.expression.*;
 import com.dat3m.dartagnan.expression.op.IOpUn;
 import com.dat3m.dartagnan.expression.processing.ExpressionVisitor;
+import com.dat3m.dartagnan.expression.type.IntegerType;
+import com.dat3m.dartagnan.expression.type.PointerType;
 import com.dat3m.dartagnan.expression.type.Type;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.core.Event;
 import com.dat3m.dartagnan.program.memory.Location;
@@ -12,6 +15,9 @@
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 
 import java.math.BigInteger;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.IntStream;
 
 import static com.google.common.base.Preconditions.checkState;
 import static com.google.common.base.Verify.verify;
@@ -124,6 +130,10 @@ public Formula visit(IExprBin iBin) {
                 case MOD:
                     return integerFormulaManager.modulo(i1, i2);
                 case AND:
+                    // optimized encoding for (x bitand 1), (x bitand 3), etc.
+                    if (iBin.getRHS() instanceof IValue rightValue && isAllOnes(rightValue.getValue())) {
+                        return integerFormulaManager.modulo(i1, integerFormulaManager.makeNumber(rightValue.getValue().add(BigInteger.ONE)));
+                    }
                     bitvectorFormulaManager = bitvectorFormulaManager();
                     return bitvectorFormulaManager.toIntegerFormula(
                             bitvectorFormulaManager.and(
@@ -225,6 +235,11 @@ public Formula visit(IExprBin iBin) {
         }
     }
 
+    private static boolean isAllOnes(BigInteger value) {
+        int length = value.bitLength();
+        return value.signum() != -1 && IntStream.range(0, length).allMatch(value::testBit);
+    }
+
     @Override
     public Formula visit(IExprUn iUn) {
         Formula inner = encode(iUn.getInner());
@@ -249,19 +264,8 @@ public Formula visit(IExprUn iUn) {
                     }
                     //TODO If narrowing, constrain the value.
                     return inner;
-                } else {
-                    final int bitWidth = iUn.getType().getBitWidth();
-                    if (inner instanceof IntegerFormula number) {
-                        return bitvectorFormulaManager().makeBitvector(bitWidth, number);
-                    }
-                    if (inner instanceof BitvectorFormula number) {
-                        int innerBitWidth = bitvectorFormulaManager().getLength(number);
-                        if (innerBitWidth < bitWidth) {
-                            return bitvectorFormulaManager().extend(number, bitWidth - innerBitWidth, signed);
-                        }
-                        return bitvectorFormulaManager().extract(number, bitWidth - 1, 0);
-                    }
                 }
+                return applyBitWidth(inner, iUn.getType().getBitWidth(), signed);
             }
             case CTLZ -> {
                 if (inner instanceof BitvectorFormula bv) {
@@ -319,4 +323,80 @@ public Formula visit(Location location) {
         checkState(event == null, "Cannot evaluate %s at event %s.", location, event);
         return context.lastValue(location.getMemoryObject(), location.getOffset());
     }
+
+    @Override
+    public Formula visit(NullPointer constant) {
+        return context.useIntegers ? integerFormulaManager().makeNumber(0) :
+                bitvectorFormulaManager().makeBitvector(64, 0);
+    }
+
+    @Override
+    public Formula visit(GEPExpression gep) {
+        final TypeFactory types = TypeFactory.getInstance();
+        final List<Expression> expressions = gep.getOffsetExpressions();
+        final Formula base = gep.getBaseExpression().accept(this);
+        final boolean integer = base instanceof IntegerFormula;
+        verify(integer || base instanceof BitvectorFormula, "%s cannot represent pointers", base);
+        final IntegerFormulaManager integerFormulaManager = integer ? integerFormulaManager() : null;
+        final BitvectorFormulaManager bitvectorFormulaManager = integer ? null : bitvectorFormulaManager();
+        final List<IntegerFormula> integers = integer ? new ArrayList<>(List.of((IntegerFormula) base)) : null;
+        final List<BitvectorFormula> bitvectors = new ArrayList<>();
+        final int length = integer ? 0 : bitvectorFormulaManager.getLength((BitvectorFormula) base);
+        final List<Integer> constants = expressions.stream()
+                .map(x -> x instanceof IValue v ? v.getValueAsInt() : 1)
+                .toList();
+        final List<Integer> byteCounts = types.getByteCounts(gep.getIndexingType(), constants);
+        for (int i = 0; i < expressions.size(); i++) {
+            final Expression offset = expressions.get(i);
+            final IValue constant = offset instanceof IValue v ? v : null;
+            if (constant != null && constant.isZero()) {
+                continue;
+            }
+            // only encode offset expressions if not constant.
+            // byteCounts already contains constant offset values.
+            final Formula count = constant != null ? null : offset.accept(this);
+            final int byteCount = byteCounts.get(i);
+            if (integer) {
+                final IntegerFormula coefficient = integerFormulaManager.makeNumber(byteCount);
+                integers.add(count == null ? coefficient : integerFormulaManager.multiply(coefficient,
+                        count instanceof IntegerFormula f ? f :
+                                bitvectorFormulaManager().toIntegerFormula((BitvectorFormula) count, false)));
+            } else {
+                final BitvectorFormula coefficient = bitvectorFormulaManager.makeBitvector(byteCount, length);
+                bitvectors.add(count == null ? coefficient : bitvectorFormulaManager.multiply(coefficient,
+                        count instanceof BitvectorFormula f ? f :
+                                bitvectorFormulaManager.makeBitvector(length, (IntegerFormula) count)));
+            }
+        }
+        return integer ? integerFormulaManager.sum(integers) :
+                bitvectors.stream().reduce((BitvectorFormula) base, bitvectorFormulaManager::add);
+    }
+
+    @Override
+    public Formula visit(PointerCast cast) {
+        final Type targetType = cast.getType();
+        final Formula inner = cast.getInnerExpression().accept(this);
+        verify(targetType instanceof IntegerType || targetType instanceof PointerType, "Invalid type for %s", cast);
+        if (context.useIntegers || targetType instanceof IntegerType t && t.isMathematical()) {
+            return inner;
+        }
+        final int bitWith = targetType instanceof IntegerType t ? t.getBitWidth() : ((PointerType) targetType).getBitWidth();
+        return applyBitWidth(inner, bitWith, cast.isSigned());
+    }
+
+    private Formula applyBitWidth(Formula inner, int bitWidth, boolean signed) {
+        if (inner instanceof BooleanFormula) {
+            return inner;
+        }
+        if (inner instanceof IntegerFormula number) {
+            return bitvectorFormulaManager().makeBitvector(bitWidth, number);
+        }
+        verify(inner instanceof BitvectorFormula);
+        final var number = (BitvectorFormula) inner;
+        final int innerBitWidth = bitvectorFormulaManager().getLength(number);
+        if (innerBitWidth < bitWidth) {
+            return bitvectorFormulaManager().extend(number, bitWidth - innerBitWidth, signed);
+        }
+        return bitvectorFormulaManager().extract(number, bitWidth - 1, 0);
+    }
 }

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

@@ -15,7 +15,7 @@ default ImmutableSet<Register> getRegs() {
 
     <T> T accept(ExpressionVisitor<T> visitor);
 
-    default IConst reduce() {
+    default IValue reduce() {
         throw new UnsupportedOperationException("Reduce not supported for " + this);
     }
 }

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

@@ -16,6 +16,7 @@ public final class ExpressionFactory {
     private final BooleanType booleanType = types.getBooleanType();
     private final BConst falseConstant = new BConst(booleanType, false);
     private final BConst trueConstant = new BConst(booleanType, true);
+    private final NullPointer nullPointer = new NullPointer(types.getPointerType());
 
     private ExpressionFactory() {}
 
@@ -72,6 +73,8 @@ public Expression makeGeneralZero(Type type) {
                 zeroes.add(makeGeneralZero(fieldType));
             }
             return makeConstruct(zeroes);
+        } else if (type instanceof PointerType) {
+            return makeNullPointer();
         } else if (type instanceof IntegerType intType) {
             return makeZero(intType);
         } else if (type == booleanType) {
@@ -98,11 +101,18 @@ 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 PointerType pointerType) {
+            return makeToPointerCast(expression, pointerType, signed);
+        }
         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));
     }
@@ -161,6 +171,9 @@ public Expression makeIntegerCast(Expression operand, IntegerType targetType, bo
         if (operand.getType() instanceof BooleanType) {
             return makeConditional(operand, makeOne(targetType), makeZero(targetType));
         }
+        if (operand.getType() instanceof PointerType) {
+            return new PointerCast(operand, targetType, signed);
+        }
         return makeUnary(signed ? IOpUn.CAST_SIGNED : IOpUn.CAST_UNSIGNED, operand, targetType);
     }
 
@@ -241,10 +254,20 @@ public Expression makeExtract(int fieldIndex, Expression object) {
     // -----------------------------------------------------------------------------------------------------------------
     // Pointers
 
+    public NullPointer makeNullPointer() {
+        return nullPointer;
+    }
+
     public Expression makeGetElementPointer(Type indexingType, Expression base, List<Expression> offsets) {
-        //TODO getPointerType()
-        Preconditions.checkArgument(base.getType().equals(types.getArchType()),
+        Preconditions.checkArgument(base.getType() instanceof PointerType,
                 "Applying offsets to non-pointer expression.");
-        return new GEPExpression(types.getArchType(), indexingType, base, offsets);
+        return new GEPExpression((PointerType) base.getType(), indexingType, base, offsets);
+    }
+
+    public Expression makeToPointerCast(Expression expression, PointerType targetType, boolean signed) {
+        if (expression.getType() instanceof PointerType) {
+            return expression;
+        }
+        return new PointerCast(expression, targetType, signed);
     }
 }

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

@@ -1,18 +1,26 @@
 package com.dat3m.dartagnan.expression;
 
 import com.dat3m.dartagnan.expression.processing.ExpressionVisitor;
+import com.dat3m.dartagnan.expression.type.AggregateType;
+import com.dat3m.dartagnan.expression.type.ArrayType;
+import com.dat3m.dartagnan.expression.type.PointerType;
 import com.dat3m.dartagnan.expression.type.Type;
+import com.dat3m.dartagnan.program.Register;
+import com.google.common.collect.ImmutableSet;
 
+import java.util.ArrayList;
 import java.util.List;
 
+import static com.google.common.base.Preconditions.checkState;
+
 public final class GEPExpression implements Expression {
 
-    private final Type type;
+    private final PointerType type;
     private final Type indexingType;
     private final Expression base;
     private final List<Expression> offsets;
 
-    public GEPExpression(Type t, Type e, Expression b, List<Expression> o) {
+    GEPExpression(PointerType t, Type e, Expression b, List<Expression> o) {
         type = t;
         indexingType = e;
         base = b;
@@ -23,6 +31,25 @@ public Type getIndexingType() {
         return indexingType;
     }
 
+    public List<Type> getIndexingTypes() {
+        List<Type> result = new ArrayList<>();
+        result.add(indexingType);
+        Type t = indexingType;
+        for (Expression offset : offsets.subList(1, offsets.size())) {
+            if (t instanceof ArrayType array) {
+                t = array.getElementType();
+            } else {
+                checkState(t instanceof AggregateType struct &&
+                        offset instanceof IValue literal &&
+                        literal.getValueAsInt() >= 0 &&
+                        literal.getValueAsInt() < struct.getDirectFields().size());
+                t = ((AggregateType) t).getDirectFields().get(((IValue) offset).getValueAsInt());
+            }
+            result.add(t);
+        }
+        return result;
+    }
+
     public Expression getBaseExpression() {
         return base;
     }
@@ -32,7 +59,7 @@ public List<Expression> getOffsetExpressions() {
     }
 
     @Override
-    public Type getType() {
+    public PointerType getType() {
         return type;
     }
 
@@ -41,6 +68,16 @@ public <T> T accept(ExpressionVisitor<T> visitor) {
         return visitor.visit(this);
     }
 
+    @Override
+    public ImmutableSet<Register> getRegs() {
+        final ImmutableSet.Builder<Register> set = ImmutableSet.builder();
+        set.addAll(base.getRegs());
+        for (final Expression offset : offsets) {
+            set.addAll(offset.getRegs());
+        }
+        return set.build();
+    }
+
     @Override
     public String toString() {
         final StringBuilder string = new StringBuilder();