Merge branch 'refs/heads/development' into fixLlvmParsingOrder

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<Event> inlineCallAsNonDet(FunctionCall call) {
+        return List.of(
+                EventFactory.Svcomp.newSignedNonDetChoice(getResultRegister(call), true)
+        );
+    }
+
     private List<Event> inlineNonDet(FunctionCall call) {
         assert call.isDirectCall() && call instanceof ValueFunctionCall;
         final Register result = getResultRegister(call);
@@ -1315,6 +1325,7 @@ private List<Event> 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<Event> 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<Event> inlineMemSet(FunctionCall call) {
         return replacement;
     }
 
+    private List<Event> 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()));
     }

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");

svcomp.properties

@@ -1,5 +1,4 @@
 method=eager
 encoding.integers=true
-svcomp.step=5
-svcomp.umax=27
 witness=graphml
+wmm.analysis.relationAnalysis=lazy

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++;
         }
     }