Various fixes/cleanup

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/PthreadsProcedures.java

@@ -15,12 +15,15 @@ public static boolean handlePthreadsFunctions(VisitorBoogie visitor, Call_cmdCon
             case "pthread_cond_wait":
             case "pthread_cond_signal":
             case "pthread_cond_broadcast":
-            case "pthread_exit":
             case "pthread_mutex_destroy":
                 // TODO: These are skipped for now
                 VisitorBoogie.logger.warn(
                         "Skipped call to {} because the function is not supported right now.", funcName);
                 return true;
+            case "pthread_exit":
+                final Expression retVal = (Expression) ctx.call_params().exprs().expr(0).accept(visitor);
+                visitor.addEvent(EventFactory.newFunctionReturn(retVal));
+                return true;
             case "pthread_mutex_init":
                 mutexInit(visitor, ctx);
                 return true;

dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java

@@ -173,6 +173,9 @@ private void visitDeclarations(MainContext ctx) {
         for (Func_declContext funDecContext : ctx.func_decl()) {
             registerBoogieFunction(funDecContext);
         }
+        for (Proc_declContext procDecContext : ctx.proc_decl()) {
+            registerProcedure(procDecContext);
+        }
         for (Const_declContext constDecContext : ctx.const_decl()) {
             registerConstants(constDecContext);
         }
@@ -182,9 +185,6 @@ private void visitDeclarations(MainContext ctx) {
         for (Var_declContext varDecContext : ctx.var_decl()) {
             visitVar_decl(varDecContext);
         }
-        for (Proc_declContext procDecContext : ctx.proc_decl()) {
-            registerProcedure(procDecContext);
-        }
 
         //FIXME: Some Svcomp loop benchmarks reference declared but unassigned constants!?
         // Those should probably be non-deterministic, but we set them to zero here to match our previous semantics.

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

@@ -3,8 +3,8 @@
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.event.core.Event;
-import com.dat3m.dartagnan.program.event.core.annotations.FunCall;
-import com.dat3m.dartagnan.program.event.core.annotations.FunRet;
+import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker;
+import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker;
 import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Iterables;
@@ -66,15 +66,15 @@ public String toString() {
     }
 
     public static class CallContext implements Context {
-        private final FunCall funCall;
+        private final FunCallMarker funCallMarker;
 
-        private CallContext(FunCall funCall) { this.funCall = funCall; }
+        private CallContext(FunCallMarker funCallMarker) { this.funCallMarker = funCallMarker; }
 
-        public FunCall getFunctionCall() { return this.funCall; }
+        public FunCallMarker getFunctionCall() { return this.funCallMarker; }
 
         @Override
         public String toString() {
-            return String.format("%s %s", funCall.getFunctionName(), getSourceLocationString(funCall));
+            return String.format("%s %s", funCallMarker.getFunctionName(), getSourceLocationString(funCallMarker));
         }
     }
 
@@ -161,9 +161,9 @@ private void run(Thread thread, LoopAnalysis loops) {
             infoMap.put(ev, new Info(ev, copyOfCurContextStack));
             // TODO: The above could be made more efficient by sharing unchanged context
 
-            if (ev instanceof FunCall fc) {
+            if (ev instanceof FunCallMarker fc) {
                 curContextStack.push(new CallContext(fc));
-            } else if (ev instanceof FunRet) {
+            } else if (ev instanceof FunReturnMarker) {
                 assert curContextStack.peek() instanceof CallContext;
                 curContextStack.pop();
             }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java

@@ -14,8 +14,8 @@
 import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp;
 import com.dat3m.dartagnan.program.event.arch.tso.TSOXchg;
 import com.dat3m.dartagnan.program.event.core.*;
-import com.dat3m.dartagnan.program.event.core.annotations.FunCall;
-import com.dat3m.dartagnan.program.event.core.annotations.FunRet;
+import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker;
+import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker;
 import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation;
 import com.dat3m.dartagnan.program.event.core.rmw.RMWStore;
 import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive;
@@ -145,12 +145,12 @@ public static Skip newSkip() {
         return new Skip();
     }
 
-    public static FunCall newFunctionCall(String funName) {
-        return new FunCall(funName);
+    public static FunCallMarker newFunctionCallMarker(String funName) {
+        return new FunCallMarker(funName);
     }
 
-    public static FunRet newFunctionReturn(String funName) {
-        return new FunRet(funName);
+    public static FunReturnMarker newFunctionReturnMarker(String funName) {
+        return new FunReturnMarker(funName);
     }
 
     public static StringAnnotation newStringAnnotation(String annotation) {

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java

@@ -14,7 +14,7 @@ public FenceBase(String name, String mo) {
         this.mo = mo;
         this.addTags(Tag.VISIBLE, Tag.FENCE);
         if (mo != null && !mo.isEmpty()) {
-            this.tags.add(mo);
+            addTags(mo);
         }
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java

@@ -17,14 +17,15 @@
 
 public abstract class AbstractEvent implements Event {
 
-    protected final MetadataMap metadataMap = new MetadataMap();
-    protected final Set<String> tags;
-    protected Function function; // The thread this event belongs to
+    private final MetadataMap metadataMap = new MetadataMap();
+    private final Set<String> tags;
+    private final Set<EventUser> currentUsers = new HashSet<>();
     // This id is dynamically changing during processing.
-    protected transient int globalId = -1; // (Global) ID within a program
+    private transient int globalId = -1; // (Global) ID within a program
+
+    private transient Function function; // The function this event belongs to
     private transient AbstractEvent successor;
     private transient AbstractEvent predecessor;
-    private final Set<EventUser> currentUsers = new HashSet<>();
 
     protected AbstractEvent() {
         tags = new HashSet<>();
@@ -33,7 +34,6 @@ protected AbstractEvent() {
     protected AbstractEvent(AbstractEvent other) {
         copyAllMetadataFrom(other);
         this.tags = other.tags; // TODO: Dangerous code! A Copy-on-Write Set should be used (e.g. PersistentSet/Map)
-        this.function = other.function;
     }
 
     @Override
@@ -68,8 +68,7 @@ public Thread getThread() {
     @Override
     public void replaceAllUsages(Event replacement) {
         final Map<Event, Event> replacementMap = Map.of(this, replacement);
-
-        new ArrayList<>(getUsers()).forEach(e -> e.updateReferences(replacementMap));
+        List.copyOf(getUsers()).forEach(e -> e.updateReferences(replacementMap));
     }
 
     // ============================================ Metadata ============================================

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java

@@ -1,6 +1,7 @@
 package com.dat3m.dartagnan.program.event.core;
 
 import com.dat3m.dartagnan.encoding.EncodingContext;
+import com.dat3m.dartagnan.expression.type.BooleanType;
 import com.dat3m.dartagnan.expression.type.IntegerType;
 import com.dat3m.dartagnan.expression.type.Type;
 import com.dat3m.dartagnan.program.Register;
@@ -55,31 +56,36 @@ public boolean doesTrackDep() {
 
     @Override
     public String defaultString() {
-        return register + " <- status(" + event.toString() + ")";
+        return register + " <- not_exec(" + event + ")";
     }
 
     @Override
     public BooleanFormula encodeExec(EncodingContext context) {
-        FormulaManager formulaManager = context.getFormulaManager();
-        BooleanFormulaManager booleanFormulaManager = context.getBooleanFormulaManager();
-        Type type = register.getType();
-        BooleanFormula eventExecuted = context.execution(event);
-        Formula result = context.result(this);
+        final FormulaManager fmgr = context.getFormulaManager();
+        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
+        final Type type = register.getType();
+        final BooleanFormula eventExecuted = context.execution(event);
+        final Formula result = context.result(this);
+
         if (type instanceof IntegerType integerType) {
-            Formula one;
+            final Formula one;
             if (integerType.isMathematical()) {
-                IntegerFormulaManager integerFormulaManager = formulaManager.getIntegerFormulaManager();
+                IntegerFormulaManager integerFormulaManager = fmgr.getIntegerFormulaManager();
                 one = integerFormulaManager.makeNumber(1);
             } else {
-                BitvectorFormulaManager bitvectorFormulaManager = formulaManager.getBitvectorFormulaManager();
+                BitvectorFormulaManager bitvectorFormulaManager = fmgr.getBitvectorFormulaManager();
                 int bitWidth = integerType.getBitWidth();
                 one = bitvectorFormulaManager.makeBitvector(bitWidth, 1);
             }
-            return booleanFormulaManager.and(super.encodeExec(context),
-                    booleanFormulaManager.implication(eventExecuted,
-                            context.equalZero(result)),
-                    booleanFormulaManager.or(eventExecuted,
-                            context.equal(result, one)));
+            return bmgr.and(super.encodeExec(context),
+                    bmgr.ifThenElse(eventExecuted, context.equalZero(result), context.equal(result, one))
+            );
+        } else if (type instanceof BooleanType) {
+            //TODO: We have "result == not exec(event)", because we use 0/false for executed events.
+            // The reason is that ExecutionStatus follows the behavior of Store-Conditionals on hardware.
+            // However, this is very counterintuitive and I think we should return 1/true on success and instead
+            // change the compilation of Store-Conditional to invert the value.
+            return bmgr.and(super.encodeExec(context), context.equal(result, bmgr.not(eventExecuted)));
         }
         throw new UnsupportedOperationException(String.format("Encoding ExecutionStatus on type %s.", type));
     }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCall.java → dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunCallMarker.java

@@ -1,15 +1,15 @@
 package com.dat3m.dartagnan.program.event.core.annotations;
 
-public class FunCall extends StringAnnotation {
+public class FunCallMarker extends StringAnnotation {
 
     private final String funName;
 
-    public FunCall(String funName) {
+    public FunCallMarker(String funName) {
         super("=== Calling " + funName + " ===");
         this.funName = funName;
     }
 
-    protected FunCall(FunCall other) {
+    protected FunCallMarker(FunCallMarker other) {
         super(other);
         this.funName = other.funName;
     }
@@ -19,7 +19,7 @@ public String getFunctionName() {
     }
 
     @Override
-    public FunCall getCopy() {
-        return new FunCall(this);
+    public FunCallMarker getCopy() {
+        return new FunCallMarker(this);
     }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunRet.java → dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/FunReturnMarker.java

@@ -1,15 +1,15 @@
 package com.dat3m.dartagnan.program.event.core.annotations;
 
-public class FunRet extends StringAnnotation {
+public class FunReturnMarker extends StringAnnotation {
 
     private final String funName;
 
-    public FunRet(String funName) {
+    public FunReturnMarker(String funName) {
         super("=== Returning from " + funName + " ===");
         this.funName = funName;
     }
 
-    protected FunRet(FunRet other) {
+    protected FunReturnMarker(FunReturnMarker other) {
         super(other);
         this.funName = other.funName;
     }
@@ -19,7 +19,7 @@ public String getFunctionName() {
     }
 
     @Override
-    public FunRet getCopy() {
-        return new FunRet(this);
+    public FunReturnMarker getCopy() {
+        return new FunReturnMarker(this);
     }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/DirectFunctionCall.java

@@ -32,6 +32,7 @@ protected DirectFunctionCall(Function func, List<Expression> arguments) {
     }
 
     protected DirectFunctionCall(DirectFunctionCall other) {
+        super(other);
         this.callTarget = other.callTarget;
         this.arguments = new ArrayList<>(other.arguments);
     }

dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java

@@ -49,7 +49,7 @@ public List<Event> getBlock() {
     public void runLocalAnalysis(Program program, Context context) {
         //===== Temporary fix to rematch atomic blocks correctly =====
         BranchEquivalence eq = context.requires(BranchEquivalence.class);
-        List<Event> begins = this.function.getEvents()
+        List<Event> begins = this.getFunction().getEvents()
                 .stream().filter(x -> x instanceof BeginAtomic && eq.isReachableFrom(x, this))
                 .toList();
         this.begin = (BeginAtomic) begins.get(begins.size() - 1);

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java

@@ -2,7 +2,7 @@
 
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.ExpressionFactory;
-import com.dat3m.dartagnan.expression.type.IntegerType;
+import com.dat3m.dartagnan.expression.type.Type;
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Register;
@@ -122,23 +122,20 @@ private void insertSideEffectChecks(IterationData iter) {
         final List<Event> sideEffects = iter.sideEffects;
 
         final List<Register> trackingRegs = new ArrayList<>();
+        final Type type = TypeFactory.getInstance().getBooleanType();
         Event insertionPoint = iterInfo.getIterationEnd();
-        IntegerType type = TypeFactory.getInstance().getArchType();
         for (int i = 0; i < sideEffects.size(); i++) {
             final Event sideEffect = sideEffects.get(i);
-            final Register trackingReg = thread.newRegister(
-                    String.format("Loop%s_%s_%s", loopNumber, iterNumber, i),
-                    type);
+            final Register trackingReg = thread.newRegister(String.format("Loop%s_%s_%s", loopNumber, iterNumber, i), type);
             trackingRegs.add(trackingReg);
 
             final Event execCheck = EventFactory.newExecutionStatus(trackingReg, sideEffect);
             insertionPoint.insertAfter(execCheck);
             insertionPoint = execCheck;
         }
 
-        ExpressionFactory expressionFactory = ExpressionFactory.getInstance();
+        final ExpressionFactory expressionFactory = ExpressionFactory.getInstance();
         final Expression atLeastOneSideEffect = trackingRegs.stream()
-                .map(expressionFactory::makeBooleanCast)
                 .map(expressionFactory::makeNot)
                 .reduce(expressionFactory.makeFalse(), expressionFactory::makeOr);
         final CondJump assumeSideEffect = EventFactory.newJumpUnless(atLeastOneSideEffect, (Label) thread.getExit());

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java

@@ -82,8 +82,12 @@ private void inlineAllCalls(Function function) {
                             String.format("Cannot call thread %s directly.",
                                     call.getCallTarget()));
                 }
-                call.getPredecessor().insertAfter(EventFactory.newFunctionCall(callTarget.getName()));
-                call.insertAfter(EventFactory.newFunctionReturn(callTarget.getName()));
+                final Event callMarker = EventFactory.newFunctionCallMarker(callTarget.getName());
+                final Event returnMarker = EventFactory.newFunctionReturnMarker(callTarget.getName());
+                callMarker.copyAllMetadataFrom(call);
+                returnMarker.copyAllMetadataFrom(call);
+                call.getPredecessor().insertAfter(callMarker);
+                call.insertAfter(returnMarker);
                 // Calls with result will write the return value to this register.
                 Register result = call instanceof DirectValueFunctionCall c ? c.getResultRegister() : null;
                 inlineBodyAfterCall(call, result, call.getArguments(), callTarget, ++scopeCounter);

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogProgramStatistics.java

@@ -39,11 +39,6 @@ public void run(Program program) {
         }
 
         int numNonInitThreads = (int)program.getThreads().stream().filter(t -> !(t.getEntry() instanceof Init)).count();
-        if (program.getFormat() == Program.SourceLanguage.BOOGIE) {
-            numNonInitThreads--; // We subtract 1, because for Boogie code we always create an extra empty thread
-            // TODO: Why do we do this?
-        }
-
         int staticAddressSpaceSize = program.getMemory().getObjects().stream()
                 .filter(MemoryObject::isStaticallyAllocated).mapToInt(MemoryObject::size).sum();
         int dynamicAddressSpaceSize = program.getMemory().getObjects().stream()

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java

@@ -86,10 +86,10 @@ private void createInitEvents(Program program) {
         int nextThreadId = threads.get(threads.size() - 1).getId() + 1;
         for(MemoryObject memObj : program.getMemory().getObjects()) {
             // The last case "heuristically checks" if Smack generated initialization or not:
-            // we expect at least every 8 bytes to be initialized.
+            // if any field is statically initialized, then likely everything is initialized.
             final boolean isStaticallyInitialized = !isLitmus
                     && memObj.isStaticallyAllocated()
-                    && (memObj.getStaticallyInitializedFields().size() >= memObj.size() / 8);
+                    && memObj.getStaticallyInitializedFields().size() > 1;
             final Iterable<Integer> fieldsToInit = isStaticallyInitialized ?
                     memObj.getStaticallyInitializedFields() : IntStream.range(0, memObj.size()).boxed()::iterator;