Merge branch 'development_rework' into llvm-grammar0

# Conflicts:
#	dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
#	dartagnan/src/main/java/com/dat3m/dartagnan/program/Register.java
#	dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java
#	dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/Return.java
#	dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IntrinsicsInlining.java
#	dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
#	dartagnan/src/test/java/com/dat3m/dartagnan/exceptions/ExceptionsTest.java

README.md

@@ -45,7 +45,7 @@ At least the following compiler flag needs to be set, further can be added (only
 ```
 export CFLAGS="-I$DAT3M_HOME/include"
 export SMACK_FLAGS="-q -t --no-memory-splitting"
-export ATOMIC_REPLACE_OPTS="-mem2reg -sroa -early-cse -indvars -loop-unroll -simplifycfg -gvn"
+export ATOMIC_REPLACE_OPTS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn"
 ```
 
 If you are verifying C code, be sure both `clang` and `smack` are in your `PATH`.

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/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();

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java

@@ -23,9 +23,10 @@
 import com.dat3m.dartagnan.program.memory.Memory;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.program.memory.VirtualMemoryObject;
-import com.dat3m.dartagnan.program.processing.EventIdReassignment;
+import com.dat3m.dartagnan.program.processing.IdReassignment;
 import com.dat3m.dartagnan.program.specification.AbstractAssert;
 import com.google.common.base.Verify;
+import com.google.common.collect.Iterables;
 
 import java.util.*;
 
@@ -74,8 +75,12 @@ public Program build() {
 
     public static void processAfterParsing(Program program) {
         program.getFunctions().forEach(Function::validate);
-        EventIdReassignment.newInstance().run(program);
-        program.getEvents().forEach(e -> e.setMetadata(new OriginalId(e.getGlobalId())));
+        IdReassignment.newInstance().run(program);
+        for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) {
+            if (func.hasBody()) {
+                func.getEvents().forEach(e -> e.setMetadata(new OriginalId(e.getGlobalId())));
+            }
+        }
     }
 
     // ----------------------------------------------------------------------------------------------------------------

dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java

@@ -62,11 +62,15 @@ public Type getType() {
 
     public String getName() { return this.name; }
     public void setName(String name) { this.name = name; }
+
     public FunctionType getFunctionType() { return this.functionType; }
     public List<Register> getParameterRegisters() {
         return Collections.unmodifiableList(parameterRegs);
     }
+
     public int getId() { return id; }
+    public void setId(int id) { this.id = id; }
+
     public Program getProgram() { return this.program; }
     public void setProgram(Program program) { this.program = program; }
 
@@ -185,4 +189,9 @@ public <T> T accept(ExpressionVisitor<T> visitor) {
     public IConst reduce() {
         throw new UnsupportedOperationException("Cannot reduce functions");
     }
+
+    // TODO: Ugly function, but we need it for now to create copies of functions.
+    public void copyDummyCountFrom(Function func) {
+        this.dummyCount = func.dummyCount;
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java

@@ -120,28 +120,17 @@ public Collection<INonDet> getConstants() {
         return Collections.unmodifiableCollection(constants);
     }
 
-    /**
-     * Iterates all events in this program.
-     *
-     * @return {@code cId}-ordered complete sequence of all events in this program.
-     */
-    public List<Event> getEvents() {
+    public List<Event> getThreadEvents() {
+        Preconditions.checkState(!threads.isEmpty(), "The program has no threads yet.");
         List<Event> events = new ArrayList<>();
-        for (Thread t : threads) {
-            events.addAll(t.getEvents());
+        for (Function func : threads) {
+            events.addAll(func.getEvents());
         }
         return events;
     }
 
-    /**
-     * Iterates a subset of events in this program.
-     *
-     * @param cls Class of events to be selected.
-     * @param <T> Desired subclass of {@link Event}.
-     * @return {@code cId}-ordered complete sequence of all events of class {@code cls} in this program.
-     */
-    public <T extends Event> List<T> getEvents(Class<T> cls) {
-        return getEvents().stream().filter(cls::isInstance).map(cls::cast).collect(Collectors.toList());
+    public <T extends Event> List<T> getThreadEvents(Class<T> cls) {
+        return getThreadEvents().stream().filter(cls::isInstance).map(cls::cast).collect(Collectors.toList());
     }
 
     // Unrolling

dartagnan/src/main/java/com/dat3m/dartagnan/program/Register.java

@@ -5,6 +5,7 @@
 import com.dat3m.dartagnan.expression.type.Type;
 import com.google.common.collect.ImmutableSet;
 
+import java.util.Objects;
 import java.util.Set;
 
 import static com.google.common.base.Preconditions.checkNotNull;
@@ -54,7 +55,7 @@ public String toString() {
 
     @Override
     public int hashCode() {
-        return name.hashCode() + function.hashCode();
+        return name.hashCode() + Objects.hashCode(function);
     }
 
     @Override

dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java

@@ -114,7 +114,7 @@ private void process(Thread thread, ExecutionAnalysis exec) {
                         writers = finalWriters.get(register);
                         checkArgument(writers != null,
                                 "Helper thread %s should be listed after their creator thread %s.",
-                                thread.getId(),
+                                thread,
                                 register.getFunction());
                         if (writers.may.size() != 1) {
                             logger.warn("Writers {} for inter-thread register {} read by event {} of thread {}",