From cd1af7ae737a97047a72e3d59bee569e006f0657 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 May 2022 12:57:52 +0300
Subject: [PATCH] Add yaml witness parsing prototype

---
 src/framework/control.ml     |  5 ++++
 src/util/options.schema.json |  6 +++++
 src/witness/yamlWitness.ml   | 50 ++++++++++++++++++++++++++++++++++++
 3 files changed, 61 insertions(+)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 7393cd1b4b..295a212e81 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -683,6 +683,11 @@ struct
       YWitness.write lh gh
     );
 
+    if get_string "witness.yaml.validate" <> "" then (
+      let module YWitness = YamlWitness.Validator (Spec) (EQSys) (LHT) (GHT) in
+      YWitness.validate lh gh
+    );
+
     let marshal = Spec.finalize () in
     (* copied from solve_and_postprocess *)
     let gobview = get_bool "gobview" in
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index e52a9b0bc5..c4c7ce8490 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1805,6 +1805,12 @@
               "description": "YAML witness output path",
               "type": "string",
               "default": "witness.yml"
+            },
+            "validate": {
+              "title": "witness.yaml.validate",
+              "description": "YAML witness input path",
+              "type": "string",
+              "default": ""
             }
           },
           "additionalProperties": false
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index ad73090e05..c4ea4b97a8 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -112,3 +112,53 @@ struct
     let yaml = `A yaml_entries in
     Yaml_unix.to_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.path")) yaml
 end
+
+
+module Validator
+    (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 validate lh gh =
+    let nh = join_contexts lh in
+
+    let yaml = Yaml_unix.of_file_exn (Fpath.v (GobConfig.get_string "witness.yaml.validate")) in
+    let yaml_entries = match yaml with
+      | `A yaml_entries -> yaml_entries
+      | _ -> failwith "invalid YAML"
+    in
+    List.iter (fun yaml_entry ->
+        let yaml_location = Yaml.Util.(yaml_entry |> find_exn "location" |> Option.get) in
+        let file = Yaml.Util.(yaml_location |> find_exn "file_name" |> Option.get |> to_string_exn) in
+        let line = Yaml.Util.(yaml_location |> find_exn "line" |> Option.get |> to_float_exn |> int_of_float) in
+        let column = Yaml.Util.(yaml_location |> find_exn "column" |> Option.get |> to_float_exn |> int_of_float) + 1 in
+        let inv = Yaml.Util.(yaml_entry |> find_exn "loop_invariant" |> Option.get |> find_exn "string" |> Option.get |> to_string_exn) in
+        let loc: Cil.location = {
+          file;
+          line;
+          column;
+          byte = -1;
+          endLine = -1;
+          endColumn = -1;
+          endByte = -1;
+        }
+        in
+        ignore (Pretty.printf "%a: %s\n" CilType.Location.pretty loc inv)
+      ) yaml_entries
+end