Merge branch 'master' into reanalyze-dce

Author: sim642

.github/workflows/semgrep.yml

@@ -11,20 +11,15 @@ jobs:
   semgrep:
     runs-on: ubuntu-latest
 
-    continue-on-error: true # TODO: remove when semgrep fixed: https://github.com/returntocorp/semgrep-action/issues/429
+    container:
+      image: returntocorp/semgrep
 
     steps:
       - name: Checkout code
         uses: actions/checkout@v3
 
       - name: Run semgrep
-        uses: returntocorp/semgrep-action@v1
-        with:
-          config: >-
-            .semgrep/
-          generateSarif: "1"
-        env:
-          SEMGREP_AGENT_DEBUG: 1 # https://github.com/returntocorp/semgrep-action/issues/429
+        run: semgrep scan --sarif --output=semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
         uses: github/codeql-action/upload-sarif@v2

.gitignore

@@ -53,7 +53,9 @@ goblint.bc.js
 
 sv-comp/goblint.zip
 
-privPrecCompare*
+privPrecCompare
+privPrecCompare-creduce
+privPrecCompareRes
 apronPrecCompare
 messagesCompare
 tests/regression/*/run

.semgrep/stats.yml

@@ -0,0 +1,7 @@
+rules:
+  - id: stats-time-partial
+    patterns:
+      - pattern: Stats.time $NAME $FUNC $ARG $BADARG ...
+    message: Stats.time measuring only partial, not complete function application (see https://goblint.readthedocs.io/en/latest/developer-guide/profiling/#stats)
+    languages: [ocaml]
+    severity: ERROR

dune-project

@@ -45,6 +45,8 @@
     (sha (>= 1.12))
     cpu
     arg-complete
+    yaml
+    uuidm
     (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS
     (conf-ruby :with-test)
     (benchmark :with-test) ; TODO: make this optional somehow, (optional) on bench executable doesn't work

goblint.opam

@@ -41,6 +41,8 @@ depends: [
   "sha" {>= "1.12"}
   "cpu"
   "arg-complete"
+  "yaml"
+  "uuidm"
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}
   "benchmark" {with-test}

goblint.opam.locked

@@ -31,6 +31,7 @@ depends: [
   "bigarray-compat" {= "1.1.0"}
   "bigstringaf" {= "0.8.0"}
   "biniou" {= "1.2.1"}
+  "bos" {= "0.2.1"}
   "camlidl" {= "1.09"}
   "cmdliner" {= "1.1.1" & with-doc}
   "conf-autoconf" {= "0.1"}
@@ -43,16 +44,20 @@ depends: [
   "cppo" {= "1.6.8"}
   "cpu" {= "2.0.0"}
   "csexp" {= "1.5.1"}
+  "ctypes" {= "0.20.1"}
   "dune" {= "3.0.3"}
   "dune-private-libs" {= "3.0.3"}
   "dune-site" {= "3.0.3"}
   "dyn" {= "3.0.3"}
+  "dune-configurator" {= "3.0.3"}
   "easy-format" {= "1.3.2"}
-  "fmt" {= "0.9.0" & with-doc}
+  "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
   "goblint-cil" {= "1.8.2"}
+  "integers" {= "0.7.0"}
   "json-data-encoding" {= "0.11"}
   "jsonrpc" {= "1.10.3"}
+  "logs" {= "0.7.0"}
   "mlgmpidl" {= "1.2.14"}
   "num" {= "1.4"}
   "ocaml" {= "4.14.0"}
@@ -80,6 +85,7 @@ depends: [
   "qcheck-ounit" {= "0.18.1" & with-test}
   "re" {= "1.10.3" & with-doc}
   "result" {= "1.5"}
+  "rresult" {= "0.7.0"}
   "seq" {= "base" & with-test}
   "sexplib0" {= "v0.14.0"}
   "sha" {= "1.15.2"}
@@ -89,7 +95,9 @@ depends: [
   "topkg" {= "1.0.5"}
   "tyxml" {= "4.5.0" & with-doc}
   "uri" {= "4.2.0"}
+  "uuidm" {= "0.9.8"}
   "uutf" {= "1.0.3" & with-doc}
+  "yaml" {= "3.1.0"}
   "yojson" {= "1.7.0"}
   "zarith" {= "1.12"}
 ]

src/dune

@@ -8,7 +8,7 @@
   (public_name goblint.lib)
   (wrapped false)
   (modules :standard \ goblint mainarinc mainspec privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.

src/framework/analyses.ml

@@ -197,7 +197,7 @@ struct
         Messages.xml_file_name := fn;
         BatPrintf.printf "Writing xml to temp. file: %s\n%!" fn;
         BatPrintf.fprintf f "<run>";
-        BatPrintf.fprintf f "<parameters>%a</parameters>" (BatArray.print ~first:"" ~last:"" ~sep:" " BatString.print) BatSys.argv;
+        BatPrintf.fprintf f "<parameters>%s</parameters>" Goblintutil.command_line;
         BatPrintf.fprintf f "<statistics>";
         (* FIXME: This is a super ridiculous hack we needed because BatIO has no way to get the raw channel CIL expects here. *)
         let name, chn = Filename.open_temp_file "stat" "goblint" in
@@ -241,7 +241,7 @@ struct
       let p_file f x = fprintf f "{\n  \"name\": \"%s\",\n  \"path\": \"%s\",\n  \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in
       let write_file f fn =
         printf "Writing json to temp. file: %s\n%!" fn;
-        fprintf f "{\n  \"parameters\": \"%a\",\n  " (BatArray.print ~first:"" ~last:"" ~sep:" " BatString.print) BatSys.argv;
+        fprintf f "{\n  \"parameters\": \"%s\",\n  " Goblintutil.command_line;
         fprintf f "\"files\": %a,\n  " (p_enum p_file) (SH.keys file2funs);
         fprintf f "\"results\": [\n  %a\n]\n" printJson (Lazy.force table);
         (*gtfxml f gtable;*)

src/framework/control.ml

@@ -492,7 +492,7 @@ struct
             GobConfig.write_file config;
             let module Meta = struct
                 type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]
-                let json = to_yojson { command = GU.command; version = Version.goblint; timestamp = Unix.time (); localtime = localtime () }
+                let json = to_yojson { command = GU.command_line; version = Version.goblint; timestamp = Unix.time (); localtime = localtime () }
               end
             in
             (* Yojson.Safe.to_file meta Meta.json; *)
@@ -673,6 +673,11 @@ struct
     if get_bool "ana.sv-comp.enabled" then
       WResult.write lh gh entrystates;
 
+    if get_bool "witness.yaml.enabled" then (
+      let module YWitness = YamlWitness.Make (struct let file = file end) (Cfg) (Spec) (EQSys) (LHT) (GHT) in
+      YWitness.write lh gh
+    );
+
     let marshal = Spec.finalize () in
     (* copied from solve_and_postprocess *)
     let gobview = get_bool "gobview" in

src/goblint.ml

@@ -21,7 +21,7 @@ let main () =
     handle_flags ();
     if get_bool "dbg.verbose" then (
       print_endline (localtime ());
-      print_endline command;
+      print_endline Goblintutil.command_line;
     );
     let file = Fun.protect ~finally:GoblintDir.finalize preprocess_and_merge in
     if get_bool "server.enabled" then Server.start file else (