Merge pull request #859 from goblint/svcomp23

SV-COMP 2023 setup

Author: sim642

.gitignore

@@ -52,6 +52,7 @@ goblint.bc.js
 *.orig
 *.rej
 
+lib/
 sv-comp/goblint.zip
 
 privPrecCompare

conf/dune

@@ -8,6 +8,7 @@
     svcomp.json
     svcomp21.json
     svcomp22.json
+    svcomp23.json
     ; no way to glob here...
   )
 )

conf/svcomp.json

@@ -1,10 +1,5 @@
 {
   "ana": {
-    "base": {
-      "arrays": {
-        "domain": "partitioned"
-      }
-    },
     "sv-comp": {
       "enabled": true,
       "functions": true
@@ -23,8 +18,10 @@
       "mutexEvents",
       "mutex",
       "access",
+      "race",
       "escape",
       "expRelation",
+      "assert",
       "mhp",
       "var_eq",
       "symb_locks",
@@ -53,15 +50,16 @@
         "ldv_xzalloc",
         "ldv_calloc"
       ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
     }
   },
   "exp": {
     "region-offsets": true
   },
-  "witness": {
-    "id": "enumerate",
-    "unknown": false
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {
@@ -73,5 +71,9 @@
     "null-pointer": {
       "dereference": "assume_none"
     }
+  },
+  "witness": {
+    "id": "enumerate",
+    "unknown": false
   }
-}
+}

conf/svcomp21.json

@@ -17,8 +17,10 @@
       "mutexEvents",
       "mutex",
       "access",
+      "race",
       "escape",
       "expRelation",
+      "assert",
       "var_eq",
       "symb_locks",
       "region",

conf/svcomp22.json

@@ -17,8 +17,10 @@
       "mutexEvents",
       "mutex",
       "access",
+      "race",
       "escape",
       "expRelation",
+      "assert",
       "var_eq",
       "symb_locks",
       "region",

conf/svcomp23.json

@@ -0,0 +1,94 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "arrayDomain",
+        "octagon",
+        "wideningThresholds"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "id": "enumerate",
+    "unknown": false
+  }
+}

make.sh

@@ -25,7 +25,7 @@ rule() {
       cp _build/default/$TARGET.exe goblint
     ;; release)
       eval $(opam config env)
-      dune build --profile release $TARGET.exe &&
+      dune build --profile=release $TARGET.exe &&
       rm -f goblint &&
       cp _build/default/$TARGET.exe goblint
     # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable

src/autoTune.ml

@@ -135,7 +135,7 @@ let disableIntervalContextsInRecursiveFunctions () =
 (*escape is also still enabled, because otherwise we get a warning*)
 (*does not consider dynamic calls!*)
 
-let notNeccessaryThreadAnalyses = ["deadlock"; "maylocks"; "symb_locks"; "thread"; "threadflag"; "threadid"; "threadJoins"; "threadreturn"]
+let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"]
 let reduceThreadAnalyses () =
   let hasThreadCreate () =
     ResettableLazy.force functionCallMaps

sv-comp/archive.sh

@@ -3,7 +3,22 @@
 # must have goblint checked out into goblint not analyzer directory
 
 make clean
-make
+
+git tag -m "SV-COMP 2023" svcomp23
+
+dune build --profile=release src/goblint.exe
+rm -f goblint
+cp _build/default/src/goblint.exe goblint
+chmod +w goblint
+# must replace absolute apron runpath to C library with relative
+chrpath -r '$ORIGIN/lib' goblint
+# copy just necessary apron C libraries
+mkdir -p lib/
+cp _opam/share/apron/lib/libapron.so lib/
+cp _opam/share/apron/lib/liboctD.so lib/
+cp _opam/share/apron/lib/libboxD.so lib/
+cp _opam/share/apron/lib/libpolkaMPQ.so lib/
+cp _opam/.opam-switch/sources/apron/COPYING lib/LICENSE.APRON
 
 # done outside to ensure archive contains goblint/ directory
 cd ..
@@ -12,7 +27,14 @@ rm goblint/sv-comp/goblint.zip
 
 zip goblint/sv-comp/goblint.zip \
     goblint/goblint \
-    goblint/conf/svcomp22.json \
+    goblint/lib/libapron.so \
+    goblint/lib/liboctD.so \
+    goblint/lib/libboxD.so \
+    goblint/lib/libpolkaMPQ.so \
+    goblint/lib/LICENSE.APRON \
+    goblint/conf/svcomp23.json \
+    goblint/includes/assert.h \
+    goblint/includes/goblint.h \
     goblint/includes/stdlib.c \
     goblint/includes/pthread.c \
     goblint/includes/sv-comp.c \

tests/regression/46-apron2/24-pipeline-no-threadflag.c

@@ -0,0 +1,16 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[-] threadflag
+// Minimized from sv-benchmarks/c/systemc/pipeline.cil-1.c
+#include <assert.h>
+
+int main_clk_pos_edge;
+int main_in1_req_up;
+
+int main()
+{
+  // main_clk_pos_edge = 2; // TODO: uncomment to unskip apron test
+  if (main_in1_req_up == 1) // TODO: both branches are dead
+    assert(0); // TODO: uncomment to unskip apron test, FAIL (unreachable)
+  else
+    assert(1); // reachable
+  return (0);
+}