From 0e852a16d87ec82dde613a69197af6cd85b94b8d Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Tue, 10 Dec 2024 14:50:34 +0100 Subject: [PATCH] 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. --- .../nontermination/nontermination_sanity.c | 20 ++++++ .../encoding/NonTerminationEncoder.java | 19 +++++- .../com/dat3m/dartagnan/program/Register.java | 8 +++ .../dartagnan/program/event/EventFactory.java | 11 ++++ .../event/core/special/StateSnapshot.java | 52 ++++++++++++++++ .../processing/CoreCodeVerification.java | 4 +- .../processing/DynamicSpinLoopDetection.java | 27 ++++++-- .../com/dat3m/dartagnan/c/LivenessTest.java | 3 +- .../nontermination/nontermination_sanity.ll | 62 +++++++++++++++++++ 9 files changed, 197 insertions(+), 9 deletions(-) create mode 100644 benchmarks/nontermination/nontermination_sanity.c create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/special/StateSnapshot.java create mode 100644 dartagnan/src/test/resources/nontermination/nontermination_sanity.ll diff --git a/benchmarks/nontermination/nontermination_sanity.c b/benchmarks/nontermination/nontermination_sanity.c new file mode 100644 index 0000000000..e8f56f0ad1 --- /dev/null +++ b/benchmarks/nontermination/nontermination_sanity.c @@ -0,0 +1,20 @@ +#include +#include + +/* + 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; +} \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java index d38f649a94..84f98b6229 100644 --- 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 index 0f0c5d193b..0d3d95a71a 100644 --- 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 collectRegisterReads(Expression expr, Register.UsageType return collector; } + public static Set collectRegisterReads(Collection exprs, Register.UsageType usageType, Set 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 index b8185aa230..219197c876 100644 --- 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 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 new file mode 100644 index 0000000000..f11c7e46fa --- /dev/null +++ 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 expressions; + + public StateSnapshot(Collection expressions) { + this.expressions = new ArrayList<>(expressions); + } + + private StateSnapshot(StateSnapshot stateSnapshot) { + super(stateSnapshot); + this.expressions = new ArrayList<>(stateSnapshot.expressions); + } + + public List 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 getRegisterReads() { + return Register.collectRegisterReads(expressions, Register.UsageType.OTHER, new HashSet<>()); + } + + @Override + public void transformExpressions(ExpressionVisitor 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 index bf5d1605fc..144ff3f546 100644 --- 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 index 16e787d345..a082b1f374 100644 --- 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 computeLoopData(Function func, LoopAnalysis loopAnalysis) private void collectSideEffects(LoopData loop, LiveRegistersAnalysis liveRegsAna) { final Set writtenRegisters = new HashSet<>(); + final Set 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 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 globalSideEffects = new ArrayList<>(); private final List writtenLiveRegisters = new ArrayList<>(); + private final List 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 index b480c22bdf..7f00d30016 100644 --- 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 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 new file mode 100644 index 0000000000..f44132cb37 --- /dev/null +++ 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)