Skip to content

Commit

Permalink
Add encoding for dynamic memory layouts.
Browse files Browse the repository at this point in the history
  • Loading branch information
ThomasHaas committed Oct 9, 2024
1 parent ba29901 commit 3a60ebf
Show file tree
Hide file tree
Showing 2 changed files with 178 additions and 6 deletions.
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<MemoryObject, Formula> where each formula describes a
// unique, properly aligned, and non-overlapping address of the memory object.
final Map<MemoryObject, BigInteger> memObj2Addr = computeStaticMemoryLayout(memory);

return encodeDynamicMemoryLayout(memory);

/*final Map<MemoryObject, BigInteger> memObj2Addr = computeStaticMemoryLayout(memory);
final var enc = new ArrayList<BooleanFormula>();
for (final MemoryObject memObj : memory.getObjects()) {
Expand Down Expand Up @@ -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);*/
}

/*
Expand All @@ -332,7 +333,7 @@ private Map<MemoryObject, BigInteger> 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:
Expand All @@ -348,6 +349,54 @@ private Map<MemoryObject, BigInteger> computeStaticMemoryLayout(Memory memory) {
return memObj2Addr;
}

private BooleanFormula encodeDynamicMemoryLayout(Memory memory) {
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
final EncodingHelper helper = new EncodingHelper(context.getFormulaManager());
final List<BooleanFormula> 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<MemoryObject> 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,
Expand Down

0 comments on commit 3a60ebf

Please sign in to comment.