Merge pull request #744 from goblint/yaml-witness

Add YAML witness output

Author: sim642

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

@@ -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;*)

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; *)
@@ -678,6 +678,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 (

src/transform/evalAssert.ml

@@ -1,17 +1,16 @@
 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 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.after-lock), about all locals and globals
 
-    Limitations without trans.assert.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
@@ -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,30 +31,12 @@ 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 "trans.assert.full"
-    val only_at_locks = GobConfig.get_bool "trans.assert.only-at-locks"
+    val full = GobConfig.get_bool "witness.invariant.full"
+    (* 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 =
@@ -78,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
@@ -94,13 +72,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,10 +110,10 @@ 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 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; ()
         | _ -> ()
@@ -161,7 +139,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

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 *)

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
@@ -1286,6 +1265,7 @@
           "title": "exp.architecture",
           "description": "Architecture for analysis, currently for witness",
           "type": "string",
+          "enum": ["64bit", "32bit"],
           "default": "64bit"
         },
         "gcc_path": {
@@ -1753,13 +1733,39 @@
           "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
+            },
+            "after-lock": {
+              "title": "witness.invariant.after-lock",
+              "description":
+                "Emit invariants after mutex locking",
+              "type": "boolean",
+              "default": true
+            },
+            "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":
+                "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
+              "type": "boolean",
+              "default": true
             }
           },
           "additionalProperties": false
@@ -1788,6 +1794,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