Add YAML witness output

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 (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/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

@@ -1286,6 +1286,7 @@
           "title": "exp.architecture",
           "description": "Architecture for analysis, currently for witness",
           "type": "string",
+          "enum": ["64bit", "32bit"],
           "default": "64bit"
         },
         "gcc_path": {
@@ -1788,6 +1789,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

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;

src/witness/yamlWitness.ml

@@ -0,0 +1,114 @@
+open Analyses
+
+let uuid_random_state = Random.State.make_self_init ()
+
+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
+
+  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 =
+    (* 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 *)
+        ("command_line", `String Goblintutil.command_line);
+        (* TODO: description *)
+      ]
+    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 file ->
+            (file, `String (sha256_file file))
+          ) files));
+        ("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
+
+    let yaml_entries = NH.fold (fun n local acc ->
+        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
+          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
+
+    let yaml = `A yaml_entries in
+    Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.path")) yaml
+end