diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java new file mode 100644 index 0000000000..a5f78bde04 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java @@ -0,0 +1,123 @@ +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) { + if (left instanceof NumeralFormula.IntegerFormula iLeft && right instanceof NumeralFormula.IntegerFormula iRight) { + // NOTE: This is not the same as the BV version in terms of signedness (here the sign is from the numerator) + 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().remainder(bvLeft, bvRight, true); + } + + 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); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 0c0f8b660b..140cdfb659 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -23,6 +23,7 @@ import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -284,10 +285,10 @@ public BooleanFormula encodeMemory() { logger.info("Encoding memory"); final Memory memory = context.getTask().getProgram().getMemory(); final FormulaManager fmgr = context.getFormulaManager(); - // TODO: Once we want to encode dynamic memory layouts (e.g., due to dynamically-sized mallocs) - // we need to compute a Map where each formula describes a - // unique, properly aligned, and non-overlapping address of the memory object. - final Map memObj2Addr = computeStaticMemoryLayout(memory); + + return encodeDynamicMemoryLayout(memory); + + /*final Map memObj2Addr = computeStaticMemoryLayout(memory); final var enc = new ArrayList(); for (final MemoryObject memObj : memory.getObjects()) { @@ -315,7 +316,7 @@ public BooleanFormula encodeMemory() { enc.add(imgr.equal((IntegerFormula) sizeVariable, imgr.makeNumber(sizeInteger))); } } - return fmgr.getBooleanFormulaManager().and(enc); + return fmgr.getBooleanFormulaManager().and(enc);*/ } /* @@ -332,7 +333,7 @@ private Map computeStaticMemoryLayout(Memory memory) { BigInteger nextAddr = alignment; for(MemoryObject memObj : memory.getObjects()) { Preconditions.checkState(memObj.hasKnownSize(), "Cannot encode static memory layout for" + - "variable-sized memory object: %s", memObj); + " variable-sized memory object: %s", memObj); memObj2Addr.put(memObj, nextAddr); // Compute next aligned address as follows: @@ -348,6 +349,54 @@ private Map computeStaticMemoryLayout(Memory memory) { return memObj2Addr; } + private BooleanFormula encodeDynamicMemoryLayout(Memory memory) { + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final EncodingHelper helper = new EncodingHelper(context.getFormulaManager()); + final List enc = new ArrayList<>(); + + // TODO: We could sort the objects to generate better encoding: + // "static -> dynamic with known size -> dynamic with unknown size" + // For the former two we can then statically assign addresses as we do now and + // only the latter needs dynamic encodings. + final List memoryObjects = ImmutableList.copyOf(memory.getObjects()); + for (int i = 0; i < memoryObjects.size(); i++) { + final MemoryObject cur = memoryObjects.get(i); + final Formula addr = context.address(cur); + final Formula size = context.size(cur); + + // Encode size (non-allocated objects are 0-sized) + if (cur.isStaticallyAllocated()) { + enc.add(helper.equals(size, context.encodeFinalExpression(cur.size()))); + } else { + enc.add(helper.equals(size, + bmgr.ifThenElse(context.execution(cur.getAllocationSite()), + context.encodeExpressionAt(cur.size(), cur.getAllocationSite()), + helper.value(BigInteger.ZERO, helper.typeOf(size))) + ) + ); + } + + // Encode address (we even give non-allocated objects a proper address) + // We 8-align by default because it works for most real code. + final Formula alignment = helper.value(BigInteger.valueOf(8), helper.typeOf(addr)); + final MemoryObject prev = i > 0 ? memoryObjects.get(i - 1) : null; + if (prev == null) { + // First object is placed at alignment + enc.add(helper.equals(addr, alignment)); + } else { + final Formula prevAddr = context.address(prev); + final Formula prevSize = context.size(prev); + final Formula nextAvailableAddr = helper.add(prevAddr, prevSize); + final Formula nextAlignedAddr = helper.add(nextAvailableAddr, + helper.subtract(alignment, helper.remainder(nextAvailableAddr, alignment)) + ); + enc.add(helper.equals(addr, nextAlignedAddr)); + } + } + + return bmgr.and(enc); + } + /** * @return * Describes that for each pair of events, if the reader uses the result of the writer,