From ce1eb909cbea3aa092d5a66942ee215aee60fcad Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 9 Oct 2024 13:46:20 +0200 Subject: [PATCH 01/14] Added proper size and address variables for MemoryObject encoding Generalized MemoryObject.size to arbitrary expressions. Updated all existing code to use new MemoryObject.has/getKnownSize() to work only over constant size allocations like before (these are first steps to more general support) --- cat/power.cat | 2 + .../dartagnan/encoding/EncodingContext.java | 17 ++++++- .../dartagnan/encoding/ExpressionEncoder.java | 3 +- .../dartagnan/encoding/ProgramEncoder.java | 20 ++++++-- .../spirv/utils/MemoryTransformer.java | 9 ++-- .../analysis/alias/AndersenAliasAnalysis.java | 9 ++-- .../alias/FieldSensitiveAndersen.java | 6 +-- .../alias/InclusionBasedPointerAnalysis.java | 5 +- .../dartagnan/program/memory/Memory.java | 4 +- .../program/memory/MemoryObject.java | 47 +++++++++++++------ .../processing/LogThreadStatistics.java | 9 ++-- .../program/processing/MemoryAllocation.java | 4 +- .../program/processing/ThreadCreation.java | 3 +- .../verification/model/ExecutionModel.java | 11 +++-- .../graphviz/ExecutionGraphVisualizer.java | 23 +++++---- 15 files changed, 115 insertions(+), 57 deletions(-) diff --git a/cat/power.cat b/cat/power.cat index 7711ce90a3..25e781e525 100644 --- a/cat/power.cat +++ b/cat/power.cat @@ -45,5 +45,7 @@ let prop = (W*W & propbase)| (com*;propbase*;sync;hb*) acyclic co | prop irreflexive fre;prop;hb* +acyclic (prop | hb) + (* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *) empty rmw & (fre; coe) as atomic diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java index d4e369c89d..491a864500 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -76,6 +76,8 @@ public final class EncodingContext { private final Map addresses = new HashMap<>(); private final Map values = new HashMap<>(); private final Map results = new HashMap<>(); + private final Map objAddress = new HashMap<>(); + private final Map 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())); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index 914fb9c383..dcf629961a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/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 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 a7fbbad893..0c0f8b660b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -291,10 +291,8 @@ public BooleanFormula encodeMemory() { final var enc = new ArrayList(); for (final MemoryObject memObj : memory.getObjects()) { - // For all objects, their 'final' value fetched here represents their constant value. - final Formula addressVariable = context.encodeFinalExpression(memObj); + final Formula addressVariable = context.address(memObj); final BigInteger addressInteger = memObj2Addr.get(memObj); - if (addressVariable instanceof BitvectorFormula bitvectorVariable) { final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager(); final int length = bvmgr.getLength(bitvectorVariable); @@ -304,6 +302,18 @@ public BooleanFormula encodeMemory() { final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); enc.add(imgr.equal((IntegerFormula) addressVariable, imgr.makeNumber(addressInteger))); } + + final Formula sizeVariable = context.size(memObj); + final BigInteger sizeInteger = BigInteger.valueOf(memObj.getKnownSize()); + if (sizeVariable instanceof BitvectorFormula bitvectorVariable) { + final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager(); + final int length = bvmgr.getLength(bitvectorVariable); + enc.add(bvmgr.equal(bitvectorVariable, bvmgr.makeBitvector(length, sizeInteger))); + } else { + assert addressVariable instanceof IntegerFormula; + final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); + enc.add(imgr.equal((IntegerFormula) sizeVariable, imgr.makeNumber(sizeInteger))); + } } return fmgr.getBooleanFormulaManager().and(enc); } @@ -321,6 +331,8 @@ private Map computeStaticMemoryLayout(Memory memory) { Map memObj2Addr = new HashMap<>(); BigInteger nextAddr = alignment; for(MemoryObject memObj : memory.getObjects()) { + Preconditions.checkState(memObj.hasKnownSize(), "Cannot encode static memory layout for" + + "variable-sized memory object: %s", memObj); memObj2Addr.put(memObj, nextAddr); // Compute next aligned address as follows: @@ -328,7 +340,7 @@ private Map computeStaticMemoryLayout(Memory memory) { // => padding = k*alignment - curAddr - size // => padding mod alignment = (-size) mod alignment // k*alignment and curAddr are 0 mod alignment. // => padding = (-size) mod alignment // Because padding < alignment - final BigInteger memObjSize = BigInteger.valueOf(memObj.size()); + final BigInteger memObjSize = BigInteger.valueOf(memObj.getKnownSize()); final BigInteger padding = memObjSize.negate().mod(alignment); nextAddr = nextAddr.add(memObjSize).add(padding); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/MemoryTransformer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/MemoryTransformer.java index 16b4062580..610ca8c89f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/MemoryTransformer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/utils/MemoryTransformer.java @@ -13,7 +13,10 @@ import com.dat3m.dartagnan.program.memory.VirtualMemoryObject; import com.dat3m.dartagnan.program.misc.NonDetValue; -import java.util.*; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; import java.util.function.IntUnaryOperator; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -96,8 +99,8 @@ private Expression applyMapping(MemoryObject memObj, int scopeDepth) { Map mapping = scopeMapping.get(scopeDepth); if (!mapping.containsKey(memObj)) { MemoryObject copy = memObj instanceof VirtualMemoryObject - ? program.getMemory().allocateVirtual(memObj.size(), true, null) - : program.getMemory().allocate(memObj.size()); + ? program.getMemory().allocateVirtual(memObj.getKnownSize(), true, null) + : program.getMemory().allocate(memObj.getKnownSize()); copy.setName(makeVariableName(scopeDepth, memObj.getName())); for (int offset : memObj.getInitializedFields()) { Expression value = memObj.getInitialValue(offset); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java index 7b5b4dec29..545dc9db88 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java @@ -53,7 +53,7 @@ private AndersenAliasAnalysis(Program program) { Preconditions.checkArgument(program.isCompiled(), "The program must be compiled first."); ImmutableSet.Builder builder = new ImmutableSet.Builder<>(); for (MemoryObject a : program.getMemory().getObjects()) { - for (int i = 0; i < a.size(); i++) { + for (int i = 0; i < a.getKnownSize(); i++) { builder.add(new Location(a, i)); } } @@ -227,7 +227,7 @@ private void processResults(Local e) { Expression rhs = ((IntBinaryExpr) exp).getRight(); if (rhs instanceof IntLiteral ic) { int o = target.offset + ic.getValueAsInt(); - if (o < target.base.size()) { + if (o < target.base.getKnownSize()) { addTarget(reg, new Location(target.base, o)); } } else { @@ -302,7 +302,8 @@ private static final class Location { final int offset; Location(MemoryObject b, int o) { - Preconditions.checkArgument(0 <= o && o < b.size(), "Array out of bounds"); + b.isInRange(o); + Preconditions.checkArgument(b.isInRange(o), "Array out of bounds"); base = b; offset = o; } @@ -356,7 +357,7 @@ private void addTarget(Register r, Location l) { } private void addTargetArray(Register r, MemoryObject b) { - targets.put(r, IntStream.range(0, b.size()) + targets.put(r, IntStream.range(0, b.getKnownSize()) .mapToObj(i -> new Location(b, i)) .collect(Collectors.toSet())); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java index 3cb317c7bc..3127715cf8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java @@ -256,9 +256,9 @@ public String toString() { private static List fields(Collection v, int offset, int alignment) { final List result = new ArrayList<>(); for (Location l : v) { - for (int i = 0; i < div(l.base.size(), alignment); i++) { + for (int i = 0; i < div(l.base.getKnownSize(), alignment); i++) { int mapped = l.offset + offset + i * alignment; - if (0 <= mapped && mapped < l.base.size()) { + if (0 <= mapped && mapped < l.base.getKnownSize()) { Location loc = new Location(l.base, mapped); result.add(loc); } @@ -300,7 +300,7 @@ List address() { verify(address.size() == 1); return fields(List.of(new Location(result.address, 0)), result.offset.intValue(), result.alignment); } - return address.stream().flatMap(a -> range(0, a.size()).mapToObj(i -> new Location(a, i))) + return address.stream().flatMap(a -> range(0, a.getKnownSize()).mapToObj(i -> new Location(a, i))) .collect(toList()); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java index 4321914963..73c626da7d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/InclusionBasedPointerAnalysis.java @@ -397,7 +397,10 @@ private void postProcess(Map.Entry entry) { final Modifier modifier = compose(includeEdge.modifier, address.modifier); assert includeEdge.source.object != null; // If the only included address refers to the last element, treat it as a direct static offset instead. - final int remainingSize = includeEdge.source.object.size() - modifier.offset; + if (!includeEdge.source.object.hasKnownSize()) { + return; + } + final int remainingSize = includeEdge.source.object.getKnownSize() - modifier.offset; for (final Integer a : modifier.alignment) { if (a < remainingSize) { return; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java index 7b02309d37..9df50dff65 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java @@ -28,9 +28,7 @@ public MemoryObject allocate(int size) { // Generates a new, dynamically allocated memory object. public MemoryObject allocate(Alloc allocationSite) { Preconditions.checkNotNull(allocationSite); - // TODO: Add support for dynamically-sized allocations. - final int size = getStaticAllocSize(allocationSite); - final MemoryObject memoryObject = new MemoryObject(nextIndex++, size, allocationSite, ptrType); + final MemoryObject memoryObject = new MemoryObject(nextIndex++, allocationSite.getAllocationSize(), allocationSite, ptrType); objects.add(memoryObject); return memoryObject; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java index cc0de95fbe..c2f9a320c1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java @@ -1,13 +1,12 @@ package com.dat3m.dartagnan.program.memory; -import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.ExpressionKind; -import com.dat3m.dartagnan.expression.ExpressionVisitor; -import com.dat3m.dartagnan.expression.Type; +import com.dat3m.dartagnan.expression.*; import com.dat3m.dartagnan.expression.base.LeafExpressionBase; +import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.misc.ConstructExpr; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.program.event.core.Alloc; +import com.google.common.base.Preconditions; import java.util.List; import java.util.Map; @@ -22,13 +21,11 @@ */ public class MemoryObject extends LeafExpressionBase { - private static final TypeFactory types = TypeFactory.getInstance(); - // TODO: (TH) I think is mostly useless. // Its only benefit is that we can have different memory objects with the same name (but why would we?) private final int id; // TODO: Generalize to Expression - private final int size; + private final Expression size; private final Alloc allocationSite; private String name = null; @@ -36,13 +33,20 @@ public class MemoryObject extends LeafExpressionBase { private final Map initialValues = new TreeMap<>(); - MemoryObject(int id, int size, Alloc allocationSite, Type ptrType) { + MemoryObject(int id, Expression size, Alloc allocationSite, Type ptrType) { super(ptrType); this.id = id; this.size = size; this.allocationSite = allocationSite; } + MemoryObject(int id, int size, Alloc allocationSite, Type ptrType) { + super(ptrType); + this.id = id; + this.size = ExpressionFactory.getInstance().makeValue(size, TypeFactory.getInstance().getArchType()); + this.allocationSite = allocationSite; + } + public boolean hasName() { return name != null; } public String getName() { return name; } public void setName(String name) { this.name = name; } @@ -54,10 +58,20 @@ public class MemoryObject extends LeafExpressionBase { public boolean isThreadLocal() { return this.isThreadLocal; } public void setIsThreadLocal(boolean value) { this.isThreadLocal = value;} - /** - * @return Number of fields in this array. - */ - public int size() { return size; } + public Expression size() { return size; } + + public boolean hasKnownSize() { + return size instanceof IntLiteral; + } + + public int getKnownSize() { + Preconditions.checkState(hasKnownSize()); + return ((IntLiteral)size).getValueAsInt(); + } + + public boolean isInRange(int offset) { + return hasKnownSize() && offset >= 0 && offset < getKnownSize(); + } public Set getInitializedFields() { return initialValues.keySet(); @@ -70,7 +84,8 @@ public Set getInitializedFields() { * @return Readable value at the start of each execution. */ public Expression getInitialValue(int offset) { - checkArgument(offset >= 0 && offset < size, "array index out of bounds"); + checkState(hasKnownSize()); + checkArgument(isInRange(offset), "array index out of bounds"); checkState(initialValues.containsKey(offset), "%s[%s] has no init value", this, offset); return initialValues.get(offset); } @@ -82,6 +97,8 @@ public Expression getInitialValue(int offset) { * @param value New value to be read at the start of each execution. */ public void setInitialValue(int offset, Expression value) { + checkState(hasKnownSize()); + final TypeFactory types = TypeFactory.getInstance(); if (value.getType() instanceof ArrayType arrayType) { checkArgument(value instanceof ConstructExpr); final ConstructExpr constArray = (ConstructExpr) value; @@ -100,7 +117,7 @@ public void setInitialValue(int offset, Expression value) { } } else if (value.getType() instanceof IntegerType || value.getType() instanceof BooleanType) { - checkArgument(offset >= 0 && offset < size, "array index out of bounds"); + checkArgument(isInRange(offset), "array index out of bounds"); initialValues.put(offset, value); } else { throw new UnsupportedOperationException("Unrecognized constant value: " + value); @@ -136,4 +153,6 @@ public ExpressionKind getKind() { public T accept(ExpressionVisitor visitor) { return visitor.visitMemoryObject(this); } + + } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java index 90d7fb1b95..675b6ef305 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java @@ -54,10 +54,12 @@ public void run(Program program) { int numNonInitThreads = (int)threads.stream().filter(t -> !(t.getEntry().getSuccessor() instanceof Init)).count(); int staticAddressSpaceSize = program.getMemory().getObjects().stream() - .filter(MemoryObject::isStaticallyAllocated).mapToInt(MemoryObject::size).sum(); + .filter(m -> m.isStaticallyAllocated() && m.hasKnownSize()).mapToInt(MemoryObject::getKnownSize).sum(); int dynamicAddressSpaceSize = program.getMemory().getObjects().stream() - .filter(MemoryObject::isDynamicallyAllocated).mapToInt(MemoryObject::size).sum(); + .filter(m -> m.isDynamicallyAllocated() && m.hasKnownSize()).mapToInt(MemoryObject::getKnownSize).sum(); int totalAddressSpaceSize = dynamicAddressSpaceSize + staticAddressSpaceSize; + int numUnknownSizedAllocations = Math.toIntExact(program.getMemory().getObjects().stream() + .filter(m -> !m.hasKnownSize()).count()); StringBuilder output = new StringBuilder(); output.append("\n======== Program statistics ========").append("\n"); @@ -70,7 +72,8 @@ public void run(Program program) { .append("\t#Others: ").append(otherVisibleCount).append("\n") .append("#Allocated bytes: ").append(totalAddressSpaceSize).append("\n") .append("\tStatically allocated: ").append(staticAddressSpaceSize).append("\n") - .append("\tDynamically allocated: ").append(dynamicAddressSpaceSize).append("\n"); + .append("\tDynamically allocated: ").append(dynamicAddressSpaceSize).append("\n") + .append("\t#Unknown allocations: ").append(numUnknownSizedAllocations).append("\n"); output.append("========================================"); logger.info(output); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java index 141e35a7d8..24e86b05bc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java @@ -11,6 +11,7 @@ import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.core.Alloc; import com.dat3m.dartagnan.program.memory.MemoryObject; +import com.google.common.base.Preconditions; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.configuration.Option; @@ -65,7 +66,8 @@ private void processAllocations(Program program) { alloc.setAllocatedObject(allocatedObject); if (alloc.doesZeroOutMemory() || createInitsForDynamicAllocations) { - for (int i = 0; i < allocatedObject.size(); i++) { + Preconditions.checkState(allocatedObject.hasKnownSize(), "Cannot initialize dynamic allocation of unknown size."); + for (int i = 0; i < allocatedObject.getKnownSize(); i++) { allocatedObject.setInitialValue(i, zero); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java index c1567f2e42..56b78042c7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java @@ -345,7 +345,8 @@ public Expression visitRegister(Register reg) { @Override public Expression visitMemoryObject(MemoryObject memObj) { if (memObj.isThreadLocal() && !global2ThreadLocal.containsKey(memObj)) { - final MemoryObject threadLocalCopy = memory.allocate(memObj.size()); + Preconditions.checkState(memObj.hasKnownSize()); + final MemoryObject threadLocalCopy = memory.allocate(memObj.getKnownSize()); assert memObj.hasName(); final String varName = String.format("%s@T%s", memObj.getName(), thread.getId()); threadLocalCopy.setName(varName); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java index c22bb47dbf..614aaf999f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java @@ -54,7 +54,7 @@ public class ExecutionModel { // The event list is sorted lexicographically by (threadID, cID) private final ArrayList eventList; private final ArrayList threadList; - private final Map memoryLayoutMap; + private final Map memoryLayoutMap; private final Map> threadEventsMap; private final Map>> atomicBlocksMap; private final Map readWriteMap; @@ -74,7 +74,7 @@ public class ExecutionModel { // The following are a read-only views which get passed to the outside private List eventListView; private List threadListView; - private Map memoryLayoutMapView; + private Map memoryLayoutMapView; private Map> threadEventsMapView; private Map>> atomicBlocksMapView; private Map readWriteMapView; @@ -172,7 +172,7 @@ public List getThreads() { return threadListView; } - public Map getMemoryLayoutMap() { return memoryLayoutMapView; } + public Map getMemoryLayoutMap() { return memoryLayoutMapView; } public Map> getThreadEventsMap() { return threadEventsMapView; } @@ -496,8 +496,9 @@ private void extractMemoryLayout() { for (MemoryObject obj : getProgram().getMemory().getObjects()) { final boolean isAllocated = obj.isStaticallyAllocated() || isTrue(encodingContext.execution(obj.getAllocationSite())); if (isAllocated) { - final BigInteger address = (BigInteger) model.evaluate(encodingContext.encodeFinalExpression(obj)); - memoryLayoutMap.put(obj, address); + final BigInteger address = (BigInteger) model.evaluate(encodingContext.address(obj)); + final BigInteger size = (BigInteger) model.evaluate(encodingContext.size(obj)); + memoryLayoutMap.put(obj, new MemoryObjectModel(obj, address, size)); } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java index a41e035499..2b4f452cb0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java @@ -7,6 +7,7 @@ import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.verification.model.EventData; import com.dat3m.dartagnan.verification.model.ExecutionModel; +import com.dat3m.dartagnan.verification.model.MemoryObjectModel; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -34,7 +35,7 @@ public class ExecutionGraphVisualizer { private BiPredicate rfFilter = (x, y) -> true; private BiPredicate frFilter = (x, y) -> true; private BiPredicate coFilter = (x, y) -> true; - private final LinkedHashMap objToAddrMap = new LinkedHashMap<>(); + private final LinkedHashMap objToAddrMap = new LinkedHashMap<>(); public ExecutionGraphVisualizer() { this.graphviz = new Graphviz(); @@ -74,9 +75,9 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu } private void computeAddressMap(ExecutionModel model) { - final Map memLayout = model.getMemoryLayoutMap(); + final Map memLayout = model.getMemoryLayoutMap(); final List objs = new ArrayList<>(memLayout.keySet()); - objs.sort(Comparator.comparing(memLayout::get)); + objs.sort(Comparator.comparing(obj -> memLayout.get(obj).address())); for (MemoryObject obj : objs) { objToAddrMap.put(obj, memLayout.get(obj)); @@ -187,24 +188,22 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model } private String getAddressString(BigInteger address) { - MemoryObject obj = null; - BigInteger objAddress = null; - for (Map.Entry entry : objToAddrMap.entrySet()) { - final BigInteger nextObjAddr = entry.getValue(); + MemoryObjectModel obj = null; + for (Map.Entry entry : objToAddrMap.entrySet()) { + final BigInteger nextObjAddr = entry.getValue().address(); if (nextObjAddr.compareTo(address) > 0) { break; } - obj = entry.getKey(); - objAddress = nextObjAddr; + obj = entry.getValue(); } if (obj == null) { return address + " [OOB]"; - } else if (address.equals(objAddress)) { + } else if (address.equals(obj.address())) { return obj.toString(); } else { - final boolean isOOB = address.compareTo(objAddress.add(BigInteger.valueOf(obj.size()))) >= 0; - return String.format("%s + %s%s", obj, address.subtract(objAddress), isOOB ? " [OOB]" : ""); + final boolean isOOB = address.compareTo(obj.address().add(obj.size())) >= 0; + return String.format("%s + %s%s", obj, address.subtract(obj.address()), isOOB ? " [OOB]" : ""); } } From ba29901f69a3cd463367d0a4360dbb2eaa9c04a2 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 9 Oct 2024 16:07:46 +0200 Subject: [PATCH 02/14] Added missing MemoryObjectModel class and fix/simplify ExecutionGraphVisualizer --- .../verification/model/MemoryObjectModel.java | 8 ++++ .../graphviz/ExecutionGraphVisualizer.java | 42 +++++++++---------- 2 files changed, 27 insertions(+), 23 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java new file mode 100644 index 0000000000..d5356d3d87 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/MemoryObjectModel.java @@ -0,0 +1,8 @@ +package com.dat3m.dartagnan.verification.model; + +import com.dat3m.dartagnan.program.memory.MemoryObject; + +import java.math.BigInteger; + +public record MemoryObjectModel(MemoryObject object, BigInteger address, BigInteger size) { +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java index 2b4f452cb0..038e7310ea 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java @@ -4,10 +4,10 @@ import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.verification.model.EventData; import com.dat3m.dartagnan.verification.model.ExecutionModel; import com.dat3m.dartagnan.verification.model.MemoryObjectModel; +import com.google.common.collect.Lists; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -16,7 +16,10 @@ import java.io.IOException; import java.io.Writer; import java.math.BigInteger; -import java.util.*; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.List; +import java.util.Map; import java.util.function.BiPredicate; import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; @@ -35,7 +38,7 @@ public class ExecutionGraphVisualizer { private BiPredicate rfFilter = (x, y) -> true; private BiPredicate frFilter = (x, y) -> true; private BiPredicate coFilter = (x, y) -> true; - private final LinkedHashMap objToAddrMap = new LinkedHashMap<>(); + private final List sortedMemoryObjects = new ArrayList<>(); public ExecutionGraphVisualizer() { this.graphviz = new Graphviz(); @@ -75,13 +78,9 @@ public void generateGraphOfExecutionModel(Writer writer, String graphName, Execu } private void computeAddressMap(ExecutionModel model) { - final Map memLayout = model.getMemoryLayoutMap(); - final List objs = new ArrayList<>(memLayout.keySet()); - objs.sort(Comparator.comparing(obj -> memLayout.get(obj).address())); - - for (MemoryObject obj : objs) { - objToAddrMap.put(obj, memLayout.get(obj)); - } + model.getMemoryLayoutMap().entrySet().stream() + .sorted(Comparator.comparing(entry -> entry.getValue().address())) + .forEach(entry -> sortedMemoryObjects.add(entry.getValue())); } private boolean ignore(EventData e) { @@ -188,22 +187,19 @@ private ExecutionGraphVisualizer addThreadPo(Thread thread, ExecutionModel model } private String getAddressString(BigInteger address) { - MemoryObjectModel obj = null; - for (Map.Entry entry : objToAddrMap.entrySet()) { - final BigInteger nextObjAddr = entry.getValue().address(); - if (nextObjAddr.compareTo(address) > 0) { - break; - } - obj = entry.getValue(); - } + final MemoryObjectModel accObj = Lists.reverse(sortedMemoryObjects).stream() + .filter(o -> o.address().compareTo(address) <= 0) + .findFirst().orElse(null); - if (obj == null) { + if (accObj == null) { return address + " [OOB]"; - } else if (address.equals(obj.address())) { - return obj.toString(); } else { - final boolean isOOB = address.compareTo(obj.address().add(obj.size())) >= 0; - return String.format("%s + %s%s", obj, address.subtract(obj.address()), isOOB ? " [OOB]" : ""); + final boolean isOOB = address.compareTo(accObj.address().add(accObj.size())) >= 0; + final BigInteger offset = address.subtract(accObj.address()); + return String.format("%s[size=%s]%s%s", accObj.object(), accObj.size(), + !offset.equals(BigInteger.ZERO) ? " + " + offset : "", + isOOB ? " [OOB]" : "" + ); } } From 3a60ebfdcb31cac3b95f55eba84ba6fd72f75f3e Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 9 Oct 2024 16:08:12 +0200 Subject: [PATCH 03/14] Add encoding for dynamic memory layouts. --- .../dartagnan/encoding/EncodingHelper.java | 123 ++++++++++++++++++ .../dartagnan/encoding/ProgramEncoder.java | 61 ++++++++- 2 files changed, 178 insertions(+), 6 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java 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, From 111ce901bcba903ea289ffb1f790832b54b6087c Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 9 Oct 2024 16:10:01 +0200 Subject: [PATCH 04/14] Revert accidental change --- cat/power.cat | 2 -- 1 file changed, 2 deletions(-) diff --git a/cat/power.cat b/cat/power.cat index 25e781e525..7711ce90a3 100644 --- a/cat/power.cat +++ b/cat/power.cat @@ -45,7 +45,5 @@ let prop = (W*W & propbase)| (com*;propbase*;sync;hb*) acyclic co | prop irreflexive fre;prop;hb* -acyclic (prop | hb) - (* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *) empty rmw & (fre; coe) as atomic From f193e15f84cbe250a7ca742026b4bf3adbacc0b9 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 9 Oct 2024 16:17:46 +0200 Subject: [PATCH 05/14] Added two tests with non-deterministic array allocations. --- benchmarks/miscellaneous/nondet_alloc.c | 27 +++ benchmarks/miscellaneous/nondet_alloc_2.c | 20 ++ .../dat3m/dartagnan/c/MiscellaneousTest.java | 4 +- .../resources/miscellaneous/nondet_alloc.ll | 225 ++++++++++++++++++ .../resources/miscellaneous/nondet_alloc_2.ll | 183 ++++++++++++++ 5 files changed, 458 insertions(+), 1 deletion(-) create mode 100644 benchmarks/miscellaneous/nondet_alloc.c create mode 100644 benchmarks/miscellaneous/nondet_alloc_2.c create mode 100644 dartagnan/src/test/resources/miscellaneous/nondet_alloc.ll create mode 100644 dartagnan/src/test/resources/miscellaneous/nondet_alloc_2.ll diff --git a/benchmarks/miscellaneous/nondet_alloc.c b/benchmarks/miscellaneous/nondet_alloc.c new file mode 100644 index 0000000000..436fdd7565 --- /dev/null +++ b/benchmarks/miscellaneous/nondet_alloc.c @@ -0,0 +1,27 @@ +#include +#include +#include + + +#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); +} diff --git a/benchmarks/miscellaneous/nondet_alloc_2.c b/benchmarks/miscellaneous/nondet_alloc_2.c new file mode 100644 index 0000000000..dcc41fa50b --- /dev/null +++ b/benchmarks/miscellaneous/nondet_alloc_2.c @@ -0,0 +1,20 @@ +#include +#include +#include +#include + +int main() +{ + int size_int = __VERIFIER_nondet_int(); + __VERIFIER_assume(size_int > 0); + // NOTE: Putting the assumption on the below rather than 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); +} diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java index 7a2c27dc89..13a6da97d7 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java @@ -91,7 +91,9 @@ public static Iterable data() throws IOException { {"offsetof", IMM, PASS, 1}, {"ctlz", IMM, PASS, 1}, {"cttz", IMM, PASS, 1}, - {"jumpIntoLoop", IMM, PASS, 11} + {"jumpIntoLoop", IMM, PASS, 11}, + {"nondet_alloc", IMM, FAIL, 1}, + {"nondet_alloc_2", IMM, PASS, 1}, }); } diff --git a/dartagnan/src/test/resources/miscellaneous/nondet_alloc.ll b/dartagnan/src/test/resources/miscellaneous/nondet_alloc.ll new file mode 100644 index 0000000000..b33b6d6058 --- /dev/null +++ b/dartagnan/src/test/resources/miscellaneous/nondet_alloc.ll @@ -0,0 +1,225 @@ +; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_alloc.c' +source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_alloc.c" +target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128" +target triple = "arm64-apple-macosx14.0.0" + +@__func__.main = private unnamed_addr constant [5 x i8] c"main\00", align 1 +@.str = private unnamed_addr constant [15 x i8] c"nondet_alloc.c\00", align 1 +@.str.1 = private unnamed_addr constant [38 x i8] c"sum < (MAX_SIZE * (MAX_SIZE - 1)) / 2\00", align 1 + +; Function Attrs: noinline nounwind ssp uwtable +define i32 @main() #0 !dbg !13 { + %1 = alloca i32, align 4 + %2 = alloca i32, align 4 + %3 = alloca i32*, align 8 + %4 = alloca i32, align 4 + %5 = alloca i32, align 4 + %6 = alloca i32, align 4 + store i32 0, i32* %1, align 4 + call void @llvm.dbg.declare(metadata i32* %2, metadata !19, metadata !DIExpression()), !dbg !20 + %7 = call i32 @__VERIFIER_nondet_int(), !dbg !21 + store i32 %7, i32* %2, align 4, !dbg !20 + %8 = load i32, i32* %2, align 4, !dbg !22 + %9 = icmp sgt i32 %8, 0, !dbg !23 + br i1 %9, label %10, label %13, !dbg !24 + +10: ; preds = %0 + %11 = load i32, i32* %2, align 4, !dbg !25 + %12 = icmp sle i32 %11, 10, !dbg !26 + br label %13 + +13: ; preds = %10, %0 + %14 = phi i1 [ false, %0 ], [ %12, %10 ], !dbg !27 + %15 = zext i1 %14 to i32, !dbg !24 + call void @__VERIFIER_assume(i32 noundef %15), !dbg !28 + call void @llvm.dbg.declare(metadata i32** %3, metadata !29, metadata !DIExpression()), !dbg !31 + %16 = load i32, i32* %2, align 4, !dbg !32 + %17 = sext i32 %16 to i64, !dbg !32 + %18 = mul i64 %17, 4, !dbg !33 + %19 = call i8* @malloc(i64 noundef %18), !dbg !34 + %20 = bitcast i8* %19 to i32*, !dbg !34 + store i32* %20, i32** %3, align 8, !dbg !31 + call void @__VERIFIER_loop_bound(i32 noundef 11), !dbg !35 + call void @llvm.dbg.declare(metadata i32* %4, metadata !36, metadata !DIExpression()), !dbg !38 + store i32 0, i32* %4, align 4, !dbg !38 + br label %21, !dbg !39 + +21: ; preds = %31, %13 + %22 = load i32, i32* %4, align 4, !dbg !40 + %23 = load i32, i32* %2, align 4, !dbg !42 + %24 = icmp slt i32 %22, %23, !dbg !43 + br i1 %24, label %25, label %34, !dbg !44 + +25: ; preds = %21 + %26 = load i32, i32* %4, align 4, !dbg !45 + %27 = load i32*, i32** %3, align 8, !dbg !47 + %28 = load i32, i32* %4, align 4, !dbg !48 + %29 = sext i32 %28 to i64, !dbg !47 + %30 = getelementptr inbounds i32, i32* %27, i64 %29, !dbg !47 + store i32 %26, i32* %30, align 4, !dbg !49 + br label %31, !dbg !50 + +31: ; preds = %25 + %32 = load i32, i32* %4, align 4, !dbg !51 + %33 = add nsw i32 %32, 1, !dbg !51 + store i32 %33, i32* %4, align 4, !dbg !51 + br label %21, !dbg !52, !llvm.loop !53 + +34: ; preds = %21 + call void @llvm.dbg.declare(metadata i32* %5, metadata !56, metadata !DIExpression()), !dbg !57 + store i32 0, i32* %5, align 4, !dbg !57 + call void @__VERIFIER_loop_bound(i32 noundef 11), !dbg !58 + call void @llvm.dbg.declare(metadata i32* %6, metadata !59, metadata !DIExpression()), !dbg !61 + store i32 0, i32* %6, align 4, !dbg !61 + br label %35, !dbg !62 + +35: ; preds = %47, %34 + %36 = load i32, i32* %6, align 4, !dbg !63 + %37 = load i32, i32* %2, align 4, !dbg !65 + %38 = icmp slt i32 %36, %37, !dbg !66 + br i1 %38, label %39, label %50, !dbg !67 + +39: ; preds = %35 + %40 = load i32*, i32** %3, align 8, !dbg !68 + %41 = load i32, i32* %6, align 4, !dbg !70 + %42 = sext i32 %41 to i64, !dbg !68 + %43 = getelementptr inbounds i32, i32* %40, i64 %42, !dbg !68 + %44 = load i32, i32* %43, align 4, !dbg !68 + %45 = load i32, i32* %5, align 4, !dbg !71 + %46 = add nsw i32 %45, %44, !dbg !71 + store i32 %46, i32* %5, align 4, !dbg !71 + br label %47, !dbg !72 + +47: ; preds = %39 + %48 = load i32, i32* %6, align 4, !dbg !73 + %49 = add nsw i32 %48, 1, !dbg !73 + store i32 %49, i32* %6, align 4, !dbg !73 + br label %35, !dbg !74, !llvm.loop !75 + +50: ; preds = %35 + %51 = load i32, i32* %5, align 4, !dbg !77 + %52 = icmp slt i32 %51, 45, !dbg !77 + %53 = xor i1 %52, true, !dbg !77 + %54 = zext i1 %53 to i32, !dbg !77 + %55 = sext i32 %54 to i64, !dbg !77 + %56 = icmp ne i64 %55, 0, !dbg !77 + br i1 %56, label %57, label %59, !dbg !77 + +57: ; preds = %50 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([15 x i8], [15 x i8]* @.str, i64 0, i64 0), i32 noundef 26, i8* noundef getelementptr inbounds ([38 x i8], [38 x i8]* @.str.1, i64 0, i64 0)) #4, !dbg !77 + unreachable, !dbg !77 + +58: ; No predecessors! + br label %60, !dbg !77 + +59: ; preds = %50 + br label %60, !dbg !77 + +60: ; preds = %59, %58 + %61 = load i32, i32* %1, align 4, !dbg !78 + ret i32 %61, !dbg !78 +} + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +declare i32 @__VERIFIER_nondet_int() #2 + +declare void @__VERIFIER_assume(i32 noundef) #2 + +declare i8* @malloc(i64 noundef) #2 + +declare void @__VERIFIER_loop_bound(i32 noundef) #2 + +; Function Attrs: cold noreturn +declare void @__assert_rtn(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #3 + +attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #1 = { nofree nosync nounwind readnone speculatable willreturn } +attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #3 = { cold noreturn "disable-tail-calls"="true" "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #4 = { cold noreturn } + +!llvm.dbg.cu = !{!0} +!llvm.module.flags = !{!2, !3, !4, !5, !6, !7, !8, !9, !10, !11} +!llvm.ident = !{!12} + +!0 = distinct !DICompileUnit(language: DW_LANG_C99, file: !1, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk") +!1 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_alloc.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!2 = !{i32 7, !"Dwarf Version", i32 4} +!3 = !{i32 2, !"Debug Info Version", i32 3} +!4 = !{i32 1, !"wchar_size", i32 4} +!5 = !{i32 1, !"branch-target-enforcement", i32 0} +!6 = !{i32 1, !"sign-return-address", i32 0} +!7 = !{i32 1, !"sign-return-address-all", i32 0} +!8 = !{i32 1, !"sign-return-address-with-bkey", i32 0} +!9 = !{i32 7, !"PIC Level", i32 2} +!10 = !{i32 7, !"uwtable", i32 1} +!11 = !{i32 7, !"frame-pointer", i32 1} +!12 = !{!"Homebrew clang version 14.0.6"} +!13 = distinct !DISubprogram(name: "main", scope: !14, file: !14, line: 8, type: !15, scopeLine: 9, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !18) +!14 = !DIFile(filename: "benchmarks/miscellaneous/nondet_alloc.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!15 = !DISubroutineType(types: !16) +!16 = !{!17} +!17 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!18 = !{} +!19 = !DILocalVariable(name: "size", scope: !13, file: !14, line: 10, type: !17) +!20 = !DILocation(line: 10, column: 9, scope: !13) +!21 = !DILocation(line: 10, column: 16, scope: !13) +!22 = !DILocation(line: 11, column: 23, scope: !13) +!23 = !DILocation(line: 11, column: 28, scope: !13) +!24 = !DILocation(line: 11, column: 32, scope: !13) +!25 = !DILocation(line: 11, column: 35, scope: !13) +!26 = !DILocation(line: 11, column: 40, scope: !13) +!27 = !DILocation(line: 0, scope: !13) +!28 = !DILocation(line: 11, column: 5, scope: !13) +!29 = !DILocalVariable(name: "array", scope: !13, file: !14, line: 12, type: !30) +!30 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !17, size: 64) +!31 = !DILocation(line: 12, column: 10, scope: !13) +!32 = !DILocation(line: 12, column: 25, scope: !13) +!33 = !DILocation(line: 12, column: 30, scope: !13) +!34 = !DILocation(line: 12, column: 18, scope: !13) +!35 = !DILocation(line: 14, column: 5, scope: !13) +!36 = !DILocalVariable(name: "i", scope: !37, file: !14, line: 15, type: !17) +!37 = distinct !DILexicalBlock(scope: !13, file: !14, line: 15, column: 5) +!38 = !DILocation(line: 15, column: 14, scope: !37) +!39 = !DILocation(line: 15, column: 10, scope: !37) +!40 = !DILocation(line: 15, column: 21, scope: !41) +!41 = distinct !DILexicalBlock(scope: !37, file: !14, line: 15, column: 5) +!42 = !DILocation(line: 15, column: 25, scope: !41) +!43 = !DILocation(line: 15, column: 23, scope: !41) +!44 = !DILocation(line: 15, column: 5, scope: !37) +!45 = !DILocation(line: 16, column: 20, scope: !46) +!46 = distinct !DILexicalBlock(scope: !41, file: !14, line: 15, column: 36) +!47 = !DILocation(line: 16, column: 9, scope: !46) +!48 = !DILocation(line: 16, column: 15, scope: !46) +!49 = !DILocation(line: 16, column: 18, scope: !46) +!50 = !DILocation(line: 17, column: 5, scope: !46) +!51 = !DILocation(line: 15, column: 32, scope: !41) +!52 = !DILocation(line: 15, column: 5, scope: !41) +!53 = distinct !{!53, !44, !54, !55} +!54 = !DILocation(line: 17, column: 5, scope: !37) +!55 = !{!"llvm.loop.mustprogress"} +!56 = !DILocalVariable(name: "sum", scope: !13, file: !14, line: 19, type: !17) +!57 = !DILocation(line: 19, column: 9, scope: !13) +!58 = !DILocation(line: 20, column: 5, scope: !13) +!59 = !DILocalVariable(name: "i", scope: !60, file: !14, line: 21, type: !17) +!60 = distinct !DILexicalBlock(scope: !13, file: !14, line: 21, column: 5) +!61 = !DILocation(line: 21, column: 14, scope: !60) +!62 = !DILocation(line: 21, column: 10, scope: !60) +!63 = !DILocation(line: 21, column: 21, scope: !64) +!64 = distinct !DILexicalBlock(scope: !60, file: !14, line: 21, column: 5) +!65 = !DILocation(line: 21, column: 25, scope: !64) +!66 = !DILocation(line: 21, column: 23, scope: !64) +!67 = !DILocation(line: 21, column: 5, scope: !60) +!68 = !DILocation(line: 22, column: 16, scope: !69) +!69 = distinct !DILexicalBlock(scope: !64, file: !14, line: 21, column: 36) +!70 = !DILocation(line: 22, column: 22, scope: !69) +!71 = !DILocation(line: 22, column: 13, scope: !69) +!72 = !DILocation(line: 23, column: 5, scope: !69) +!73 = !DILocation(line: 21, column: 32, scope: !64) +!74 = !DILocation(line: 21, column: 5, scope: !64) +!75 = distinct !{!75, !67, !76, !55} +!76 = !DILocation(line: 23, column: 5, scope: !60) +!77 = !DILocation(line: 26, column: 5, scope: !13) +!78 = !DILocation(line: 27, column: 1, scope: !13) diff --git a/dartagnan/src/test/resources/miscellaneous/nondet_alloc_2.ll b/dartagnan/src/test/resources/miscellaneous/nondet_alloc_2.ll new file mode 100644 index 0000000000..9d3116ab1c --- /dev/null +++ b/dartagnan/src/test/resources/miscellaneous/nondet_alloc_2.ll @@ -0,0 +1,183 @@ +; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_alloc_2.c' +source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_alloc_2.c" +target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128" +target triple = "arm64-apple-macosx14.0.0" + +@__func__.main = private unnamed_addr constant [5 x i8] c"main\00", align 1 +@.str = private unnamed_addr constant [17 x i8] c"nondet_alloc_2.c\00", align 1 +@.str.1 = private unnamed_addr constant [17 x i8] c"array != array_2\00", align 1 +@.str.2 = private unnamed_addr constant [25 x i8] c"((size_t)array) % 8 == 0\00", align 1 +@.str.3 = private unnamed_addr constant [27 x i8] c"((size_t)array_2) % 8 == 0\00", align 1 + +; Function Attrs: noinline nounwind ssp uwtable +define i32 @main() #0 !dbg !19 { + %1 = alloca i32, align 4 + %2 = alloca i32, align 4 + %3 = alloca i64, align 8 + %4 = alloca i32*, align 8 + %5 = alloca i32*, align 8 + store i32 0, i32* %1, align 4 + call void @llvm.dbg.declare(metadata i32* %2, metadata !25, metadata !DIExpression()), !dbg !26 + %6 = call i32 @__VERIFIER_nondet_int(), !dbg !27 + store i32 %6, i32* %2, align 4, !dbg !26 + %7 = load i32, i32* %2, align 4, !dbg !28 + %8 = icmp sgt i32 %7, 0, !dbg !29 + %9 = zext i1 %8 to i32, !dbg !29 + call void @__VERIFIER_assume(i32 noundef %9), !dbg !30 + call void @llvm.dbg.declare(metadata i64* %3, metadata !31, metadata !DIExpression()), !dbg !32 + %10 = load i32, i32* %2, align 4, !dbg !33 + %11 = sext i32 %10 to i64, !dbg !34 + store i64 %11, i64* %3, align 8, !dbg !32 + call void @llvm.dbg.declare(metadata i32** %4, metadata !35, metadata !DIExpression()), !dbg !37 + %12 = load i64, i64* %3, align 8, !dbg !38 + %13 = mul i64 %12, 4, !dbg !39 + %14 = call i8* @malloc(i64 noundef %13) #5, !dbg !40 + %15 = bitcast i8* %14 to i32*, !dbg !40 + store i32* %15, i32** %4, align 8, !dbg !37 + call void @llvm.dbg.declare(metadata i32** %5, metadata !41, metadata !DIExpression()), !dbg !42 + %16 = load i64, i64* %3, align 8, !dbg !43 + %17 = mul i64 %16, 4, !dbg !44 + %18 = call i8* @malloc(i64 noundef %17) #5, !dbg !45 + %19 = bitcast i8* %18 to i32*, !dbg !45 + store i32* %19, i32** %5, align 8, !dbg !42 + %20 = load i32*, i32** %4, align 8, !dbg !46 + %21 = load i32*, i32** %5, align 8, !dbg !46 + %22 = icmp ne i32* %20, %21, !dbg !46 + %23 = xor i1 %22, true, !dbg !46 + %24 = zext i1 %23 to i32, !dbg !46 + %25 = sext i32 %24 to i64, !dbg !46 + %26 = icmp ne i64 %25, 0, !dbg !46 + br i1 %26, label %27, label %29, !dbg !46 + +27: ; preds = %0 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([17 x i8], [17 x i8]* @.str, i64 0, i64 0), i32 noundef 14, i8* noundef getelementptr inbounds ([17 x i8], [17 x i8]* @.str.1, i64 0, i64 0)) #6, !dbg !46 + unreachable, !dbg !46 + +28: ; No predecessors! + br label %30, !dbg !46 + +29: ; preds = %0 + br label %30, !dbg !46 + +30: ; preds = %29, %28 + %31 = load i32*, i32** %4, align 8, !dbg !47 + %32 = ptrtoint i32* %31 to i64, !dbg !47 + %33 = urem i64 %32, 8, !dbg !47 + %34 = icmp eq i64 %33, 0, !dbg !47 + %35 = xor i1 %34, true, !dbg !47 + %36 = zext i1 %35 to i32, !dbg !47 + %37 = sext i32 %36 to i64, !dbg !47 + %38 = icmp ne i64 %37, 0, !dbg !47 + br i1 %38, label %39, label %41, !dbg !47 + +39: ; preds = %30 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([17 x i8], [17 x i8]* @.str, i64 0, i64 0), i32 noundef 15, i8* noundef getelementptr inbounds ([25 x i8], [25 x i8]* @.str.2, i64 0, i64 0)) #6, !dbg !47 + unreachable, !dbg !47 + +40: ; No predecessors! + br label %42, !dbg !47 + +41: ; preds = %30 + br label %42, !dbg !47 + +42: ; preds = %41, %40 + %43 = load i32*, i32** %5, align 8, !dbg !48 + %44 = ptrtoint i32* %43 to i64, !dbg !48 + %45 = urem i64 %44, 8, !dbg !48 + %46 = icmp eq i64 %45, 0, !dbg !48 + %47 = xor i1 %46, true, !dbg !48 + %48 = zext i1 %47 to i32, !dbg !48 + %49 = sext i32 %48 to i64, !dbg !48 + %50 = icmp ne i64 %49, 0, !dbg !48 + br i1 %50, label %51, label %53, !dbg !48 + +51: ; preds = %42 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([17 x i8], [17 x i8]* @.str, i64 0, i64 0), i32 noundef 16, i8* noundef getelementptr inbounds ([27 x i8], [27 x i8]* @.str.3, i64 0, i64 0)) #6, !dbg !48 + unreachable, !dbg !48 + +52: ; No predecessors! + br label %54, !dbg !48 + +53: ; preds = %42 + br label %54, !dbg !48 + +54: ; preds = %53, %52 + %55 = load i32, i32* %1, align 4, !dbg !49 + ret i32 %55, !dbg !49 +} + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +declare i32 @__VERIFIER_nondet_int() #2 + +declare void @__VERIFIER_assume(i32 noundef) #2 + +; Function Attrs: allocsize(0) +declare i8* @malloc(i64 noundef) #3 + +; Function Attrs: cold noreturn +declare void @__assert_rtn(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #4 + +attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #1 = { nofree nosync nounwind readnone speculatable willreturn } +attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #3 = { allocsize(0) "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #4 = { cold noreturn "disable-tail-calls"="true" "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #5 = { allocsize(0) } +attributes #6 = { cold noreturn } + +!llvm.dbg.cu = !{!0} +!llvm.module.flags = !{!8, !9, !10, !11, !12, !13, !14, !15, !16, !17} +!llvm.ident = !{!18} + +!0 = distinct !DICompileUnit(language: DW_LANG_C99, file: !1, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !2, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk") +!1 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_alloc_2.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!2 = !{!3} +!3 = !DIDerivedType(tag: DW_TAG_typedef, name: "size_t", file: !4, line: 31, baseType: !5) +!4 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_types/_size_t.h", directory: "") +!5 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_size_t", file: !6, line: 70, baseType: !7) +!6 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/arm/_types.h", directory: "") +!7 = !DIBasicType(name: "unsigned long", size: 64, encoding: DW_ATE_unsigned) +!8 = !{i32 7, !"Dwarf Version", i32 4} +!9 = !{i32 2, !"Debug Info Version", i32 3} +!10 = !{i32 1, !"wchar_size", i32 4} +!11 = !{i32 1, !"branch-target-enforcement", i32 0} +!12 = !{i32 1, !"sign-return-address", i32 0} +!13 = !{i32 1, !"sign-return-address-all", i32 0} +!14 = !{i32 1, !"sign-return-address-with-bkey", i32 0} +!15 = !{i32 7, !"PIC Level", i32 2} +!16 = !{i32 7, !"uwtable", i32 1} +!17 = !{i32 7, !"frame-pointer", i32 1} +!18 = !{!"Homebrew clang version 14.0.6"} +!19 = distinct !DISubprogram(name: "main", scope: !20, file: !20, line: 6, type: !21, scopeLine: 7, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !24) +!20 = !DIFile(filename: "benchmarks/miscellaneous/nondet_alloc_2.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!21 = !DISubroutineType(types: !22) +!22 = !{!23} +!23 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!24 = !{} +!25 = !DILocalVariable(name: "size_int", scope: !19, file: !20, line: 8, type: !23) +!26 = !DILocation(line: 8, column: 9, scope: !19) +!27 = !DILocation(line: 8, column: 20, scope: !19) +!28 = !DILocation(line: 9, column: 23, scope: !19) +!29 = !DILocation(line: 9, column: 32, scope: !19) +!30 = !DILocation(line: 9, column: 5, scope: !19) +!31 = !DILocalVariable(name: "size", scope: !19, file: !20, line: 10, type: !3) +!32 = !DILocation(line: 10, column: 12, scope: !19) +!33 = !DILocation(line: 10, column: 27, scope: !19) +!34 = !DILocation(line: 10, column: 19, scope: !19) +!35 = !DILocalVariable(name: "array", scope: !19, file: !20, line: 11, type: !36) +!36 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !23, size: 64) +!37 = !DILocation(line: 11, column: 10, scope: !19) +!38 = !DILocation(line: 11, column: 25, scope: !19) +!39 = !DILocation(line: 11, column: 30, scope: !19) +!40 = !DILocation(line: 11, column: 18, scope: !19) +!41 = !DILocalVariable(name: "array_2", scope: !19, file: !20, line: 12, type: !36) +!42 = !DILocation(line: 12, column: 10, scope: !19) +!43 = !DILocation(line: 12, column: 27, scope: !19) +!44 = !DILocation(line: 12, column: 32, scope: !19) +!45 = !DILocation(line: 12, column: 20, scope: !19) +!46 = !DILocation(line: 14, column: 5, scope: !19) +!47 = !DILocation(line: 15, column: 5, scope: !19) +!48 = !DILocation(line: 16, column: 5, scope: !19) +!49 = !DILocation(line: 17, column: 1, scope: !19) From d9abdfa8280f04534c958e30cc52832321cc296d Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Wed, 9 Oct 2024 17:05:24 +0200 Subject: [PATCH 06/14] Only allow Allocs with sizes of arch type (automatically enforced during construction) --- .../java/com/dat3m/dartagnan/program/event/EventFactory.java | 1 + 1 file changed, 1 insertion(+) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index add6cc5009..8b1f720f83 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -93,6 +93,7 @@ public static List eventSequence(Object... events) { public static Alloc newAlloc(Register register, Type allocType, Expression arraySize, boolean isHeapAlloc, boolean doesZeroOutMemory) { + arraySize = expressions.makeCast(arraySize, TypeFactory.getInstance().getArchType(), false); return new Alloc(register, allocType, arraySize, isHeapAlloc, doesZeroOutMemory); } From 925fe12781bbe5f4b56ed9164eddd57e8981988f Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 10 Oct 2024 13:26:00 +0200 Subject: [PATCH 07/14] Disabled some unsupported tests in RA Updated some test code to use "MemoryObject.getKnownSize" rather than "MemoryObject.size" --- .../encoding/RelationAnalysisTest.java | 33 ++++++++++++++----- .../visitors/spirv/VisitorOpsMemoryTest.java | 28 ++++++++-------- .../VisitorExtensionClspvReflectionTest.java | 4 +-- 3 files changed, 41 insertions(+), 24 deletions(-) diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java index f4ffc6fa82..407170ea3a 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java @@ -23,7 +23,10 @@ import java.nio.file.DirectoryStream; import java.nio.file.Files; import java.nio.file.Path; -import java.util.*; +import java.util.Arrays; +import java.util.EnumSet; +import java.util.LinkedList; +import java.util.List; import static com.dat3m.dartagnan.configuration.Alias.FIELD_SENSITIVE; import static com.dat3m.dartagnan.configuration.OptionNames.*; @@ -62,37 +65,51 @@ public static Iterable data() throws IOException { { "dartagnan/src/test/resources/lfds", "cat/c11.cat", Arch.C11 }, { "dartagnan/src/test/resources/locks", "cat/c11.cat", Arch.C11 }, { "dartagnan/src/test/resources/libvsync", "cat/c11.cat", Arch.C11 }, - { "dartagnan/src/test/resources/miscellaneous", "cat/c11.cat", Arch.C11 }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/c11.cat", Arch.C11 }, { "dartagnan/src/test/resources/lfds", "cat/imm.cat", Arch.C11 }, { "dartagnan/src/test/resources/locks", "cat/imm.cat", Arch.C11 }, { "dartagnan/src/test/resources/libvsync", "cat/imm.cat", Arch.C11 }, - { "dartagnan/src/test/resources/miscellaneous", "cat/imm.cat", Arch.C11 }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/imm.cat", Arch.C11 }, { "dartagnan/src/test/resources/lfds", "cat/vmm.cat", Arch.C11 }, { "dartagnan/src/test/resources/locks", "cat/vmm.cat", Arch.C11 }, { "dartagnan/src/test/resources/libvsync", "cat/vmm.cat", Arch.C11 }, - { "dartagnan/src/test/resources/miscellaneous", "cat/vmm.cat", Arch.C11 }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/vmm.cat", Arch.C11 }, { "dartagnan/src/test/resources/lfds", "cat/rc11.cat", Arch.C11 }, { "dartagnan/src/test/resources/locks", "cat/rc11.cat", Arch.C11 }, { "dartagnan/src/test/resources/libvsync", "cat/rc11.cat", Arch.C11 }, - { "dartagnan/src/test/resources/miscellaneous", "cat/rc11.cat", Arch.C11 }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/rc11.cat", Arch.C11 }, { "dartagnan/src/test/resources/lfds", "cat/aarch64.cat", Arch.ARM8 }, { "dartagnan/src/test/resources/locks", "cat/aarch64.cat", Arch.ARM8 }, { "dartagnan/src/test/resources/libvsync", "cat/aarch64.cat", Arch.ARM8 }, - { "dartagnan/src/test/resources/miscellaneous", "cat/aarch64.cat", Arch.ARM8 }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/aarch64.cat", Arch.ARM8 }, { "dartagnan/src/test/resources/lfds", "cat/tso.cat", Arch.TSO }, { "dartagnan/src/test/resources/locks", "cat/tso.cat", Arch.TSO }, { "dartagnan/src/test/resources/libvsync", "cat/tso.cat", Arch.TSO }, - { "dartagnan/src/test/resources/miscellaneous", "cat/tso.cat", Arch.TSO }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/tso.cat", Arch.TSO }, { "dartagnan/src/test/resources/lfds", "cat/riscv.cat", Arch.RISCV }, { "dartagnan/src/test/resources/locks", "cat/riscv.cat", Arch.RISCV }, { "dartagnan/src/test/resources/libvsync", "cat/riscv.cat", Arch.RISCV }, - { "dartagnan/src/test/resources/miscellaneous", "cat/riscv.cat", Arch.RISCV }, + // Requires new alias analysis, but we cannot enable it due to + // https://github.com/hernanponcedeleon/Dat3M/issues/746 + //{ "dartagnan/src/test/resources/miscellaneous", "cat/riscv.cat", Arch.RISCV }, { "dartagnan/src/test/resources/spirv/benchmarks", "cat/spirv.cat", Arch.VULKAN }, }); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java index e66d054595..ca5cb0ac27 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/VisitorOpsMemoryTest.java @@ -12,13 +12,13 @@ import com.dat3m.dartagnan.parsers.SpirvParser; import com.dat3m.dartagnan.parsers.program.visitors.spirv.mocks.MockProgramBuilder; import com.dat3m.dartagnan.parsers.program.visitors.spirv.mocks.MockSpirvParser; -import com.dat3m.dartagnan.program.event.Event; -import com.dat3m.dartagnan.program.memory.ScopedPointer; -import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.program.event.core.Store; +import com.dat3m.dartagnan.program.memory.ScopedPointer; +import com.dat3m.dartagnan.program.memory.ScopedPointerVariable; import org.junit.Test; import java.util.List; @@ -198,7 +198,7 @@ public void testVariable() { for (int i = 0; i < 4; i++) { ScopedPointerVariable pointer = (ScopedPointerVariable) builder.getExpression(variables[i]); assertNotNull(pointer); - assertEquals(VisitorOpsMemoryTest.types.getMemorySizeInBytes(types[i]), pointer.getAddress().size()); + assertEquals(VisitorOpsMemoryTest.types.getMemorySizeInBytes(types[i]), pointer.getAddress().getKnownSize()); } } @@ -274,17 +274,17 @@ private void doTestInitializedVariable(String input) { ScopedPointerVariable v1 = (ScopedPointerVariable) builder.getExpression("%v1"); assertNotNull(v1); - assertEquals(types.getMemorySizeInBytes(builder.getType("%bool")), v1.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(builder.getType("%bool")), v1.getAddress().getKnownSize()); assertEquals(o1, v1.getAddress().getInitialValue(0)); ScopedPointerVariable v2 = (ScopedPointerVariable) builder.getExpression("%v2"); assertNotNull(v2); - assertEquals(types.getMemorySizeInBytes(builder.getType("%int")), v2.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(builder.getType("%int")), v2.getAddress().getKnownSize()); assertEquals(o2, v2.getAddress().getInitialValue(0)); ScopedPointerVariable v3 = (ScopedPointerVariable) builder.getExpression("%v3"); assertNotNull(v3); - assertEquals(types.getMemorySizeInBytes(builder.getType("%v3int")), v3.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(builder.getType("%v3int")), v3.getAddress().getKnownSize()); List arrElements = o3.getOperands(); assertEquals(arrElements.get(0), v3.getAddress().getInitialValue(0)); assertEquals(arrElements.get(1), v3.getAddress().getInitialValue(4)); @@ -292,7 +292,7 @@ private void doTestInitializedVariable(String input) { ScopedPointerVariable v4 = (ScopedPointerVariable) builder.getExpression("%v4"); assertNotNull(v4); - assertEquals(types.getMemorySizeInBytes(builder.getType("%struct")), v4.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(builder.getType("%struct")), v4.getAddress().getKnownSize()); List structElements = o4.getOperands(); assertEquals(structElements.get(0), v4.getAddress().getInitialValue(0)); assertEquals(structElements.get(1), v4.getAddress().getInitialValue(4)); @@ -357,12 +357,12 @@ public void testRuntimeArray() { Type ot3 = types.getAggregateType(List.of(iType, ot1)); ScopedPointerVariable v1 = (ScopedPointerVariable) builder.getExpression("%v1"); - assertEquals(types.getMemorySizeInBytes(ot1), v1.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(ot1), v1.getAddress().getKnownSize()); assertEquals(o1, v1.getAddress().getInitialValue(0)); assertEquals(o2, v1.getAddress().getInitialValue(4)); ScopedPointerVariable v2 = (ScopedPointerVariable) builder.getExpression("%v2"); - assertEquals(types.getMemorySizeInBytes(ot2), v2.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(ot2), v2.getAddress().getKnownSize()); assertEquals(o1, v2.getAddress().getInitialValue(0)); assertEquals(o2, v2.getAddress().getInitialValue(4)); assertEquals(o3, v2.getAddress().getInitialValue(8)); @@ -371,7 +371,7 @@ public void testRuntimeArray() { assertEquals(o6, v2.getAddress().getInitialValue(20)); ScopedPointerVariable v3 = (ScopedPointerVariable) builder.getExpression("%v3"); - assertEquals(types.getMemorySizeInBytes(ot3), v3.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(ot3), v3.getAddress().getKnownSize()); assertEquals(o1, v3.getAddress().getInitialValue(0)); assertEquals(o1, v3.getAddress().getInitialValue(4)); assertEquals(o2, v3.getAddress().getInitialValue(8)); @@ -395,7 +395,7 @@ public void testRuntimeArrayFromConstant() { // then ScopedPointerVariable v = (ScopedPointerVariable) builder.getExpression("%v"); assertNotNull(v); - assertEquals(types.getMemorySizeInBytes(arr.getType()), v.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(arr.getType()), v.getAddress().getKnownSize()); assertEquals(arr.getOperands().get(0), v.getAddress().getInitialValue(0)); assertEquals(arr.getOperands().get(1), v.getAddress().getInitialValue(4)); } @@ -431,13 +431,13 @@ public void testReusingRuntimeArrayType() { // then ScopedPointerVariable v1 = (ScopedPointerVariable) builder.getExpression("%v1"); assertNotNull(v1); - assertEquals(types.getMemorySizeInBytes(a1.getType()), v1.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(a1.getType()), v1.getAddress().getKnownSize()); assertEquals(i1, v1.getAddress().getInitialValue(0)); assertEquals(i2, v1.getAddress().getInitialValue(8)); ScopedPointerVariable v2 = (ScopedPointerVariable) builder.getExpression("%v2"); assertNotNull(v2); - assertEquals(types.getMemorySizeInBytes(a2.getType()), v2.getAddress().size()); + assertEquals(types.getMemorySizeInBytes(a2.getType()), v2.getAddress().getKnownSize()); assertEquals(i1, v2.getAddress().getInitialValue(0)); assertEquals(i2, v2.getAddress().getInitialValue(8)); assertEquals(i3, v2.getAddress().getInitialValue(16)); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/extensions/VisitorExtensionClspvReflectionTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/extensions/VisitorExtensionClspvReflectionTest.java index 9f2868d4d2..b97d9b9752 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/extensions/VisitorExtensionClspvReflectionTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/parsers/program/visitors/spirv/extensions/VisitorExtensionClspvReflectionTest.java @@ -195,7 +195,7 @@ public void testPodPushConstant() { new MockSpirvParser(input).spv().accept(new VisitorExtensionClspvReflection(builder)); // then - assertEquals(12, pointer.getAddress().size()); + assertEquals(12, pointer.getAddress().getKnownSize()); } @Test @@ -215,7 +215,7 @@ public void testPodPushConstantMixed() { new MockSpirvParser(input).spv().accept(new VisitorExtensionClspvReflection(builder)); // then - assertEquals(16, pointer.getAddress().size()); + assertEquals(16, pointer.getAddress().getKnownSize()); verifyPushConstant(pointer, 0, List.of(24, 1, 1)); } From a10938047f614748db42b5c44656f387f1bcd7b7 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 10 Oct 2024 13:20:04 +0200 Subject: [PATCH 08/14] Some improvements to aarch64 pseudo-assembly (#741) Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/LitmusAArch64.g4 | 26 +++++++++++++++- .../parsers/program/utils/ProgramBuilder.java | 23 ++++++++++++++ .../visitors/VisitorLitmusAArch64.java | 23 ++++++++++++-- .../program/visitors/VisitorLitmusRISCV.java | 30 +++---------------- .../program/processing/ProcessingManager.java | 2 +- .../wmm/analysis/LazyRelationAnalysis.java | 12 ++------ .../wmm/analysis/NativeRelationAnalysis.java | 11 ------- 7 files changed, 76 insertions(+), 51 deletions(-) diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4 index 152c34d8e4..bae408b323 100644 --- a/dartagnan/src/main/antlr4/LitmusAArch64.g4 +++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4 @@ -76,6 +76,8 @@ instruction | branchRegister | branchLabel | fence + | return + | nop ; mov locals [String rD, int size] @@ -131,6 +133,14 @@ branchLabel : label Colon ; +return + : Ret + ; + +nop + : Nop + ; + loadInstruction locals [String mo] : LDR {$mo = MO_RX;} | LDAR {$mo = MO_ACQ;} @@ -252,7 +262,7 @@ location ; immediate - : Num constant + : Num Hexa? constant ; label @@ -265,6 +275,18 @@ assertionValue | constant ; +Hexa + : '0x' + ; + +Ret + : 'ret' + ; + +Nop + : 'nop' + ; + Locations : 'locations' ; @@ -371,10 +393,12 @@ BitfieldOperator Register64 : 'X' DigitSequence + | 'XZR' // zero register ; Register32 : 'W' DigitSequence + | 'WZR' // zero register ; LitmusLanguage diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java index b0bff0d508..1d1e773a9a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java @@ -7,12 +7,14 @@ import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.FunctionType; +import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.*; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; import com.dat3m.dartagnan.program.event.metadata.OriginalId; @@ -89,6 +91,27 @@ public static void processAfterParsing(Program program) { } } + public static void replaceZeroRegisters(Program program, List zeroRegNames) { + for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) { + if (func.hasBody()) { + for (String zeroRegName : zeroRegNames) { + Register zr = func.getRegister(zeroRegName); + if (zr != null) { + for (RegWriter rw : func.getEvents(RegWriter.class)) { + if (rw.getResultRegister().equals(zr)) { + Register dummy = rw.getThread().getOrNewRegister("__zeroRegDummy_" + zr.getName(), zr.getType()); + rw.setResultRegister(dummy); + } + } + // This comes after the loop to avoid the renaming in the initialization event + Event initToZero = EventFactory.newLocal(zr, expressions.makeGeneralZero(zr.getType())); + func.getEntry().insertAfter(initToZero); + } + } + } + } + } + // ---------------------------------------------------------------------------------------------------------------- // Misc diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java index 4c0d1e5091..455c285ad0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java @@ -17,9 +17,13 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Load; +import java.math.BigInteger; +import java.util.Arrays; import java.util.HashMap; import java.util.Map; +import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters; + public class VisitorLitmusAArch64 extends LitmusAArch64BaseVisitor { private static class CmpInstruction { @@ -53,10 +57,11 @@ public Object visitMain(LitmusAArch64Parser.MainContext ctx) { visitVariableDeclaratorList(ctx.variableDeclaratorList()); visitInstructionList(ctx.program().instructionList()); VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter()); - return programBuilder.build(); + Program prog = programBuilder.build(); + replaceZeroRegisters(prog, Arrays.asList("XZR, WZR")); + return prog; } - // ---------------------------------------------------------------------------------------------------------------- // Variable declarator list, e.g., { 0:EAX=0; 1:EAX=1; x=2; } @@ -211,6 +216,12 @@ public Object visitFence(LitmusAArch64Parser.FenceContext ctx) { return programBuilder.addChild(mainThread, EventFactory.newFenceOpt(ctx.Fence().getText(), ctx.opt)); } + @Override + public Object visitReturn(LitmusAArch64Parser.ReturnContext ctx) { + Label end = programBuilder.getEndOfThreadLabel(mainThread); + return programBuilder.addChild(mainThread, EventFactory.newGoto(end)); + } + @Override public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegister64Context ctx) { Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, archType); @@ -255,4 +266,12 @@ private Register visitOffset(LitmusAArch64Parser.OffsetContext ctx, Register reg programBuilder.addChild(mainThread, EventFactory.newLocal(result, expressions.makeAdd(register, expr))); return result; } + + @Override + public Expression visitImmediate(LitmusAArch64Parser.ImmediateContext ctx) { + final int radix = ctx.Hexa() != null ? 16 : 10; + BigInteger value = new BigInteger(ctx.constant().getText(), radix); + return expressions.makeValue(value, archType); + } + } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java index 8959730977..92568decfd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java @@ -1,12 +1,11 @@ package com.dat3m.dartagnan.parsers.program.visitors; +import java.util.Arrays; import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.ExpressionVisitor; import com.dat3m.dartagnan.expression.integers.IntLiteral; -import com.dat3m.dartagnan.expression.processing.ExprTransformer; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusRISCVBaseVisitor; @@ -16,10 +15,11 @@ import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Label; +import static com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder.replaceZeroRegisters; + public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor { private final ProgramBuilder programBuilder = ProgramBuilder.forArch(Program.SourceLanguage.LITMUS, Arch.RISCV); @@ -42,32 +42,10 @@ public Object visitMain(LitmusRISCVParser.MainContext ctx) { visitInstructionList(ctx.program().instructionList()); VisitorLitmusAssertions.parseAssertions(programBuilder, ctx.assertionList(), ctx.assertionFilter()); Program prog = programBuilder.build(); - replaceX0Register(prog); - + replaceZeroRegisters(prog, Arrays.asList("x0")); return prog; } - /* - The "x0" register plays a special role in RISCV: - 1. Reading accesses always return the value 0. - 2. Writing accesses are discarded. - TODO: The below code is a simple fix to guarantee point 1. above. - Point 2. might also be resolved: although we do not prevent writing to x0, - the value of x0 is never read after the transformation so its value is effectively 0. - However, the exists/forall clauses could still refer to that register and observe a non-zero value. - */ - private void replaceX0Register(Program program) { - final ExpressionVisitor x0Replacer = new ExprTransformer() { - @Override - public Expression visitRegister(Register reg) { - return reg.getName().equals("x0") ? expressions.makeGeneralZero(reg.getType()) : reg; - } - }; - program.getThreadEvents(RegReader.class) - .forEach(e -> e.transformExpressions(x0Replacer)); - } - - // ---------------------------------------------------------------------------------------------------------------- // Variable declarator list diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java index 60b209d087..451fc3678c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java @@ -96,7 +96,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep ComplexBlockSplitting.newInstance(), BranchReordering.fromConfig(config), Simplifier.fromConfig(config) - ), Target.FUNCTIONS, true + ), Target.ALL, true ), ProgramProcessor.fromFunctionProcessor(NormalizeLoops.newInstance(), Target.ALL, true), RegisterDecomposition.newInstance(), diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java index c02bd2aa9a..32db0c5cff 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java @@ -238,16 +238,8 @@ private EventGraph computeInternalDependencies(Set usageType reader.getRegisterReads().forEach(read -> { if (usageTypes.contains(read.usageType())) { Register register = read.register(); - // TODO: Update after this is merged - // https://github.com/hernanponcedeleon/Dat3M/pull/741 - // Register x0 is hardwired to the constant 0 in RISCV - // https://en.wikichip.org/wiki/risc-v/registers, - // and thus it generates no dependency, see - // https://github.com/herd/herdtools7/issues/408 - if (!program.getArch().equals(RISCV) || !register.getName().equals("x0")) { - state.ofRegister(register).getMayWriters().forEach(writer -> - data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader)); - } + state.ofRegister(register).getMayWriters() + .forEach(writer -> data.computeIfAbsent(writer, x -> new HashSet<>()).add(reader)); } }); }); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java index dca921255b..e2cf68ff7b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java @@ -40,7 +40,6 @@ import java.util.stream.Collectors; import java.util.stream.Stream; -import static com.dat3m.dartagnan.configuration.Arch.RISCV; import static com.dat3m.dartagnan.program.Register.UsageType.*; import static com.dat3m.dartagnan.program.event.Tag.*; import static com.google.common.base.Preconditions.checkArgument; @@ -915,16 +914,6 @@ private MutableKnowledge computeInternalDependencies(Set usageTypes) continue; } final Register register = regRead.register(); - // TODO: Update after this is merged - // https://github.com/hernanponcedeleon/Dat3M/pull/741 - // Register x0 is hardwired to the constant 0 in RISCV - // https://en.wikichip.org/wiki/risc-v/registers, - // and thus it generates no dependency, see - // https://github.com/herd/herdtools7/issues/408 - // TODO: Can't we just replace all reads of "x0" by 0 in RISC-specific preprocessing? - if (program.getArch().equals(RISCV) && register.getName().equals("x0")) { - continue; - } final List writers = state.ofRegister(register).getMayWriters(); for (Event regWriter : writers) { may.add(regWriter, regReader); From f23e627741b9c3a74ba339341d6453747278ce9d Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 10 Oct 2024 13:22:42 +0200 Subject: [PATCH 09/14] Allow show statements in cat grammar (#742) Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon --- dartagnan/src/main/antlr4/Cat.g4 | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4 index 84b4323be7..c5f899f394 100755 --- a/dartagnan/src/main/antlr4/Cat.g4 +++ b/dartagnan/src/main/antlr4/Cat.g4 @@ -5,7 +5,7 @@ import com.dat3m.dartagnan.wmm.axiom.*; } mcm - : (NAME)? (QUOTED_STRING)? (definition | include)+ EOF + : (NAME)? (QUOTED_STRING)? (definition | include | show)+ EOF ; definition @@ -58,7 +58,11 @@ expression ; include - : 'include' path = QUOTED_STRING + : INCLUDE path = QUOTED_STRING + ; + +show + : SHOW expression (AS NAME)? ; parameterList @@ -74,6 +78,8 @@ REC : 'rec'; AND : 'and'; AS : 'as'; TOID : 'toid'; +SHOW : 'show'; +INCLUDE : 'include'; ACYCLIC : 'acyclic'; IRREFLEXIVE : 'irreflexive'; From 6016dc4f2da6406d150c0533453b40159b9a6555 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 10 Oct 2024 15:11:04 +0200 Subject: [PATCH 10/14] Some cleanup --- .../dartagnan/encoding/ProgramEncoder.java | 93 ++++--------------- .../dartagnan/program/event/core/Alloc.java | 2 +- .../dartagnan/program/memory/Memory.java | 10 +- .../program/memory/MemoryObject.java | 17 ++-- .../program/memory/VirtualMemoryObject.java | 3 +- 5 files changed, 38 insertions(+), 87 deletions(-) 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 140cdfb659..c1db0641e3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -30,11 +30,17 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; -import org.sosy_lab.java_smt.api.*; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import java.math.BigInteger; -import java.util.*; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.List; +import java.util.Map; import static com.dat3m.dartagnan.configuration.OptionNames.INITIALIZE_REGISTERS; import static com.google.common.collect.Lists.reverse; @@ -73,7 +79,7 @@ public static ProgramEncoder withContext(EncodingContext context) throws Invalid return encoder; } - // ============================== Encoding ============================== + // ====================================== Encoding ====================================== public BooleanFormula encodeFullProgram() { return context.getBooleanFormulaManager().and( @@ -102,7 +108,7 @@ public BooleanFormula encodeConstants() { return context.getBooleanFormulaManager().and(enc); } - // =============================== Control flow ============================== + // ====================================== Control flow ====================================== private boolean isInitThread(Thread thread) { return thread.getEntry().getSuccessor() instanceof Init; @@ -278,78 +284,15 @@ private BooleanFormula encodeForwardProgress(Program program, ProgressModel prog }; } - // ===================================================================================== + // ====================================== Memory layout ====================================== - // Encodes the address values of memory objects. + // Encodes the address values and sizes of memory objects. public BooleanFormula encodeMemory() { logger.info("Encoding memory"); - final Memory memory = context.getTask().getProgram().getMemory(); - final FormulaManager fmgr = context.getFormulaManager(); - - return encodeDynamicMemoryLayout(memory); - - /*final Map memObj2Addr = computeStaticMemoryLayout(memory); - - final var enc = new ArrayList(); - for (final MemoryObject memObj : memory.getObjects()) { - final Formula addressVariable = context.address(memObj); - final BigInteger addressInteger = memObj2Addr.get(memObj); - if (addressVariable instanceof BitvectorFormula bitvectorVariable) { - final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager(); - final int length = bvmgr.getLength(bitvectorVariable); - enc.add(bvmgr.equal(bitvectorVariable, bvmgr.makeBitvector(length, addressInteger))); - } else { - assert addressVariable instanceof IntegerFormula; - final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); - enc.add(imgr.equal((IntegerFormula) addressVariable, imgr.makeNumber(addressInteger))); - } - - final Formula sizeVariable = context.size(memObj); - final BigInteger sizeInteger = BigInteger.valueOf(memObj.getKnownSize()); - if (sizeVariable instanceof BitvectorFormula bitvectorVariable) { - final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager(); - final int length = bvmgr.getLength(bitvectorVariable); - enc.add(bvmgr.equal(bitvectorVariable, bvmgr.makeBitvector(length, sizeInteger))); - } else { - assert addressVariable instanceof IntegerFormula; - final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager(); - enc.add(imgr.equal((IntegerFormula) sizeVariable, imgr.makeNumber(sizeInteger))); - } - } - return fmgr.getBooleanFormulaManager().and(enc);*/ - } - - /* - Computes a static memory layout, i.e., a mapping from memory objects to fixed addresses. - */ - private Map computeStaticMemoryLayout(Memory memory) { - // Addresses are typically at least two byte aligned - // https://stackoverflow.com/questions/23315939/why-2-lsbs-of-32-bit-arm-instruction-address-not-used - // Many algorithms rely on this assumption for correctness. - // Many objects have even stricter alignment requirements and need up to 8-byte alignment. - final BigInteger alignment = BigInteger.valueOf(8); - - Map memObj2Addr = new HashMap<>(); - BigInteger nextAddr = alignment; - for(MemoryObject memObj : memory.getObjects()) { - Preconditions.checkState(memObj.hasKnownSize(), "Cannot encode static memory layout for" + - " variable-sized memory object: %s", memObj); - memObj2Addr.put(memObj, nextAddr); - - // Compute next aligned address as follows: - // nextAddr = curAddr + size + padding = k*alignment // Alignment requirement - // => padding = k*alignment - curAddr - size - // => padding mod alignment = (-size) mod alignment // k*alignment and curAddr are 0 mod alignment. - // => padding = (-size) mod alignment // Because padding < alignment - final BigInteger memObjSize = BigInteger.valueOf(memObj.getKnownSize()); - final BigInteger padding = memObjSize.negate().mod(alignment); - nextAddr = nextAddr.add(memObjSize).add(padding); - } - - return memObj2Addr; + return encodeMemoryLayout(context.getTask().getProgram().getMemory()); } - private BooleanFormula encodeDynamicMemoryLayout(Memory memory) { + private BooleanFormula encodeMemoryLayout(Memory memory) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); final EncodingHelper helper = new EncodingHelper(context.getFormulaManager()); final List enc = new ArrayList<>(); @@ -369,9 +312,9 @@ private BooleanFormula encodeDynamicMemoryLayout(Memory memory) { 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))) + bmgr.ifThenElse(context.execution(cur.getAllocationSite()), + context.encodeExpressionAt(cur.size(), cur.getAllocationSite()), + helper.value(BigInteger.ZERO, helper.typeOf(size))) ) ); } @@ -397,6 +340,8 @@ private BooleanFormula encodeDynamicMemoryLayout(Memory memory) { return bmgr.and(enc); } + // ====================================== Data flow ====================================== + /** * @return * Describes that for each pair of events, if the reader uses the result of the writer, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java index a3c4fbfe60..7b2b66d33b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java @@ -37,7 +37,7 @@ public final class Alloc extends AbstractEvent implements RegReader, RegWriter { public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation, boolean doesZeroOutMemory) { - Preconditions.checkArgument(resultRegister.getType() == TypeFactory.getInstance().getArchType()); + Preconditions.checkArgument(resultRegister.getType() == TypeFactory.getInstance().getPointerType()); Preconditions.checkArgument(arraySize.getType() instanceof IntegerType); this.resultRegister = resultRegister; this.arraySize = arraySize; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java index 9df50dff65..f32e2d0ed8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java @@ -1,8 +1,11 @@ package com.dat3m.dartagnan.program.memory; import com.dat3m.dartagnan.exception.MalformedProgramException; +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.integers.IntLiteral; +import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.event.core.Alloc; import com.google.common.base.Preconditions; @@ -14,13 +17,15 @@ public class Memory { private final ArrayList objects = new ArrayList<>(); private final Type ptrType = TypeFactory.getInstance().getPointerType(); + private final IntegerType archType = TypeFactory.getInstance().getArchType(); private int nextIndex = 1; // Generates a new, statically allocated memory object. public MemoryObject allocate(int size) { Preconditions.checkArgument(size > 0, "Illegal allocation. Size must be positive"); - final MemoryObject memoryObject = new MemoryObject(nextIndex++, size, null, ptrType); + final Expression sizeExpr = ExpressionFactory.getInstance().makeValue(size, archType); + final MemoryObject memoryObject = new MemoryObject(nextIndex++, sizeExpr, null, ptrType); objects.add(memoryObject); return memoryObject; } @@ -35,7 +40,8 @@ public MemoryObject allocate(Alloc allocationSite) { public VirtualMemoryObject allocateVirtual(int size, boolean generic, VirtualMemoryObject alias) { Preconditions.checkArgument(size > 0, "Illegal allocation. Size must be positive"); - final VirtualMemoryObject address = new VirtualMemoryObject(nextIndex++, size, generic, alias, ptrType); + final Expression sizeExpr = ExpressionFactory.getInstance().makeValue(size, archType); + final VirtualMemoryObject address = new VirtualMemoryObject(nextIndex++, sizeExpr, generic, alias, ptrType); objects.add(address); return address; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java index c2f9a320c1..08b57b4050 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java @@ -1,6 +1,9 @@ package com.dat3m.dartagnan.program.memory; -import com.dat3m.dartagnan.expression.*; +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionKind; +import com.dat3m.dartagnan.expression.ExpressionVisitor; +import com.dat3m.dartagnan.expression.Type; import com.dat3m.dartagnan.expression.base.LeafExpressionBase; import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.misc.ConstructExpr; @@ -24,7 +27,6 @@ public class MemoryObject extends LeafExpressionBase { // TODO: (TH) I think is mostly useless. // Its only benefit is that we can have different memory objects with the same name (but why would we?) private final int id; - // TODO: Generalize to Expression private final Expression size; private final Alloc allocationSite; @@ -35,18 +37,15 @@ public class MemoryObject extends LeafExpressionBase { MemoryObject(int id, Expression size, Alloc allocationSite, Type ptrType) { super(ptrType); + final TypeFactory types = TypeFactory.getInstance(); + Preconditions.checkArgument(size instanceof IntegerType, "Size %s must be of integer type.", size); + Preconditions.checkArgument(types.getMemorySizeInBytes(size.getType()) == types.getMemorySizeInBytes(ptrType), + "Size expression %s should be of a type whose size matches the pointer type %s.", size, ptrType); this.id = id; this.size = size; this.allocationSite = allocationSite; } - MemoryObject(int id, int size, Alloc allocationSite, Type ptrType) { - super(ptrType); - this.id = id; - this.size = ExpressionFactory.getInstance().makeValue(size, TypeFactory.getInstance().getArchType()); - this.allocationSite = allocationSite; - } - public boolean hasName() { return name != null; } public String getName() { return name; } public void setName(String name) { this.name = name; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java index 0f343d03cd..19f6b70eaf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.program.memory; +import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.Type; import java.util.Objects; @@ -15,7 +16,7 @@ public class VirtualMemoryObject extends MemoryObject { // the generic address of this virtual address private final VirtualMemoryObject genericAddress; - VirtualMemoryObject(int index, int size, boolean generic, VirtualMemoryObject alias, Type ptrType) { + VirtualMemoryObject(int index, Expression size, boolean generic, VirtualMemoryObject alias, Type ptrType) { super(index, size, null, ptrType); checkArgument(generic || alias != null, "Non-generic virtualMemoryObject must have generic address it alias target"); From a13bdf98f88e973d71fb962f2818dc138b932f81 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 10 Oct 2024 15:26:16 +0200 Subject: [PATCH 11/14] Fixed wrong check. Added alignment property to MemoryObject --- .../dartagnan/encoding/ProgramEncoder.java | 9 ++++---- .../dartagnan/program/memory/Memory.java | 20 ++++++------------ .../program/memory/MemoryObject.java | 21 ++++++++++++------- .../program/memory/VirtualMemoryObject.java | 4 ++-- 4 files changed, 27 insertions(+), 27 deletions(-) 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 c1db0641e3..cdbd0d24a1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -306,10 +306,12 @@ private BooleanFormula encodeMemoryLayout(Memory memory) { final MemoryObject cur = memoryObjects.get(i); final Formula addr = context.address(cur); final Formula size = context.size(cur); + final Formula alignment; - // Encode size (non-allocated objects are 0-sized) + // Encode size (non-allocated objects are 0-sized) & compute alignment if (cur.isStaticallyAllocated()) { enc.add(helper.equals(size, context.encodeFinalExpression(cur.size()))); + alignment = context.encodeFinalExpression(cur.alignment()); } else { enc.add(helper.equals(size, bmgr.ifThenElse(context.execution(cur.getAllocationSite()), @@ -317,11 +319,10 @@ private BooleanFormula encodeMemoryLayout(Memory memory) { helper.value(BigInteger.ZERO, helper.typeOf(size))) ) ); + alignment = context.encodeExpressionAt(cur.alignment(), cur.getAllocationSite()); } - // 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)); + // Encode address (we even give non-allocated objects a proper, well-aligned address) final MemoryObject prev = i > 0 ? memoryObjects.get(i - 1) : null; if (prev == null) { // First object is placed at alignment diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java index f32e2d0ed8..4316e174a5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java @@ -1,10 +1,8 @@ package com.dat3m.dartagnan.program.memory; -import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.Type; -import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.event.core.Alloc; @@ -18,6 +16,7 @@ public class Memory { private final ArrayList objects = new ArrayList<>(); private final Type ptrType = TypeFactory.getInstance().getPointerType(); private final IntegerType archType = TypeFactory.getInstance().getArchType(); + private final Expression defaultAlignment = ExpressionFactory.getInstance().makeValue(8, archType); private int nextIndex = 1; @@ -25,7 +24,7 @@ public class Memory { public MemoryObject allocate(int size) { Preconditions.checkArgument(size > 0, "Illegal allocation. Size must be positive"); final Expression sizeExpr = ExpressionFactory.getInstance().makeValue(size, archType); - final MemoryObject memoryObject = new MemoryObject(nextIndex++, sizeExpr, null, ptrType); + final MemoryObject memoryObject = new MemoryObject(nextIndex++, sizeExpr, defaultAlignment, null, ptrType); objects.add(memoryObject); return memoryObject; } @@ -33,7 +32,8 @@ public MemoryObject allocate(int size) { // Generates a new, dynamically allocated memory object. public MemoryObject allocate(Alloc allocationSite) { Preconditions.checkNotNull(allocationSite); - final MemoryObject memoryObject = new MemoryObject(nextIndex++, allocationSite.getAllocationSize(), allocationSite, ptrType); + final MemoryObject memoryObject = new MemoryObject(nextIndex++, allocationSite.getAllocationSize(), + defaultAlignment, allocationSite, ptrType); objects.add(memoryObject); return memoryObject; } @@ -41,7 +41,8 @@ public MemoryObject allocate(Alloc allocationSite) { public VirtualMemoryObject allocateVirtual(int size, boolean generic, VirtualMemoryObject alias) { Preconditions.checkArgument(size > 0, "Illegal allocation. Size must be positive"); final Expression sizeExpr = ExpressionFactory.getInstance().makeValue(size, archType); - final VirtualMemoryObject address = new VirtualMemoryObject(nextIndex++, sizeExpr, generic, alias, ptrType); + final VirtualMemoryObject address = new VirtualMemoryObject(nextIndex++, sizeExpr, defaultAlignment, + generic, alias, ptrType); objects.add(address); return address; } @@ -59,13 +60,4 @@ public ImmutableSet getObjects() { return ImmutableSet.copyOf(objects); } - private int getStaticAllocSize(Alloc alloc) { - try { - return ((IntLiteral)alloc.getAllocationSize()).getValueAsInt(); - } catch (Exception e) { - final String error = String.format("Variable-sized alloc '%s' is not supported", alloc); - throw new MalformedProgramException(error); - } - } - } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java index 08b57b4050..184873a899 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java @@ -28,6 +28,7 @@ public class MemoryObject extends LeafExpressionBase { // Its only benefit is that we can have different memory objects with the same name (but why would we?) private final int id; private final Expression size; + private final Expression alignment; private final Alloc allocationSite; private String name = null; @@ -35,13 +36,16 @@ public class MemoryObject extends LeafExpressionBase { private final Map initialValues = new TreeMap<>(); - MemoryObject(int id, Expression size, Alloc allocationSite, Type ptrType) { + MemoryObject(int id, Expression size, Expression alignment, Alloc allocationSite, Type ptrType) { super(ptrType); final TypeFactory types = TypeFactory.getInstance(); - Preconditions.checkArgument(size instanceof IntegerType, "Size %s must be of integer type.", size); + Preconditions.checkArgument(size.getType() instanceof IntegerType, "Size %s must be of integer type.", size); + Preconditions.checkArgument(alignment.getType() == size.getType(), + "Size %s and alignment %s must have matching types.", size, alignment); Preconditions.checkArgument(types.getMemorySizeInBytes(size.getType()) == types.getMemorySizeInBytes(ptrType), "Size expression %s should be of a type whose size matches the pointer type %s.", size, ptrType); this.id = id; + this.alignment = alignment; this.size = size; this.allocationSite = allocationSite; } @@ -58,16 +62,19 @@ public class MemoryObject extends LeafExpressionBase { public void setIsThreadLocal(boolean value) { this.isThreadLocal = value;} public Expression size() { return size; } - - public boolean hasKnownSize() { - return size instanceof IntLiteral; - } - + public boolean hasKnownSize() { return size instanceof IntLiteral; } public int getKnownSize() { Preconditions.checkState(hasKnownSize()); return ((IntLiteral)size).getValueAsInt(); } + public Expression alignment() { return alignment; } + public boolean hasKnownAlignment() { return alignment instanceof IntLiteral; } + public int getKnownAlignment() { + Preconditions.checkState(hasKnownAlignment()); + return ((IntLiteral)alignment).getValueAsInt(); + } + public boolean isInRange(int offset) { return hasKnownSize() && offset >= 0 && offset < getKnownSize(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java index 19f6b70eaf..66b2ea8c7f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/VirtualMemoryObject.java @@ -16,8 +16,8 @@ public class VirtualMemoryObject extends MemoryObject { // the generic address of this virtual address private final VirtualMemoryObject genericAddress; - VirtualMemoryObject(int index, Expression size, boolean generic, VirtualMemoryObject alias, Type ptrType) { - super(index, size, null, ptrType); + VirtualMemoryObject(int index, Expression size, Expression alignment, boolean generic, VirtualMemoryObject alias, Type ptrType) { + super(index, size, alignment, null, ptrType); checkArgument(generic || alias != null, "Non-generic virtualMemoryObject must have generic address it alias target"); if (alias == null) { From 19d638964af28d2c34bd2b82e6e4076265390214 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Thu, 10 Oct 2024 16:48:56 +0200 Subject: [PATCH 12/14] Added alignment to Alloc (even variable-sized!) and added support for aligned_alloc intrinsic Added a test for non-deterministic alignment Reformatting --- .../miscellaneous/nondet_aligned_alloc.c | 24 ++ .../dartagnan/encoding/ProgramEncoder.java | 9 +- .../dartagnan/program/event/EventFactory.java | 14 +- .../dartagnan/program/event/core/Alloc.java | 15 +- .../dartagnan/program/memory/Memory.java | 2 +- .../program/processing/Intrinsics.java | 11 + .../verification/solving/AssumeSolver.java | 25 +- .../dat3m/dartagnan/c/MiscellaneousTest.java | 1 + .../miscellaneous/nondet_aligned_alloc.ll | 215 ++++++++++++++++++ 9 files changed, 295 insertions(+), 21 deletions(-) create mode 100644 benchmarks/miscellaneous/nondet_aligned_alloc.c create mode 100644 dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll diff --git a/benchmarks/miscellaneous/nondet_aligned_alloc.c b/benchmarks/miscellaneous/nondet_aligned_alloc.c new file mode 100644 index 0000000000..2145e0c5bb --- /dev/null +++ b/benchmarks/miscellaneous/nondet_aligned_alloc.c @@ -0,0 +1,24 @@ +#include +#include +#include +#include + +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(42 * 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 (array != array_2); + assert (((size_t)array) % 8 == 0); // Default alignment + assert (((size_t)array_2) % align == 0); // Custom alignment +} 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 cdbd0d24a1..917cd0ec20 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -308,18 +308,23 @@ private BooleanFormula encodeMemoryLayout(Memory memory) { final Formula size = context.size(cur); final Formula alignment; - // Encode size (non-allocated objects are 0-sized) & compute alignment + // Encode size & compute alignment if (cur.isStaticallyAllocated()) { enc.add(helper.equals(size, context.encodeFinalExpression(cur.size()))); alignment = context.encodeFinalExpression(cur.alignment()); } else { + // Non-allocated objects get size 0 enc.add(helper.equals(size, bmgr.ifThenElse(context.execution(cur.getAllocationSite()), context.encodeExpressionAt(cur.size(), cur.getAllocationSite()), helper.value(BigInteger.ZERO, helper.typeOf(size))) ) ); - alignment = context.encodeExpressionAt(cur.alignment(), cur.getAllocationSite()); + // Non-allocated objects with variable alignment get alignment 1 + alignment = cur.hasKnownAlignment() ? context.encodeExpressionAt(cur.alignment(), cur.getAllocationSite()) + : bmgr.ifThenElse(context.execution(cur.getAllocationSite()), + context.encodeExpressionAt(cur.alignment(), cur.getAllocationSite()), + helper.value(BigInteger.ONE, helper.typeOf(size))); } // Encode address (we even give non-allocated objects a proper, well-aligned address) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index 8b1f720f83..9a23566d9b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -50,6 +50,7 @@ public class EventFactory { private static final ExpressionFactory expressions = ExpressionFactory.getInstance(); + private static final TypeFactory types = TypeFactory.getInstance(); // Static class private EventFactory() { @@ -93,8 +94,15 @@ public static List eventSequence(Object... events) { public static Alloc newAlloc(Register register, Type allocType, Expression arraySize, boolean isHeapAlloc, boolean doesZeroOutMemory) { - arraySize = expressions.makeCast(arraySize, TypeFactory.getInstance().getArchType(), false); - return new Alloc(register, allocType, arraySize, isHeapAlloc, doesZeroOutMemory); + final Expression defaultAlignment = expressions.makeValue(8, types.getArchType()); + return newAlignedAlloc(register, allocType, arraySize, defaultAlignment, isHeapAlloc, doesZeroOutMemory); + } + + public static Alloc newAlignedAlloc(Register register, Type allocType, Expression arraySize, Expression alignment, + boolean isHeapAlloc, boolean doesZeroOutMemory) { + arraySize = expressions.makeCast(arraySize, types.getArchType(), false); + alignment = expressions.makeCast(alignment, types.getArchType(), false); + return new Alloc(register, allocType, arraySize, alignment, isHeapAlloc, doesZeroOutMemory); } public static Load newLoad(Register register, Expression address) { @@ -320,7 +328,7 @@ private Pthread() { public static InitLock newInitLock(String name, Expression address, Expression ignoreAttributes) { //TODO store attributes inside mutex object - return new InitLock(name, address, expressions.makeZero(TypeFactory.getInstance().getArchType())); + return new InitLock(name, address, expressions.makeZero(types.getArchType())); } public static Lock newLock(String name, Expression address) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java index 7b2b66d33b..4ada179a8e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java @@ -29,18 +29,21 @@ public final class Alloc extends AbstractEvent implements RegReader, RegWriter { private Register resultRegister; private Type allocationType; private Expression arraySize; + private Expression alignment; private boolean isHeapAllocation; private boolean doesZeroOutMemory; // This will be set at the end of the program processing. private transient MemoryObject allocatedObject; - public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation, + public Alloc(Register resultRegister, Type allocType, Expression arraySize, Expression alignment, boolean isHeapAllocation, boolean doesZeroOutMemory) { Preconditions.checkArgument(resultRegister.getType() == TypeFactory.getInstance().getPointerType()); Preconditions.checkArgument(arraySize.getType() instanceof IntegerType); + Preconditions.checkArgument(alignment.getType() instanceof IntegerType); this.resultRegister = resultRegister; this.arraySize = arraySize; + this.alignment = alignment; this.allocationType = allocType; this.isHeapAllocation = isHeapAllocation; this.doesZeroOutMemory = doesZeroOutMemory; @@ -53,6 +56,7 @@ private Alloc(Alloc other) { this.resultRegister = other.resultRegister; this.allocationType = other.allocationType; this.arraySize = other.arraySize; + this.alignment = other.alignment; this.isHeapAllocation = other.isHeapAllocation; this.doesZeroOutMemory = other.doesZeroOutMemory; } @@ -64,6 +68,7 @@ private Alloc(Alloc other) { public Type getAllocationType() { return allocationType; } public Expression getArraySize() { return arraySize; } + public Expression getAlignment() { return alignment; } public boolean isHeapAllocation() { return isHeapAllocation; } public boolean doesZeroOutMemory() { return doesZeroOutMemory; } @@ -100,18 +105,20 @@ public Expression getAllocationSize() { @Override public Set getRegisterReads() { - return Register.collectRegisterReads(arraySize, Register.UsageType.DATA, new HashSet<>()); + final Set reads = Register.collectRegisterReads(alignment, Register.UsageType.DATA, new HashSet<>()); + return Register.collectRegisterReads(arraySize, Register.UsageType.DATA, reads); } @Override public void transformExpressions(ExpressionVisitor exprTransformer) { arraySize = arraySize.accept(exprTransformer); + alignment = alignment.accept(exprTransformer); } @Override protected String defaultString() { - return String.format("%s <- %salloc(%s, %s)", - resultRegister, isHeapAllocation ? "heap" : "stack", allocationType, arraySize); + return String.format("%s <- %salloc(type=%s, size=%s, align=%s)", + resultRegister, isHeapAllocation ? "heap" : "stack", allocationType, arraySize, alignment); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java index 4316e174a5..f891b25eed 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Memory.java @@ -33,7 +33,7 @@ public MemoryObject allocate(int size) { public MemoryObject allocate(Alloc allocationSite) { Preconditions.checkNotNull(allocationSite); final MemoryObject memoryObject = new MemoryObject(nextIndex++, allocationSite.getAllocationSize(), - defaultAlignment, allocationSite, ptrType); + allocationSite.getAlignment(), allocationSite, ptrType); objects.add(memoryObject); return memoryObject; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index b81f2a43e5..f4f9452262 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -214,6 +214,7 @@ public enum Info { STD_MEMCMP("memcmp", false, true, true, false, Intrinsics::inlineMemCmp), STD_MALLOC("malloc", false, false, true, true, Intrinsics::inlineMalloc), STD_CALLOC("calloc", false, false, true, true, Intrinsics::inlineCalloc), + STD_ALIGNED_ALLOC("aligned_alloc", false, false, true, true, Intrinsics::inlineAlignedAlloc), STD_FREE("free", true, false, true, true, Intrinsics::inlineAsZero),//TODO support free STD_ASSERT(List.of("__assert_fail", "__assert_rtn"), false, false, false, true, Intrinsics::inlineUserAssert), STD_EXIT("exit", false, false, false, true, Intrinsics::inlineExit), @@ -894,6 +895,16 @@ private List inlineCalloc(FunctionCall call) { ); } + private List inlineAlignedAlloc(FunctionCall call) { + final Register resultRegister = getResultRegisterAndCheckArguments(2, call); + final Type allocType = types.getByteType(); + final Expression alignment = call.getArguments().get(0); + final Expression totalSize = call.getArguments().get(1); + return List.of( + EventFactory.newAlignedAlloc(resultRegister, allocType, totalSize, alignment, true, false) + ); + } + private List inlineAssert(FunctionCall call, AssertionType skip, String errorMsg) { if(notToInline.contains(skip)) { return List.of(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java index a8108aa9f1..d1682665ca 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java @@ -10,7 +10,10 @@ import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.java_smt.api.*; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; import static com.dat3m.dartagnan.utils.Result.FAIL; import static com.dat3m.dartagnan.utils.Result.PASS; @@ -72,24 +75,24 @@ private void run() throws InterruptedException, SolverException, InvalidConfigur BooleanFormula assumedSpec = bmgr.implication(assumptionLiteral, propertyEncoding); prover.writeComment("Property encoding"); prover.addConstraint(assumedSpec); - + logger.info("Starting first solver.check()"); - if(prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { + if (prover.isUnsatWithAssumptions(singletonList(assumptionLiteral))) { prover.writeComment("Bound encoding"); - prover.addConstraint(propertyEncoder.encodeBoundEventExec()); + prover.addConstraint(propertyEncoder.encodeBoundEventExec()); logger.info("Starting second solver.check()"); - res = prover.isUnsat()? PASS : Result.UNKNOWN; + res = prover.isUnsat() ? PASS : Result.UNKNOWN; } else { res = FAIL; saveFlaggedPairsOutput(memoryModel, wmmEncoder, prover, context, task.getProgram()); } - if(logger.isDebugEnabled()) { - String smtStatistics = "\n ===== SMT Statistics ===== \n"; - for(String key : prover.getStatistics().keySet()) { - smtStatistics += String.format("\t%s -> %s\n", key, prover.getStatistics().get(key)); - } - logger.debug(smtStatistics); + if (logger.isDebugEnabled()) { + String smtStatistics = "\n ===== SMT Statistics ===== \n"; + for (String key : prover.getStatistics().keySet()) { + smtStatistics += String.format("\t%s -> %s\n", key, prover.getStatistics().get(key)); + } + logger.debug(smtStatistics); } // For Safety specs, we have SAT=FAIL, but for reachability specs, we have SAT=PASS diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java index 13a6da97d7..10680a4d37 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java @@ -94,6 +94,7 @@ public static Iterable data() throws IOException { {"jumpIntoLoop", IMM, PASS, 11}, {"nondet_alloc", IMM, FAIL, 1}, {"nondet_alloc_2", IMM, PASS, 1}, + {"nondet_aligned_alloc", IMM, PASS, 1}, }); } diff --git a/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll b/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll new file mode 100644 index 0000000000..129eb47edc --- /dev/null +++ b/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll @@ -0,0 +1,215 @@ +; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_aligned_alloc.c' +source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_aligned_alloc.c" +target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128" +target triple = "arm64-apple-macosx14.0.0" + +@__func__.main = private unnamed_addr constant [5 x i8] c"main\00", align 1 +@.str = private unnamed_addr constant [23 x i8] c"nondet_aligned_alloc.c\00", align 1 +@.str.1 = private unnamed_addr constant [17 x i8] c"array != array_2\00", align 1 +@.str.2 = private unnamed_addr constant [25 x i8] c"((size_t)array) % 8 == 0\00", align 1 +@.str.3 = private unnamed_addr constant [31 x i8] c"((size_t)array_2) % align == 0\00", align 1 + +; Function Attrs: noinline nounwind ssp uwtable +define i32 @main() #0 !dbg !19 { + %1 = alloca i32, align 4 + %2 = alloca i32, align 4 + %3 = alloca i32, align 4 + %4 = alloca i64, align 8 + %5 = alloca i64, align 8 + %6 = alloca i32*, align 8 + %7 = alloca i32*, align 8 + store i32 0, i32* %1, align 4 + call void @llvm.dbg.declare(metadata i32* %2, metadata !25, metadata !DIExpression()), !dbg !26 + %8 = call i32 @__VERIFIER_nondet_int(), !dbg !27 + store i32 %8, i32* %2, align 4, !dbg !26 + call void @llvm.dbg.declare(metadata i32* %3, metadata !28, metadata !DIExpression()), !dbg !29 + %9 = call i32 @__VERIFIER_nondet_int(), !dbg !30 + store i32 %9, i32* %3, align 4, !dbg !29 + %10 = load i32, i32* %2, align 4, !dbg !31 + %11 = icmp sgt i32 %10, 0, !dbg !32 + %12 = zext i1 %11 to i32, !dbg !32 + call void @__VERIFIER_assume(i32 noundef %12), !dbg !33 + %13 = load i32, i32* %3, align 4, !dbg !34 + %14 = icmp sgt i32 %13, 0, !dbg !35 + %15 = zext i1 %14 to i32, !dbg !35 + call void @__VERIFIER_assume(i32 noundef %15), !dbg !36 + call void @llvm.dbg.declare(metadata i64* %4, metadata !37, metadata !DIExpression()), !dbg !38 + %16 = load i32, i32* %2, align 4, !dbg !39 + %17 = sext i32 %16 to i64, !dbg !40 + store i64 %17, i64* %4, align 8, !dbg !38 + call void @llvm.dbg.declare(metadata i64* %5, metadata !41, metadata !DIExpression()), !dbg !42 + %18 = load i32, i32* %3, align 4, !dbg !43 + %19 = sext i32 %18 to i64, !dbg !44 + store i64 %19, i64* %5, align 8, !dbg !42 + call void @llvm.dbg.declare(metadata i32** %6, metadata !45, metadata !DIExpression()), !dbg !47 + %20 = call i8* @malloc(i64 noundef 168) #7, !dbg !48 + %21 = bitcast i8* %20 to i32*, !dbg !48 + store i32* %21, i32** %6, align 8, !dbg !47 + call void @llvm.dbg.declare(metadata i32** %7, metadata !49, metadata !DIExpression()), !dbg !50 + %22 = load i64, i64* %5, align 8, !dbg !51 + %23 = load i64, i64* %4, align 8, !dbg !52 + %24 = mul i64 %23, 4, !dbg !53 + %25 = call i8* @aligned_alloc(i64 noundef %22, i64 noundef %24) #8, !dbg !54 + call void @llvm.assume(i1 true) [ "align"(i8* %25, i64 %22) ], !dbg !54 + %26 = bitcast i8* %25 to i32*, !dbg !54 + store i32* %26, i32** %7, align 8, !dbg !50 + %27 = load i32*, i32** %6, align 8, !dbg !55 + %28 = load i32*, i32** %7, align 8, !dbg !55 + %29 = icmp ne i32* %27, %28, !dbg !55 + %30 = xor i1 %29, true, !dbg !55 + %31 = zext i1 %30 to i32, !dbg !55 + %32 = sext i32 %31 to i64, !dbg !55 + %33 = icmp ne i64 %32, 0, !dbg !55 + br i1 %33, label %34, label %36, !dbg !55 + +34: ; preds = %0 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 20, i8* noundef getelementptr inbounds ([17 x i8], [17 x i8]* @.str.1, i64 0, i64 0)) #9, !dbg !55 + unreachable, !dbg !55 + +35: ; No predecessors! + br label %37, !dbg !55 + +36: ; preds = %0 + br label %37, !dbg !55 + +37: ; preds = %36, %35 + %38 = load i32*, i32** %6, align 8, !dbg !56 + %39 = ptrtoint i32* %38 to i64, !dbg !56 + %40 = urem i64 %39, 8, !dbg !56 + %41 = icmp eq i64 %40, 0, !dbg !56 + %42 = xor i1 %41, true, !dbg !56 + %43 = zext i1 %42 to i32, !dbg !56 + %44 = sext i32 %43 to i64, !dbg !56 + %45 = icmp ne i64 %44, 0, !dbg !56 + br i1 %45, label %46, label %48, !dbg !56 + +46: ; preds = %37 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 21, i8* noundef getelementptr inbounds ([25 x i8], [25 x i8]* @.str.2, i64 0, i64 0)) #9, !dbg !56 + unreachable, !dbg !56 + +47: ; No predecessors! + br label %49, !dbg !56 + +48: ; preds = %37 + br label %49, !dbg !56 + +49: ; preds = %48, %47 + %50 = load i32*, i32** %7, align 8, !dbg !57 + %51 = ptrtoint i32* %50 to i64, !dbg !57 + %52 = load i64, i64* %5, align 8, !dbg !57 + %53 = urem i64 %51, %52, !dbg !57 + %54 = icmp eq i64 %53, 0, !dbg !57 + %55 = xor i1 %54, true, !dbg !57 + %56 = zext i1 %55 to i32, !dbg !57 + %57 = sext i32 %56 to i64, !dbg !57 + %58 = icmp ne i64 %57, 0, !dbg !57 + br i1 %58, label %59, label %61, !dbg !57 + +59: ; preds = %49 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 22, i8* noundef getelementptr inbounds ([31 x i8], [31 x i8]* @.str.3, i64 0, i64 0)) #9, !dbg !57 + unreachable, !dbg !57 + +60: ; No predecessors! + br label %62, !dbg !57 + +61: ; preds = %49 + br label %62, !dbg !57 + +62: ; preds = %61, %60 + %63 = load i32, i32* %1, align 4, !dbg !58 + ret i32 %63, !dbg !58 +} + +; Function Attrs: nofree nosync nounwind readnone speculatable willreturn +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +declare i32 @__VERIFIER_nondet_int() #2 + +declare void @__VERIFIER_assume(i32 noundef) #2 + +; Function Attrs: allocsize(0) +declare i8* @malloc(i64 noundef) #3 + +; Function Attrs: allocsize(1) +declare i8* @aligned_alloc(i64 noundef, i64 noundef) #4 + +; Function Attrs: inaccessiblememonly nofree nosync nounwind willreturn +declare void @llvm.assume(i1 noundef) #5 + +; Function Attrs: cold noreturn +declare void @__assert_rtn(i8* noundef, i8* noundef, i32 noundef, i8* noundef) #6 + +attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #1 = { nofree nosync nounwind readnone speculatable willreturn } +attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #3 = { allocsize(0) "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #4 = { allocsize(1) "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #5 = { inaccessiblememonly nofree nosync nounwind willreturn } +attributes #6 = { cold noreturn "disable-tail-calls"="true" "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" } +attributes #7 = { allocsize(0) } +attributes #8 = { allocsize(1) } +attributes #9 = { cold noreturn } + +!llvm.dbg.cu = !{!0} +!llvm.module.flags = !{!8, !9, !10, !11, !12, !13, !14, !15, !16, !17} +!llvm.ident = !{!18} + +!0 = distinct !DICompileUnit(language: DW_LANG_C99, file: !1, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !2, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk") +!1 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/miscellaneous/nondet_aligned_alloc.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!2 = !{!3} +!3 = !DIDerivedType(tag: DW_TAG_typedef, name: "size_t", file: !4, line: 31, baseType: !5) +!4 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_types/_size_t.h", directory: "") +!5 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_size_t", file: !6, line: 70, baseType: !7) +!6 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/arm/_types.h", directory: "") +!7 = !DIBasicType(name: "unsigned long", size: 64, encoding: DW_ATE_unsigned) +!8 = !{i32 7, !"Dwarf Version", i32 4} +!9 = !{i32 2, !"Debug Info Version", i32 3} +!10 = !{i32 1, !"wchar_size", i32 4} +!11 = !{i32 1, !"branch-target-enforcement", i32 0} +!12 = !{i32 1, !"sign-return-address", i32 0} +!13 = !{i32 1, !"sign-return-address-all", i32 0} +!14 = !{i32 1, !"sign-return-address-with-bkey", i32 0} +!15 = !{i32 7, !"PIC Level", i32 2} +!16 = !{i32 7, !"uwtable", i32 1} +!17 = !{i32 7, !"frame-pointer", i32 1} +!18 = !{!"Homebrew clang version 14.0.6"} +!19 = distinct !DISubprogram(name: "main", scope: !20, file: !20, line: 6, type: !21, scopeLine: 7, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !24) +!20 = !DIFile(filename: "benchmarks/miscellaneous/nondet_aligned_alloc.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!21 = !DISubroutineType(types: !22) +!22 = !{!23} +!23 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!24 = !{} +!25 = !DILocalVariable(name: "size_int", scope: !19, file: !20, line: 8, type: !23) +!26 = !DILocation(line: 8, column: 9, scope: !19) +!27 = !DILocation(line: 8, column: 20, scope: !19) +!28 = !DILocalVariable(name: "align_int", scope: !19, file: !20, line: 9, type: !23) +!29 = !DILocation(line: 9, column: 9, scope: !19) +!30 = !DILocation(line: 9, column: 21, scope: !19) +!31 = !DILocation(line: 10, column: 23, scope: !19) +!32 = !DILocation(line: 10, column: 32, scope: !19) +!33 = !DILocation(line: 10, column: 5, scope: !19) +!34 = !DILocation(line: 11, column: 23, scope: !19) +!35 = !DILocation(line: 11, column: 33, scope: !19) +!36 = !DILocation(line: 11, column: 5, scope: !19) +!37 = !DILocalVariable(name: "size", scope: !19, file: !20, line: 12, type: !3) +!38 = !DILocation(line: 12, column: 12, scope: !19) +!39 = !DILocation(line: 12, column: 27, scope: !19) +!40 = !DILocation(line: 12, column: 19, scope: !19) +!41 = !DILocalVariable(name: "align", scope: !19, file: !20, line: 13, type: !3) +!42 = !DILocation(line: 13, column: 12, scope: !19) +!43 = !DILocation(line: 13, column: 28, scope: !19) +!44 = !DILocation(line: 13, column: 20, scope: !19) +!45 = !DILocalVariable(name: "array", scope: !19, file: !20, line: 14, type: !46) +!46 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !23, size: 64) +!47 = !DILocation(line: 14, column: 10, scope: !19) +!48 = !DILocation(line: 14, column: 18, scope: !19) +!49 = !DILocalVariable(name: "array_2", scope: !19, file: !20, line: 15, type: !46) +!50 = !DILocation(line: 15, column: 10, scope: !19) +!51 = !DILocation(line: 15, column: 34, scope: !19) +!52 = !DILocation(line: 15, column: 41, scope: !19) +!53 = !DILocation(line: 15, column: 46, scope: !19) +!54 = !DILocation(line: 15, column: 20, scope: !19) +!55 = !DILocation(line: 20, column: 5, scope: !19) +!56 = !DILocation(line: 21, column: 5, scope: !19) +!57 = !DILocation(line: 22, column: 5, scope: !19) +!58 = !DILocation(line: 23, column: 1, scope: !19) From eca6374ab74011ce5800c29963ffa71a50b8f95f Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 11 Oct 2024 10:34:21 +0200 Subject: [PATCH 13/14] Minor fixes --- .../java/com/dat3m/dartagnan/encoding/EncodingHelper.java | 6 ++++-- .../program/analysis/alias/AndersenAliasAnalysis.java | 1 - 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java index a5f78bde04..6772b52575 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingHelper.java @@ -84,15 +84,17 @@ public Formula subtract(Formula left, Formula 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 is positive which is the most usual case. 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); + return fmgr.getBitvectorFormulaManager().smodulo(bvLeft, bvRight); } throw new UnsupportedOperationException("Mismatching types: " + left + " and " + right); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java index 545dc9db88..3aa76b80fe 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java @@ -302,7 +302,6 @@ private static final class Location { final int offset; Location(MemoryObject b, int o) { - b.isInRange(o); Preconditions.checkArgument(b.isInRange(o), "Array out of bounds"); base = b; offset = o; From 86072e7370127facdd1167133648a8ded98f4dfc Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 11 Oct 2024 18:13:59 +0200 Subject: [PATCH 14/14] Feedback --- .../miscellaneous/nondet_aligned_alloc.c | 6 +- .../dartagnan/encoding/ProgramEncoder.java | 2 +- .../miscellaneous/nondet_aligned_alloc.ll | 187 +++++++++--------- 3 files changed, 100 insertions(+), 95 deletions(-) diff --git a/benchmarks/miscellaneous/nondet_aligned_alloc.c b/benchmarks/miscellaneous/nondet_aligned_alloc.c index 2145e0c5bb..dd7c8a1989 100644 --- a/benchmarks/miscellaneous/nondet_aligned_alloc.c +++ b/benchmarks/miscellaneous/nondet_aligned_alloc.c @@ -3,6 +3,8 @@ #include #include +#define SIZE_1 42 + int main() { int size_int = __VERIFIER_nondet_int(); @@ -11,14 +13,14 @@ int main() __VERIFIER_assume(align_int > 0); size_t size = (size_t)size_int; size_t align = (size_t)align_int; - int *array = malloc(42 * sizeof(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 (array != array_2); + 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 } 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 917cd0ec20..96d14f501e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -313,7 +313,7 @@ private BooleanFormula encodeMemoryLayout(Memory memory) { enc.add(helper.equals(size, context.encodeFinalExpression(cur.size()))); alignment = context.encodeFinalExpression(cur.alignment()); } else { - // Non-allocated objects get size 0 + // Non-allocated objects, i.e. objects whose Alloc event was not executed, get size 0 enc.add(helper.equals(size, bmgr.ifThenElse(context.execution(cur.getAllocationSite()), context.encodeExpressionAt(cur.size(), cur.getAllocationSite()), diff --git a/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll b/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll index 129eb47edc..cd91bc1f5a 100644 --- a/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll +++ b/dartagnan/src/test/resources/miscellaneous/nondet_aligned_alloc.ll @@ -5,7 +5,7 @@ target triple = "arm64-apple-macosx14.0.0" @__func__.main = private unnamed_addr constant [5 x i8] c"main\00", align 1 @.str = private unnamed_addr constant [23 x i8] c"nondet_aligned_alloc.c\00", align 1 -@.str.1 = private unnamed_addr constant [17 x i8] c"array != array_2\00", align 1 +@.str.1 = private unnamed_addr constant [56 x i8] c"(size_t)array_2 - (size_t)array >= SIZE_1 * sizeof(int)\00", align 1 @.str.2 = private unnamed_addr constant [25 x i8] c"((size_t)array) % 8 == 0\00", align 1 @.str.3 = private unnamed_addr constant [31 x i8] c"((size_t)array_2) % align == 0\00", align 1 @@ -53,71 +53,74 @@ define i32 @main() #0 !dbg !19 { call void @llvm.assume(i1 true) [ "align"(i8* %25, i64 %22) ], !dbg !54 %26 = bitcast i8* %25 to i32*, !dbg !54 store i32* %26, i32** %7, align 8, !dbg !50 - %27 = load i32*, i32** %6, align 8, !dbg !55 - %28 = load i32*, i32** %7, align 8, !dbg !55 - %29 = icmp ne i32* %27, %28, !dbg !55 - %30 = xor i1 %29, true, !dbg !55 - %31 = zext i1 %30 to i32, !dbg !55 - %32 = sext i32 %31 to i64, !dbg !55 - %33 = icmp ne i64 %32, 0, !dbg !55 - br i1 %33, label %34, label %36, !dbg !55 - -34: ; preds = %0 - call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 20, i8* noundef getelementptr inbounds ([17 x i8], [17 x i8]* @.str.1, i64 0, i64 0)) #9, !dbg !55 + %27 = load i32*, i32** %7, align 8, !dbg !55 + %28 = ptrtoint i32* %27 to i64, !dbg !55 + %29 = load i32*, i32** %6, align 8, !dbg !55 + %30 = ptrtoint i32* %29 to i64, !dbg !55 + %31 = sub i64 %28, %30, !dbg !55 + %32 = icmp uge i64 %31, 168, !dbg !55 + %33 = xor i1 %32, true, !dbg !55 + %34 = zext i1 %33 to i32, !dbg !55 + %35 = sext i32 %34 to i64, !dbg !55 + %36 = icmp ne i64 %35, 0, !dbg !55 + br i1 %36, label %37, label %39, !dbg !55 + +37: ; preds = %0 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 23, i8* noundef getelementptr inbounds ([56 x i8], [56 x i8]* @.str.1, i64 0, i64 0)) #9, !dbg !55 unreachable, !dbg !55 -35: ; No predecessors! - br label %37, !dbg !55 - -36: ; preds = %0 - br label %37, !dbg !55 - -37: ; preds = %36, %35 - %38 = load i32*, i32** %6, align 8, !dbg !56 - %39 = ptrtoint i32* %38 to i64, !dbg !56 - %40 = urem i64 %39, 8, !dbg !56 - %41 = icmp eq i64 %40, 0, !dbg !56 - %42 = xor i1 %41, true, !dbg !56 - %43 = zext i1 %42 to i32, !dbg !56 - %44 = sext i32 %43 to i64, !dbg !56 - %45 = icmp ne i64 %44, 0, !dbg !56 - br i1 %45, label %46, label %48, !dbg !56 - -46: ; preds = %37 - call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 21, i8* noundef getelementptr inbounds ([25 x i8], [25 x i8]* @.str.2, i64 0, i64 0)) #9, !dbg !56 +38: ; No predecessors! + br label %40, !dbg !55 + +39: ; preds = %0 + br label %40, !dbg !55 + +40: ; preds = %39, %38 + %41 = load i32*, i32** %6, align 8, !dbg !56 + %42 = ptrtoint i32* %41 to i64, !dbg !56 + %43 = urem i64 %42, 8, !dbg !56 + %44 = icmp eq i64 %43, 0, !dbg !56 + %45 = xor i1 %44, true, !dbg !56 + %46 = zext i1 %45 to i32, !dbg !56 + %47 = sext i32 %46 to i64, !dbg !56 + %48 = icmp ne i64 %47, 0, !dbg !56 + br i1 %48, label %49, label %51, !dbg !56 + +49: ; preds = %40 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 24, i8* noundef getelementptr inbounds ([25 x i8], [25 x i8]* @.str.2, i64 0, i64 0)) #9, !dbg !56 unreachable, !dbg !56 -47: ; No predecessors! - br label %49, !dbg !56 - -48: ; preds = %37 - br label %49, !dbg !56 - -49: ; preds = %48, %47 - %50 = load i32*, i32** %7, align 8, !dbg !57 - %51 = ptrtoint i32* %50 to i64, !dbg !57 - %52 = load i64, i64* %5, align 8, !dbg !57 - %53 = urem i64 %51, %52, !dbg !57 - %54 = icmp eq i64 %53, 0, !dbg !57 - %55 = xor i1 %54, true, !dbg !57 - %56 = zext i1 %55 to i32, !dbg !57 - %57 = sext i32 %56 to i64, !dbg !57 - %58 = icmp ne i64 %57, 0, !dbg !57 - br i1 %58, label %59, label %61, !dbg !57 - -59: ; preds = %49 - call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 22, i8* noundef getelementptr inbounds ([31 x i8], [31 x i8]* @.str.3, i64 0, i64 0)) #9, !dbg !57 +50: ; No predecessors! + br label %52, !dbg !56 + +51: ; preds = %40 + br label %52, !dbg !56 + +52: ; preds = %51, %50 + %53 = load i32*, i32** %7, align 8, !dbg !57 + %54 = ptrtoint i32* %53 to i64, !dbg !57 + %55 = load i64, i64* %5, align 8, !dbg !57 + %56 = urem i64 %54, %55, !dbg !57 + %57 = icmp eq i64 %56, 0, !dbg !57 + %58 = xor i1 %57, true, !dbg !57 + %59 = zext i1 %58 to i32, !dbg !57 + %60 = sext i32 %59 to i64, !dbg !57 + %61 = icmp ne i64 %60, 0, !dbg !57 + br i1 %61, label %62, label %64, !dbg !57 + +62: ; preds = %52 + call void @__assert_rtn(i8* noundef getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* noundef getelementptr inbounds ([23 x i8], [23 x i8]* @.str, i64 0, i64 0), i32 noundef 25, i8* noundef getelementptr inbounds ([31 x i8], [31 x i8]* @.str.3, i64 0, i64 0)) #9, !dbg !57 unreachable, !dbg !57 -60: ; No predecessors! - br label %62, !dbg !57 +63: ; No predecessors! + br label %65, !dbg !57 -61: ; preds = %49 - br label %62, !dbg !57 +64: ; preds = %52 + br label %65, !dbg !57 -62: ; preds = %61, %60 - %63 = load i32, i32* %1, align 4, !dbg !58 - ret i32 %63, !dbg !58 +65: ; preds = %64, %63 + %66 = load i32, i32* %1, align 4, !dbg !58 + ret i32 %66, !dbg !58 } ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn @@ -173,43 +176,43 @@ attributes #9 = { cold noreturn } !16 = !{i32 7, !"uwtable", i32 1} !17 = !{i32 7, !"frame-pointer", i32 1} !18 = !{!"Homebrew clang version 14.0.6"} -!19 = distinct !DISubprogram(name: "main", scope: !20, file: !20, line: 6, type: !21, scopeLine: 7, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !24) +!19 = distinct !DISubprogram(name: "main", scope: !20, file: !20, line: 8, type: !21, scopeLine: 9, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !24) !20 = !DIFile(filename: "benchmarks/miscellaneous/nondet_aligned_alloc.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") !21 = !DISubroutineType(types: !22) !22 = !{!23} !23 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) !24 = !{} -!25 = !DILocalVariable(name: "size_int", scope: !19, file: !20, line: 8, type: !23) -!26 = !DILocation(line: 8, column: 9, scope: !19) -!27 = !DILocation(line: 8, column: 20, scope: !19) -!28 = !DILocalVariable(name: "align_int", scope: !19, file: !20, line: 9, type: !23) -!29 = !DILocation(line: 9, column: 9, scope: !19) -!30 = !DILocation(line: 9, column: 21, scope: !19) -!31 = !DILocation(line: 10, column: 23, scope: !19) -!32 = !DILocation(line: 10, column: 32, scope: !19) -!33 = !DILocation(line: 10, column: 5, scope: !19) -!34 = !DILocation(line: 11, column: 23, scope: !19) -!35 = !DILocation(line: 11, column: 33, scope: !19) -!36 = !DILocation(line: 11, column: 5, scope: !19) -!37 = !DILocalVariable(name: "size", scope: !19, file: !20, line: 12, type: !3) -!38 = !DILocation(line: 12, column: 12, scope: !19) -!39 = !DILocation(line: 12, column: 27, scope: !19) -!40 = !DILocation(line: 12, column: 19, scope: !19) -!41 = !DILocalVariable(name: "align", scope: !19, file: !20, line: 13, type: !3) -!42 = !DILocation(line: 13, column: 12, scope: !19) -!43 = !DILocation(line: 13, column: 28, scope: !19) -!44 = !DILocation(line: 13, column: 20, scope: !19) -!45 = !DILocalVariable(name: "array", scope: !19, file: !20, line: 14, type: !46) +!25 = !DILocalVariable(name: "size_int", scope: !19, file: !20, line: 10, type: !23) +!26 = !DILocation(line: 10, column: 9, scope: !19) +!27 = !DILocation(line: 10, column: 20, scope: !19) +!28 = !DILocalVariable(name: "align_int", scope: !19, file: !20, line: 11, type: !23) +!29 = !DILocation(line: 11, column: 9, scope: !19) +!30 = !DILocation(line: 11, column: 21, scope: !19) +!31 = !DILocation(line: 12, column: 23, scope: !19) +!32 = !DILocation(line: 12, column: 32, scope: !19) +!33 = !DILocation(line: 12, column: 5, scope: !19) +!34 = !DILocation(line: 13, column: 23, scope: !19) +!35 = !DILocation(line: 13, column: 33, scope: !19) +!36 = !DILocation(line: 13, column: 5, scope: !19) +!37 = !DILocalVariable(name: "size", scope: !19, file: !20, line: 14, type: !3) +!38 = !DILocation(line: 14, column: 12, scope: !19) +!39 = !DILocation(line: 14, column: 27, scope: !19) +!40 = !DILocation(line: 14, column: 19, scope: !19) +!41 = !DILocalVariable(name: "align", scope: !19, file: !20, line: 15, type: !3) +!42 = !DILocation(line: 15, column: 12, scope: !19) +!43 = !DILocation(line: 15, column: 28, scope: !19) +!44 = !DILocation(line: 15, column: 20, scope: !19) +!45 = !DILocalVariable(name: "array", scope: !19, file: !20, line: 16, type: !46) !46 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !23, size: 64) -!47 = !DILocation(line: 14, column: 10, scope: !19) -!48 = !DILocation(line: 14, column: 18, scope: !19) -!49 = !DILocalVariable(name: "array_2", scope: !19, file: !20, line: 15, type: !46) -!50 = !DILocation(line: 15, column: 10, scope: !19) -!51 = !DILocation(line: 15, column: 34, scope: !19) -!52 = !DILocation(line: 15, column: 41, scope: !19) -!53 = !DILocation(line: 15, column: 46, scope: !19) -!54 = !DILocation(line: 15, column: 20, scope: !19) -!55 = !DILocation(line: 20, column: 5, scope: !19) -!56 = !DILocation(line: 21, column: 5, scope: !19) -!57 = !DILocation(line: 22, column: 5, scope: !19) -!58 = !DILocation(line: 23, column: 1, scope: !19) +!47 = !DILocation(line: 16, column: 10, scope: !19) +!48 = !DILocation(line: 16, column: 18, scope: !19) +!49 = !DILocalVariable(name: "array_2", scope: !19, file: !20, line: 17, type: !46) +!50 = !DILocation(line: 17, column: 10, scope: !19) +!51 = !DILocation(line: 17, column: 34, scope: !19) +!52 = !DILocation(line: 17, column: 41, scope: !19) +!53 = !DILocation(line: 17, column: 46, scope: !19) +!54 = !DILocation(line: 17, column: 20, scope: !19) +!55 = !DILocation(line: 23, column: 5, scope: !19) +!56 = !DILocation(line: 24, column: 5, scope: !19) +!57 = !DILocation(line: 25, column: 5, scope: !19) +!58 = !DILocation(line: 26, column: 1, scope: !19)