Version 4.3.1 (hernanponcedeleon#954)

This PR adds several changes related to SVCOMP 2026

- minor fixes (witness generation for data-races, UBSAN instrumentation options, removed unsound intrinsic)
- support for the mem-track property
- fix missing calls to TSS destructors
---------

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Co-authored-by: René Maseli <r.maseli@tu-bs.de>

Author: 3 people

benchmarks/miscellaneous/pthread.c

@@ -402,7 +402,7 @@ void key_test()
     status = pthread_key_delete(local_data);
     assert(status == 0);
 
-    //assert(pthread_equal(latest_thread, worker));//TODO add support for destructors
+    assert(pthread_equal(latest_thread, worker));
 }
 
 // -------- detaching threads
@@ -455,9 +455,11 @@ void detach_test()
 
 int main()
 {
-    mutex_test();
-    cond_test();
-    rwlock_test();
-    key_test();
-    detach_test();
+    switch (__VERIFIER_nondet_int()) {
+        case 1: mutex_test(); break;
+        case 2: cond_test(); break;
+        case 3: rwlock_test(); break;
+        case 4: key_test(); break;
+        case 5: detach_test(); break;
+    }
 }

benchmarks/mixed/memtrack1-fail.c

@@ -0,0 +1,8 @@
+#include <stdlib.h>
+int* volatile m_global;
+int main()
+{
+  m_global = (int*) malloc(sizeof(int));
+  *((char volatile*) &m_global) = '\0';
+  return 0;
+}

benchmarks/mixed/memtrack2-pass.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+int* volatile m_global;
+int main()
+{
+  m_global = (int*) malloc(sizeof(int));
+  int* temp = m_global;
+  *((char volatile*) &m_global) = '\0';
+  m_global = temp;
+  return 0;
+}

benchmarks/mixed/memtrack3-pass.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+int* volatile m_global;
+int main()
+{
+  m_global = (int*) malloc(sizeof(int));
+  int* temp = m_global;
+  *((char volatile*) &m_global) = '\0';
+  free(temp);
+  return 0;
+}

dartagnan/pom.xml

@@ -5,7 +5,7 @@
     <parent>
         <groupId>com.dat3m</groupId>
         <artifactId>dat3m</artifactId>
-        <version>4.3.0</version>
+        <version>4.3.1</version>
     </parent>
     <artifactId>dartagnan</artifactId>
     <packaging>jar</packaging>

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

@@ -19,6 +19,7 @@
 import com.dat3m.dartagnan.program.event.Tag;
 import com.dat3m.dartagnan.program.event.core.Assert;
 import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.program.processing.LoopUnrolling;
 import com.dat3m.dartagnan.program.Entrypoint;
 import com.dat3m.dartagnan.utils.ExitCode;
@@ -316,7 +317,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme
         // ------------------ Generate Witness, if possible ------------------
         final EnumSet<Property> properties = task.getProperty();
         if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel()
