Merge pull request #1859 from goblint/yaml-witness-2.1-version

Automatically determine generated YAML witness version

Author: sim642

src/config/options.schema.json

@@ -2791,9 +2791,10 @@
               "type": "string",
               "enum": [
                 "2.0",
-                "2.1"
+                "2.1",
+                "2.1-goblint"
               ],
-              "default": "2.0"
+              "default": "2.1"
             },
             "entry-types": {
               "title": "witness.yaml.entry-types",

src/goblint_lib.ml

@@ -360,6 +360,7 @@ module WitnessUtil = WitnessUtil
 
 module YamlWitness = YamlWitness
 module YamlWitnessType = YamlWitnessType
+module YamlWitnessVersion = YamlWitnessVersion
 module WitnessGhost = WitnessGhost
 
 (** {2 SARIF} *)

src/witness/yamlWitness.ml

@@ -21,17 +21,25 @@ struct
     command_line = Some GobSys.command_line;
   }
 
-  let metadata ?task (): Metadata.t =
+  let metadata ~format_version ?task (): Metadata.t =
     let uuid = Uuidm.v4_gen uuid_random_state () in
+    let conf_format_version = YamlWitnessVersion.of_option () in
+    if YamlWitnessVersion.compare format_version conf_format_version > 0 then
+      M.warn_noloc ~category:Witness "witness entry version (%a) exceeds configured witness.yaml.format-version (%a)" YamlWitnessVersion.pretty format_version YamlWitnessVersion.pretty conf_format_version;
     let creation_time = TimeUtil.iso8601_now () in
     {
-      format_version = GobConfig.get_string "witness.yaml.format-version";
+      format_version = YamlWitnessVersion.show format_version;
       uuid = Uuidm.to_string uuid;
       creation_time;
       producer;
       task
     }
 
+  let with_metadata ~task entry_type: Entry.t = {
+    entry_type;
+    metadata = metadata ~format_version:(EntryType.min_version entry_type) ~task ();
+  }
+
   let task ~input_files ~data_model ~(specification): Task.t =
     {
       input_files;
@@ -44,14 +52,9 @@ struct
     }
 
   let location ~location:(loc: Cil.location) ~(location_function): Location.t =
-    let file_hash =
-      match GobConfig.get_string "witness.yaml.format-version" with
-      | "2.0" -> None (* TODO: 2.1? *)
-      | _ -> assert false
-    in
     {
       file_name = loc.file;
-      file_hash;
+      file_hash = None;
       line = loc.line;
       column = Some loc.column;
       function_ = Some location_function;
@@ -86,12 +89,10 @@ struct
         };
     }
 
-  let invariant_set ~task ~(invariants): Entry.t = {
-    entry_type = InvariantSet {
-        content = invariants;
-      };
-    metadata = metadata ~task ();
-  }
+  let invariant_set ~task ~(invariants): Entry.t =
+    with_metadata ~task @@ InvariantSet {
+      content = invariants;
+    }
 
   let ghost_variable' ~variable ~type_ ~(initial): GhostInstrumentation.Variable.t = {
     name = variable;
@@ -114,13 +115,11 @@ struct
     updates;
   }
 
-  let ghost_instrumentation ~task ~variables ~(location_updates): Entry.t = {
-    entry_type = GhostInstrumentation {
-        ghost_variables = variables;
-        ghost_updates = location_updates;
-      };
-    metadata = metadata ~task ();
-  }
+  let ghost_instrumentation ~task ~variables ~(location_updates): Entry.t =
+    with_metadata ~task @@ GhostInstrumentation {
+      ghost_variables = variables;
+      ghost_updates = location_updates;
+    }
 end
 
 let yaml_entries_to_file yaml_entries file =

src/witness/yamlWitnessType.ml

@@ -165,6 +165,10 @@ struct
 
     let invariant_type = "loop_invariant"
 
