Add support for variable-sized and variable-aligned allocations (#750)

benchmarks/miscellaneous/nondet_aligned_alloc.c

@@ -0,0 +1,26 @@
+#include <stdint.h>
+#include <assert.h>
+#include <dat3m.h>
+#include <stdlib.h>
+
+#define SIZE_1 42
+
+int main()
+{
+    int size_int = __VERIFIER_nondet_int();
+    int align_int = __VERIFIER_nondet_int();
+    __VERIFIER_assume(size_int > 0);
+    __VERIFIER_assume(align_int > 0);
+    size_t size = (size_t)size_int;
+    size_t align = (size_t)align_int;
+    int *array = malloc(SIZE_1 * sizeof(int));
+    int *array_2 = aligned_alloc(align, size * sizeof(int));
+    // NOTE: making the first allocation non-det-sized makes the solver extremely slow to verify the
+    // custom aligned allocation. Even when fixing the alignment to a constant it gets super slow if that constant
+    // is not a power of two. In other words, aligning variable-sized addresses is very expensive currently, especially
+    // for non-power-of-two alignments (those don't exist in practice though).
+
+    assert ((size_t)array_2 - (size_t)array >= SIZE_1 * sizeof(int));
+    assert (((size_t)array) % 8 == 0); // Default alignment
+    assert (((size_t)array_2) % align == 0); // Custom alignment
+}

benchmarks/miscellaneous/nondet_alloc.c

@@ -0,0 +1,27 @@
+#include <stdint.h>
+#include <assert.h>
+#include <dat3m.h>
+
+
+#define MAX_SIZE 10
+
+int main()
+{
+    int size = __VERIFIER_nondet_int();
+    __VERIFIER_assume(size > 0 && size <= MAX_SIZE);
+    int *array = malloc(size * sizeof(int));
+
+    __VERIFIER_loop_bound(MAX_SIZE + 1);
+    for (int i = 0; i < size; i++) {
+        array[i] = i;
+    }
+
+    int sum = 0;
+    __VERIFIER_loop_bound(MAX_SIZE + 1);
+    for (int i = 0; i < size; i++) {
+        sum += array[i];
+    }
+
+    // Fails if size == MAX_SIZE because then equality holds
+    assert(sum < (MAX_SIZE * (MAX_SIZE - 1)) / 2);
+}

benchmarks/miscellaneous/nondet_alloc_2.c

@@ -0,0 +1,20 @@
+#include <stdint.h>
+#include <assert.h>
+#include <dat3m.h>
+#include <stdlib.h>
+
+int main()
+{
+    int size_int = __VERIFIER_nondet_int();
+    __VERIFIER_assume(size_int > 0);
+    // NOTE: Putting the assumption on the below <size> rather than <size_int> gives FAIL.
+    // This is because the non-det int value is sign-extended to size_t and so negative values are extended
+    // to very large sizes that can overflow, allowing the addresses of different allocations to overlap!
+    size_t size = (size_t)size_int;
+    int *array = malloc(size * sizeof(int));
+    int *array_2 = malloc(size * sizeof(int));
+
+    assert (array != array_2);
+    assert (((size_t)array) % 8 == 0);
+    assert (((size_t)array_2) % 8 == 0);
+}

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

@@ -76,6 +76,8 @@ public final class EncodingContext {
     private final Map<Event, Formula> addresses = new HashMap<>();
     private final Map<Event, Formula> values = new HashMap<>();
     private final Map<Event, Formula> results = new HashMap<>();
+    private final Map<MemoryObject, Formula> objAddress = new HashMap<>();
+    private final Map<MemoryObject, Formula> objSize = new HashMap<>();
 
     private EncodingContext(VerificationTask t, Context a, FormulaManager m) {
         verificationTask = checkNotNull(t);
@@ -215,7 +217,7 @@ public BooleanFormula dependency(Event first, Event second) {
     }
 
     public Formula lastValue(MemoryObject base, int offset, int size) {
-        checkArgument(0 <= offset && offset < base.size(), "array index out of bounds");
+        checkArgument(base.isInRange(offset), "Array index out of bounds");
         final String name = String.format("last_val_at_%s_%d", base, offset);
         if (useIntegers) {
             return formulaManager.getIntegerFormulaManager().makeVariable(name);
@@ -306,6 +308,10 @@ public Formula address(MemoryEvent event) {
         return addresses.get(event);
     }
 
+    public Formula address(MemoryObject memoryObject) { return objAddress.get(memoryObject); }
+
+    public Formula size(MemoryObject memoryObject) { return objSize.get(memoryObject); }
+
     public Formula value(MemoryEvent event) {
         return values.get(event);
     }
@@ -370,6 +376,7 @@ public Formula makeLiteral(Type type, BigInteger value) {
     }
 
     private void initialize() {
+        // ------- Control flow variables -------
         // Only for the standard fair progress model we can merge CF variables.
         // TODO: It would also be possible for OBE/HSA in some cases if we refine the cf-equivalence classes
         //  to classes per thread.
@@ -386,6 +393,14 @@ private void initialize() {
                 controlFlowVariables.put(e, booleanFormulaManager.makeVariable("cf " + e.getGlobalId()));
             }
         }
+
+        // ------- Memory object variables -------
+        for (MemoryObject memoryObject : verificationTask.getProgram().getMemory().getObjects()) {
+            objAddress.put(memoryObject, makeVariable(String.format("addrof(%s)", memoryObject), memoryObject.getType()));
+            objSize.put(memoryObject, makeVariable(String.format("sizeof(%s)", memoryObject), memoryObject.getType()));
+        }
+
+        // ------- Event variables  -------
         for (Event e : verificationTask.getProgram().getThreadEvents()) {
             if (!e.cfImpliesExec()) {
                 executionVariables.put(e, booleanFormulaManager.makeVariable("exec " + e.getGlobalId()));

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

@@ -0,0 +1,125 @@
+package com.dat3m.dartagnan.encoding;
+
+import com.google.common.base.Preconditions;
+import org.sosy_lab.java_smt.api.*;
+
+import java.math.BigInteger;
+
+public class EncodingHelper {
+
+    private final FormulaManager fmgr;
+
+    public EncodingHelper(FormulaManager fmgr) {
+        this.fmgr = fmgr;
+    }
+
+    public BooleanFormula equals(Formula left, Formula right) {
+        if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) {
+            return fmgr.getIntegerFormulaManager().equal(iLeft, iRight);
+        }
+
+        if (left instanceof BitvectorFormula bvLeft && right instanceof BitvectorFormula bvRight) {
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            Preconditions.checkState(bvmgr.getLength(bvLeft) == bvmgr.getLength(bvRight));
+            return fmgr.getBitvectorFormulaManager().equal(bvLeft, bvRight);
+        }
+
+        throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right);
+    }
+
+    public BooleanFormula greaterThan(Formula left, Formula right, boolean signed) {
+        if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) {
+            return fmgr.getIntegerFormulaManager().greaterThan(iLeft, iRight);
+        }
+
+        if (left instanceof BitvectorFormula bvLeft && right instanceof BitvectorFormula bvRight) {
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            Preconditions.checkState(bvmgr.getLength(bvLeft) == bvmgr.getLength(bvRight));
+            return fmgr.getBitvectorFormulaManager().greaterThan(bvLeft, bvRight, signed);
+        }
+
+        throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right);
+    }
+
+    public BooleanFormula greaterOrEquals(Formula left, Formula right, boolean signed) {
+        if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) {
+            return fmgr.getIntegerFormulaManager().greaterOrEquals(iLeft, iRight);
+        }
+
+        if (left instanceof BitvectorFormula bvLeft && right instanceof BitvectorFormula bvRight) {
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            Preconditions.checkState(bvmgr.getLength(bvLeft) == bvmgr.getLength(bvRight));
+            return fmgr.getBitvectorFormulaManager().greaterOrEquals(bvLeft, bvRight, signed);
+        }
+
+        throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right);
+    }
+
+    public Formula add(Formula left, Formula right) {
+        if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) {
+            return fmgr.getIntegerFormulaManager().add(iLeft, iRight);
+        }
+
+        if (left instanceof BitvectorFormula bvLeft && right instanceof BitvectorFormula bvRight) {
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            Preconditions.checkState(bvmgr.getLength(bvLeft) == bvmgr.getLength(bvRight));
+            return fmgr.getBitvectorFormulaManager().add(bvLeft, bvRight);
+        }
+
+        throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right);
+    }
+
+    public Formula subtract(Formula left, Formula right) {
+        if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) {
+            return fmgr.getIntegerFormulaManager().subtract(iLeft, iRight);
+        }
+
+        if (left instanceof BitvectorFormula bvLeft && right instanceof BitvectorFormula bvRight) {
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            Preconditions.checkState(bvmgr.getLength(bvLeft) == bvmgr.getLength(bvRight));
+            return fmgr.getBitvectorFormulaManager().subtract(bvLeft, bvRight);
+        }
+
+        throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right);
+    }
+
+    public Formula remainder(Formula left, Formula right) {
+        //FIXME: integer modulo and BV modulo have different semantics, the former is always positive, the latter
+        // returns a value whose sign depends on one of the two BVs.
+        // The results in this implementation will match if the denominator <right> is positive which is the most usual case.
+        if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) {
+            return fmgr.getIntegerFormulaManager().modulo(iLeft, iRight);
+        }
+
+        if (left instanceof BitvectorFormula bvLeft && right instanceof BitvectorFormula bvRight) {
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            Preconditions.checkState(bvmgr.getLength(bvLeft) == bvmgr.getLength(bvRight));
+            return fmgr.getBitvectorFormulaManager().smodulo(bvLeft, bvRight);
+        }
+
+        throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right);
+    }
+
+    public Formula value(BigInteger value, FormulaType<?> type) {
+        if (type.isIntegerType()) {
+            return fmgr.getIntegerFormulaManager().makeNumber(value);
+        } else if (type.isBitvectorType()) {
+            int size = getBitSize(type);
+            return fmgr.getBitvectorFormulaManager().makeBitvector(size, value);
+        }
+        throw new UnsupportedOperationException("Cannot generate value of type " + type);
+    }
+
+    public int getBitSize(FormulaType<?> type) {
+        if (type.isIntegerType()) {
+            return -1;
+        } else if (type.isBitvectorType()) {
+            return ((FormulaType.BitvectorType)type).getSize();
+        }
+        throw new UnsupportedOperationException("Cannot get bit-size for type " + type);
+    }
+
+    public FormulaType<?> typeOf(Formula formula) {
+        return fmgr.getFormulaType(formula);
+    }
+}

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

@@ -102,7 +102,6 @@ public Formula visitNonDetValue(NonDetValue nonDet) {
 
     @Override
     public Formula visitIntLiteral(IntLiteral intLiteral) {
-
         BigInteger value = intLiteral.getValue();
         Type type = intLiteral.getType();
         return context.makeLiteral(type, value);
@@ -294,7 +293,7 @@ public Formula visitRegister(Register reg) {
 
     @Override
     public Formula visitMemoryObject(MemoryObject memObj) {
-        return context.makeVariable(memObj.toString(), memObj.getType());
+        return context.address(memObj);
     }
 
     @Override