-                && (properties.contains(PROGRAM_SPEC) || properties.contains(DATARACEFREEDOM)) && properties.size() == 1
+                && (properties.contains(PROGRAM_SPEC) || properties.contains(DATARACEFREEDOM))
                 && modelChecker.getResult() != UNKNOWN) {
             try {
                 WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover,
@@ -362,14 +363,7 @@ private static ResultSummary summaryFromResult(VerificationTask task, ModelCheck
                     .stream().filter(model::assertionViolated)
                     .toList();
                 for (Assert ass : violations) {
-                    final String callStack = makeContextString(synContext.getContextInfo(ass).getContextOfType(CallContext.class), " -> ");
-                    details
-                            .append("\tE").append(ass.getGlobalId())
-                            .append(":\t")
-                            .append(callStack.isEmpty() ? callStack : callStack + " -> ")
-                            .append(getSourceLocationString(ass))
-                            .append(": ").append(ass.getErrorMessage())
-                            .append("\n");
+                    appendTo(details, ass, synContext);
                 }
                 // In validation mode, we expect to find the violation, thus NORMAL_TERMINATION
                 ExitCode code = task.getWitness().isEmpty() ? PROGRAM_SPEC_VIOLATION : NORMAL_TERMINATION;
@@ -385,14 +379,7 @@ private static ResultSummary summaryFromResult(VerificationTask task, ModelCheck
                             && model.isBlocked(barrier);
 
                     if (isStuckLoop || isStuckBarrier) {
-                        final String callStack = makeContextString(
-                                synContext.getContextInfo(e).getContextOfType(CallContext.class), " -> ");
-                        details
-                                .append("\tE").append(e.getGlobalId())
-                                .append(":\t")
-                                .append(callStack.isEmpty() ? callStack : callStack + " -> ")
-                                .append(getSourceLocationString(e))
-                                .append("\n");
+                        appendTo(details, e, synContext);
                     }
                 }
                 // In validation mode, we expect to find the violation, thus NORMAL_TERMINATION
@@ -405,6 +392,16 @@ private static ResultSummary summaryFromResult(VerificationTask task, ModelCheck
                 ExitCode code = task.getWitness().isEmpty() ? DATA_RACE_FREEDOM_VIOLATION : NORMAL_TERMINATION;
                 return new ResultSummary(path, filter, FAIL, condition, reason, details.toString(), time, code);
             }
+            if (props.contains(TRACKABILITY) && model.propertyViolated(TRACKABILITY)) {
+                reason = ResultSummary.SVCOMP_UNTRACKABLE_OBJECT_REASON;
+                for (MemoryObject o : p.getMemory().getObjects()) {
+                    if (model.isLeaked(o) && !model.isTrackable(o)) {
+                        appendTo(details, o.getAllocationSite(), synContext);
+                    }
+                }
+                ExitCode code = task.getWitness().isEmpty() ? MEMORY_TRACKABILITY_VIOLATION : NORMAL_TERMINATION;
+                return new ResultSummary(path, filter, FAIL, condition, reason, details.toString(), time, code);
+            }
             final List<Axiom> violatedCATSpecs = !props.contains(CAT_SPEC) ? List.of()
                     : task.getMemoryModel().getAxioms().stream()
                     .filter(Axiom::isFlagged)
@@ -447,6 +444,17 @@ private static ResultSummary summaryFromResult(VerificationTask task, ModelCheck
         return new ResultSummary(path, filter, result, condition, reason, details.toString(), time, code);
     }
 
+    private static void appendTo(StringBuilder details, Event event, SyntacticContextAnalysis synContext) {
+        final String callStack = makeContextString(synContext.getContextInfo(event).getContextOfType(CallContext.class), " -> ");
+        details.append("\tE").append(event.getGlobalId())
+                .append(":\t").append(callStack.isEmpty() ? callStack : callStack + " -> ")
+                .append(getSourceLocationString(event));
+        if (event instanceof Assert ass) {
+            details.append(": ").append(ass.getErrorMessage());
+        }
+        details.append("\n");
+    }
+
     private static void increaseBoundAndDump(List<Event> boundEvents, Configuration config) throws IOException {
         if(!config.hasProperty(BOUNDS_SAVE_PATH)) {
             return;

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/Property.java

@@ -14,8 +14,9 @@ public enum Property implements OptionInterface {
     PROGRAM_SPEC,        // Litmus queries OR assertion safety in C-code
     TERMINATION,         // All executions terminate (absence of deadlocks/livelocks)
     CAT_SPEC,            // CAT-spec defined via flagged axioms in .cat file (~bug specification)
-    DATARACEFREEDOM;     // Special option for data-race detection in SVCOMP only
-
+    DATARACEFREEDOM,     // Special option for data-race detection in SVCOMP only
+    TRACKABILITY,        // All heap-allocated objects are either freed or remain reachable at the end of the execution.
+    ;
 
     public enum Type {
         SAFETY,
@@ -31,6 +32,7 @@ public String toString() {
             case DATARACEFREEDOM -> "Data-race freedom (SVCOMP only)";
             case TERMINATION -> "Termination";
             case CAT_SPEC -> "CAT specification";
+            case TRACKABILITY -> "Memory Trackability";
         };
     }
 
@@ -66,7 +68,7 @@ public static EnumSet<Property> getDefault() {
 
     // Used to decide the order shown by the selector in the UI
     public static Property[] orderedValues() {
-        Property[] order = {PROGRAM_SPEC, TERMINATION, CAT_SPEC, DATARACEFREEDOM};
+        Property[] order = {PROGRAM_SPEC, TERMINATION, CAT_SPEC, DATARACEFREEDOM, TRACKABILITY};
         // Be sure no element is missing
         assert (Arrays.asList(order).containsAll(Arrays.asList(values())));
         return order;

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

@@ -209,6 +209,18 @@ public BooleanFormula sameValue(MemoryCoreEvent first, MemoryCoreEvent second) {
         return objSize.get(memoryObject);
     }
 
+    /// Describes that {@code object} has been allocated, but has not been deallocated during the execution.
+    public BooleanFormula leakVariable(MemoryObject object) {
+        final int allocationSiteId = object.getAllocationSite().getGlobalId();
+        return booleanFormulaManager.makeVariable(formulaManager.escape("leak%d".formatted(allocationSiteId)));
+    }
+
+    /// Describes that {@code object} is reachable from static memory at the end of the execution.
+    public BooleanFormula trackVariable(MemoryObject object) {
+        final int allocationSiteId = object.getAllocationSite().getGlobalId();
+        return booleanFormulaManager.makeVariable(formulaManager.escape("track%d".formatted(allocationSiteId)));
+    }
+
     public TypedFormula<?, ?> value(MemoryCoreEvent event) {
         return values.get(event);
     }

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

@@ -114,6 +114,14 @@ public TypedValue<IntegerType, BigInteger> size(MemoryObject memoryObject) {
         return (TypedValue<IntegerType, BigInteger>) evaluate(ctx.size(memoryObject));
     }
 
+    public boolean isLeaked(MemoryObject object) {
+        return object.isHeapAllocated() && TRUE.equals(smtModel.evaluate(ctx.leakVariable(object)));
+    }
+
+    public boolean isTrackable(MemoryObject object) {
+        return object.isHeapAllocated() && TRUE.equals(smtModel.evaluate(ctx.trackVariable(object)));
+    }
+
     // ====================================================================================
     // Memory Model