+    let min_version = function
+      | {labels = Some _; _} -> YamlWitnessVersion.V2_1
+      | _ -> YamlWitnessVersion.V2_0
+
     let to_yaml' {location; value; format; labels} =
       [
         ("location", Location.to_yaml location);
@@ -197,13 +201,15 @@ struct
     include LoopInvariant
 
     let invariant_type = "loop_transition_invariant"
+    let min_version _ = YamlWitnessVersion.V2_1
   end
 
   module LocationTransitionInvariant =
   struct
     include LoopTransitionInvariant
 
     let invariant_type = "location_transition_invariant"
+    let min_version _ = YamlWitnessVersion.V2_1
   end
 
   module FlowInsensitiveInvariant =
@@ -215,6 +221,7 @@ struct
     [@@deriving eq, ord, hash]
 
     let invariant_type = "flow_insensitive_invariant"
+    let min_version _ = YamlWitnessVersion.V2_1_Goblint
 
     let to_yaml' {value; format} =
       [
@@ -247,6 +254,13 @@ struct
       | LocationTransitionInvariant _ -> LocationTransitionInvariant.invariant_type
       | FlowInsensitiveInvariant _ -> FlowInsensitiveInvariant.invariant_type
 
+    let min_version = function
+      | LocationInvariant x -> LocationInvariant.min_version x
+      | LoopInvariant x -> LoopInvariant.min_version x
+      | LoopTransitionInvariant x -> LoopTransitionInvariant.min_version x
+      | LocationTransitionInvariant x -> LocationTransitionInvariant.min_version x
+      | FlowInsensitiveInvariant x -> FlowInsensitiveInvariant.min_version x
+
     let to_yaml' = function
       | LocationInvariant x -> LocationInvariant.to_yaml' x
       | LoopInvariant x -> LoopInvariant.to_yaml' x
@@ -285,6 +299,8 @@ struct
 
     let invariant_kind = "invariant"
 
+    let min_version {invariant_type} = InvariantType.min_version invariant_type
+
     let to_yaml {invariant_type} =
       `O [
         ("invariant", `O ([
@@ -311,6 +327,7 @@ struct
     [@@deriving eq, ord, hash]
 
     let contract_type = "function_contract"
+    let min_version _ = YamlWitnessVersion.V2_1
 
     let to_yaml' {location; requires; ensures; format; labels} =
       [
@@ -344,6 +361,9 @@ struct
     let contract_type = function
       | FunctionContract _ -> FunctionContract.contract_type
 
+    let min_version = function
+      | FunctionContract x -> FunctionContract.min_version x
+
     let to_yaml' = function
       | FunctionContract x -> FunctionContract.to_yaml' x
 
@@ -366,6 +386,8 @@ struct
 
     let invariant_kind = "contract"
 
+    let min_version {contract_type} = ContractType.min_version contract_type
+
     let to_yaml {contract_type} =
       `O [
         ("contract", `O ([
@@ -391,6 +413,10 @@ struct
       | Invariant _ -> Invariant.invariant_kind
       | Contract _ -> Contract.invariant_kind
 
+    let min_version = function
+      | Invariant x -> Invariant.min_version x
+      | Contract x -> Contract.min_version x
+
     let to_yaml = function
       | Invariant x -> Invariant.to_yaml x
       | Contract x -> Contract.to_yaml x
@@ -419,6 +445,11 @@ struct
 
   let entry_type = "invariant_set"
 
+  let min_version {content} =
+    List.to_seq content
+    |> Seq.map InvariantKind.min_version
+    |> Seq.fold_left YamlWitnessVersion.max YamlWitnessVersion.V2_0
+
   let to_yaml' {content} =
     [("content", `A (List.map InvariantKind.to_yaml content))]
 
@@ -636,6 +667,7 @@ struct
   [@@deriving eq, ord, hash]
 
   let entry_type = "violation_sequence"
+  let min_version _ = YamlWitnessVersion.V2_0
 
   let to_yaml' {content} =
     [("content", `A (List.map Segment.to_yaml content))]
@@ -749,6 +781,7 @@ struct
   [@@deriving eq, ord, hash]
 
   let entry_type = "ghost_instrumentation"
+  let min_version _ = YamlWitnessVersion.V2_1
 
   let to_yaml' {ghost_variables; ghost_updates} =
     [("content",
@@ -780,6 +813,11 @@ struct
     | ViolationSequence _ -> ViolationSequence.entry_type
     | GhostInstrumentation _ -> GhostInstrumentation.entry_type
 
+  let min_version = function
+    | InvariantSet x -> InvariantSet.min_version x
+    | ViolationSequence x -> ViolationSequence.min_version x
+    | GhostInstrumentation x -> GhostInstrumentation.min_version x
+
   let to_yaml' = function
     | InvariantSet x -> InvariantSet.to_yaml' x
     | ViolationSequence x -> ViolationSequence.to_yaml' x

src/witness/yamlWitnessVersion.ml

@@ -0,0 +1,34 @@
+(** YAML witness format version. *)
+
+type t =
+  | V2_0
+  | V2_1
+  | V2_1_Goblint
+[@@deriving ord, enum]
+
+let show = function
+  | V2_0 -> "2.0"
+  | V2_1 -> "2.1"
+  | V2_1_Goblint -> "2.1-goblint"
+
+include Printable.SimpleShow (
+  struct
+    type nonrec t = t
+    let show = show
+  end
+  )
+
+let of_string = function
+  | "2.0" -> V2_0
+  | "2.1" -> V2_1
+  | "2.1-goblint" -> V2_1_Goblint
+  | _ -> invalid_arg "YamlWitnessVersion.of_string"
+
+let of_option () =
+  of_string (GobConfig.get_string "witness.yaml.format-version")
+
+let min x y =
+  Option.get (of_enum (Int.min (to_enum x) (to_enum y)))
+
+let max x y =
+  Option.get (of_enum (Int.max (to_enum x) (to_enum y)))

tests/regression/13-privatized/01-priv_nr.t

@@ -20,6 +20,9 @@
     unsafe: 0
     total memory locations: 1
 
+  $ grep format_version witness.yml
+      format_version: "2.0"
+
   $ yamlWitnessStrip < witness.yml
   - entry_type: invariant_set
     content:

tests/regression/13-privatized/04-priv_multi.t

@@ -1,4 +1,4 @@
-  $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant 04-priv_multi.c
+  $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant --set witness.yaml.format-version 2.1-goblint 04-priv_multi.c
   [Success][Assert] Assertion "p == 5" will succeed (04-priv_multi.c:50:7-50:30)
   [Success][Assert] Assertion "A == B" will succeed (04-priv_multi.c:71:5-71:28)
   [Warning][Deadcode] Function 'dispose' has dead code:

tests/regression/13-privatized/25-struct_nr.t

@@ -1,4 +1,4 @@
-  $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant 25-struct_nr.c
+  $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant --set witness.yaml.format-version 2.1-goblint 25-struct_nr.c
   [Success][Assert] Assertion "glob1 == 5" will succeed (25-struct_nr.c:26:3-26:30)
   [Success][Assert] Assertion "t == 5" will succeed (25-struct_nr.c:16:3-16:26)
   [Success][Assert] Assertion "glob1 == -10" will succeed (25-struct_nr.c:18:3-18:32)

tests/regression/13-privatized/74-mutex.t

@@ -1,4 +1,4 @@
-  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant 74-mutex.c
+  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant --set witness.yaml.format-version 2.1-goblint 74-mutex.c
   [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)
   [Warning][Deadcode] Function 'producer' has dead code:
     on line 26 (74-mutex.c:26-26)
@@ -18,6 +18,10 @@
     unsafe: 0
     total memory locations: 1
 
+  $ grep format_version witness.yml
+      format_version: "2.1"
+      format_version: 2.1-goblint
+
   $ yamlWitnessStrip < witness.yml | tee witness.flow_insensitive.yml
   - entry_type: ghost_instrumentation
     content:
@@ -113,6 +117,11 @@ Flow-insensitive invariants as location invariants.
     unsafe: 0
     total memory locations: 1
 
+TODO: should invariant_set-s which use ghosts also be 2.1?
+  $ grep format_version witness.yml
+      format_version: "2.1"
+      format_version: "2.0"
+
   $ yamlWitnessStrip < witness.yml > witness.location.yml
 
   $ diff witness.flow_insensitive.yml witness.location.yml
@@ -261,7 +270,7 @@ Same with ghost_instrumentation and invariant_set entries.
 
 Same protected invariant with vojdani but no unprotected invariant.
 
-  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization vojdani --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant 74-mutex.c
+  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization vojdani --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant --set witness.yaml.format-version 2.1-goblint 74-mutex.c
   [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)
   [Warning][Deadcode] Function 'producer' has dead code:
     on line 26 (74-mutex.c:26-26)
@@ -352,7 +361,7 @@ Same protected invariant with vojdani but no unprotected invariant.
 
 Same as protection with mutex-meet.
 
-  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant 74-mutex.c
+  $ goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant --set witness.yaml.format-version 2.1-goblint 74-mutex.c
   [Success][Assert] Assertion "used == 0" will succeed (74-mutex.c:37:3-37:29)
   [Warning][Deadcode] Function 'producer' has dead code:
     on line 26 (74-mutex.c:26-26)

tests/regression/13-privatized/92-idx_priv.t

@@ -1,4 +1,4 @@
-  $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant 92-idx_priv.c
+  $ goblint --set ana.base.privatization protection --enable witness.yaml.enabled --set ana.activated[+] mutexGhosts --set witness.yaml.entry-types[+] ghost_instrumentation --set witness.yaml.invariant-types[*] flow_insensitive_invariant --set witness.yaml.format-version 2.1-goblint 92-idx_priv.c
   [Success][Assert] Assertion "data == 0" will succeed (92-idx_priv.c:22:3-22:29)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 14