From f8e5927c773642c5fb3cedb7ec397de22963b24e Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 8 Nov 2024 22:23:34 +0100 Subject: [PATCH 1/8] Make use of bound.save and bound.load for svcomp Signed-off-by: Hernan Ponce de Leon --- .../dat3m/dartagnan/witness/graphml/WitnessBuilder.java | 9 ++++++++- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 5 ++++- 2 files changed, 12 insertions(+), 2 deletions(-) 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 7eb14e0af0..d8837cb666 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 @@ -11,6 +11,7 @@ import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; +import com.dat3m.dartagnan.program.event.metadata.UnrollingBound; import com.dat3m.dartagnan.utils.Result; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.configuration.Option; @@ -91,14 +92,20 @@ private static String getLtlPropertyFromSummary(String summary) { } public WitnessGraph build() { + Integer bound = 1; for (Thread t : context.getTask().getProgram().getThreads()) { for (Event e : t.getEntry().getSuccessors()) { eventThreadMap.put(e, t.getId()); + // TODO: move the bound attribute from graph to nodes and make the + // LoopUnrolling pass get the bounds from the witness when available + if(e.hasMetadata(UnrollingBound.class)) { + bound = Integer.max(bound, e.getMetadata(UnrollingBound.class).value()); + } } } WitnessGraph graph = new WitnessGraph(); - graph.addAttribute(UNROLLBOUND.toString(), valueOf(context.getTask().getProgram().getUnrollingBound())); + graph.addAttribute(UNROLLBOUND.toString(), bound.toString()); graph.addAttribute(WITNESSTYPE.toString(), type + "_witness"); graph.addAttribute(SOURCECODELANG.toString(), "C"); graph.addAttribute(PRODUCER.toString(), "Dartagnan"); diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 54ff09cb9e..409b75ec66 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -73,6 +73,8 @@ public static void main(String[] args) throws Exception { File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst().get()); String programPath = Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)).findFirst().get(); File fileProgram = new File(programPath); + // To be sure we do not mixed benchmarks, if the bounds file exists, delete it + new File(System.getenv("DAT3M_OUTPUT") + "/bounds.csv").delete(); String[] argKeyword = Arrays.stream(args) .filter(s->s.startsWith("-")) @@ -107,6 +109,8 @@ public static void main(String[] args) throws Exception { cmd.add(fileModel.toString()); cmd.add(programPath); cmd.add("svcomp.properties"); + cmd.add("--bound.load=" + System.getenv().get("DAT3M_OUTPUT") + "/bounds.csv"); + cmd.add("--bound.save=" + System.getenv().get("DAT3M_OUTPUT") + "/bounds.csv"); 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_ORIGINAL_PROGRAM_PATH, programPath)); @@ -138,7 +142,6 @@ public static void main(String[] args) throws Exception { System.out.println(e.getMessage()); System.exit(0); } - bound++; } } From 33c5161a2e3a2fe09c4be54801075c54828b80a2 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 8 Nov 2024 22:27:58 +0100 Subject: [PATCH 2/8] Remove outdated svcomp options Signed-off-by: Hernan Ponce de Leon --- svcomp.properties | 2 -- 1 file changed, 2 deletions(-) diff --git a/svcomp.properties b/svcomp.properties index eaf61f6a87..bb55074f34 100644 --- a/svcomp.properties +++ b/svcomp.properties @@ -1,5 +1,3 @@ method=eager encoding.integers=true -svcomp.step=5 -svcomp.umax=27 witness=graphml From 0d2fdc15675a3cff3507cca668c0d8cec903025b Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 9 Nov 2024 13:47:46 +0100 Subject: [PATCH 3/8] Add support for llvm.threadlocal.address intrinsic Signed-off-by: Hernan Ponce de Leon --- .../dartagnan/program/processing/Intrinsics.java | 11 +++++++++++ 1 file changed, 11 insertions(+) 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 1ef4613035..6c88ae5bcb 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 @@ -21,6 +21,7 @@ import com.dat3m.dartagnan.program.event.functions.FunctionCall; import com.dat3m.dartagnan.program.event.functions.ValueFunctionCall; import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic; +import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableList; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -196,6 +197,7 @@ public enum Info { LLVM_EXPECT("llvm.expect", false, false, true, true, Intrinsics::inlineLLVMExpect), LLVM_MEMCPY("llvm.memcpy", true, true, true, false, Intrinsics::inlineMemCpy), LLVM_MEMSET("llvm.memset", true, false, true, false, Intrinsics::inlineMemSet), + LLVM_THREADLOCAL("llvm.threadlocal.address.p0", false, false, true, true, Intrinsics::inlineLLVMThreadLocal), // --------------------------- LKMM --------------------------- LKMM_LOAD("__LKMM_LOAD", false, true, true, true, Intrinsics::handleLKMMIntrinsic), LKMM_STORE("__LKMM_STORE", true, false, true, true, Intrinsics::handleLKMMIntrinsic), @@ -1565,6 +1567,15 @@ private List inlineMemSet(FunctionCall call) { return replacement; } + private List inlineLLVMThreadLocal(FunctionCall call) { + final Register resultReg = getResultRegisterAndCheckArguments(1, call); + final Expression exp = call.getArguments().get(0); + checkArgument(exp instanceof MemoryObject object && object.isThreadLocal(), "Calling thread local instrinsic on a non thread local object \"%s\"", call); + return List.of( + EventFactory.newLocal(resultReg, exp) + ); + } + private Event assignSuccess(Register errorRegister) { return EventFactory.newLocal(errorRegister, expressions.makeGeneralZero(errorRegister.getType())); } From 252f913aa217d3589165bad9e96af85198751c6a Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 9 Nov 2024 19:19:19 +0100 Subject: [PATCH 4/8] Use lazy RA for svcomp Signed-off-by: Hernan Ponce de Leon --- svcomp.properties | 1 + 1 file changed, 1 insertion(+) diff --git a/svcomp.properties b/svcomp.properties index bb55074f34..4d1b8fc39a 100644 --- a/svcomp.properties +++ b/svcomp.properties @@ -1,3 +1,4 @@ method=eager encoding.integers=true witness=graphml +wmm.analysis.relationAnalysis=lazy From 81066d0e4b30cef1b07d78374158445ced38e829 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 9 Nov 2024 19:46:37 +0100 Subject: [PATCH 5/8] Add support for more intrinsics Signed-off-by: Hernan Ponce de Leon --- .../dartagnan/program/processing/Intrinsics.java | 13 +++++++++++-- 1 file changed, 11 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 6c88ae5bcb..59807e8261 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 @@ -183,6 +183,7 @@ public enum Info { "__VERIFIER_nondet_int", "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned_int", "__VERIFIER_nondet_short", "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_unsigned_short", "__VERIFIER_nondet_long", "__VERIFIER_nondet_ulong", + "__VERIFIER_nondet_longlong", "__VERIFIER_nondet_ulonglong", "__VERIFIER_nondet_char", "__VERIFIER_nondet_uchar"), false, false, true, true, Intrinsics::inlineNonDet), // --------------------------- LLVM --------------------------- @@ -221,7 +222,8 @@ public enum Info { STD_ASSERT(List.of("__assert_fail", "__assert_rtn"), false, false, false, true, Intrinsics::inlineUserAssert), STD_EXIT("exit", false, false, false, true, Intrinsics::inlineExit), STD_ABORT("abort", false, false, false, true, Intrinsics::inlineExit), - STD_IO(List.of("puts", "putchar", "printf"), false, false, true, true, Intrinsics::inlineAsZero), + STD_IO(List.of("puts", "putchar", "printf", "fflush"), false, false, true, true, Intrinsics::inlineAsZero), + STD_IO_NONDET(List.of("__isoc99_sscanf", "fprintf"), false, false, true, true, Intrinsics::inlineCallAsNonDet), STD_SLEEP("sleep", false, false, true, true, Intrinsics::inlineAsZero), // --------------------------- UBSAN --------------------------- UBSAN_OVERFLOW(List.of("__ubsan_handle_add_overflow", "__ubsan_handle_sub_overflow", @@ -1299,6 +1301,12 @@ private void inlineLate(Function function) { } } + private List inlineCallAsNonDet(FunctionCall call) { + return List.of( + EventFactory.Svcomp.newSignedNonDetChoice(getResultRegister(call), true) + ); + } + private List inlineNonDet(FunctionCall call) { assert call.isDirectCall() && call instanceof ValueFunctionCall; final Register result = getResultRegister(call); @@ -1317,6 +1325,7 @@ private List inlineNonDet(FunctionCall call) { } else { // Nondeterministic integers final int bits = switch (suffix) { + case "longlong", "ulonglong" -> 128; case "long", "ulong" -> 64; case "int", "uint", "unsigned_int" -> 32; case "short", "ushort", "unsigned_short" -> 16; @@ -1325,7 +1334,7 @@ private List inlineNonDet(FunctionCall call) { }; signed = switch (suffix) { - case "int", "short", "long", "char" -> true; + case "int", "short", "long", "longlong", "char" -> true; default -> false; }; nonDetType = types.getIntegerType(bits); From 455ebfc95425db48e55393e99c49bfe8112122bf Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 11 Nov 2024 21:23:03 +0800 Subject: [PATCH 6/8] Feedback implemented Signed-off-by: Hernan Ponce de Leon --- .../dat3m/dartagnan/program/processing/Intrinsics.java | 4 ++-- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 8 +++++--- 2 files changed, 7 insertions(+), 5 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 59807e8261..f1d85baf00 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 @@ -1325,7 +1325,7 @@ private List inlineNonDet(FunctionCall call) { } else { // Nondeterministic integers final int bits = switch (suffix) { - case "longlong", "ulonglong" -> 128; + case "longlong", "ulonglong" -> 64; case "long", "ulong" -> 64; case "int", "uint", "unsigned_int" -> 32; case "short", "ushort", "unsigned_short" -> 16; @@ -1579,7 +1579,7 @@ private List inlineMemSet(FunctionCall call) { private List inlineLLVMThreadLocal(FunctionCall call) { final Register resultReg = getResultRegisterAndCheckArguments(1, call); final Expression exp = call.getArguments().get(0); - checkArgument(exp instanceof MemoryObject object && object.isThreadLocal(), "Calling thread local instrinsic on a non thread local object \"%s\"", call); + checkArgument(exp instanceof MemoryObject object && object.isThreadLocal(), "Calling thread-local intrinsic on a non-thread-local object \"%s\"", call); return List.of( EventFactory.newLocal(resultReg, exp) ); diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 409b75ec66..81e5369432 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -59,6 +59,8 @@ private void property(String p) { public static void main(String[] args) throws Exception { + String final boundsFilePath = System.getenv("DAT3M_OUTPUT") + "/bounds.csv"; + if(Arrays.asList(args).contains("--help")) { collectOptions(); return; @@ -74,7 +76,7 @@ public static void main(String[] args) throws Exception { String programPath = Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)).findFirst().get(); File fileProgram = new File(programPath); // To be sure we do not mixed benchmarks, if the bounds file exists, delete it - new File(System.getenv("DAT3M_OUTPUT") + "/bounds.csv").delete(); + new File(boundsFilePath).delete(); String[] argKeyword = Arrays.stream(args) .filter(s->s.startsWith("-")) @@ -109,8 +111,8 @@ public static void main(String[] args) throws Exception { cmd.add(fileModel.toString()); cmd.add(programPath); cmd.add("svcomp.properties"); - cmd.add("--bound.load=" + System.getenv().get("DAT3M_OUTPUT") + "/bounds.csv"); - cmd.add("--bound.save=" + System.getenv().get("DAT3M_OUTPUT") + "/bounds.csv"); + cmd.add("--bound.load=" + boundsFilePath); + cmd.add("--bound.save=" + boundsFilePath); 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_ORIGINAL_PROGRAM_PATH, programPath)); From d0ed9dfc1072ee56dfc6f3597ee4b319b298166f Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 11 Nov 2024 21:35:26 +0800 Subject: [PATCH 7/8] Fix Signed-off-by: Hernan Ponce de Leon --- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 81e5369432..1941e635ea 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -59,7 +59,7 @@ private void property(String p) { public static void main(String[] args) throws Exception { - String final boundsFilePath = System.getenv("DAT3M_OUTPUT") + "/bounds.csv"; + final String boundsFilePath = System.getenv("DAT3M_OUTPUT") + "/bounds.csv"; if(Arrays.asList(args).contains("--help")) { collectOptions(); From e2c9b0225ef70842dec8e24cc3376aca10102cb4 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 11 Nov 2024 21:36:55 +0800 Subject: [PATCH 8/8] Move variable down Signed-off-by: Hernan Ponce de Leon --- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 1941e635ea..2318cc332f 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -59,8 +59,6 @@ private void property(String p) { public static void main(String[] args) throws Exception { - final String boundsFilePath = System.getenv("DAT3M_OUTPUT") + "/bounds.csv"; - if(Arrays.asList(args).contains("--help")) { collectOptions(); return; @@ -76,6 +74,7 @@ public static void main(String[] args) throws Exception { String programPath = Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)).findFirst().get(); File fileProgram = new File(programPath); // To be sure we do not mixed benchmarks, if the bounds file exists, delete it + final String boundsFilePath = System.getenv("DAT3M_OUTPUT") + "/bounds.csv"; new File(boundsFilePath).delete(); String[] argKeyword = Arrays.stream(args)