Added new StateSnapshot event for instrumentation of non-termination …

…detection: this removes a wrong verdict related to SCCP removing the whole loop body. Added new test related to above issue. Minor updates to related code.
hernanponcedeleon · Dec 10, 2024 · 0e852a1 · 0e852a1
1 parent 768b090
commit 0e852a1
Show file tree

Hide file tree

Showing 9 changed files with 197 additions and 9 deletions.
diff --git a/benchmarks/nontermination/nontermination_sanity.c b/benchmarks/nontermination/nontermination_sanity.c
@@ -0,0 +1,20 @@
+#include <pthread.h>
+#include <stdatomic.h>
+
+/*
+    Test case: Special case to ensure that Dartagnan's internal optimization pipeline does not hide side-effects:
+               Naively, unrolling the loop k < 10 times and performing SCCP results in k empty iteration bodies,
+               which looks identical to a k-times unrolled while(1)-loop.
+               However, the insufficiently unrolled loop will terminate, the while(1)-loop will not and
+               so need to be distinguished somehow (e.g. by instrumentation).
+*/
+
+int main()
+{
+    int i = 0;
+    while(!(i > 10)) {
+        i++;
+    }
+
+    return 0;
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java
@@ -1,5 +1,6 @@
 package com.dat3m.dartagnan.encoding;
 
+import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.program.Program;
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.analysis.LoopAnalysis;
@@ -9,6 +10,7 @@
 import com.dat3m.dartagnan.program.event.core.Local;
 import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent;
 import com.dat3m.dartagnan.program.event.core.Store;
+import com.dat3m.dartagnan.program.event.core.special.StateSnapshot;
 import com.dat3m.dartagnan.program.event.metadata.UnrollingId;
 import com.dat3m.dartagnan.verification.VerificationTask;
 import com.dat3m.dartagnan.wmm.Relation;
@@ -71,8 +73,7 @@ but since we might not have encoded fr (lazy solving), we formulate this indirec
     TODO: We have not considered uninit reads, i.e., reads without rf-edges in the implementation.
           There might be issues if init events are missing.
     TODO 2: We do not consider ControlBarriers at all. The current version is only for loop-based nontermination.
-    TODO 3: The old encoding also ensured no exceptional termination due to e.g. failed assertions.
-            We might have to include this here as well.
+    TODO 3: We do not (yet) consider fairness of weak atomics like StoreExclusive
  */
 public class NonTerminationEncoder {
 
@@ -445,6 +446,20 @@ private BooleanFormula areEquivalent(Event x, Event y) {
                     context.equal(context.result(e), context.result(f))
             );
         }
+        if (x instanceof StateSnapshot e && y instanceof StateSnapshot f) {
+            if (e.getExpressions().size() != f.getExpressions().size()) {
+                equality = bmgr.makeFalse();
+            } else {
+                for (int i = 0; i < e.getExpressions().size(); i++) {
+                    final Expression exprE = e.getExpressions().get(i);
+                    final Expression exprF = f.getExpressions().get(i);
+                    equality = bmgr.and(
+                            equality,
+                            context.equal(context.encodeExpressionAt(exprE, e), context.encodeExpressionAt(exprF, f))
+                    );
+                }
+            }
+        }
         if (x instanceof MemoryCoreEvent e && y instanceof MemoryCoreEvent f) {
             equality = bmgr.and(
                     equality,

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Register.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Register.java
@@ -7,6 +7,7 @@
 import com.dat3m.dartagnan.expression.base.LeafExpressionBase;
 import com.google.common.collect.ImmutableSet;
 
+import java.util.Collection;
 import java.util.Objects;
 import java.util.Set;
 
@@ -86,6 +87,13 @@ public static Set<Read> collectRegisterReads(Expression expr, Register.UsageType
         return collector;
     }
 
+    public static Set<Read> collectRegisterReads(Collection<? extends Expression> exprs, Register.UsageType usageType, Set<Read> collector) {
+        for (Expression expr : exprs) {
+            collectRegisterReads(expr, usageType, collector);
+        }
+        return collector;
+    }
+
     // ==========================================================================
     // ==========================================================================
     // ============================== Inner classes =============================

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
@@ -25,6 +25,7 @@
 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.special.StateSnapshot;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadCreate;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
@@ -309,6 +310,16 @@ public static ThreadStart newThreadStart(ThreadCreate creator) {
         return new ThreadStart(creator);
     }
 
+    public static class Special {
+        private Special() {
+        }
+
+
+        public static StateSnapshot newStateSnapshot(List<? extends Expression> expressions) {
+            return new StateSnapshot(expressions);
+        }
+    }
+
     // =============================================================================================
     // ========================================== Common ===========================================
     // =============================================================================================

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/special/StateSnapshot.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/special/StateSnapshot.java
@@ -0,0 +1,52 @@
+package com.dat3m.dartagnan.program.event.core.special;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionVisitor;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.event.AbstractEvent;
+import com.dat3m.dartagnan.program.event.RegReader;
+
+import java.util.*;
+import java.util.stream.Collectors;
+
+/*
+    Currently, this event is only used to instrument loops for non-termination detection.
+ */
+public class StateSnapshot extends AbstractEvent implements RegReader {
+
+    private final List<Expression> expressions;
+
+    public StateSnapshot(Collection<? extends Expression> expressions) {
+        this.expressions = new ArrayList<>(expressions);
+    }
+
+    private StateSnapshot(StateSnapshot stateSnapshot) {
+        super(stateSnapshot);
+        this.expressions = new ArrayList<>(stateSnapshot.expressions);
+    }
+
+    public List<Expression> getExpressions() {
+        return expressions;
+    }
+
+    @Override
+    protected String defaultString() {
+        return String.format("StateSnapshot(%s)",
+                expressions.stream().map(Expression::toString).collect(Collectors.joining(", ")));
+    }
+
+    @Override
+    public StateSnapshot getCopy() {
+        return new StateSnapshot(this);
+    }
+
+    @Override
+    public Set<Register.Read> getRegisterReads() {
+        return Register.collectRegisterReads(expressions, Register.UsageType.OTHER, new HashSet<>());
+    }
+
+    @Override
+    public void transformExpressions(ExpressionVisitor<? extends Expression> exprTransformer) {
+        expressions.replaceAll(expression -> expression.accept(exprTransformer));
+    }
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java
@@ -5,6 +5,7 @@
 import com.dat3m.dartagnan.program.event.Event;
 import com.dat3m.dartagnan.program.event.core.*;
 import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation;
+import com.dat3m.dartagnan.program.event.core.special.StateSnapshot;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadCreate;
 import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
@@ -38,7 +39,8 @@ public static CoreCodeVerification fromConfig(Configuration config) {
             Assume.class, Assert.class,
             ThreadCreate.class, ThreadArgument.class, ThreadStart.class,
             ControlBarrier.class, // For PTX and Vulkan
-            BeginAtomic.class, EndAtomic.class
+            BeginAtomic.class, EndAtomic.class,
+            StateSnapshot.class
             // We add SVCOMP atomic blocks here as well, despite them not being part of the core package.
             // TODO: We might want to find a more systematic way to extend the core with these custom events.
     ));

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java
@@ -10,10 +10,7 @@
 import com.dat3m.dartagnan.program.Thread;
 import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis;
 import com.dat3m.dartagnan.program.analysis.LoopAnalysis;
-import com.dat3m.dartagnan.program.event.Event;
-import com.dat3m.dartagnan.program.event.EventFactory;
-import com.dat3m.dartagnan.program.event.RegWriter;
-import com.dat3m.dartagnan.program.event.Tag;
+import com.dat3m.dartagnan.program.event.*;
 import com.dat3m.dartagnan.program.event.core.Label;
 import com.dat3m.dartagnan.program.event.functions.FunctionCall;
 import com.google.common.base.Preconditions;
@@ -92,8 +89,12 @@ private List<LoopData> computeLoopData(Function func, LoopAnalysis loopAnalysis)
 
     private void collectSideEffects(LoopData loop, LiveRegistersAnalysis liveRegsAna) {
         final Set<Register> writtenRegisters = new HashSet<>();
+        final Set<Register> readRegisters = new HashSet<>();
         Event cur = loop.getStart();
         do {
+            if (cur instanceof RegReader reader) {
+                reader.getRegisterReads().stream().map(Register.Read::register).forEach(readRegisters::add);
+            }
             if (cur instanceof RegWriter writer) {
                 writtenRegisters.add(writer.getResultRegister());
             }
@@ -107,9 +108,17 @@ private void collectSideEffects(LoopData loop, LiveRegistersAnalysis liveRegsAna
         } while ((cur = cur.getSuccessor()) != loop.getEnd().getSuccessor());
 
         // Every live register that is written to is a potential local side effect.
-        loop.writtenLiveRegisters.addAll(Sets.intersection(
+        final Set<Register> writtenLiveRegisters = Sets.intersection(
                 writtenRegisters,
                 liveRegsAna.getLiveRegistersAt(loop.getStart())
+        );
+        loop.writtenLiveRegisters.addAll(writtenLiveRegisters);
+
+        // Every written live register that is also read within the loop is potentially live on backjump.
+        // (This is a rough approximation).
+        loop.writtenLiveOnBackjumpRegisters.addAll(Sets.intersection(
+                writtenLiveRegisters,
+                readRegisters
         ));
     }
 
@@ -159,6 +168,13 @@ private void instrumentLoop(LoopData loop) {
                 assumeSideEffect
         ));
 
+        // Special snapshot event for non-termination detection
+        if (!loop.writtenLiveOnBackjumpRegisters.isEmpty()) {
+            loop.getEnd().getPredecessor().insertAfter(List.of(
+                    EventFactory.Special.newStateSnapshot(loop.writtenLiveOnBackjumpRegisters)
+            ));
+        }
+
         // Special case: If the loop is fully side-effect-free, we can set its unrolling bound to 1.
         if (loop.isSideEffectFree()) {
             final Event loopBound = EventFactory.Svcomp.newLoopBound(expressions.makeValue(1, types.getArchType()));
@@ -188,6 +204,7 @@ private static class LoopData {
         private final LoopAnalysis.LoopInfo loopInfo;
         private final List<Event> globalSideEffects = new ArrayList<>();
         private final List<Register> writtenLiveRegisters = new ArrayList<>();
+        private final List<Register> writtenLiveOnBackjumpRegisters = new ArrayList<>();
 
         public boolean isSideEffectFree() {
             return writtenLiveRegisters.isEmpty() && globalSideEffects.isEmpty();

diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java
@@ -143,11 +143,12 @@ public static Iterable<Object[]> data() throws IOException {
                 {"locks/deadlock", POWER, FAIL},
                 {"locks/deadlock", RISCV, FAIL},
                 // Side-effectful nontermination
+                {"nontermination/nontermination_sanity", TSO, UNKNOWN},
                 {"nontermination/nontermination", TSO, FAIL},
                 {"nontermination/nontermination_xchg", TSO, FAIL},
                 {"nontermination/nontermination_zero_effect", TSO, FAIL},
                 {"nontermination/nontermination_complex", TSO, FAIL},
-                {"nontermination/nontermination_weak", TSO, UNKNOWN},
+                {"nontermination/nontermination_weak", TSO, PASS},
                 {"nontermination/nontermination_weak", ARM8, FAIL}
         });
     }

diff --git a/dartagnan/src/test/resources/nontermination/nontermination_sanity.ll b/dartagnan/src/test/resources/nontermination/nontermination_sanity.ll
@@ -0,0 +1,62 @@
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/nontermination/nontermination_sanity.c'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/nontermination/nontermination_sanity.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+@x = global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !18 {
+  %1 = alloca i32, align 4
+  %2 = alloca i32, align 4
+  store i32 0, i32* %1, align 4
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !22, metadata !DIExpression()), !dbg !23
+  store i32 0, i32* %2, align 4, !dbg !23
+  br label %3, !dbg !24
+
+3:                                                ; preds = %0, %3
+  %4 = load i32, i32* @x, align 4, !dbg !25
+  %5 = add nsw i32 %4, 1, !dbg !25
+  store i32 %5, i32* @x, align 4, !dbg !25
+  br label %3, !dbg !24, !llvm.loop !27
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!7, !8, !9, !10, !11, !12, !13, !14, !15, !16}
+!llvm.ident = !{!17}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !5, line: 12, type: !6, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, globals: !4, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/nontermination/nontermination_sanity.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!0}
+!5 = !DIFile(filename: "benchmarks/nontermination/nontermination_sanity.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!6 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!7 = !{i32 7, !"Dwarf Version", i32 4}
+!8 = !{i32 2, !"Debug Info Version", i32 3}
+!9 = !{i32 1, !"wchar_size", i32 4}
+!10 = !{i32 1, !"branch-target-enforcement", i32 0}
+!11 = !{i32 1, !"sign-return-address", i32 0}
+!12 = !{i32 1, !"sign-return-address-all", i32 0}
+!13 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!14 = !{i32 7, !"PIC Level", i32 2}
+!15 = !{i32 7, !"uwtable", i32 1}
+!16 = !{i32 7, !"frame-pointer", i32 1}
+!17 = !{!"Homebrew clang version 14.0.6"}
+!18 = distinct !DISubprogram(name: "main", scope: !5, file: !5, line: 14, type: !19, scopeLine: 15, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !21)
+!19 = !DISubroutineType(types: !20)
+!20 = !{!6}
+!21 = !{}
+!22 = !DILocalVariable(name: "i", scope: !18, file: !5, line: 16, type: !6)
+!23 = !DILocation(line: 16, column: 9, scope: !18)
+!24 = !DILocation(line: 17, column: 5, scope: !18)
+!25 = !DILocation(line: 19, column: 10, scope: !26)
+!26 = distinct !DILexicalBlock(scope: !18, file: !5, line: 17, column: 14)
+!27 = distinct !{!27, !24, !28}
+!28 = !DILocation(line: 20, column: 5, scope: !18)