diff --git a/benchmarks/c/miscellaneous/uninitRead.c b/benchmarks/c/miscellaneous/uninitRead.c new file mode 100644 index 0000000000..7152ba4806 --- /dev/null +++ b/benchmarks/c/miscellaneous/uninitRead.c @@ -0,0 +1,17 @@ +#include +#include + +/* + This test shows that we can read from uninitialized memory. + EXPECTED: FAIL + PREVIOUSLY: We returned PASS because the array read had no possible rf-edge and thus the program had no valid executions. +*/ + +#define SIZE 10 +volatile int array[SIZE]; + +int main() +{ + assert (array[SIZE] == 42); + return 0; +} diff --git a/cat/c11-orig.cat b/cat/c11-orig.cat new file mode 100644 index 0000000000..e216b2a4f0 --- /dev/null +++ b/cat/c11-orig.cat @@ -0,0 +1,128 @@ +C "C++11" + +(* All c11_*.cat files are C11 models +Overhauling SC atomics in C11 and OpenCL. +M. Batty, A. Donaldson, J. Wickerson. In Proc. +43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016. + +Rewritten by Luc Maranget for herd7 + +*) + +include "c11_cos.cat" +include "c11_los.cat" + +let asw = IW * (M \ IW) +let sb = po +let mo = co + +let cacq = ACQ | (SC & (R | F)) | ACQ_REL | (F & CON) +let crel = REL | (SC & (W | F)) | ACQ_REL +let ccon = R & CON + +let fr = rf^-1 ; mo + +let dd = (data | addr)+ + +let fsb = sb & (F * _) +let sbf = sb & (_ * F) + +(* release_acquire_fenced_synchronizes_with, + hypothetical_release_sequence_set, + release_sequence_set *) + +(* OLD: let rs = [crel] ; fsb? ; [A & W] ; + (((mo ; [rmw]) | coi) & ~(coe ; [!rmw] ; mo))? *) + +let rs_prime = int | (_ * (R & W)) +let rs = mo & rs_prime \ ((mo \ rs_prime) ; mo) + +(* OLD: let swra = ext (rs ; rf ; [A] ; sbf? ; [cacq]) *) +let swra = + ext & + ([crel] ; fsb? ; [A & W] ; rs? ; rf ; + [R & A] ; sbf? ; [cacq]) + +//let swul = ext & ([UL] ; lo ; [LK]) +let pp_asw = asw \ (asw ; sb) +//let sw = pp_asw | swul | swra +let sw = pp_asw | swra + +(* with_consume_cad_set, + dependency_ordered_before *) +let cad = ((rf & sb) | dd)+ +let dob = + (ext & + ([W & crel] ; fsb? ; [A & W] ; + rs?; rf; [ccon])); + cad? + +(* happens_before, + inter_thread_happens_before, + consistent_hb *) +let ithbr = sw | dob | (sw ; sb) +let ithb = (ithbr | (sb ; ithbr))+ +let hb = sb | ithb +acyclic hb as Hb + +(* coherent_memory_use *) +let hbl = hb & loc + +irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh + +(* visible_side_effect_set *) +let vis = (hbl & (W * R)) \ (hbl; [W] ; hbl) + +(* consistent_atomic_rf *) +irreflexive (rf ; hb) as Rf + +(* consistent_non_atomic_rf *) +empty ((rf ; [R\A]) \ vis) as NaRf +// NOTE FW is a dynamic tag which we don't yet support +//empty [FW\A];hbl;[W] as NaRf (* implicit read of Na final writes.. *) + +irreflexive (rf | (mo ; mo ; rf^-1) | (mo ; rf)) as Rmw + + +(* locks_only_consistent_lo *) +//irreflexive (lo ; hb) as Lo1 + +(* locks_only_consistent_locks *) +//irreflexive ([LS] ; lo^-1 ; [LS] ; ~(lo ; [UL] ; lo)) as Lo2 + + +(* data_races *) +//let Mutex = UL|LS +//let cnf = (((W * _) | (_ * W)) & loc) \ ((Mutex * _) | (_ * Mutex)) +//let dr = ext & (cnf \ hb \ (hb^-1) \ (A * A)) + +(* unsequenced_races *) +//let ur = int & ((W * M) | (M * W)) & loc & ~id & ~(sb+) & ~((sb+)^-1) + +(* locks_only_good_mutex_use, locks_only_bad_mutexes *) + +//let bl = ([LS]; (sb & lo); [LK]) & ~(lo; [UL]; lo) + +//let losbwoul = (sb & lo & ~(lo; [UL]; lo)) + +//let lu = [UL] & ~([UL] ; losbwoul^-1 ; [LS] ; losbwoul ; [UL]) + +let r1 = hb +let r2 = fsb? ; mo ; sbf? +let r3 = rf^-1; [SC] ; mo +let r4 = rf^-1 ; hbl ; [W] +let r5 = fsb ; fr +let r6 = fr ; sbf +let r7 = fsb ; fr ; sbf + +let scp = r1|r2|r3|r4|r5|r6|r7 + +acyclic (((SC * SC) & scp) \ id) as Spartial + +//undefined_unless empty dr as Dr +//undefined_unless empty ur as unsequencedRace +//undefined_unless empty bl as badLock +//undefined_unless empty lu as badUnlock + +// Atomicity +empty rmw & (fre; coe) as atomic diff --git a/cat/c11.cat b/cat/c11.cat index e216b2a4f0..ddd736defd 100644 --- a/cat/c11.cat +++ b/cat/c11.cat @@ -9,6 +9,11 @@ Rewritten by Luc Maranget for herd7 *) +(* + This is an adapted version of C11 that supports an execution model where explicit init events + may be missing. As a consequence, reads may have no rf-edge if they read from initial memory. +*) + include "c11_cos.cat" include "c11_los.cat" @@ -20,7 +25,8 @@ let cacq = ACQ | (SC & (R | F)) | ACQ_REL | (F & CON) let crel = REL | (SC & (W | F)) | ACQ_REL let ccon = R & CON -let fr = rf^-1 ; mo +// To be compatible with reads from uninit memory, we use our default definition of fr +//let fr = rf^-1 ; mo let dd = (data | addr)+ @@ -68,7 +74,9 @@ acyclic hb as Hb (* coherent_memory_use *) let hbl = hb & loc -irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh +// irreflexive ((rf^-1)? ; mo ; rf? ; hb) as Coh +// To support reads from uninitialized memory +irreflexive ((fr | mo) ; rf? ; hb) as Coh (* visible_side_effect_set *) let vis = (hbl & (W * R)) \ (hbl; [W] ; hbl) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index a5f79f1502..cdede24330 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -15,6 +15,8 @@ public class OptionNames { // Modeling Options public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds"; public static final String RECURSION_BOUND = "modeling.recursionBound"; + public static final String MEMORY_IS_ZEROED = "modeling.memoryIsZeroed"; + public static final String INIT_DYNAMIC_ALLOCATIONS = "modeling.initDynamicAllocations"; // Compilation Options public static final String USE_RC11_TO_ARCH_SCHEME = "compilation.rc11ToArch"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index cf4a2650ab..7cd860cd17 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -10,6 +10,7 @@ import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.FenceWithId; +import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.RMWStoreExclusive; import com.dat3m.dartagnan.program.filter.Filter; @@ -35,6 +36,7 @@ import java.util.*; import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS; +import static com.dat3m.dartagnan.configuration.OptionNames.MEMORY_IS_ZEROED; import static com.dat3m.dartagnan.program.event.Tag.*; import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; @@ -54,6 +56,13 @@ public class WmmEncoder implements Encoder { secure = true) private boolean enableActiveSets = true; + @Option(name = MEMORY_IS_ZEROED, + description = "Assumes the whole memory is zeroed before the program runs." + + "In particular, if set to TRUE, reads from uninitialized memory will return zero." + + "Otherwise, uninitialized memory has a nondeterministic value.", + secure = true) + private boolean memoryIsZeroed = true; + // ===================================================================== private WmmEncoder(EncodingContext c) { @@ -65,6 +74,7 @@ public static WmmEncoder withContext(EncodingContext context) throws InvalidConf WmmEncoder encoder = new WmmEncoder(context); context.getTask().getConfig().inject(encoder); logger.info("{}: {}", ENABLE_ACTIVE_SETS, encoder.enableActiveSets); + logger.info("{}: {}", MEMORY_IS_ZEROED, encoder.memoryIsZeroed); long t0 = System.currentTimeMillis(); if (encoder.enableActiveSets) { encoder.initializeEncodeSets(); @@ -508,7 +518,7 @@ public Void visitSameLocation(SameLocation locDef) { public Void visitReadFrom(ReadFrom rfDef) { final Relation rf = rfDef.getDefinedRelation(); Map> edgeMap = new HashMap<>(); - EncodingContext.EdgeEncoder edge = context.edge(rf); + final EncodingContext.EdgeEncoder edge = context.edge(rf); ra.getKnowledge(rf).getMaySet().apply((e1, e2) -> { MemoryCoreEvent w = (MemoryCoreEvent) e1; MemoryCoreEvent r = (MemoryCoreEvent) e2; @@ -518,19 +528,24 @@ public Void visitReadFrom(ReadFrom rfDef) { edgeMap.computeIfAbsent(r, key -> new ArrayList<>()).add(e); enc.add(bmgr.implication(e, bmgr.and(execution(w, r), sameAddress, sameValue))); }); - for (MemoryEvent r : edgeMap.keySet()) { - List edges = edgeMap.get(r); + for (Load r : program.getThreadEvents(Load.class)) { + final BooleanFormula uninit = getUninitReadVar(r); + if (memoryIsZeroed) { + enc.add(bmgr.implication(uninit, context.equalZero(context.value(r)))); + } + + final List rfEdges = edgeMap.getOrDefault(r, List.of()); if (GlobalSettings.ALLOW_MULTIREADS) { - enc.add(bmgr.implication(context.execution(r), bmgr.or(edges))); + enc.add(bmgr.implication(context.execution(r), bmgr.or(bmgr.or(rfEdges), uninit))); continue; } - int num = edges.size(); + String rPrefix = "s(" + RF + ",E" + r.getGlobalId() + ","; - BooleanFormula lastSeqVar = edges.get(0); - for (int i = 1; i < num; i++) { + BooleanFormula lastSeqVar = uninit; + for (int i = 0; i < rfEdges.size(); i++) { BooleanFormula newSeqVar = bmgr.makeVariable(rPrefix + i + ")"); - enc.add(bmgr.equivalence(newSeqVar, bmgr.or(lastSeqVar, edges.get(i)))); - enc.add(bmgr.not(bmgr.and(edges.get(i), lastSeqVar))); + enc.add(bmgr.equivalence(newSeqVar, bmgr.or(lastSeqVar, rfEdges.get(i)))); + enc.add(bmgr.not(bmgr.and(rfEdges.get(i), lastSeqVar))); lastSeqVar = newSeqVar; } enc.add(bmgr.implication(context.execution(r), lastSeqVar)); @@ -538,6 +553,10 @@ public Void visitReadFrom(ReadFrom rfDef) { return null; } + private BooleanFormula getUninitReadVar(Load load) { + return bmgr.makeVariable("uninit_read " + load.getGlobalId()); + } + @Override public Void visitCoherence(Coherence coDef) { final Relation co = coDef.getDefinedRelation(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index fad0add96b..220ae6b01f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -514,7 +514,7 @@ public Expression visitAllocaInst(AllocaInstContext ctx) { } //final int alignment = parseAlignment(ctx.align()); //final int addressSpace = parseAddressSpace(ctx.addrSpace()); - block.events.add(EventFactory.newAlloc(register, elementType, sizeExpression, false)); + block.events.add(EventFactory.newAlloc(register, elementType, sizeExpression, false, false)); return register; } 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 2d3f14c54d..78a668db3b 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 @@ -89,8 +89,9 @@ public static List eventSequence(Object... events) { // ------------------------------------------ Memory events ------------------------------------------ - public static Alloc newAlloc(Register register, Type allocType, Expression arraySize, boolean isHeapAlloc) { - return new Alloc(register, allocType, arraySize, isHeapAlloc); + public static Alloc newAlloc(Register register, Type allocType, Expression arraySize, + boolean isHeapAlloc, boolean doesZeroOutMemory) { + return new Alloc(register, allocType, arraySize, isHeapAlloc, doesZeroOutMemory); } public static Load newLoad(Register register, Expression address) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java index 02d98343d4..fa527e5945 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java @@ -1,6 +1,5 @@ package com.dat3m.dartagnan.program.event.lang; -import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.ExpressionVisitor; @@ -13,7 +12,6 @@ import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.RegWriter; import com.google.common.base.Preconditions; -import org.sosy_lab.java_smt.api.BooleanFormula; import java.math.BigInteger; import java.util.HashSet; @@ -31,14 +29,17 @@ public class Alloc extends AbstractEvent implements RegReader, RegWriter { private Type allocationType; private Expression arraySize; private boolean isHeapAllocation; + private boolean doesZeroOutMemory; - public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation) { + public Alloc(Register resultRegister, Type allocType, Expression arraySize, boolean isHeapAllocation, + boolean doesZeroOutMemory) { Preconditions.checkArgument(resultRegister.getType() == TypeFactory.getInstance().getArchType()); Preconditions.checkArgument(arraySize.getType() instanceof IntegerType); this.resultRegister = resultRegister; this.arraySize = arraySize; this.allocationType = allocType; this.isHeapAllocation = isHeapAllocation; + this.doesZeroOutMemory = doesZeroOutMemory; } protected Alloc(Alloc other) { @@ -47,6 +48,7 @@ protected Alloc(Alloc other) { this.allocationType = other.allocationType; this.arraySize = other.arraySize; this.isHeapAllocation = other.isHeapAllocation; + this.doesZeroOutMemory = other.doesZeroOutMemory; } @Override @@ -57,10 +59,12 @@ protected Alloc(Alloc other) { public Type getAllocationType() { return allocationType; } public Expression getArraySize() { return arraySize; } public boolean isHeapAllocation() { return isHeapAllocation; } + public boolean doesZeroOutMemory() { return doesZeroOutMemory; } public boolean isSimpleAllocation() { return (arraySize instanceof IntLiteral size && size.isOne()); } public boolean isArrayAllocation() { return !isSimpleAllocation(); } + public Expression getAllocationSize() { final ExpressionFactory expressions = ExpressionFactory.getInstance(); final TypeFactory types = TypeFactory.getInstance(); @@ -99,9 +103,4 @@ protected String defaultString() { @Override public Alloc getCopy() { return new Alloc(this); } - - @Override - public BooleanFormula encodeExec(EncodingContext context) { - throw new UnsupportedOperationException("Cannot encode alloc events."); - } } 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 bcc84029d5..c0ec14bb60 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 @@ -13,7 +13,6 @@ import java.util.Set; import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkState; /** * Associated with an array of memory locations. @@ -55,9 +54,7 @@ public class MemoryObject extends LeafExpressionBase { public boolean isStaticallyAllocated() { return isStatic; } public boolean isDynamicallyAllocated() { return !isStatic; } - // Should only be called for statically allocated objects. - public Set getStaticallyInitializedFields() { - checkState(this.isStaticallyAllocated(), "Unexpected dynamic object %s", this); + public Set getInitializedFields() { return initialValues.keySet(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java index 577bebd853..3ceb211f33 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java @@ -36,7 +36,7 @@ public void run(Program program) { } for (MemoryObject memoryObject : program.getMemory().getObjects()) { - for (int field : memoryObject.getStaticallyInitializedFields()) { + for (int field : memoryObject.getInitializedFields()) { memoryObject.setInitialValue(field, memoryObject.getInitialValue(field).accept(transformer)); } } 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 2aff76c10a..a4ec500381 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 @@ -367,7 +367,7 @@ private List inlineAsZero(FunctionCall call) { } private List inlineExit(FunctionCall ignored) { - return List.of(EventFactory.newAbortIf(ExpressionFactory.getInstance().makeTrue())); + return List.of(EventFactory.newAbortIf(expressions.makeTrue())); } private List inlineLoopBegin(FunctionCall ignored) { @@ -549,7 +549,7 @@ private List inlinePthreadKeyCreate(FunctionCall call) { final Expression destructorOffset = expressions.makeValue(threadCount * pointerBytes, types.getArchType()); //TODO call destructor at each thread's normal exit return List.of( - EventFactory.newAlloc(storageAddressRegister, types.getArchType(), size, true), + EventFactory.newAlloc(storageAddressRegister, types.getArchType(), size, true, true), EventFactory.newStore(keyAddress, storageAddressRegister), EventFactory.newStore(expressions.makeAdd(storageAddressRegister, destructorOffset), destructor), assignSuccess(errorRegister) @@ -862,19 +862,21 @@ private List inlinePthreadRwlockAttr(FunctionCall call) { private List inlineMalloc(FunctionCall call) { final Register resultRegister = getResultRegisterAndCheckArguments(1, call); + final Type allocType = types.getByteType(); final Expression totalSize = call.getArguments().get(0); return List.of( - EventFactory.newAlloc(resultRegister, TypeFactory.getInstance().getByteType(), totalSize, true) + EventFactory.newAlloc(resultRegister, allocType, totalSize, true, false) ); } private List inlineCalloc(FunctionCall call) { final Register resultRegister = getResultRegisterAndCheckArguments(2, call); + final Type allocType = types.getByteType(); final Expression elementCount = call.getArguments().get(0); final Expression elementSize = call.getArguments().get(1); final Expression totalSize = expressions.makeMul(elementCount, elementSize); return List.of( - EventFactory.newAlloc(resultRegister, TypeFactory.getInstance().getByteType(), totalSize, true) + EventFactory.newAlloc(resultRegister, allocType, totalSize, true, true) ); } 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 9f894f6cd9..85af4ec7f2 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 @@ -1,6 +1,9 @@ package com.dat3m.dartagnan.program.processing; +import com.dat3m.dartagnan.configuration.OptionNames; import com.dat3m.dartagnan.exception.MalformedProgramException; +import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.integers.IntLiteral; import com.dat3m.dartagnan.expression.type.FunctionType; import com.dat3m.dartagnan.expression.type.TypeFactory; @@ -14,6 +17,10 @@ import com.dat3m.dartagnan.program.event.lang.Alloc; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; import java.math.BigInteger; import java.util.List; @@ -27,11 +34,31 @@ (TODO: If possible, only allocate subset of relevant init events) (3) replaces the Malloc event with a local register assignment, assigning the newly created MemoryObject */ +@Options public class MemoryAllocation implements ProgramProcessor { - private MemoryAllocation() { } + // =========================== Configurables =========================== - public static MemoryAllocation newInstance() { return new MemoryAllocation(); } + @Option(name = OptionNames.INIT_DYNAMIC_ALLOCATIONS, + description = "Creates init events for all dynamic allocations. Those init events zero out the memory.", + secure = true) + private boolean createInitsForDynamicAllocations = false; + + // ====================================================================== + + + private MemoryAllocation() { + } + + public static MemoryAllocation newInstance() { + return new MemoryAllocation(); + } + + public static MemoryAllocation fromConfig(Configuration config) throws InvalidConfigurationException { + final MemoryAllocation memAlloc = new MemoryAllocation(); + config.inject(memAlloc); + return memAlloc; + } @Override public void run(Program program) { @@ -41,14 +68,22 @@ public void run(Program program) { } private void processAllocations(Program program) { + final ExpressionFactory expressions = ExpressionFactory.getInstance(); + // FIXME: We should probably initialize depending on the allocation type of the alloc + final Expression zero = expressions.makeZero(TypeFactory.getInstance().getByteType()); for (Alloc alloc : program.getThreadEvents(Alloc.class)) { - final MemoryObject allocatedObject = program.getMemory().allocate(getSize(alloc), false); + final int size = getSize(alloc); + final MemoryObject allocatedObject = program.getMemory().allocate(size, false); final Local local = EventFactory.newLocal(alloc.getResultRegister(), allocatedObject); local.addTags(Tag.Std.MALLOC); local.copyAllMetadataFrom(alloc); alloc.replaceBy(local); - // TODO: We can initialize the initial memory based on the allocation type. + if (alloc.doesZeroOutMemory() || createInitsForDynamicAllocations) { + for (int i = 0; i < size; i++) { + allocatedObject.setInitialValue(i, zero); + } + } } } @@ -90,10 +125,12 @@ private void createInitEvents(Program program) { int nextThreadId = Stream.concat(program.getThreads().stream(), program.getFunctions().stream()) .mapToInt(Function::getId).max().getAsInt() + 1; for(MemoryObject memObj : program.getMemory().getObjects()) { - final boolean isStaticallyInitialized = !isLitmus - && memObj.isStaticallyAllocated(); - final Iterable fieldsToInit = isStaticallyInitialized ? - memObj.getStaticallyInitializedFields() : IntStream.range(0, memObj.size()).boxed()::iterator; + final Iterable fieldsToInit; + if (isLitmus) { + fieldsToInit = IntStream.range(0, memObj.size()).boxed()::iterator; + } else { + fieldsToInit = memObj.getInitializedFields(); + } for(int i : fieldsToInit) { final Event init = EventFactory.newInit(memObj, i); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java index d6e39aa97b..49e8cb14d8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java @@ -71,7 +71,7 @@ private void findAndTransformAddressTakenFunctionsInMemory( Memory memory, FunctionCollector functionCollector, FunctionToAddressTransformer toAddressTransformer ) { for (MemoryObject memoryObject : memory.getObjects()) { - for (Integer field : memoryObject.getStaticallyInitializedFields()) { + for (Integer field : memoryObject.getInitializedFields()) { functionCollector.reset(); final Expression initValue = memoryObject.getInitialValue(field).accept(functionCollector); 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 159c072757..2cfd9fc356 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 @@ -115,7 +115,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep intrinsics.lateInliningPass(), RemoveUnusedMemory.newInstance(), ProgramProcessor.fromFunctionProcessor(MemToReg.fromConfig(config), Target.THREADS, true), - MemoryAllocation.newInstance(), + MemoryAllocation.fromConfig(config), // --- Statistics + verification --- IdReassignment.newInstance(), // Normalize used Ids (remove any gaps) printAfterProcessing ? DebugPrint.withHeader("After processing", Printer.Mode.THREADS) : null, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java index 70cdf940a4..271cb9629d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java @@ -46,7 +46,7 @@ private Set findReachableFunctions(Program program) { // (1) Find functions referenced by memory for (MemoryObject memoryObject : program.getMemory().getObjects()) { - for (Integer field : memoryObject.getStaticallyInitializedFields()) { + for (Integer field : memoryObject.getInitializedFields()) { memoryObject.getInitialValue(field).accept(functionCollector); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index bfce249fb6..14ac942bc0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -25,7 +25,7 @@ public void run(Program program) { program.getThreadEvents(RegReader.class).forEach(r -> r.transformExpressions(collector)); // Also add MemoryObjects referenced by initial values (this does happen in Litmus code) for (MemoryObject obj : memory.getObjects()) { - for (Integer field : obj.getStaticallyInitializedFields()) { + for (Integer field : obj.getInitializedFields()) { obj.getInitialValue(field).accept(collector); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/ReadFromGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/ReadFromGraph.java index fcb2f4444f..a77b721539 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/ReadFromGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/ReadFromGraph.java @@ -46,7 +46,7 @@ public Stream edgeStream(int id, EdgeDirection dir) { if (e.isWrite()) { return dir == EdgeDirection.INGOING ? Stream.empty() : model.getWriteReadsMap().get(e).stream().map(read -> makeEdge(id, read.getId())); - } else if (e.isRead()) { + } else if (e.isRead() && e.getReadFrom() != null) { return dir == EdgeDirection.INGOING ? Stream.of(new Edge(e.getReadFrom().getId(), id)) : Stream.empty(); } else { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java index 222819f1e5..d39af3c995 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/visualization/ExecutionGraphVisualizer.java @@ -197,6 +197,9 @@ private String eventToNode(EventData e) { String tag = e.getEvent().toString(); if (e.isMemoryEvent()) { Object address = addresses.get(e.getAccessedAddress()); + if (address == null) { + address = e.getAccessedAddress(); + } BigInteger value = e.getValue(); MemoryOrder mo = e.getEvent().getMetadata(MemoryOrder.class); String moString = mo == null ? "" : ", " + mo.value(); 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 6ca5531079..9e1eb46e57 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 @@ -493,9 +493,6 @@ private void extractReadsFrom() { for (EventData read : addressedReads.getValue()) { for (EventData write : addressWritesMap.get(address)) { BooleanFormula rfExpr = rf.encode(write.getEvent(), read.getEvent()); - // The null check in isTrue is important: Currently there are cases where no rf-edge between - // init writes and loads get encoded (in case of arrays/structs). This is usually no problem, - // since in a well-initialized program, the init write should not be readable anyway. if (isTrue(rfExpr)) { readWriteMap.put(read, write); read.setReadFrom(write); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java index 84e2583a57..d72941cc91 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java @@ -203,8 +203,22 @@ private Relation makePredefinedRelation(String name) { case CTRLDIRECT -> new DirectControlDependency(r); case EMPTY -> new Empty(r); case FR -> { - Relation rfinv = addDefinition(new Inverse(newRelation(), getOrCreatePredefinedRelation(RF))); - yield composition(r, rfinv, getOrCreatePredefinedRelation(CO)); + // rf^-1;co + final Relation rfinv = addDefinition(new Inverse(newRelation(), getOrCreatePredefinedRelation(RF))); + final Relation co = getOrCreatePredefinedRelation(CO); + final Relation frStandard = addDefinition(composition(newRelation(), rfinv, co)); + + // ([R] \ [range(rf)]);loc;[W] + final Relation reads = addDefinition(new SetIdentity(newRelation(), getFilter(Tag.READ))); + final Relation rfRange = addDefinition(new RangeIdentity(newRelation(), getOrCreatePredefinedRelation(RF))); + final Relation loc = getOrCreatePredefinedRelation(LOC); + final Relation writes = addDefinition(new SetIdentity(newRelation(), Filter.byTag(Tag.WRITE))); + final Relation ur = addDefinition(new Difference(newRelation(), reads, rfRange)); + final Relation urloc = addDefinition(composition(newRelation(), ur, loc)); + final Relation urlocwrites = addDefinition(composition(newRelation(), urloc, writes)); + + // let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W] + yield union(r, frStandard, urlocwrites); } case IDDTRANS -> new TransitiveClosure(r, getOrCreatePredefinedRelation(IDD)); case DATA -> intersection(r, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java index c87a9a4b49..f9e1477fb2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java @@ -907,12 +907,7 @@ private Knowledge computeInternalDependencies(Set usageTypes) { EventGraph may = new EventGraph(); EventGraph must = new EventGraph(); - for (Event regReaderEvent : program.getThreadEvents()) { - //TODO: Once "Event" is an interface and RegReader inherits from it, - // we can use program.getEvents(RegReader.class) here. - if (!(regReaderEvent instanceof RegReader regReader)) { - continue; - } + for (RegReader regReader : program.getThreadEvents(RegReader.class)) { for (Register.Read regRead : regReader.getRegisterReads()) { if (!usageTypes.contains(regRead.usageType())) { continue; @@ -926,12 +921,12 @@ private Knowledge computeInternalDependencies(Set usageTypes) { if (program.getArch().equals(RISCV) && register.getName().equals("x0")) { continue; } - Dependency.State r = dep.of(regReaderEvent, register); + Dependency.State r = dep.of(regReader, register); for (Event regWriter : r.may) { - may.add(regWriter, regReaderEvent); + may.add(regWriter, regReader); } for (Event regWriter : r.must) { - must.add(regWriter, regReaderEvent); + must.add(regWriter, regReader); } } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/AddInitReadHandling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/AddInitReadHandling.java new file mode 100644 index 0000000000..71aa4a6a0c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/AddInitReadHandling.java @@ -0,0 +1,38 @@ +package com.dat3m.dartagnan.wmm.processing; + +import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.Wmm; +import com.dat3m.dartagnan.wmm.axiom.Emptiness; +import com.dat3m.dartagnan.wmm.definition.Composition; +import com.dat3m.dartagnan.wmm.definition.Difference; +import com.dat3m.dartagnan.wmm.definition.RangeIdentity; +import com.dat3m.dartagnan.wmm.definition.SetIdentity; + +import static com.dat3m.dartagnan.wmm.RelationNameRepository.LOC; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; + + +// Add empty (([R] \ [range(rf)]);loc;[IW]) to enforce that reads from uninitialized memory +// are impossible if an init write exists. +public class AddInitReadHandling implements WmmProcessor { + + private AddInitReadHandling() {} + + public static AddInitReadHandling newInstance() { + return new AddInitReadHandling(); + } + + @Override + public void run(Wmm mm) { + final Relation reads = mm.addDefinition(new SetIdentity(mm.newRelation(), mm.getFilter(Tag.READ))); + final Relation rfRange = mm.addDefinition(new RangeIdentity(mm.newRelation(), mm.getOrCreatePredefinedRelation(RF))); + final Relation loc = mm.getOrCreatePredefinedRelation(LOC); + final Relation iw = mm.addDefinition(new SetIdentity(mm.newRelation(), mm.getFilter(Tag.INIT))); + final Relation ur = mm.addDefinition(new Difference(mm.newRelation(), reads, rfRange)); + final Relation urloc = mm.addDefinition(new Composition(mm.newRelation(), ur, loc)); + final Relation urlociw = mm.addDefinition(new Composition(mm.newRelation(), urloc, iw)); + + mm.addConstraint(new Emptiness(urlociw)); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java index 932d804a9d..f614f31079 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java @@ -26,6 +26,7 @@ public class WmmProcessingManager implements WmmProcessor { private WmmProcessingManager(Configuration config) throws InvalidConfigurationException { config.inject(this); processors.addAll(Arrays.asList( + AddInitReadHandling.newInstance(), RemoveDeadRelations.newInstance(), MergeEquivalentRelations.newInstance(), FlattenAssociatives.newInstance(), diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessor.java index 06eaee638a..55ee105418 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessor.java @@ -4,4 +4,4 @@ public interface WmmProcessor { void run(Wmm wmm); -} +} \ No newline at end of file diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java index ea591b53e9..759319238f 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java @@ -15,6 +15,7 @@ import org.junit.rules.Timeout; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; @@ -37,12 +38,18 @@ public AbstractCTest(String name, Arch target, Result expected) { // =================== Modifiable behavior ==================== + protected abstract long getTimeout(); + + protected Configuration getConfiguration() throws InvalidConfigurationException { + return Configuration.builder() + .setOption(OptionNames.USE_INTEGERS, "true") + .build(); + } + protected Provider getProgramPathProvider() { return Provider.fromSupplier(() -> getTestResourcePath(name + ".ll")); } - protected abstract long getTimeout(); - protected Provider getBoundProvider() { return Provider.fromSupplier(() -> 1); } @@ -60,9 +67,7 @@ protected Provider> getPropertyProvider() { } protected Provider getConfigurationProvider() { - return Provider.fromSupplier(() -> Configuration.builder() - .setOption(OptionNames.USE_INTEGERS, "true") - .build()); + return Provider.fromSupplier(this::getConfiguration); } // ============================================================= diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java index 6cb169ad52..1564eea802 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LFDSTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.C11; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.FAIL; import static com.dat3m.dartagnan.utils.Result.PASS; @@ -45,7 +43,7 @@ protected Provider getBoundProvider() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/c11.cat")))); + return Providers.createWmmFromName(() -> "c11"); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") @@ -59,7 +57,7 @@ public static Iterable data() throws IOException { // {"treiber", C11, UNKNOWN}, {"treiber-CAS-relaxed", C11, FAIL}, {"chase-lev", C11, PASS}, - // These ones have an extra thief that violate the assertion + // These have an extra thief that violate the assertion {"chase-lev-fail", C11, FAIL}, {"hash_table", C11, PASS}, {"hash_table-fail", C11, FAIL}, @@ -72,8 +70,7 @@ public void testAssume() throws Exception { assertEquals(expected, s.getResult()); } - // CAAT might not yet work for C11 - // @Test + @Test public void testRefinement() throws Exception { RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get()); assertEquals(expected, s.getResult()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LocksTest.java index 0d74df1a55..0c0e41cb9d 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LocksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11LocksTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,11 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.C11; -import static com.dat3m.dartagnan.utils.ResourceHelper.*; +import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @@ -39,7 +38,7 @@ protected long getTimeout() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/c11.cat")))); + return Providers.createWmmFromName(() -> "c11"); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") @@ -82,8 +81,7 @@ public void testAssume() throws Exception { assertEquals(expected, s.getResult()); } - // CAAT might not yet work for C11 - // @Test + @Test public void testRefinement() throws Exception { RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get()); assertEquals(expected, s.getResult()); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLFDSTest.java new file mode 100644 index 0000000000..66a2c7a387 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLFDSTest.java @@ -0,0 +1,33 @@ +package com.dat3m.dartagnan.c; + +import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.OptionNames; +import com.dat3m.dartagnan.utils.Result; +import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; +import com.dat3m.dartagnan.wmm.Wmm; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; + +@RunWith(Parameterized.class) +public class C11OrigLFDSTest extends C11LFDSTest { + + public C11OrigLFDSTest(String name, Arch target, Result expected) { + super(name, target, expected); + } + + @Override + protected Configuration getConfiguration() throws InvalidConfigurationException { + return Configuration.builder() + .copyFrom(super.getConfiguration()) + .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true") + .build(); + } + + @Override + protected Provider getWmmProvider() { + return Providers.createWmmFromName(() -> "c11-orig"); + } +} \ No newline at end of file diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLocksTest.java new file mode 100644 index 0000000000..304e49b730 --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/C11OrigLocksTest.java @@ -0,0 +1,33 @@ +package com.dat3m.dartagnan.c; + +import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.configuration.OptionNames; +import com.dat3m.dartagnan.utils.Result; +import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; +import com.dat3m.dartagnan.wmm.Wmm; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; + +@RunWith(Parameterized.class) +public class C11OrigLocksTest extends C11LocksTest { + + public C11OrigLocksTest(String name, Arch target, Result expected) { + super(name, target, expected); + } + + @Override + protected Configuration getConfiguration() throws InvalidConfigurationException { + return Configuration.builder() + .copyFrom(super.getConfiguration()) + .setOption(OptionNames.INIT_DYNAMIC_ALLOCATIONS, "true") + .build(); + } + + @Override + protected Provider getWmmProvider() { + return Providers.createWmmFromName(() -> "c11-orig"); + } +} \ No newline at end of file diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/CLocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/CLocksTest.java index 9117541c74..48eff8dc9e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/CLocksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/CLocksTest.java @@ -19,7 +19,7 @@ @RunWith(Parameterized.class) public class CLocksTest extends AbstractCTest { - + public CLocksTest(String name, Arch target, Result expected) { super(name, target, expected); } @@ -34,101 +34,101 @@ protected long getTimeout() { return 60000; } - @Parameterized.Parameters(name = "{index}: {0}, target={1}") + @Parameterized.Parameters(name = "{index}: {0}, target={1}") public static Iterable data() throws IOException { - return Arrays.asList(new Object[][]{ - {"ttas", TSO, UNKNOWN}, - {"ttas", ARM8, UNKNOWN}, - {"ttas", POWER, UNKNOWN}, - {"ttas", RISCV, UNKNOWN}, - {"ttas-acq2rx", TSO, UNKNOWN}, - {"ttas-acq2rx", ARM8, FAIL}, - {"ttas-acq2rx", POWER, FAIL}, - {"ttas-acq2rx", RISCV, FAIL}, - {"ttas-rel2rx", TSO, UNKNOWN}, - {"ttas-rel2rx", ARM8, FAIL}, - {"ttas-rel2rx", POWER, FAIL}, - {"ttas-rel2rx", RISCV, FAIL}, - {"ticketlock", TSO, PASS}, - {"ticketlock", ARM8, PASS}, - {"ticketlock", POWER, PASS}, - {"ticketlock", RISCV, PASS}, - {"ticketlock-acq2rx", TSO, PASS}, - {"ticketlock-acq2rx", ARM8, FAIL}, - {"ticketlock-acq2rx", POWER, FAIL}, - {"ticketlock-acq2rx", RISCV, FAIL}, - {"ticketlock-rel2rx", TSO, PASS}, - {"ticketlock-rel2rx", ARM8, FAIL}, - {"ticketlock-rel2rx", POWER, FAIL}, - {"ticketlock-rel2rx", RISCV, FAIL}, - {"mutex", TSO, UNKNOWN}, - {"mutex", ARM8, UNKNOWN}, - {"mutex", POWER, UNKNOWN}, - {"mutex", RISCV, UNKNOWN}, - {"mutex-acq2rx_futex", TSO, UNKNOWN}, - {"mutex-acq2rx_futex", ARM8, UNKNOWN}, - {"mutex-acq2rx_futex", POWER, UNKNOWN}, - {"mutex-acq2rx_futex", RISCV, UNKNOWN}, - {"mutex-acq2rx_lock", TSO, UNKNOWN}, - {"mutex-acq2rx_lock", ARM8, FAIL}, - {"mutex-acq2rx_lock", POWER, FAIL}, - {"mutex-acq2rx_lock", RISCV, FAIL}, - {"mutex-rel2rx_futex", TSO, UNKNOWN}, - {"mutex-rel2rx_futex", ARM8, UNKNOWN}, - {"mutex-rel2rx_futex", POWER, UNKNOWN}, - {"mutex-rel2rx_futex", RISCV, UNKNOWN}, - {"mutex-rel2rx_unlock", TSO, UNKNOWN}, - {"mutex-rel2rx_unlock", ARM8, FAIL}, - {"mutex-rel2rx_unlock", POWER, FAIL}, - {"mutex-rel2rx_unlock", RISCV, FAIL}, - {"spinlock", TSO, PASS}, - {"spinlock", ARM8, PASS}, - {"spinlock", POWER, PASS}, - {"spinlock", RISCV, PASS}, - {"spinlock-acq2rx", TSO, PASS}, - {"spinlock-acq2rx", ARM8, FAIL}, - {"spinlock-acq2rx", POWER, FAIL}, - {"spinlock-acq2rx", RISCV, FAIL}, - {"spinlock-rel2rx", TSO, PASS}, - {"spinlock-rel2rx", ARM8, FAIL}, - {"spinlock-rel2rx", POWER, FAIL}, - {"spinlock-rel2rx", RISCV, FAIL}, - {"linuxrwlock", TSO, UNKNOWN}, - {"linuxrwlock", ARM8, UNKNOWN}, - {"linuxrwlock", POWER, UNKNOWN}, - {"linuxrwlock", RISCV, UNKNOWN}, - {"linuxrwlock-acq2rx", TSO, UNKNOWN}, - {"linuxrwlock-acq2rx", ARM8, FAIL}, - {"linuxrwlock-acq2rx", POWER, FAIL}, - {"linuxrwlock-acq2rx", RISCV, FAIL}, - {"linuxrwlock-rel2rx", TSO, UNKNOWN}, - {"linuxrwlock-rel2rx", ARM8, FAIL}, - {"linuxrwlock-rel2rx", POWER, FAIL}, - {"linuxrwlock-rel2rx", RISCV, FAIL}, - {"mutex_musl", TSO, UNKNOWN}, - {"mutex_musl", ARM8, UNKNOWN}, - {"mutex_musl", POWER, UNKNOWN}, - {"mutex_musl", RISCV, UNKNOWN}, - {"mutex_musl-acq2rx_futex", TSO, UNKNOWN}, - {"mutex_musl-acq2rx_futex", ARM8, UNKNOWN}, - {"mutex_musl-acq2rx_futex", POWER, UNKNOWN}, - {"mutex_musl-acq2rx_futex", RISCV, UNKNOWN}, - {"mutex_musl-acq2rx_lock", TSO, UNKNOWN}, - {"mutex_musl-acq2rx_lock", ARM8, FAIL}, - {"mutex_musl-acq2rx_lock", POWER, FAIL}, - {"mutex_musl-acq2rx_lock", RISCV, FAIL}, - {"mutex_musl-rel2rx_futex", TSO, UNKNOWN}, - {"mutex_musl-rel2rx_futex", ARM8, UNKNOWN}, - {"mutex_musl-rel2rx_futex", POWER, UNKNOWN}, - {"mutex_musl-rel2rx_futex", RISCV, UNKNOWN}, - {"mutex_musl-rel2rx_unlock", TSO, UNKNOWN}, - {"mutex_musl-rel2rx_unlock", ARM8, FAIL}, - {"mutex_musl-rel2rx_unlock", POWER, FAIL}, - {"mutex_musl-rel2rx_unlock", RISCV, FAIL}, - {"seqlock", TSO, PASS}, - {"seqlock", ARM8, PASS}, - {"seqlock", POWER, PASS}, - {"seqlock", RISCV, PASS}, + return Arrays.asList(new Object[][]{ + {"ttas", TSO, UNKNOWN}, + {"ttas", ARM8, UNKNOWN}, + {"ttas", POWER, UNKNOWN}, + {"ttas", RISCV, UNKNOWN}, + {"ttas-acq2rx", TSO, UNKNOWN}, + {"ttas-acq2rx", ARM8, FAIL}, + {"ttas-acq2rx", POWER, FAIL}, + {"ttas-acq2rx", RISCV, FAIL}, + {"ttas-rel2rx", TSO, UNKNOWN}, + {"ttas-rel2rx", ARM8, FAIL}, + {"ttas-rel2rx", POWER, FAIL}, + {"ttas-rel2rx", RISCV, FAIL}, + {"ticketlock", TSO, PASS}, + {"ticketlock", ARM8, PASS}, + {"ticketlock", POWER, PASS}, + {"ticketlock", RISCV, PASS}, + {"ticketlock-acq2rx", TSO, PASS}, + {"ticketlock-acq2rx", ARM8, FAIL}, + {"ticketlock-acq2rx", POWER, FAIL}, + {"ticketlock-acq2rx", RISCV, FAIL}, + {"ticketlock-rel2rx", TSO, PASS}, + {"ticketlock-rel2rx", ARM8, FAIL}, + {"ticketlock-rel2rx", POWER, FAIL}, + {"ticketlock-rel2rx", RISCV, FAIL}, + {"mutex", TSO, UNKNOWN}, + {"mutex", ARM8, UNKNOWN}, + {"mutex", POWER, UNKNOWN}, + {"mutex", RISCV, UNKNOWN}, + {"mutex-acq2rx_futex", TSO, UNKNOWN}, + {"mutex-acq2rx_futex", ARM8, UNKNOWN}, + {"mutex-acq2rx_futex", POWER, UNKNOWN}, + {"mutex-acq2rx_futex", RISCV, UNKNOWN}, + {"mutex-acq2rx_lock", TSO, UNKNOWN}, + {"mutex-acq2rx_lock", ARM8, FAIL}, + {"mutex-acq2rx_lock", POWER, FAIL}, + {"mutex-acq2rx_lock", RISCV, FAIL}, + {"mutex-rel2rx_futex", TSO, UNKNOWN}, + {"mutex-rel2rx_futex", ARM8, UNKNOWN}, + {"mutex-rel2rx_futex", POWER, UNKNOWN}, + {"mutex-rel2rx_futex", RISCV, UNKNOWN}, + {"mutex-rel2rx_unlock", TSO, UNKNOWN}, + {"mutex-rel2rx_unlock", ARM8, FAIL}, + {"mutex-rel2rx_unlock", POWER, FAIL}, + {"mutex-rel2rx_unlock", RISCV, FAIL}, + {"spinlock", TSO, PASS}, + {"spinlock", ARM8, PASS}, + {"spinlock", POWER, PASS}, + {"spinlock", RISCV, PASS}, + {"spinlock-acq2rx", TSO, PASS}, + {"spinlock-acq2rx", ARM8, FAIL}, + {"spinlock-acq2rx", POWER, FAIL}, + {"spinlock-acq2rx", RISCV, FAIL}, + {"spinlock-rel2rx", TSO, PASS}, + {"spinlock-rel2rx", ARM8, FAIL}, + {"spinlock-rel2rx", POWER, FAIL}, + {"spinlock-rel2rx", RISCV, FAIL}, + {"linuxrwlock", TSO, UNKNOWN}, + {"linuxrwlock", ARM8, UNKNOWN}, + {"linuxrwlock", POWER, UNKNOWN}, + {"linuxrwlock", RISCV, UNKNOWN}, + {"linuxrwlock-acq2rx", TSO, UNKNOWN}, + {"linuxrwlock-acq2rx", ARM8, FAIL}, + {"linuxrwlock-acq2rx", POWER, FAIL}, + {"linuxrwlock-acq2rx", RISCV, FAIL}, + {"linuxrwlock-rel2rx", TSO, UNKNOWN}, + {"linuxrwlock-rel2rx", ARM8, FAIL}, + {"linuxrwlock-rel2rx", POWER, FAIL}, + {"linuxrwlock-rel2rx", RISCV, FAIL}, + {"mutex_musl", TSO, UNKNOWN}, + {"mutex_musl", ARM8, UNKNOWN}, + {"mutex_musl", POWER, UNKNOWN}, + {"mutex_musl", RISCV, UNKNOWN}, + {"mutex_musl-acq2rx_futex", TSO, UNKNOWN}, + {"mutex_musl-acq2rx_futex", ARM8, UNKNOWN}, + {"mutex_musl-acq2rx_futex", POWER, UNKNOWN}, + {"mutex_musl-acq2rx_futex", RISCV, UNKNOWN}, + {"mutex_musl-acq2rx_lock", TSO, UNKNOWN}, + {"mutex_musl-acq2rx_lock", ARM8, FAIL}, + {"mutex_musl-acq2rx_lock", POWER, FAIL}, + {"mutex_musl-acq2rx_lock", RISCV, FAIL}, + {"mutex_musl-rel2rx_futex", TSO, UNKNOWN}, + {"mutex_musl-rel2rx_futex", ARM8, UNKNOWN}, + {"mutex_musl-rel2rx_futex", POWER, UNKNOWN}, + {"mutex_musl-rel2rx_futex", RISCV, UNKNOWN}, + {"mutex_musl-rel2rx_unlock", TSO, UNKNOWN}, + {"mutex_musl-rel2rx_unlock", ARM8, FAIL}, + {"mutex_musl-rel2rx_unlock", POWER, FAIL}, + {"mutex_musl-rel2rx_unlock", RISCV, FAIL}, + {"seqlock", TSO, PASS}, + {"seqlock", ARM8, PASS}, + {"seqlock", POWER, PASS}, + {"seqlock", RISCV, PASS}, {"pthread_mutex", TSO, PASS}, {"pthread_mutex", ARM8, PASS}, {"pthread_mutex", POWER, PASS}, @@ -149,18 +149,18 @@ public static Iterable data() throws IOException { {"ticket_awnsb_mutex-acq2rx", POWER, FAIL}, {"ticket_awnsb_mutex", RISCV, PASS}, {"ticket_awnsb_mutex-acq2rx", RISCV, FAIL}, - }); + }); } -// @Test - public void testAssume() throws Exception { - AssumeSolver s = AssumeSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get()); - assertEquals(expected, s.getResult()); - } + // @Test + public void testAssume() throws Exception { + AssumeSolver s = AssumeSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get()); + assertEquals(expected, s.getResult()); + } @Test - public void testRefinement() throws Exception { - RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get()); - assertEquals(expected, s.getResult()); - } + public void testRefinement() throws Exception { + RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get()); + assertEquals(expected, s.getResult()); + } } \ No newline at end of file diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/EBRTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/EBRTest.java index 33249bbae1..c08cb42aff 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/EBRTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/EBRTest.java @@ -12,9 +12,11 @@ import java.io.IOException; import java.util.Arrays; + import static com.dat3m.dartagnan.configuration.Arch.*; -import static com.dat3m.dartagnan.utils.ResourceHelper.*; -import static com.dat3m.dartagnan.utils.Result.*; +import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; +import static com.dat3m.dartagnan.utils.Result.FAIL; +import static com.dat3m.dartagnan.utils.Result.PASS; import static org.junit.Assert.assertEquals; @RunWith(Parameterized.class) @@ -40,8 +42,8 @@ protected Provider getSolverProvider() { } @Override - protected Provider getConfigurationProvider() { - return Provider.fromSupplier(() -> Configuration.defaultConfiguration()); + protected Configuration getConfiguration() { + return Configuration.defaultConfiguration(); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLFDSTest.java index e21d7fa0f7..a3d3978173 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLFDSTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLFDSTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.IMM; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @@ -44,7 +42,7 @@ protected Provider getBoundProvider() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/imm.cat")))); + return Providers.createWmmFromArch(() -> IMM); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") @@ -57,7 +55,7 @@ public static Iterable data() throws IOException { {"treiber", IMM, UNKNOWN}, {"treiber-CAS-relaxed", IMM, FAIL}, {"chase-lev", IMM, PASS}, - // These ones have an extra thief that violate the assertion + // These have an extra thief that violate the assertion {"chase-lev-fail", IMM, FAIL}, {"hash_table", IMM, PASS}, {"hash_table-fail", IMM, FAIL}, diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLocksTest.java index c42c25c00b..a339ae5b7c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLocksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMLocksTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.IMM; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @@ -40,7 +38,7 @@ protected long getTimeout() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/imm.cat")))); + return Providers.createWmmFromArch(() -> IMM); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMTest.java index 61fa53237c..7c7cad0b2c 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/IMMTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.IMM; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.FAIL; import static com.dat3m.dartagnan.utils.Result.PASS; @@ -41,7 +39,7 @@ protected long getTimeout() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/imm.cat")))); + return Providers.createWmmFromArch(() -> IMM); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LibvsyncTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LibvsyncTest.java index bcc78e5905..fa5522e28a 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LibvsyncTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LibvsyncTest.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; import org.junit.Test; @@ -12,16 +12,14 @@ import org.junit.runners.Parameterized; import org.sosy_lab.common.configuration.Configuration; -import java.io.File; import java.io.IOException; import java.util.Arrays; import java.util.EnumSet; import static com.dat3m.dartagnan.configuration.Arch.IMM; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; -import static com.dat3m.dartagnan.utils.Result.UNKNOWN; import static com.dat3m.dartagnan.utils.Result.PASS; +import static com.dat3m.dartagnan.utils.Result.UNKNOWN; import static org.junit.Assert.assertEquals; @RunWith(Parameterized.class) @@ -42,8 +40,8 @@ protected long getTimeout() { } @Override - protected Provider getConfigurationProvider() { - return Provider.fromSupplier(() -> Configuration.defaultConfiguration()); + protected Configuration getConfiguration(){ + return Configuration.defaultConfiguration(); } @Override @@ -53,7 +51,7 @@ protected Provider> getPropertyProvider() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/imm.cat")))); + return Providers.createWmmFromArch(() -> IMM); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java index 519b75fa9b..0ebd4ec7e5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java @@ -14,7 +14,6 @@ import java.util.EnumSet; import static com.dat3m.dartagnan.configuration.Arch.*; -import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @@ -25,11 +24,6 @@ public LivenessTest(String name, Arch target, Result expected) { super(name, target, expected); } - @Override - protected Provider getProgramPathProvider() { - return Provider.fromSupplier(() -> getTestResourcePath(name + ".ll")); - } - @Override protected long getTimeout() { return 60000; 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 5cc0a255d8..dc9d786fc6 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/MiscellaneousTest.java @@ -80,7 +80,8 @@ public static Iterable data() throws IOException { {"thread_loop", IMM, FAIL, 1}, {"thread_id", IMM, PASS, 1}, {"funcPtrInStaticMemory", IMM, PASS, 1}, - {"verifierAssert", ARM8, FAIL, 1} + {"verifierAssert", ARM8, FAIL, 1}, + {"uninitRead", IMM, FAIL, 1} }); } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LFDSTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LFDSTest.java index 330b2cc51b..64be766d93 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LFDSTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LFDSTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.C11; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @@ -44,7 +42,7 @@ protected Provider getBoundProvider() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/rc11.cat")))); + return Providers.createWmmFromName(() -> "rc11"); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") @@ -57,7 +55,7 @@ public static Iterable data() throws IOException { {"treiber", C11, UNKNOWN}, {"treiber-CAS-relaxed", C11, FAIL}, {"chase-lev", C11, PASS}, - // These ones have an extra thief that violate the assertion + // These have an extra thief that violate the assertion {"chase-lev-fail", C11, FAIL}, {"hash_table", C11, PASS}, {"hash_table-fail", C11, FAIL}, diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LocksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LocksTest.java index fd1186446b..00e05ae682 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LocksTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11LocksTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.C11; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.*; import static org.junit.Assert.assertEquals; @@ -40,7 +38,7 @@ protected long getTimeout() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/rc11.cat")))); + return Providers.createWmmFromName(() -> "rc11"); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11Test.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11Test.java index b4946186d4..c8f4e6ed77 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11Test.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/RC11Test.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.c; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.parsers.cat.ParserCat; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.rules.Provider; +import com.dat3m.dartagnan.utils.rules.Providers; import com.dat3m.dartagnan.verification.solving.AssumeSolver; import com.dat3m.dartagnan.verification.solving.RefinementSolver; import com.dat3m.dartagnan.wmm.Wmm; @@ -11,12 +11,10 @@ import org.junit.runner.RunWith; import org.junit.runners.Parameterized; -import java.io.File; import java.io.IOException; import java.util.Arrays; import static com.dat3m.dartagnan.configuration.Arch.C11; -import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; import static com.dat3m.dartagnan.utils.Result.FAIL; import static com.dat3m.dartagnan.utils.Result.PASS; @@ -41,7 +39,7 @@ protected long getTimeout() { @Override protected Provider getWmmProvider() { - return Provider.fromSupplier(() -> new ParserCat().parse(new File(getRootPath("cat/rc11.cat")))); + return Providers.createWmmFromName(() -> "rc11"); } @Parameterized.Parameters(name = "{index}: {0}, target={1}") diff --git a/dartagnan/src/test/resources/miscellaneous/uninitRead.ll b/dartagnan/src/test/resources/miscellaneous/uninitRead.ll new file mode 100644 index 0000000000..296b59fb88 --- /dev/null +++ b/dartagnan/src/test/resources/miscellaneous/uninitRead.ll @@ -0,0 +1,64 @@ +; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/output/uninitRead.ll' +source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/c/miscellaneous/uninitRead.c" +target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128" +target triple = "arm64-apple-macosx13.0.0" + +@array = dso_local global [10 x i32] zeroinitializer, align 4, !dbg !0 +@__func__.main = private unnamed_addr constant [5 x i8] c"main\00", align 1 +@.str = private unnamed_addr constant [13 x i8] c"uninitRead.c\00", align 1 +@.str.1 = private unnamed_addr constant [18 x i8] c"array[SIZE] == 42\00", align 1 + +; Function Attrs: noinline nounwind ssp uwtable +define dso_local i32 @main() #0 !dbg !21 { + %1 = load volatile i32, i32* getelementptr inbounds ([10 x i32], [10 x i32]* @array, i64 1, i64 0), align 4, !dbg !24 + %2 = icmp eq i32 %1, 42, !dbg !24 + %3 = xor i1 %2, true, !dbg !24 + %4 = zext i1 %3 to i32, !dbg !24 + %5 = sext i32 %4 to i64, !dbg !24 + br i1 %3, label %6, label %7, !dbg !24 + +6: ; preds = %0 + call void @__assert_rtn(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @__func__.main, i64 0, i64 0), i8* getelementptr inbounds ([13 x i8], [13 x i8]* @.str, i64 0, i64 0), i32 15, i8* getelementptr inbounds ([18 x i8], [18 x i8]* @.str.1, i64 0, i64 0)) #2, !dbg !24 + unreachable, !dbg !24 + +7: ; preds = %0 + ret i32 0, !dbg !25 +} + +; Function Attrs: cold noreturn +declare void @__assert_rtn(i8*, i8*, i32, i8*) #1 + +attributes #0 = { noinline nounwind ssp uwtable "disable-tail-calls"="false" "frame-pointer"="non-leaf" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-a12" "target-features"="+aes,+crc,+crypto,+fp-armv8,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.3a,+zcm,+zcz" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #1 = { cold noreturn "disable-tail-calls"="true" "frame-pointer"="non-leaf" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-a12" "target-features"="+aes,+crc,+crypto,+fp-armv8,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.3a,+zcm,+zcz" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #2 = { cold noreturn } + +!llvm.dbg.cu = !{!2} +!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18, !19} +!llvm.ident = !{!20} + +!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression()) +!1 = distinct !DIGlobalVariable(name: "array", scope: !2, file: !6, line: 11, type: !7, isLocal: false, isDefinition: true) +!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 12.0.1", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, enums: !4, globals: !5, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk") +!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/c/miscellaneous/uninitRead.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!4 = !{} +!5 = !{!0} +!6 = !DIFile(filename: "benchmarks/c/miscellaneous/uninitRead.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M") +!7 = !DICompositeType(tag: DW_TAG_array_type, baseType: !8, size: 320, elements: !10) +!8 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !9) +!9 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!10 = !{!11} +!11 = !DISubrange(count: 10) +!12 = !{i32 7, !"Dwarf Version", i32 4} +!13 = !{i32 2, !"Debug Info Version", i32 3} +!14 = !{i32 1, !"wchar_size", i32 4} +!15 = !{i32 1, !"branch-target-enforcement", i32 0} +!16 = !{i32 1, !"sign-return-address", i32 0} +!17 = !{i32 1, !"sign-return-address-all", i32 0} +!18 = !{i32 1, !"sign-return-address-with-bkey", i32 0} +!19 = !{i32 7, !"PIC Level", i32 2} +!20 = !{!"Homebrew clang version 12.0.1"} +!21 = distinct !DISubprogram(name: "main", scope: !6, file: !6, line: 13, type: !22, scopeLine: 14, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !4) +!22 = !DISubroutineType(types: !23) +!23 = !{!9} +!24 = !DILocation(line: 15, column: 5, scope: !21) +!25 = !DILocation(line: 16, column: 5, scope: !21)