From 87ad4dc56cab87bf7b0d88e01bbbad6fd2154188 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Thu, 24 Oct 2024 11:21:22 +0200 Subject: [PATCH 1/2] Some updates for SVCOMP 2025 Signed-off-by: Hernan Ponce de Leon --- Dartagnan-SVCOMP.sh | 2 -- dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java | 6 +++++- .../com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java | 3 +++ svcomp.properties | 1 + svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 1 - 5 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Dartagnan-SVCOMP.sh b/Dartagnan-SVCOMP.sh index 469a2e5004..66b4f0aabc 100755 --- a/Dartagnan-SVCOMP.sh +++ b/Dartagnan-SVCOMP.sh @@ -21,8 +21,6 @@ else export DAT3M_HOME=$(pwd) export DAT3M_OUTPUT=$DAT3M_HOME/output - export OPTFLAGS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn" - skip_assertions_of_type="--program.processing.skipAssertionsOfType=USER" if [[ $propertypath == *"no-overflow.prp"* ]]; then export CFLAGS="-fgnu89-inline -fsanitize=signed-integer-overflow" diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 2bbb4721ef..eaa18658a4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -251,7 +251,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme // ------------------ Generate Witness, if possible ------------------ final EnumSet properties = task.getProperty(); if (task.getProgram().getFormat().equals(SourceLanguage.LLVM) && modelChecker.hasModel() - && properties.contains(PROGRAM_SPEC) && properties.size() == 1 + && (properties.contains(PROGRAM_SPEC) || properties.contains(DATARACEFREEDOM)) && properties.size() == 1 && modelChecker.getResult() != UNKNOWN) { try { WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, @@ -319,6 +319,10 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm } summary.append("=================================================\n"); } + if (props.contains(DATARACEFREEDOM) && FALSE.equals(model.evaluate(DATARACEFREEDOM.getSMTVariable(encCtx)))) { + summary.append("============= SVCOMP data race found ============\n"); + summary.append("=================================================\n"); + } final List violatedCATSpecs = task.getMemoryModel().getAxioms().stream() .filter(Axiom::isFlagged) .filter(ax -> props.contains(CAT_SPEC) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java index 7e71e3baac..7eb14e0af0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessBuilder.java @@ -84,6 +84,9 @@ private static String getLtlPropertyFromSummary(String summary) { if (summary.contains("user assertion")) { return "CHECK( init(main()), LTL(G ! call(reach_error())))"; } + if (summary.contains("SVCOMP data race found")) { + return "CHECK( init(main()), LTL(G ! data-race) )"; + } throw new UnsupportedOperationException("Violation found for unsupported property"); } diff --git a/svcomp.properties b/svcomp.properties index d11788f771..eaf61f6a87 100644 --- a/svcomp.properties +++ b/svcomp.properties @@ -2,3 +2,4 @@ method=eager encoding.integers=true svcomp.step=5 svcomp.umax=27 +witness=graphml diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 6f5a6e80c7..1df0f337e5 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -127,7 +127,6 @@ public static void main(String[] args) throws Exception { cmd.add("svcomp.properties"); cmd.add(String.format("--%s=%s", PROPERTY, r.property.asStringOption())); cmd.add(String.format("--%s=%s", BOUND, bound)); - cmd.add(String.format("--%s=%s", WITNESS, GRAPHML.asStringOption())); cmd.add(String.format("--%s=%s", WITNESS_ORIGINAL_PROGRAM_PATH, programPath)); cmd.addAll(filterOptions(config)); From 47ef5a359565a925bf1765e604f295c43e95da30 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 1 Nov 2024 21:13:30 +0100 Subject: [PATCH 2/2] Do not inline assert checking if a lock is released twice when we should skip AssertionType.USER assertions --- .../com/dat3m/dartagnan/program/processing/Intrinsics.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index 5c8c13e8df..bc6576c3d1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -664,9 +664,9 @@ private List inlinePthreadMutexUnlock(FunctionCall call) { final Expression lockAddress = call.getArguments().get(0); final Expression locked = expressions.makeOne(type); final Expression unlocked = expressions.makeZero(type); - return List.of( + return EventFactory.eventSequence( EventFactory.Llvm.newLoad(oldValueRegister, lockAddress, Tag.C11.MO_RELAXED), - EventFactory.newAssert(expressions.makeEQ(oldValueRegister, locked), "Unlocking an already unlocked mutex"), + notToInline.contains(AssertionType.USER) ? null : EventFactory.newAssert(expressions.makeEQ(oldValueRegister, locked), "Unlocking an already unlocked mutex"), EventFactory.Llvm.newStore(lockAddress, unlocked, Tag.C11.MO_RELEASE), assignSuccess(errorRegister) );