From 5789d532c2d1e99096b2f4d51fe056f149741ac9 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 11 Nov 2024 19:39:30 +0100 Subject: [PATCH] Further changes for SVCOMP 2025 (#777) * Make use of bound.save and bound.load for svcomp * Remove outdated svcomp options * Add support for llvm.threadlocal.address intrinsic * Use lazy RA for svcomp * Add support for more intrinsics --------- Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon --- .../program/processing/Intrinsics.java | 24 +++++++++++++++++-- .../witness/graphml/WitnessBuilder.java | 9 ++++++- svcomp.properties | 3 +-- .../java/com/dat3m/svcomp/SVCOMPRunner.java | 6 ++++- 4 files changed, 36 insertions(+), 6 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 1ef4613035..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 @@ -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; @@ -182,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 --------------------------- @@ -196,6 +198,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), @@ -219,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", @@ -1297,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); @@ -1315,6 +1325,7 @@ private List inlineNonDet(FunctionCall call) { } else { // Nondeterministic integers final int bits = switch (suffix) { + case "longlong", "ulonglong" -> 64; case "long", "ulong" -> 64; case "int", "uint", "unsigned_int" -> 32; case "short", "ushort", "unsigned_short" -> 16; @@ -1323,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); @@ -1565,6 +1576,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 intrinsic 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())); } 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.properties b/svcomp.properties index eaf61f6a87..4d1b8fc39a 100644 --- a/svcomp.properties +++ b/svcomp.properties @@ -1,5 +1,4 @@ method=eager encoding.integers=true -svcomp.step=5 -svcomp.umax=27 witness=graphml +wmm.analysis.relationAnalysis=lazy diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 54ff09cb9e..2318cc332f 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -73,6 +73,9 @@ 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 + final String boundsFilePath = System.getenv("DAT3M_OUTPUT") + "/bounds.csv"; + new File(boundsFilePath).delete(); String[] argKeyword = Arrays.stream(args) .filter(s->s.startsWith("-")) @@ -107,6 +110,8 @@ public static void main(String[] args) throws Exception { cmd.add(fileModel.toString()); cmd.add(programPath); cmd.add("svcomp.properties"); + 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)); @@ -138,7 +143,6 @@ public static void main(String[] args) throws Exception { System.out.println(e.getMessage()); System.exit(0); } - bound++; } }