Merge latest changes from rework (#498)

* Function passes & Thread creation after unrolling #492
* Thread cf & must edges #494
* Dynamic Pthread join #496

---------

Signed-off-by: Hernan Ponce de Leon <[email protected]>
Co-authored-by: Thomas Haas <[email protected]>
Co-authored-by: René Pascal Maseli <[email protected]>

benchmarks/c/miscellaneous/nondet_loop.c

@@ -1,9 +1,11 @@
 #include <stdint.h>
 #include <assert.h>
+#include <dat3m.h>
 
 int main()
 {
     int x = 0;
+    __VERIFIER_loop_bound(3);
     while (x != 5) {
         if (__VERIFIER_nondet_int() == 0) {
             x += 2;

benchmarks/c/miscellaneous/propagatableSideEffects.c

@@ -1,17 +1,23 @@
 #include <stdlib.h>
 #include <assert.h>
+#include <dat3m.h>
 
-// This test makes sure that we do not accidentally cut of side-effect-full loops
+// This test makes sure that we do not accidentally cut off side-effect-full loops
 // whose side-effects were propagated by constant propagation
 // Expected result: FAIL with B >= 3, UNKNOWN otherwise
 
-volatile int bound = 2; // To stop the compiler from optimising away our loop
+#ifndef B
+#define B 3
+#endif
+
+volatile int bound = B - 1; // To stop the compiler from optimising away our loop
 
 int main()
 {
 	int cnt = 0;
+	__VERIFIER_loop_bound(B);
 	while (cnt++ < bound) { }
-	assert (0); // FAIL, unless we cut of the loop too early
+	assert (0); // FAIL, unless we cut off the loop too early
 
 	return 0;
 }

benchmarks/c/miscellaneous/thread_chaining.c

@@ -5,7 +5,6 @@
     The test shows chaining of thread creations + parameter passing, i.e, the spawned thread
     spawns another thread and passes its argument to that one.
     Expected result: PASS
-    Current result: PASS
 */
 
 atomic_int data;

benchmarks/c/miscellaneous/thread_inlining.c

@@ -4,9 +4,6 @@
 /*
     The test checks if inlining of thread-creating functions works properly.
     Expected result: PASS
-    Current result:
-     - development: FAIL
-     - rework: Parsing error (matching between pthread_join and pthread_create fails)
 */
 
 atomic_int data;

benchmarks/c/miscellaneous/thread_inlining_complex.c

@@ -4,9 +4,6 @@
 /*
     The test checks if inlining of thread-creating functions + reassigning pthread_t variables works properly.
     Expected result: PASS
-    Current result:
-     - development: PASS
-     - rework: Parsing error (matching between pthread_join and pthread_create fails)
 */
 
 atomic_int data;

benchmarks/c/miscellaneous/thread_inlining_complex_2.c

@@ -4,9 +4,6 @@
 /*
     The test checks if inlining of thread-creating/joining functions + reassigning pthread_t variables works properly.
     Expected result: PASS
-    Current result:
-     - development: PASS
-     - rework: Parsing error (matching between pthread_join and pthread_create fails)
 */
 
 atomic_int data;

benchmarks/c/miscellaneous/thread_loop.c

@@ -0,0 +1,33 @@
+#include <pthread.h>
+#include <stdatomic.h>
+#include <dat3m.h>
+
+/*
+    The test shows thread creation inside loops
+    Expected result: FAIL
+*/
+
+#ifndef N
+#define N 5
+#endif
+
+atomic_int data;
+
+void *worker(void *arg)
+{
+   atomic_fetch_add(&data, 1);
+}
+
+int main()
+{
+    pthread_t t[N];
+    int bound = __VERIFIER_nondet_int();
+    __VERIFIER_assume(0 <= bound && bound < N);
+
+    __VERIFIER_loop_bound(N + 1);
+    for (int i = 0; i < bound; i++) {
+        pthread_create(&t[i], NULL, worker, NULL);
+    }
+
+    assert(data != N - 1);
+}

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -47,7 +47,7 @@
 import static com.dat3m.dartagnan.GlobalSettings.LogGlobalSettings;
 import static com.dat3m.dartagnan.configuration.OptionInfo.collectOptions;
 import static com.dat3m.dartagnan.configuration.OptionNames.PHANTOM_REFERENCES;
-import static com.dat3m.dartagnan.configuration.OptionNames.TARGET;;
+import static com.dat3m.dartagnan.configuration.OptionNames.TARGET;
 import static com.dat3m.dartagnan.configuration.Property.*;
 import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*;
 import static com.dat3m.dartagnan.utils.GitInfo.CreateGitInfo;
@@ -249,7 +249,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
                 printWarningIfThreadStartFailed(p, encCtx, prover);
                 if (props.contains(PROGRAM_SPEC) && FALSE.equals(model.evaluate(PROGRAM_SPEC.getSMTVariable(encCtx)))) {
                     summary.append("===== Program specification violation found =====\n");
-                    for(Event e : p.getEvents(Local.class)) {
+                    for(Event e : p.getThreadEvents(Local.class)) {
                         if(e.hasTag(Tag.ASSERTION) && TRUE.equals(model.evaluate(encCtx.execution(e)))) {
                             final String callStack = makeContextString(
                                     synContext.getContextInfo(e).getContextOfType(CallContext.class), " -> ");
@@ -265,7 +265,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
                 }
                 if (props.contains(LIVENESS) && FALSE.equals(model.evaluate(LIVENESS.getSMTVariable(encCtx)))) {
                     summary.append("============ Liveness violation found ============\n");
-                    for(CondJump e : p.getEvents(CondJump.class)) {
+                    for(CondJump e : p.getThreadEvents(CondJump.class)) {
                         if(e.hasTag(Tag.SPINLOOP) && TRUE.equals(model.evaluate(encCtx.execution(e)))
                             && TRUE.equals(model.evaluate(encCtx.jumpCondition(e)))) {
                             final String callStack = makeContextString(
@@ -350,7 +350,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
     }
 
     private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) throws SolverException {
-        for (Event e : p.getEvents()) {
+        for (Event e : p.getThreadEvents()) {
             if (e.hasTag(Tag.STARTLOAD) && BigInteger.ZERO.equals(prover.getModel().evaluate(encoder.value((Load) e)))) {
                 // This msg should be displayed even if the logging is off
                 System.out.printf(

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

@@ -343,11 +343,11 @@ private void initialize() {
                 }
             }
         } else {
-            for (Event e : verificationTask.getProgram().getEvents()) {
+            for (Event e : verificationTask.getProgram().getThreadEvents()) {
                 controlFlowVariables.put(e, booleanFormulaManager.makeVariable("cf " + e.getGlobalId()));
             }
         }
-        for (Event e : verificationTask.getProgram().getEvents()) {
+        for (Event e : verificationTask.getProgram().getThreadEvents()) {
             if (!e.cfImpliesExec()) {
                 executionVariables.put(e, booleanFormulaManager.makeVariable("exec " + e.getGlobalId()));
             }

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

@@ -312,7 +312,7 @@ public Formula visit(INonDet iNonDet) {
     @Override
     public Formula visit(Register reg) {
         String name = event == null ?
-                reg.getName() + "_" + reg.getFunctionId() + "_final" :
+                reg.getName() + "_" + reg.getFunction().getId() + "_final" :
                 reg.getName() + "(" + event.getGlobalId() + ")";
         Type type = reg.getType();
         return context.makeVariable(name, type);

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

@@ -10,6 +10,7 @@
 import com.dat3m.dartagnan.program.event.core.CondJump;
 import com.dat3m.dartagnan.program.event.core.Event;
 import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
 import com.dat3m.dartagnan.program.event.core.utils.RegWriter;
 import com.dat3m.dartagnan.program.memory.Memory;
 import com.google.common.base.Preconditions;
@@ -21,7 +22,9 @@
 import org.sosy_lab.java_smt.api.*;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
 
 import static com.dat3m.dartagnan.GlobalSettings.getArchPrecision;
 import static com.dat3m.dartagnan.configuration.OptionNames.INITIALIZE_REGISTERS;
@@ -109,23 +112,30 @@ public BooleanFormula encodeControlFlow() {
 
     private BooleanFormula encodeThreadCF(Thread thread) {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
-
-        Map<Label, Set<CondJump>> labelJumpMap = new HashMap<>();
-        Event pred = null;
+        final ThreadStart startEvent = thread.getEntry();
         final List<BooleanFormula> enc = new ArrayList<>();
-        for(Event e : thread.getEntry().getSuccessors()) {
+
+        final BooleanFormula cfStart = context.controlFlow(startEvent);
+        if (startEvent.getCreator() == null) {
+            enc.add(cfStart);
+        } else if (startEvent.mayFailSpuriously()) {
+            enc.add(bmgr.implication(cfStart, context.execution(startEvent.getCreator())));
+        } else {
+            enc.add(bmgr.equivalence(cfStart, context.execution(startEvent.getCreator())));
+        }
+        enc.add(startEvent.encodeExec(context));
+
+        Event pred = startEvent;
+        for(Event e : startEvent.getSuccessor().getSuccessors()) {
             // Immediate control flow
-            BooleanFormula cfCond = pred == null ? bmgr.makeTrue() : context.controlFlow(pred);
+            BooleanFormula cfCond = context.controlFlow(pred);
             if (pred instanceof CondJump jump) {
                 cfCond = bmgr.and(cfCond, bmgr.not(context.jumpCondition(jump)));
-                // NOTE: we need to register the actual jumps here, because the
-                // listener sets of labels is too large (it contains old copies)
-                labelJumpMap.computeIfAbsent(jump.getLabel(), key -> new HashSet<>()).add(jump);
             }
 
             // Control flow via jumps
-            if (e instanceof Label) {
-                for (CondJump jump : labelJumpMap.getOrDefault(e, Collections.emptySet())) {
+            if (e instanceof Label label) {
+                for (CondJump jump : label.getJumpSet()) {
                     cfCond = bmgr.or(cfCond, bmgr.and(context.controlFlow(jump), context.jumpCondition(jump)));
                 }
             }
@@ -145,7 +155,7 @@ public BooleanFormula encodeMemory() {
         // For all objects, their 'final' value fetched here represents their constant value.
         BooleanFormula[] addrExprs;
         if(getArchPrecision() > -1) {
-        	final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+            final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
             addrExprs = memory.getObjects().stream()
                     .map(addr -> bvmgr.equal((BitvectorFormula) context.encodeFinalExpression(addr),
                     		bvmgr.makeBitvector(getArchPrecision(), addr.getValue().intValue())))
@@ -154,7 +164,7 @@ public BooleanFormula encodeMemory() {
             final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
             addrExprs = memory.getObjects().stream()
                     .map(addr -> imgr.equal((IntegerFormula) context.encodeFinalExpression(addr),
-                    		imgr.makeNumber(addr.getValue().intValue())))
+                            imgr.makeNumber(addr.getValue().intValue())))
                     .toArray(BooleanFormula[]::new);        	
         }
         return fmgr.getBooleanFormulaManager().and(addrExprs);
@@ -209,9 +219,9 @@ public BooleanFormula encodeDependencies() {
     }
 
     public BooleanFormula encodeFilter() {
-    	return context.getTask().getProgram().getFilterSpecification() != null ?
+        return context.getTask().getProgram().getFilterSpecification() != null ?
                 context.getTask().getProgram().getFilterSpecification().encode(context) :
-    			context.getBooleanFormulaManager().makeTrue();
+                context.getBooleanFormulaManager().makeTrue();
     }
 
     public BooleanFormula encodeFinalRegisterValues() {

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

@@ -91,7 +91,7 @@ public static PropertyEncoder withContext(EncodingContext context) throws Invali
     public BooleanFormula encodeBoundEventExec() {
         logger.info("Encoding bound events execution");
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
-        return program.getEvents()
+        return program.getThreadEvents()
                 .stream().filter(e -> e.hasTag(Tag.BOUND)).map(context::execution).reduce(bmgr.makeFalse(), bmgr::or);
     }
 
@@ -163,7 +163,7 @@ private BooleanFormula encodeLastCoConstraints() {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         final EncodingContext.EdgeEncoder coEncoder = context.edge(co);
         final RelationAnalysis.Knowledge knowledge = ra.getKnowledge(co);
-        final List<Init> initEvents = program.getEvents(Init.class);
+        final List<Init> initEvents = program.getThreadEvents(Init.class);
         final boolean doEncodeFinalAddressValues = program.getFormat() == LITMUS;
         // Find transitively implied coherences. We can use these to reduce the encoding.
         final Set<Tuple> transCo = ra.findTransitivelyImpliedCo(co);
@@ -175,7 +175,7 @@ private BooleanFormula encodeLastCoConstraints() {
         // ---- Construct encoding ----
         List<BooleanFormula> enc = new ArrayList<>();
         final Function<Event, Collection<Tuple>> out = knowledge.getMayOut();
-        for (Store w1 : program.getEvents(Store.class)) {
+        for (Store w1 : program.getThreadEvents(Store.class)) {
             if (dominatedWrites.contains(w1)) {
                 enc.add(bmgr.not(lastCoVar(w1)));
                 continue;
@@ -212,12 +212,12 @@ private BooleanFormula encodeLastCoConstraints() {
             // but the final value of a location should always match that of some coLast event.
             // lastCo(w) => (lastVal(w.address) = w.val)
             //           \/ (exists w2 : lastCo(w2) /\ lastVal(w.address) = w2.val))
-            for (Init init : program.getEvents(Init.class)) {
+            for (Init init : program.getThreadEvents(Init.class)) {
                 BooleanFormula lastValueEnc = bmgr.makeFalse();
                 BooleanFormula lastStoreExistsEnc = bmgr.makeFalse();
                 Formula v2 = ExpressionEncoder.getLastMemValueExpr(init.getBase(), init.getOffset(), fmgr);
                 BooleanFormula readFromInit = context.equal(context.value(init), v2);
-                for (Store w : program.getEvents(Store.class)) {
+                for (Store w : program.getThreadEvents(Store.class)) {
                     if (!alias.mayAlias(w, init)) {
                         continue;
                     }
@@ -485,22 +485,22 @@ private BooleanFormula generateStucknessEncoding(List<SpinIteration> loops, Enco
         }
 
         private List<SpinIteration> findSpinLoopsInThread(Thread thread, LoopAnalysis loopAnalysis) {
-            final List<LoopAnalysis.LoopInfo> loops = loopAnalysis.getLoopsOfThread(thread);
+            final List<LoopAnalysis.LoopInfo> loops = loopAnalysis.getLoopsOfFunction(thread);
             final List<SpinIteration> spinIterations = new ArrayList<>();
 
             for (LoopAnalysis.LoopInfo loop : loops) {
-                for (LoopAnalysis.LoopIterationInfo iter : loop.getIterations()) {
+                for (LoopAnalysis.LoopIterationInfo iter : loop.iterations()) {
                     final List<Event> iterBody = iter.computeBody();
                     final List<CondJump> spinningJumps = iterBody.stream()
                             .filter(e -> e instanceof CondJump && e.hasTag(Tag.SPINLOOP))
                             .map(CondJump.class::cast)
-                            .collect(Collectors.toList());
+                            .toList();
 
                     if (!spinningJumps.isEmpty()) {
                         final List<Load> loads = iterBody.stream()
                                 .filter(Load.class::isInstance)
                                 .map(Load.class::cast)
-                                .collect(Collectors.toList());
+                                .toList();
 
                         final SpinIteration spinIter = new SpinIteration();
                         spinIter.spinningJumps.addAll(spinningJumps);

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

@@ -349,7 +349,7 @@ public Void visitInverse(Relation rel, Relation r1) {
         @Override
         public Void visitFences(Relation rel, Filter fenceSet) {
             final RelationAnalysis.Knowledge k = ra.getKnowledge(rel);
-            List<Event> fences = program.getEvents().stream().filter(fenceSet::apply).collect(toList());
+            List<Event> fences = program.getThreadEvents().stream().filter(fenceSet::apply).collect(toList());
             EncodingContext.EdgeEncoder encoder = context.edge(rel);
             for (Tuple tuple : encodeSets.get(rel)) {
                 Event e1 = tuple.getFirst();
@@ -434,7 +434,7 @@ public Void visitReadModifyWrites(Relation rmw) {
             final Function<Event, Collection<Tuple>> mayOut = k.getMayOut();
 
             // ----------  Encode matching for LL/SC-type RMWs ----------
-            for (RMWStoreExclusive store : program.getEvents(RMWStoreExclusive.class)) {
+            for (RMWStoreExclusive store : program.getThreadEvents(RMWStoreExclusive.class)) {
                 BooleanFormula storeExec = bmgr.makeFalse();
                 for (Tuple t : mayIn.apply(store)) {
                     MemoryCoreEvent load = (MemoryCoreEvent) t.getFirst();
@@ -548,7 +548,7 @@ public Void visitReadFrom(Relation rf) {
         @Override
         public Void visitCoherence(Relation co) {
             boolean idl = !context.useSATEncoding;
-            List<MemoryCoreEvent> allWrites = program.getEvents(MemoryCoreEvent.class).stream()
+            List<MemoryCoreEvent> allWrites = program.getThreadEvents(MemoryCoreEvent.class).stream()
                     .filter(e -> e.hasTag(WRITE))
                     .sorted(Comparator.comparingInt(Event::getGlobalId))
                     .toList();
@@ -638,7 +638,7 @@ public Void visitSyncBarrier(Relation rel) {
         @Override
         public Void visitSyncFence(Relation syncFence) {
             boolean idl = !context.useSATEncoding;
-            List<Fence> allFenceSC = program.getEvents(Fence.class).stream()
+            List<Fence> allFenceSC = program.getThreadEvents(Fence.class).stream()
                     .filter(e -> e.hasTag(Tag.PTX.SC))
                     .sorted(Comparator.comparingInt(Event::getGlobalId))
                     .toList();