From df336a33c8a6d6b19d7d8cd3e694b4dbdaa3b19f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 23 May 2022 17:24:05 +0300
Subject: [PATCH 01/19] Add yaml dependency

---
 dune-project        | 1 +
 goblint.opam        | 1 +
 goblint.opam.locked | 9 ++++++++-
 src/dune            | 2 +-
 4 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/dune-project b/dune-project
index c142b805c7..d54bd7d0d0 100644
--- a/dune-project
+++ b/dune-project
@@ -45,6 +45,7 @@
     (sha (>= 1.12))
     cpu
     arg-complete
+    yaml
     (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
diff --git a/goblint.opam b/goblint.opam
index 32260d4324..0024400d13 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -41,6 +41,7 @@ depends: [
   "sha" {>= "1.12"}
   "cpu"
   "arg-complete"
+  "yaml"
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}
   "benchmark" {with-test}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 4ae124b8cc..17965933ce 100644
--- a/goblint.opam.locked
+++ b/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"}
@@ -90,6 +96,7 @@ depends: [
   "tyxml" {= "4.5.0" & with-doc}
   "uri" {= "4.2.0"}
   "uutf" {= "1.0.3" & with-doc}
+  "yaml" {= "3.1.0"}
   "yojson" {= "1.7.0"}
   "zarith" {= "1.12"}
 ]
diff --git a/src/dune b/src/dune
index 8b2f7aca8f..0da4c3fef1 100644
--- a/src/dune
+++ b/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
     ; 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.

From e3311fd65d437d8fd4969732c5e00b2a6c3d730a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 23 May 2022 17:24:28 +0300
Subject: [PATCH 02/19] Add yaml witness prototype

---
 src/framework/control.ml   |  3 +++
 src/witness/yamlWitness.ml | 52 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 src/witness/yamlWitness.ml

diff --git a/src/framework/control.ml b/src/framework/control.ml
index ab73bd3ecf..15510583c5 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -678,6 +678,9 @@ struct
     if get_bool "ana.sv-comp.enabled" then
       WResult.write lh gh entrystates;
 
+    let module YWitness = YamlWitness.Make (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
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
new file mode 100644
index 0000000000..9ea8da523d
--- /dev/null
+++ b/src/witness/yamlWitness.ml
@@ -0,0 +1,52 @@
+open Analyses
+
+module Make
+    (Spec : Spec)
+    (EQSys : GlobConstrSys with module LVar = VarF (Spec.C)
+                        and module GVar = GVarF (Spec.V)
+                        and module D = Spec.D
+                        and module G = Spec.G)
+    (LHT : BatHashtbl.S with type key = EQSys.LVar.t)
+    (GHT : BatHashtbl.S with type key = EQSys.GVar.t) =
+struct
+
+  let write lh gh =
+    let entries = LHT.fold (fun (n, _) local acc ->
+        let context: Invariant.context = {
+            scope=Node.find_fundec n;
+            i = -1;
+            lval=None;
+            offset=Cil.NoOffset;
+            deref_invariant=(fun _ _ _ -> Invariant.none) (* TODO: should throw instead? *)
+          }
+        in
+        match Spec.D.invariant context local with
+        | Some inv ->
+          let inv = InvariantCil.exp_replace_original_name inv in
+          let loc = Node.location n in
+          let entry = `O [
+              ("entry_type", `String "loop_invariant");
+              ("metadata", `O [
+                  ("format_version", `String "0.1");
+                ]);
+              ("location", `O [
+                  ("file_name", `String loc.file);
+                  ("line", `Float (float_of_int loc.line));
+                  ("column", `Float (float_of_int (loc.column - 1)));
+                  ("function", `String (Node.find_fundec n).svar.vname);
+                ]);
+              ("loop_invariant", `O [
+                  ("string", `String (CilType.Exp.show inv));
+                  ("type", `String "assertion");
+                  ("format", `String "C");
+                ]);
+            ]
+          in
+          entry :: acc
+        | None ->
+          acc
+      ) lh []
+    in
+    let y = `A entries in
+    Format.printf "YAML:\n%a\n" Yaml.pp y
+end
\ No newline at end of file

From b25d33bbc6272de0c5d5195dde430f9150005835 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 10:48:23 +0300
Subject: [PATCH 03/19] Add options for yaml witnesses

---
 src/dune                     |  2 +-
 src/framework/control.ml     |  6 ++++--
 src/util/options.schema.json | 19 +++++++++++++++++++
 src/witness/yamlWitness.ml   |  6 +++---
 4 files changed, 27 insertions(+), 6 deletions(-)

diff --git a/src/dune b/src/dune
index 0da4c3fef1..fcadccc662 100644
--- a/src/dune
+++ b/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 yaml
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix
     ; 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.
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 15510583c5..64629899c1 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -678,8 +678,10 @@ struct
     if get_bool "ana.sv-comp.enabled" then
       WResult.write lh gh entrystates;
 
-    let module YWitness = YamlWitness.Make (Spec) (EQSys) (LHT) (GHT) in
-    YWitness.write lh gh;
+    if get_bool "witness.yaml.enabled" then (
+      let module YWitness = YamlWitness.Make (Spec) (EQSys) (LHT) (GHT) in
+      YWitness.write lh gh
+    );
 
     let marshal = Spec.finalize () in
     (* copied from solve_and_postprocess *)
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index ed8828c002..f545ac3c0b 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1788,6 +1788,25 @@
           "description": "Output witness for unknown result",
           "type": "boolean",
           "default": true
+        },
+        "yaml": {
+          "title": "witness.yaml",
+          "type": "object",
+          "properties": {
+            "enabled": {
+              "title": "witness.yaml.enabled",
+              "description": "Output YAML witness",
+              "type": "boolean",
+              "default": false
+            },
+            "path": {
+              "title": "witness.yaml.path",
+              "description": "YAML witness output path",
+              "type": "string",
+              "default": "witness.yml"
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 9ea8da523d..17fbeac53d 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -47,6 +47,6 @@ struct
           acc
       ) lh []
     in
-    let y = `A entries in
-    Format.printf "YAML:\n%a\n" Yaml.pp y
-end
\ No newline at end of file
+    let yaml = `A entries in
+    Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.path")) yaml
+end

From 9e1da44765540d298a42fdbd411866f78be46c5a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 11:07:54 +0300
Subject: [PATCH 04/19] Add uuidm dependency

---
 dune-project        | 1 +
 goblint.opam        | 1 +
 goblint.opam.locked | 1 +
 3 files changed, 3 insertions(+)

diff --git a/dune-project b/dune-project
index d54bd7d0d0..156f57ab22 100644
--- a/dune-project
+++ b/dune-project
@@ -46,6 +46,7 @@
     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
diff --git a/goblint.opam b/goblint.opam
index 0024400d13..26d33c1475 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -42,6 +42,7 @@ depends: [
   "cpu"
   "arg-complete"
   "yaml"
+  "uuidm"
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}
   "benchmark" {with-test}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 17965933ce..9946ac7b25 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -95,6 +95,7 @@ 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"}

From 81cee80a8e951510727ec2d183e0a94b77e6e88d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 11:23:30 +0300
Subject: [PATCH 05/19] Add more yaml witness fields

---
 src/dune                   |  2 +-
 src/witness/yamlWitness.ml | 34 ++++++++++++++++++++++++++++++++--
 2 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/src/dune b/src/dune
index fcadccc662..f53944d9a1 100644
--- a/src/dune
+++ b/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 yaml yaml.unix
+  (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.
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 17fbeac53d..72707cbb35 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -1,5 +1,7 @@
 open Analyses
 
+let uuid_random_state = Random.State.make_self_init ()
+
 module Make
     (Spec : Spec)
     (EQSys : GlobConstrSys with module LVar = VarF (Spec.C)
@@ -11,7 +13,28 @@ module Make
 struct
 
   let write lh gh =
-    let entries = LHT.fold (fun (n, _) local acc ->
+    let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in
+    let yaml_producer = `O [
+        ("name", `String "Goblint");
+        ("version", `String Version.goblint);
+        (* TODO: configuration *)
+        (* TODO: command_line *)
+        (* TODO: description *)
+      ]
+    in
+    let files = GobConfig.get_string_list "files" in
+    let yaml_task = `O [
+        ("input_files", `A (List.map Yaml.Util.string files));
+        ("input_file_hashes", `O (List.map (fun f ->
+            (f, `String (Sha256.(to_hex (file f))))
+          ) files));
+        (* TODO: specification *)
+        (* TODO: data_model *)
+        ("language", `String "C");
+      ]
+    in
+
+    let yaml_entries = LHT.fold (fun (n, _) local acc ->
         let context: Invariant.context = {
             scope=Node.find_fundec n;
             i = -1;
@@ -24,13 +47,19 @@ struct
         | Some inv ->
           let inv = InvariantCil.exp_replace_original_name inv in
           let loc = Node.location n in
+          let uuid = Uuidm.v4_gen uuid_random_state () in
           let entry = `O [
               ("entry_type", `String "loop_invariant");
               ("metadata", `O [
                   ("format_version", `String "0.1");
+                  ("uuid", `String (Uuidm.to_string uuid));
+                  ("creation_time", yaml_creation_time);
+                  ("producer", yaml_producer);
+                  ("task", yaml_task);
                 ]);
               ("location", `O [
                   ("file_name", `String loc.file);
+                  ("file_hash", `String (Sha256.(to_hex (file loc.file))));
                   ("line", `Float (float_of_int loc.line));
                   ("column", `Float (float_of_int (loc.column - 1)));
                   ("function", `String (Node.find_fundec n).svar.vname);
@@ -47,6 +76,7 @@ struct
           acc
       ) lh []
     in
-    let yaml = `A entries in
+
+    let yaml = `A yaml_entries in
     Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.path")) yaml
 end

From f0ca5ff93675624bc99fc65aba4709207d1d534f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 11:27:42 +0300
Subject: [PATCH 06/19] Add SHA256 caching to yaml witness

---
 src/witness/yamlWitness.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 72707cbb35..ff4e9dff4e 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -23,10 +23,13 @@ struct
       ]
     in
     let files = GobConfig.get_string_list "files" in
+    let sha256_file f = Sha256.(to_hex (file f)) in
+    let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 in
+    let sha256_file = sha256_file_cache.get in
     let yaml_task = `O [
         ("input_files", `A (List.map Yaml.Util.string files));
-        ("input_file_hashes", `O (List.map (fun f ->
-            (f, `String (Sha256.(to_hex (file f))))
+        ("input_file_hashes", `O (List.map (fun file ->
+            (file, `String (sha256_file file))
           ) files));
         (* TODO: specification *)
         (* TODO: data_model *)
@@ -59,7 +62,7 @@ struct
                 ]);
               ("location", `O [
                   ("file_name", `String loc.file);
-                  ("file_hash", `String (Sha256.(to_hex (file loc.file))));
+                  ("file_hash", `String (sha256_file loc.file));
                   ("line", `Float (float_of_int loc.line));
                   ("column", `Float (float_of_int (loc.column - 1)));
                   ("function", `String (Node.find_fundec n).svar.vname);

From 45ac46261f09af3ed346211633fc9bbc1e07f9ea Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 11:39:46 +0300
Subject: [PATCH 07/19] Add join over all contexts to yaml witness

---
 src/witness/yamlWitness.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index ff4e9dff4e..8ee8adf2b3 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -12,6 +12,17 @@ module Make
     (GHT : BatHashtbl.S with type key = EQSys.GVar.t) =
 struct
 
+  module NH = BatHashtbl.Make (Node)
+
+  (* copied from Constraints.CompareNode *)
+  let join_contexts (lh: Spec.D.t LHT.t): Spec.D.t NH.t =
+    let nh = NH.create 113 in
+    LHT.iter (fun (n, _) d ->
+        let d' = try Spec.D.join (NH.find nh n) d with Not_found -> d in
+        NH.replace nh n d'
+      ) lh;
+    nh
+
   let write lh gh =
     let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in
     let yaml_producer = `O [
@@ -37,7 +48,9 @@ struct
       ]
     in
 
-    let yaml_entries = LHT.fold (fun (n, _) local acc ->
+    let nh = join_contexts lh in
+
+    let yaml_entries = NH.fold (fun n local acc ->
         let context: Invariant.context = {
             scope=Node.find_fundec n;
             i = -1;
@@ -77,7 +90,7 @@ struct
           entry :: acc
         | None ->
           acc
-      ) lh []
+      ) nh []
     in
 
     let yaml = `A yaml_entries in

From a558f0f457fda2d6fe71df3a8ed32a395885a7ee Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 11:49:54 +0300
Subject: [PATCH 08/19] Only emit yaml entries for Statement nodes

---
 src/witness/yamlWitness.ml | 79 ++++++++++++++++++++------------------
 1 file changed, 42 insertions(+), 37 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 8ee8adf2b3..c0dea116d0 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -51,44 +51,49 @@ struct
     let nh = join_contexts lh in
 
     let yaml_entries = NH.fold (fun n local acc ->
-        let context: Invariant.context = {
-            scope=Node.find_fundec n;
-            i = -1;
-            lval=None;
-            offset=Cil.NoOffset;
-            deref_invariant=(fun _ _ _ -> Invariant.none) (* TODO: should throw instead? *)
-          }
-        in
-        match Spec.D.invariant context local with
-        | Some inv ->
-          let inv = InvariantCil.exp_replace_original_name inv in
-          let loc = Node.location n in
-          let uuid = Uuidm.v4_gen uuid_random_state () in
-          let entry = `O [
-              ("entry_type", `String "loop_invariant");
-              ("metadata", `O [
-                  ("format_version", `String "0.1");
-                  ("uuid", `String (Uuidm.to_string uuid));
-                  ("creation_time", yaml_creation_time);
-                  ("producer", yaml_producer);
-                  ("task", yaml_task);
-                ]);
-              ("location", `O [
-                  ("file_name", `String loc.file);
-                  ("file_hash", `String (sha256_file loc.file));
-                  ("line", `Float (float_of_int loc.line));
-                  ("column", `Float (float_of_int (loc.column - 1)));
-                  ("function", `String (Node.find_fundec n).svar.vname);
-                ]);
-              ("loop_invariant", `O [
-                  ("string", `String (CilType.Exp.show inv));
-                  ("type", `String "assertion");
-                  ("format", `String "C");
-                ]);
-            ]
+        match n with
+        | Statement _ ->
+          let context: Invariant.context = {
+              scope=Node.find_fundec n;
+              i = -1;
+              lval=None;
+              offset=Cil.NoOffset;
+              deref_invariant=(fun _ _ _ -> Invariant.none) (* TODO: should throw instead? *)
+            }
           in
-          entry :: acc
-        | None ->
+          begin match Spec.D.invariant context local with
+            | Some inv ->
+              let inv = InvariantCil.exp_replace_original_name inv in
+              let loc = Node.location n in
+              let uuid = Uuidm.v4_gen uuid_random_state () in
+              let entry = `O [
+                  ("entry_type", `String "loop_invariant");
+                  ("metadata", `O [
+                      ("format_version", `String "0.1");
+                      ("uuid", `String (Uuidm.to_string uuid));
+                      ("creation_time", yaml_creation_time);
+                      ("producer", yaml_producer);
+                      ("task", yaml_task);
+                    ]);
+                  ("location", `O [
+                      ("file_name", `String loc.file);
+                      ("file_hash", `String (sha256_file loc.file));
+                      ("line", `Float (float_of_int loc.line));
+                      ("column", `Float (float_of_int (loc.column - 1)));
+                      ("function", `String (Node.find_fundec n).svar.vname);
+                    ]);
+                  ("loop_invariant", `O [
+                      ("string", `String (CilType.Exp.show inv));
+                      ("type", `String "assertion");
+                      ("format", `String "C");
+                    ]);
+                ]
+              in
+              entry :: acc
+            | None ->
+              acc
+          end
+        | _ -> (* avoid FunctionEntry/Function because their locations are not inside the function where assert could be inserted *)
           acc
       ) nh []
     in

From ed66dac9fcacd5f4d21cd195f0044fb0bcefcce5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 12:03:07 +0300
Subject: [PATCH 09/19] Add commented out dumping of conf to yaml witness

---
 src/witness/yamlWitness.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index c0dea116d0..91207d0882 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -24,11 +24,14 @@ struct
     nh
 
   let write lh gh =
+    (* yaml_conf is too verbose *)
+    (* let yaml_conf: Yaml.value = Json_repr.convert (module Json_repr.Yojson) (module Json_repr.Ezjsonm) (!GobConfig.json_conf) in *)
     let yaml_creation_time = `String (TimeUtil.iso8601_now ()) in
     let yaml_producer = `O [
         ("name", `String "Goblint");
         ("version", `String Version.goblint);
         (* TODO: configuration *)
+        (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *)
         (* TODO: command_line *)
         (* TODO: description *)
       ]

From 310beddee89be85dcfafd9f7829999acc19dec33 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 12:11:55 +0300
Subject: [PATCH 10/19] Add command_line to yaml witness

---
 src/framework/analyses.ml  | 4 ++--
 src/framework/control.ml   | 2 +-
 src/goblint.ml             | 2 +-
 src/util/goblintutil.ml    | 4 +++-
 src/util/sarif.ml          | 6 +-----
 src/witness/yamlWitness.ml | 2 +-
 6 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 1fc7930e83..bb8dea5e1a 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -207,7 +207,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
@@ -251,7 +251,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;*)
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 64629899c1..7393cd1b4b 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -495,7 +495,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; *)
diff --git a/src/goblint.ml b/src/goblint.ml
index e1c0f26c69..b691c0883d 100644
--- a/src/goblint.ml
+++ b/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 (
diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml
index d218d9cae6..d0d3c4c1ee 100644
--- a/src/util/goblintutil.ml
+++ b/src/util/goblintutil.ml
@@ -138,7 +138,9 @@ let arinc_period        = if scrambled then "M165" else "PERIOD"
 let arinc_time_capacity = if scrambled then "M166" else "TIME_CAPACITY"
 
 let exe_dir = Fpath.(parent (v Sys.executable_name))
-let command = String.concat " " (Array.to_list Sys.argv)
+let command_line = match Array.to_list Sys.argv with
+  | command :: arguments -> Filename.quote_command command arguments
+  | [] -> assert false
 
 (* https://ocaml.org/api/Sys.html#2_SignalnumbersforthestandardPOSIXsignals *)
 (* https://ocaml.github.io/ocamlunix/signals.html *)
diff --git a/src/util/sarif.ml b/src/util/sarif.ml
index 7a154334ea..7deec07490 100644
--- a/src/util/sarif.ml
+++ b/src/util/sarif.ml
@@ -130,16 +130,12 @@ let artifacts_of_messages (messages: Messages.Message.t list): Artifact.t list =
   |> List.of_enum
 
 let to_yojson messages =
-  let commandLine = match Array.to_list Sys.argv with
-    | command :: arguments -> Filename.quote_command command arguments
-    | [] -> assert false
-  in
   SarifLog.to_yojson {
     version = "2.1.0";
     schema = "https://schemastore.azurewebsites.net/schemas/json/sarif-2.1.0-rtm.5.json";
     runs = [{
         invocations = [{
-            commandLine;
+            commandLine = Goblintutil.command_line;
             executionSuccessful = true;
           }];
         artifacts = artifacts_of_messages messages;
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 91207d0882..1da57862c1 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -32,7 +32,7 @@ struct
         ("version", `String Version.goblint);
         (* TODO: configuration *)
         (* ("configuration", yaml_conf); *) (* yaml_conf is too verbose *)
-        (* TODO: command_line *)
+        ("command_line", `String Goblintutil.command_line);
         (* TODO: description *)
       ]
     in

From 44141c5745b69560492dc46452b3360865f48b2d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 12:21:44 +0300
Subject: [PATCH 11/19] Add architecture and specification to yaml witness

---
 src/util/options.schema.json |  1 +
 src/witness/yamlWitness.ml   | 16 ++++++++++++----
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index f545ac3c0b..e52a9b0bc5 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1286,6 +1286,7 @@
           "title": "exp.architecture",
           "description": "Architecture for analysis, currently for witness",
           "type": "string",
+          "enum": ["64bit", "32bit"],
           "default": "64bit"
         },
         "gcc_path": {
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 1da57862c1..ad73090e05 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -40,15 +40,23 @@ struct
     let sha256_file f = Sha256.(to_hex (file f)) in
     let sha256_file_cache = BatCache.make_ht ~gen:sha256_file ~init_size:5 in
     let sha256_file = sha256_file_cache.get in
-    let yaml_task = `O [
+    let yaml_task = `O ([
         ("input_files", `A (List.map Yaml.Util.string files));
         ("input_file_hashes", `O (List.map (fun file ->
             (file, `String (sha256_file file))
           ) files));
-        (* TODO: specification *)
-        (* TODO: data_model *)
+        ("data_model", `String (match GobConfig.get_string "exp.architecture" with
+          | "64bit" -> "LP64"
+          | "32bit" -> "ILP32"
+          | _ -> failwith "invalid architecture"));
         ("language", `String "C");
-      ]
+      ] @ match !Svcomp.task with
+            | Some (module Task) -> [
+                ("specification", `String (Svcomp.Specification.to_string Task.specification))
+              ]
+            | None ->
+              []
+      )
     in
 
     let nh = join_contexts lh in

From 4fbd0ef41bb42c63a1562e1c0f648ae52b1ae3ee Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 15:05:05 +0300
Subject: [PATCH 12/19] Move trans.assert options to witness.invariant for
 unification

---
 src/transform/evalAssert.ml  | 12 ++++++------
 src/util/options.schema.json | 35 ++++++++++++++---------------------
 2 files changed, 20 insertions(+), 27 deletions(-)

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index f2e5a66ce2..e34f35b1ce 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -4,14 +4,14 @@ open Formatcil
 module ES = SetDomain.Make(Exp.Exp)
 
 (** Instruments a program by inserting asserts either:
-    - After an assignment to a variable (unless trans.assert.full is activated) and
+    - After an assignment to a variable (unless witness.invariant.full is activated) and
     - At join points about all local variables
 
                 OR
 
-    - Only after pthread_mutex_lock (trans.assert.only-at-locks), about all locals and globals
+    - Only after pthread_mutex_lock (witness.invariant.only-at-locks), about all locals and globals
 
-    Limitations without trans.assert.only-at locks:
+    Limitations without witness.invariant.only-at-locks:
     - Currently only works for top-level variables (not inside an array, a struct, ...)
     - Does not work for accesses through pointers
     - At join points asserts all locals, but ideally should only assert ones that are
@@ -57,8 +57,8 @@ module EvalAssert = struct
 
   class visitor (ask:Cil.location -> Queries.ask) = object(self)
     inherit nopCilVisitor
-    val full = GobConfig.get_bool "trans.assert.full"
-    val only_at_locks = GobConfig.get_bool "trans.assert.only-at-locks"
+    val full = GobConfig.get_bool "witness.invariant.full"
+    val only_at_locks = GobConfig.get_bool "witness.invariant.only-at-locks"
 
     method! vstmt s =
       let is_lock exp args =
@@ -135,7 +135,7 @@ module EvalAssert = struct
         | [p1; p2] when not only_at_locks ->
           (* exactly two predecessors -> join point, assert locals if they changed *)
           let join_loc = get_stmtLoc s.skind in
-          (* Possible enhancement: It would be nice to only assert locals here that were modified in either branch if trans.assert.full is false *)
+          (* Possible enhancement: It would be nice to only assert locals here that were modified in either branch if witness.invariant.full is false *)
           let asserts = make_assert join_loc None in
           self#queueInstr asserts; ()
         | _ -> ()
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index e52a9b0bc5..0331ca1f29 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1059,27 +1059,6 @@
           "description": "Output filename for transformations that output a transformed file.",
           "type":"string",
           "default": "transformed.c"
-        },
-        "assert": {
-          "title": "trans.assert",
-          "type": "object",
-          "properties": {
-            "full": {
-              "title": "trans.assert.full",
-              "description":
-                "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
-              "type": "boolean",
-              "default": true
-            },
-            "only-at-locks":{
-              "title": "trans.assert.only-at-locks",
-              "description":
-                "Only put locks after mutexes have been acquired.",
-              "type": "boolean",
-              "default": true
-            }
-          },
-          "additionalProperties": false
         }
       },
       "additionalProperties": false
@@ -1761,6 +1740,20 @@
               "type": "string",
               "enum": ["all", "loop_heads", "none"],
               "default": "all"
+            },
+            "full": {
+              "title": "witness.invariant.full",
+              "description":
+                "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
+              "type": "boolean",
+              "default": true
+            },
+            "only-at-locks":{
+              "title": "witness.invariant.only-at-locks",
+              "description":
+                "Only put locks after mutexes have been acquired.",
+              "type": "boolean",
+              "default": true
             }
           },
           "additionalProperties": false

From 87473da0a1d5f2fd64dd488f00b89abdae955daf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 15:36:13 +0300
Subject: [PATCH 13/19] Refactor witness.invariant options

---
 src/transform/evalAssert.ml  | 20 +++++++++++---------
 src/util/options.schema.json | 30 ++++++++++++++++++------------
 src/witness/witness.ml       | 13 ++++++++-----
 3 files changed, 37 insertions(+), 26 deletions(-)

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index e34f35b1ce..11454c7475 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -9,9 +9,9 @@ module ES = SetDomain.Make(Exp.Exp)
 
                 OR
 
-    - Only after pthread_mutex_lock (witness.invariant.only-at-locks), about all locals and globals
+    - Only after pthread_mutex_lock (witness.invariant.after-lock), about all locals and globals
 
-    Limitations without witness.invariant.only-at-locks:
+    Limitations without witness.invariant.after-lock:
     - Currently only works for top-level variables (not inside an array, a struct, ...)
     - Does not work for accesses through pointers
     - At join points asserts all locals, but ideally should only assert ones that are
@@ -58,7 +58,9 @@ module EvalAssert = struct
   class visitor (ask:Cil.location -> Queries.ask) = object(self)
     inherit nopCilVisitor
     val full = GobConfig.get_bool "witness.invariant.full"
-    val only_at_locks = GobConfig.get_bool "witness.invariant.only-at-locks"
+    (* TODO: handle witness.invariant.loop-head *)
+    val emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock"
+    val emit_other = GobConfig.get_bool "witness.invariant.other"
 
     method! vstmt s =
       let is_lock exp args =
@@ -94,13 +96,13 @@ module EvalAssert = struct
         let unique_succ = s.succs <> [] && (List.hd s.succs).preds |> List.length < 2 in
         let instrument i loc =
           let instrument' lval =
-            let lval_arg = if full || only_at_locks then None else lval in
+            let lval_arg = if full then None else lval in
             make_assert loc lval_arg
           in
           match i with
-          | Set  (lval, _, _, _) when not only_at_locks -> instrument' (Some lval)
-          | Call (lval, _, _, _, _) when not only_at_locks -> instrument' lval
-          | Call (_, exp, args, _, _) when is_lock exp args -> instrument' None
+          | Call (_, exp, args, _, _) when emit_after_lock && is_lock exp args -> instrument' None
+          | Set  (lval, _, _, _) when emit_other -> instrument' (Some lval)
+          | Call (lval, _, _, _, _) when emit_other -> instrument' lval
           | _ -> []
         in
         let rec instrument_instructions = function
@@ -132,7 +134,7 @@ module EvalAssert = struct
 
       let instrument_join s =
         match s.preds with
-        | [p1; p2] when not only_at_locks ->
+        | [p1; p2] when emit_other ->
           (* exactly two predecessors -> join point, assert locals if they changed *)
           let join_loc = get_stmtLoc s.skind in
           (* Possible enhancement: It would be nice to only assert locals here that were modified in either branch if witness.invariant.full is false *)
@@ -161,7 +163,7 @@ module EvalAssert = struct
             else
               ()
           in
-          if not only_at_locks then (add_asserts b1; add_asserts b2);
+          if emit_other then (add_asserts b1; add_asserts b2);
           s
         | _ -> s
       in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 0331ca1f29..5c9679cd42 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1733,25 +1733,31 @@
           "title": "witness.invariant",
           "type": "object",
           "properties": {
-            "nodes": {
-              "title": "witness.invariant.nodes",
+            "loop-head":{
+              "title": "witness.invariant.loop-head",
               "description":
-                "Which witness nodes to add invariants to? all/loop_heads/none",
-              "type": "string",
-              "enum": ["all", "loop_heads", "none"],
-              "default": "all"
+                "Emit invariants at loop heads",
+              "type": "boolean",
+              "default": true
             },
-            "full": {
-              "title": "witness.invariant.full",
+            "after-lock":{
+              "title": "witness.invariant.after-lock",
               "description":
-                "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
+                "Emit invariants after mutex locking",
               "type": "boolean",
               "default": true
             },
-            "only-at-locks":{
-              "title": "witness.invariant.only-at-locks",
+            "other":{
+              "title": "witness.invariant.other",
               "description":
-                "Only put locks after mutexes have been acquired.",
+                "Emit invariants at all other locations",
+              "type": "boolean",
+              "default": true
+            },
+            "full": {
+              "title": "witness.invariant.full",
+              "description":
+                "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
               "type": "boolean",
               "default": true
             }
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 151333c6c9..684b69ab7f 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -10,12 +10,15 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   let module Cfg = Task.Cfg in
   let loop_heads = find_loop_heads (module Cfg) Task.file in
 
+  let emit_loop_head = GobConfig.get_bool "witness.invariant.loop-head" in
+  (* TODO: handle witness.invariant.after-lock *)
+  let emit_other = GobConfig.get_bool "witness.invariant.other" in
+
   let is_invariant_node cfgnode =
-    match get_string "witness.invariant.nodes" with
-    | "all" -> true
-    | "loop_heads" -> WitnessUtil.NH.mem loop_heads cfgnode
-    | "none" -> false
-    | _ -> failwith "witness.invariant.nodes: invalid value"
+    if WitnessUtil.NH.mem loop_heads cfgnode then
+      emit_loop_head
+    else
+      emit_other
   in
 
   let module TaskResult =

From 24b7789df1194d33f8ac9f93adb0100603aaa8b1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 15:48:38 +0300
Subject: [PATCH 14/19] Extract invariant node logic from GraphML witness
 generation

---
 src/witness/svcomp.ml      |  2 +-
 src/witness/witness.ml     | 22 +++++-----------------
 src/witness/witnessUtil.ml | 21 +++++++++++++++++++++
 3 files changed, 27 insertions(+), 18 deletions(-)

diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index 10d6b1e30a..b529838cc5 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -52,7 +52,7 @@ sig
   val file: Cil.file
   val specification: Specification.t
 
-  module Cfg: MyCFG.CfgForward
+  module Cfg: MyCFG.CfgBidir
 end
 
 let task: (module Task) option ref = ref None
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 684b69ab7f..790101ee30 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -1,5 +1,4 @@
 open MyCFG
-open WitnessUtil
 open Graphml
 open Svcomp
 open GobConfig
@@ -8,18 +7,7 @@ module type WitnessTaskResult = TaskResult with module Arg.Edge = MyARG.InlineEd
 
 let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult): unit =
   let module Cfg = Task.Cfg in
-  let loop_heads = find_loop_heads (module Cfg) Task.file in
-
-  let emit_loop_head = GobConfig.get_bool "witness.invariant.loop-head" in
-  (* TODO: handle witness.invariant.after-lock *)
-  let emit_other = GobConfig.get_bool "witness.invariant.other" in
-
-  let is_invariant_node cfgnode =
-    if WitnessUtil.NH.mem loop_heads cfgnode then
-      emit_loop_head
-    else
-      emit_other
-  in
+  let module Invariant = WitnessUtil.Invariant (struct let file = Task.file end) (Cfg) in
 
   let module TaskResult =
     (val if get_bool "witness.stack" then
@@ -41,12 +29,12 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
       let to_cfgnode = N.cfgnode to_node in
       if TaskResult.is_violation to_node || TaskResult.is_sink to_node then
         true
-      else if WitnessUtil.NH.mem loop_heads to_cfgnode then
+      else if WitnessUtil.NH.mem Invariant.loop_heads to_cfgnode then
         true
       else begin match edge with
         | MyARG.CFGEdge (Test _) -> true
         | _ -> false
-      end || begin if is_invariant_node to_cfgnode then
+      end || begin if Invariant.is_invariant_node to_cfgnode then
             match to_cfgnode, TaskResult.invariant to_node with
             | Statement _, Some _ -> true
             | _, _ -> false
@@ -145,7 +133,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
             []
         end;
         begin
-          if is_invariant_node cfgnode then
+          if Invariant.is_invariant_node cfgnode then
             match cfgnode, TaskResult.invariant node with
             | Statement _, Some i ->
               let i = InvariantCil.exp_replace_original_name i in
@@ -203,7 +191,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
           else
             []
         end;
-        begin if WitnessUtil.NH.mem loop_heads to_cfgnode then
+        begin if WitnessUtil.NH.mem Invariant.loop_heads to_cfgnode then
             [("enterLoopHead", "true")]
           else
             []
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index 3d757d8e35..51f0673ef7 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -56,3 +56,24 @@ module HashedList (M: Hashtbl.HashedType):
 struct
   type t = M.t list [@@deriving eq, hash]
 end
+
+
+module type File =
+sig
+  val file: Cil.file
+end
+
+module Invariant (File: File) (Cfg: MyCFG.CfgBidir) =
+struct
+  let emit_loop_head = GobConfig.get_bool "witness.invariant.loop-head"
+  (* TODO: handle witness.invariant.after-lock *)
+  let emit_other = GobConfig.get_bool "witness.invariant.other"
+
+  let loop_heads = find_loop_heads (module Cfg) File.file
+
+  let is_invariant_node cfgnode =
+    if NH.mem loop_heads cfgnode then
+      emit_loop_head
+    else
+      emit_other
+end

From d3935a3e80488b118c958e90ed0c0510de082342 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 15:58:54 +0300
Subject: [PATCH 15/19] Handle after-lock in WitnessUtil.Invariant

---
 src/witness/myARG.ml       |  3 +--
 src/witness/witnessUtil.ml | 30 ++++++++++++++++--------------
 2 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index a05efc5cdc..41421d42ed 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -1,4 +1,3 @@
-open WitnessUtil
 open MyCFG
 
 module type Node =
@@ -68,7 +67,7 @@ end
 module StackNode (Node: Node):
   Node with type t = Node.t list =
 struct
-  include HashedList (Node)
+  type t = Node.t list [@@deriving eq, hash]
 
   let cfgnode nl = Node.cfgnode (List.hd nl)
   let to_string nl =
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index 51f0673ef7..a9454b25b8 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -45,19 +45,6 @@ let find_loop_heads (module Cfg:CfgForward) (file:Cil.file): unit NH.t =
   loop_heads
 
 
-module HashedPair (M1: Hashtbl.HashedType) (M2: Hashtbl.HashedType):
-  Hashtbl.HashedType with type t = M1.t * M2.t =
-struct
-  type t = M1.t * M2.t [@@deriving eq, hash]
-end
-
-module HashedList (M: Hashtbl.HashedType):
-  Hashtbl.HashedType with type t = M.t list =
-struct
-  type t = M.t list [@@deriving eq, hash]
-end
-
-
 module type File =
 sig
   val file: Cil.file
@@ -66,14 +53,29 @@ end
 module Invariant (File: File) (Cfg: MyCFG.CfgBidir) =
 struct
   let emit_loop_head = GobConfig.get_bool "witness.invariant.loop-head"
-  (* TODO: handle witness.invariant.after-lock *)
+  let emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock"
   let emit_other = GobConfig.get_bool "witness.invariant.other"
 
   let loop_heads = find_loop_heads (module Cfg) File.file
 
+  let is_after_lock to_node =
+    List.exists (fun (edges, from_node) ->
+        List.exists (fun (_, edge) ->
+            match edge with
+            | Proc (_, Lval (Var fv, NoOffset), args) ->
+              begin match LibraryFunctions.classify fv.vname args with
+                | `Lock _ -> true
+                | _ -> false
+              end
+            | _ -> false
+          ) edges
+      ) (Cfg.prev to_node)
+
   let is_invariant_node cfgnode =
     if NH.mem loop_heads cfgnode then
       emit_loop_head
+    else if is_after_lock cfgnode then
+      emit_after_lock
     else
       emit_other
 end

From 175775b5e0abb7d3517bc47dd5169dd54f17041f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 16:09:34 +0300
Subject: [PATCH 16/19] Use witness.invariant options for yaml witness

---
 src/framework/control.ml   | 2 +-
 src/witness/yamlWitness.ml | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 7393cd1b4b..cb48c9994f 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -679,7 +679,7 @@ struct
       WResult.write lh gh entrystates;
 
     if get_bool "witness.yaml.enabled" then (
-      let module YWitness = YamlWitness.Make (Spec) (EQSys) (LHT) (GHT) in
+      let module YWitness = YamlWitness.Make (struct let file = file end) (Cfg) (Spec) (EQSys) (LHT) (GHT) in
       YWitness.write lh gh
     );
 
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index ad73090e05..3923833c3f 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -3,6 +3,8 @@ open Analyses
 let uuid_random_state = Random.State.make_self_init ()
 
 module Make
+    (File: WitnessUtil.File)
+    (Cfg: MyCFG.CfgBidir)
     (Spec : Spec)
     (EQSys : GlobConstrSys with module LVar = VarF (Spec.C)
                         and module GVar = GVarF (Spec.V)
@@ -13,6 +15,7 @@ module Make
 struct
 
   module NH = BatHashtbl.Make (Node)
+  module WitnessInvariant = WitnessUtil.Invariant (File) (Cfg)
 
   (* copied from Constraints.CompareNode *)
   let join_contexts (lh: Spec.D.t LHT.t): Spec.D.t NH.t =
@@ -63,7 +66,7 @@ struct
 
     let yaml_entries = NH.fold (fun n local acc ->
         match n with
-        | Statement _ ->
+        | Statement _ when WitnessInvariant.is_invariant_node n ->
           let context: Invariant.context = {
               scope=Node.find_fundec n;
               i = -1;

From ad9dde7fd16d70c283313741066cf163ede2243b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 14:34:20 +0300
Subject: [PATCH 17/19] Split conjunctions in yaml witness output to work
 around misparsing

https://github.com/goblint/cil/issues/94.
---
 src/witness/yamlWitness.ml | 53 ++++++++++++++++++++------------------
 1 file changed, 28 insertions(+), 25 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 3923833c3f..56be31436c 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -79,31 +79,34 @@ struct
             | Some inv ->
               let inv = InvariantCil.exp_replace_original_name inv in
               let loc = Node.location n in
-              let uuid = Uuidm.v4_gen uuid_random_state () in
-              let entry = `O [
-                  ("entry_type", `String "loop_invariant");
-                  ("metadata", `O [
-                      ("format_version", `String "0.1");
-                      ("uuid", `String (Uuidm.to_string uuid));
-                      ("creation_time", yaml_creation_time);
-                      ("producer", yaml_producer);
-                      ("task", yaml_task);
-                    ]);
-                  ("location", `O [
-                      ("file_name", `String loc.file);
-                      ("file_hash", `String (sha256_file loc.file));
-                      ("line", `Float (float_of_int loc.line));
-                      ("column", `Float (float_of_int (loc.column - 1)));
-                      ("function", `String (Node.find_fundec n).svar.vname);
-                    ]);
-                  ("loop_invariant", `O [
-                      ("string", `String (CilType.Exp.show inv));
-                      ("type", `String "assertion");
-                      ("format", `String "C");
-                    ]);
-                ]
-              in
-              entry :: acc
+              let invs = EvalAssert.EvalAssert.pullOutCommonConjuncts inv in
+              EvalAssert.ES.fold (fun inv acc ->
+                  let uuid = Uuidm.v4_gen uuid_random_state () in
+                  let entry = `O [
+                      ("entry_type", `String "loop_invariant");
+                      ("metadata", `O [
+                          ("format_version", `String "0.1");
+                          ("uuid", `String (Uuidm.to_string uuid));
+                          ("creation_time", yaml_creation_time);
+                          ("producer", yaml_producer);
+                          ("task", yaml_task);
+                        ]);
+                      ("location", `O [
+                          ("file_name", `String loc.file);
+                          ("file_hash", `String (sha256_file loc.file));
+                          ("line", `Float (float_of_int loc.line));
+                          ("column", `Float (float_of_int (loc.column - 1)));
+                          ("function", `String (Node.find_fundec n).svar.vname);
+                        ]);
+                      ("loop_invariant", `O [
+                          ("string", `String (CilType.Exp.show inv));
+                          ("type", `String "assertion");
+                          ("format", `String "C");
+                        ]);
+                    ]
+                  in
+                  entry :: acc
+                ) invs acc
             | None ->
               acc
           end

From 0efac228f95ffdc09ab112fd3ad386a0fc9b9770 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 16:25:14 +0300
Subject: [PATCH 18/19] Add option witness.invariant.split-conjunction

---
 src/transform/evalAssert.ml  | 26 +-------------------------
 src/util/options.schema.json | 12 +++++++++---
 src/witness/witnessUtil.ml   | 32 ++++++++++++++++++++++++++++++++
 src/witness/yamlWitness.ml   |  7 +++----
 4 files changed, 45 insertions(+), 32 deletions(-)

diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index 11454c7475..71f4a40769 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -1,7 +1,6 @@
 open Prelude
 open Cil
 open Formatcil
-module ES = SetDomain.Make(Exp.Exp)
 
 (** Instruments a program by inserting asserts either:
     - After an assignment to a variable (unless witness.invariant.full is activated) and
@@ -23,9 +22,6 @@ module ES = SetDomain.Make(Exp.Exp)
 *)
 
 module EvalAssert = struct
-  (* should asserts of conjuncts be one-by-one instead of one big assert?  *)
-  let distinctAsserts = true
-
   (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
   let surroundByAtomic = true
 
@@ -35,26 +31,6 @@ module EvalAssert = struct
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
 
-  (* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)
-  let rec pullOutCommonConjuncts e =
-    let rec to_conjunct_set = function
-      | BinOp(LAnd,e1,e2,_) -> ES.join (to_conjunct_set e1) (to_conjunct_set e2)
-      | e -> ES.singleton e
-    in
-    let combine_conjuncts es = ES.fold (fun e acc -> match acc with | None -> Some e | Some acce -> Some (BinOp(LAnd,acce,e,Cil.intType))) es None in
-    match e with
-    | BinOp(LOr, e1, e2,t) ->
-      let e1s = pullOutCommonConjuncts e1 in
-      let e2s = pullOutCommonConjuncts e2 in
-      let common = ES.inter e1s e2s in
-      let e1s' = ES.diff e1s e2s in
-      let e2s' = ES.diff e2s e1s in
-      (match combine_conjuncts e1s', combine_conjuncts e2s' with
-       | Some e1e, Some e2e -> ES.add (BinOp(LOr,e1e,e2e,Cil.intType)) common
-       | _ -> common (* if one of the disjuncts is empty, it is equivalent to true here *)
-      )
-    | e -> to_conjunct_set e
-
   class visitor (ask:Cil.location -> Queries.ask) = object(self)
     inherit nopCilVisitor
     val full = GobConfig.get_bool "witness.invariant.full"
@@ -80,7 +56,7 @@ module EvalAssert = struct
         } in
         match (ask loc).f (Queries.Invariant context) with
         | `Lifted e ->
-          let es = if distinctAsserts then ES.elements (pullOutCommonConjuncts e) else [e] in
+          let es = WitnessUtil.InvariantExp.process_exp e in
           let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv ass); ("exp", Fe e)]) es in
           if surroundByAtomic then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 5c9679cd42..290ded6d73 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1733,27 +1733,33 @@
           "title": "witness.invariant",
           "type": "object",
           "properties": {
-            "loop-head":{
+            "loop-head": {
               "title": "witness.invariant.loop-head",
               "description":
                 "Emit invariants at loop heads",
               "type": "boolean",
               "default": true
             },
-            "after-lock":{
+            "after-lock": {
               "title": "witness.invariant.after-lock",
               "description":
                 "Emit invariants after mutex locking",
               "type": "boolean",
               "default": true
             },
-            "other":{
+            "other": {
               "title": "witness.invariant.other",
               "description":
                 "Emit invariants at all other locations",
               "type": "boolean",
               "default": true
             },
+            "split-conjunction": {
+              "title": "witness.invariant.split-conjunction",
+              "description": "Split conjunctive invariant to multiple invariants",
+              "type": "boolean",
+              "default": true
+            },
             "full": {
               "title": "witness.invariant.full",
               "description":
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index a9454b25b8..ef1429deb9 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -79,3 +79,35 @@ struct
     else
       emit_other
 end
+
+module InvariantExp =
+struct
+  module ES = SetDomain.Make (Exp.Exp)
+
+  (* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)
+  let rec pullOutCommonConjuncts e =
+    let rec to_conjunct_set = function
+      | Cil.BinOp(LAnd,e1,e2,_) -> ES.join (to_conjunct_set e1) (to_conjunct_set e2)
+      | e -> ES.singleton e
+    in
+    let combine_conjuncts es = ES.fold (fun e acc -> match acc with | None -> Some e | Some acce -> Some (BinOp(LAnd,acce,e,Cil.intType))) es None in
+    match e with
+    | Cil.BinOp(LOr, e1, e2,t) ->
+      let e1s = pullOutCommonConjuncts e1 in
+      let e2s = pullOutCommonConjuncts e2 in
+      let common = ES.inter e1s e2s in
+      let e1s' = ES.diff e1s e2s in
+      let e2s' = ES.diff e2s e1s in
+      (match combine_conjuncts e1s', combine_conjuncts e2s' with
+       | Some e1e, Some e2e -> ES.add (BinOp(LOr,e1e,e2e,Cil.intType)) common
+       | _ -> common (* if one of the disjuncts is empty, it is equivalent to true here *)
+      )
+    | e -> to_conjunct_set e
+
+  let process_exp inv =
+    let inv' = InvariantCil.exp_replace_original_name inv in
+    if GobConfig.get_bool "witness.invariant.split-conjunction" then
+      ES.elements (pullOutCommonConjuncts inv')
+    else
+      [inv']
+end
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 56be31436c..4ef8828909 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -77,10 +77,9 @@ struct
           in
           begin match Spec.D.invariant context local with
             | Some inv ->
-              let inv = InvariantCil.exp_replace_original_name inv in
               let loc = Node.location n in
-              let invs = EvalAssert.EvalAssert.pullOutCommonConjuncts inv in
-              EvalAssert.ES.fold (fun inv acc ->
+              let invs = WitnessUtil.InvariantExp.process_exp inv in
+              List.fold_left (fun acc inv ->
                   let uuid = Uuidm.v4_gen uuid_random_state () in
                   let entry = `O [
                       ("entry_type", `String "loop_invariant");
@@ -106,7 +105,7 @@ struct
                     ]
                   in
                   entry :: acc
-                ) invs acc
+                ) acc invs
             | None ->
               acc
           end

From e9fc8bde4377d2aff57af6dc5feee9d4ba58d1b3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 16:38:56 +0300
Subject: [PATCH 19/19] Fix YamlWitness indentation

---
 src/witness/yamlWitness.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 4ef8828909..aae89cff9e 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -46,19 +46,19 @@ struct
     let yaml_task = `O ([
         ("input_files", `A (List.map Yaml.Util.string files));
         ("input_file_hashes", `O (List.map (fun file ->
-            (file, `String (sha256_file file))
-          ) files));
+             (file, `String (sha256_file file))
+           ) files));
         ("data_model", `String (match GobConfig.get_string "exp.architecture" with
-          | "64bit" -> "LP64"
-          | "32bit" -> "ILP32"
-          | _ -> failwith "invalid architecture"));
+             | "64bit" -> "LP64"
+             | "32bit" -> "ILP32"
+             | _ -> failwith "invalid architecture"));
         ("language", `String "C");
       ] @ match !Svcomp.task with
-            | Some (module Task) -> [
-                ("specification", `String (Svcomp.Specification.to_string Task.specification))
-              ]
-            | None ->
-              []
+      | Some (module Task) -> [
+          ("specification", `String (Svcomp.Specification.to_string Task.specification))
+        ]
+      | None ->
+        []
       )
     in
 
@@ -68,12 +68,12 @@ struct
         match n with
         | Statement _ when WitnessInvariant.is_invariant_node n ->
           let context: Invariant.context = {
-              scope=Node.find_fundec n;
-              i = -1;
-              lval=None;
-              offset=Cil.NoOffset;
-              deref_invariant=(fun _ _ _ -> Invariant.none) (* TODO: should throw instead? *)
-            }
+            scope=Node.find_fundec n;
+            i = -1;
+            lval=None;
+            offset=Cil.NoOffset;
+            deref_invariant=(fun _ _ _ -> Invariant.none) (* TODO: should throw instead? *)
+          }
           in
           begin match Spec.D.invariant context local with
             | Some inv ->