Merge pull request #1817 from goblint/yaml-witness-certificates

sim642 · web-flow · commit a8d88662b918 · 2025-09-29T10:03:42.000+03:00
Remove YAML witness 0.1 validation certificates
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -2813,8 +2813,6 @@
                   "loop_invariant",
                   "flow_insensitive_invariant",
                   "precondition_loop_invariant",
-                  "loop_invariant_certificate",
-                  "precondition_loop_invariant_certificate",
                   "invariant_set",
                   "violation_sequence",
                   "ghost_instrumentation"
@@ -2863,12 +2861,6 @@
               "description": "YAML witness input path",
               "type": "string",
               "default": ""
-            },
-            "certificate": {
-              "title": "witness.yaml.certificate",
-              "description": "YAML witness certificate output path",
-              "type": "string",
-              "default": ""
             }
           },
           "additionalProperties": false
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -121,34 +121,6 @@ struct
     metadata = metadata ~task ();
   }
 
-  let target ~uuid ~type_ ~(file_name): Target.t = {
-    uuid;
-    type_;
-    file_hash = sha256_file file_name;
-  }
-
-  let certification verdict: Certification.t = {
-    string = if verdict then "confirmed" else "rejected";
-    type_ = "verdict";
-    format = "confirmed | rejected";
-  }
-
-  let loop_invariant_certificate ~target ~(certification): Entry.t = {
-    entry_type = LoopInvariantCertificate {
-        target;
-        certification;
-      };
-    metadata = metadata ();
-  }
-
-  let precondition_loop_invariant_certificate ~target ~(certification): Entry.t = {
-    entry_type = PreconditionLoopInvariantCertificate {
-        target;
-        certification;
-      };
-    metadata = metadata ();
-  }
-
   let ghost_variable' ~variable ~type_ ~(initial): GhostInstrumentation.Variable.t = {
     name = variable;
     scope = "global";
@@ -743,11 +715,10 @@ struct
     cnt_error := 0;
     cnt_disabled := 0;
 
-    let validate_entry (entry: YamlWitnessType.Entry.t): YamlWitnessType.Entry.t option =
-      let uuid = entry.metadata.uuid in
+    let validate_entry (entry: YamlWitnessType.Entry.t): unit =
       let target_type = YamlWitnessType.EntryType.entry_type entry.entry_type in
 
-      let validate_lvars_invariant ~entry_certificate ~loc ~lvars inv =
+      let validate_lvars_invariant ~loc ~lvars inv =
         let msgLoc: M.Location.t = CilLocation loc in
         match InvariantParser.parse_cabs inv with
         | Ok inv_cabs ->
@@ -773,86 +744,52 @@ struct
           begin match Option.get (VR.result_of_enum result) with
             | Confirmed ->
               incr cnt_confirmed;
-              M.success ~category:Witness ~loc:msgLoc "invariant confirmed: %s" inv;
-              Option.map (fun entry_certificate ->
-                  let target = Entry.target ~uuid ~type_:target_type ~file_name:loc.file in
-                  let certification = Entry.certification true in
-                  let certificate_entry = entry_certificate ~target ~certification in
-                  certificate_entry
-                ) entry_certificate
+              M.success ~category:Witness ~loc:msgLoc "invariant confirmed: %s" inv
             | Unconfirmed ->
               incr cnt_unconfirmed;
-              M.warn ~category:Witness ~loc:msgLoc "invariant unconfirmed: %s" inv;None
+              M.warn ~category:Witness ~loc:msgLoc "invariant unconfirmed: %s" inv
             | Refuted ->
               incr cnt_refuted;
-              M.error ~category:Witness ~loc:msgLoc "invariant refuted: %s" inv;
-              Option.map (fun entry_certificate ->
-                  let target = Entry.target ~uuid ~type_:target_type ~file_name:loc.file in
-                  let certification = Entry.certification false in
-                  let certificate_entry = entry_certificate ~target ~certification in
-                  certificate_entry
-                ) entry_certificate
+              M.error ~category:Witness ~loc:msgLoc "invariant refuted: %s" inv
             | ParseError ->
               incr cnt_error;
               M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
-              M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv;
-              None
+              M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
           end
         | Error e ->
           incr cnt_error;
           M.error ~category:Witness ~loc:msgLoc "Frontc couldn't parse invariant: %s" inv;
-          M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv;
-          None
+          M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv
       in
 
       let validate_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) =
         let loc = loc_of_location location_invariant.location in
         let inv = location_invariant.location_invariant.string in
-        let entry_certificate = (* TODO: Wrong, because there's no location_invariant_certificate, but this is the closest thing for now. *)
-          if entry_type_enabled YamlWitnessType.LoopInvariantCertificate.entry_type then
-            Some Entry.loop_invariant_certificate
-          else
-            None
-        in
 
         match Locator.find_opt location_locator loc with
         | Some lvars ->
-          validate_lvars_invariant ~entry_certificate ~loc ~lvars inv
+          validate_lvars_invariant ~loc ~lvars inv
         | None ->
           incr cnt_error;
-          M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv;
-          None
+          M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv
       in
 
       let validate_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) =
         let loc = loc_of_location loop_invariant.location in
         let inv = loop_invariant.loop_invariant.string in
-        let entry_certificate =
-          if entry_type_enabled YamlWitnessType.LoopInvariantCertificate.entry_type then
-            Some Entry.loop_invariant_certificate
-          else
-            None
-        in
 
         match Locator.find_opt loop_locator loc with
         | Some lvars ->
-          validate_lvars_invariant ~entry_certificate ~loc ~lvars inv
+          validate_lvars_invariant ~loc ~lvars inv
         | None ->
           incr cnt_error;
-          M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv;
-          None
+          M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv
       in
 
       let validate_precondition_loop_invariant (precondition_loop_invariant: YamlWitnessType.PreconditionLoopInvariant.t) =
         let loc = loc_of_location precondition_loop_invariant.location in
         let pre = precondition_loop_invariant.precondition.string in
         let inv = precondition_loop_invariant.loop_invariant.string in
-        let entry_certificate =
-          if entry_type_enabled YamlWitnessType.PreconditionLoopInvariantCertificate.entry_type then
-            Some Entry.precondition_loop_invariant_certificate
-          else
-            None
-        in
         let msgLoc: M.Location.t = CilLocation loc in
 
         match Locator.find_opt loop_locator loc with
@@ -880,21 +817,18 @@ struct
               let lvars = LvarS.filter precondition_holds lvars in
               if LvarS.is_empty lvars then (
                 incr cnt_unchecked;
-                M.warn ~category:Witness ~loc:msgLoc "precondition never definitely holds: %s" pre;
-                None
+                M.warn ~category:Witness ~loc:msgLoc "precondition never definitely holds: %s" pre
               )
               else
-                validate_lvars_invariant ~entry_certificate ~loc ~lvars inv
+                validate_lvars_invariant ~loc ~lvars inv
             | Error e ->
               incr cnt_error;
               M.error ~category:Witness ~loc:msgLoc "Frontc couldn't parse precondition: %s" pre;
-              M.info ~category:Witness ~loc:msgLoc "precondition has invalid syntax: %s" pre;
-              None
+              M.info ~category:Witness ~loc:msgLoc "precondition has invalid syntax: %s" pre
           end
         | None ->
           incr cnt_error;
-          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv;
-          None
+          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
       in
 
       let validate_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
@@ -905,7 +839,7 @@ struct
 
           match Locator.find_opt location_locator loc with
           | Some lvars ->
-            ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv)
+            validate_lvars_invariant ~loc ~lvars inv
           | None ->
             incr cnt_error;
             M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv;
@@ -917,7 +851,7 @@ struct
 
           match Locator.find_opt loop_locator loc with
           | Some lvars ->
-            ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv)
+            validate_lvars_invariant ~loc ~lvars inv
           | None ->
             incr cnt_error;
             M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv;
@@ -935,8 +869,7 @@ struct
             M.info_noloc ~category:Witness "disabled invariant of type %s" target_type;
         in
 
-        List.iter validate_invariant invariant_set.content;
-        None
+        List.iter validate_invariant invariant_set.content
       in
 
       let validate_violation_sequence (violation_sequence: YamlWitnessType.ViolationSequence.t) =
@@ -945,7 +878,7 @@ struct
            If program is correct and we can prove it, we output true, which counts as refutation of violation witness.
            If program is correct and we cannot prove it, we output unknown.
            If program is incorrect, we output unknown. *)
-        None
+        ()
       in
 
       match entry_type_enabled target_type, entry.entry_type with
@@ -961,26 +894,20 @@ struct
         validate_violation_sequence x
       | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _) ->
         incr cnt_disabled;
-        M.info_noloc ~category:Witness "disabled entry of type %s" target_type;
-        None
+        M.info_noloc ~category:Witness "disabled entry of type %s" target_type
       | _ ->
         incr cnt_unsupported;
-        M.warn_noloc ~category:Witness "cannot validate entry of type %s" target_type;
-        None
+        M.warn_noloc ~category:Witness "cannot validate entry of type %s" target_type
     in
 
-    let yaml_entries' = List.fold_left (fun yaml_entries' yaml_entry ->
+    List.iter (fun yaml_entry ->
         match YamlWitnessType.Entry.of_yaml yaml_entry with
         | Ok entry ->
-          let certificate_entry = validate_entry entry in
-          let yaml_certificate_entry = Option.map YamlWitnessType.Entry.to_yaml certificate_entry in
-          Option.to_list yaml_certificate_entry @ yaml_entry :: yaml_entries'
+          validate_entry entry
         | Error (`Msg e) ->
           incr cnt_error;
-          M.error_noloc ~category:Witness "couldn't parse entry: %s" e;
-          yaml_entry :: yaml_entries'
-      ) [] yaml_entries
-    in
+          M.error_noloc ~category:Witness "couldn't parse entry: %s" e
+      ) yaml_entries;
 
     M.msg_group Info ~category:Witness "witness validation summary" [
       (Pretty.dprintf "confirmed: %d" !cnt_confirmed, None);
@@ -993,10 +920,6 @@ struct
       (Pretty.dprintf "total validation entries: %d" (!cnt_confirmed + !cnt_unconfirmed + !cnt_refuted + !cnt_unchecked + !cnt_unsupported + !cnt_error + !cnt_disabled), None);
     ];
 
-    let certificate_path = GobConfig.get_string "witness.yaml.certificate" in
-    if certificate_path <> "" then
-      yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path);
-
     match GobConfig.get_bool "witness.yaml.strict" with
     | true when !cnt_error > 0 ->
       Error "witness error"
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
@@ -368,83 +368,6 @@ struct
     {content}
 end
 
-module Target =
-struct
-  type t = {
-    uuid: string;
-    type_: string;
-    file_hash: string;
-  }
-  [@@deriving eq, ord, hash]
-
-  let to_yaml {uuid; type_; file_hash} =
-    `O [
-      ("uuid", `String uuid);
-      ("type", `String type_);
-      ("file_hash", `String file_hash);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ uuid = y |> find "uuid" >>= to_string
-    and+ type_ = y |> find "type" >>= to_string
-    and+ file_hash = y |> find "file_hash" >>= to_string in
-    {uuid; type_; file_hash}
-end
-
-module Certification =
-struct
-  type t = {
-    string: string;
-    type_: string;
-    format: string;
-  }
-  [@@deriving eq, ord, hash]
-
-  let to_yaml {string; type_; format} =
-    `O [
-      ("string", `String string);
-      ("type", `String type_);
-      ("format", `String format);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ string = y |> find "string" >>= to_string
-    and+ type_ = y |> find "type" >>= to_string
-    and+ format = y |> find "format" >>= to_string in
-    {string; type_; format}
-end
-
-module LoopInvariantCertificate =
-struct
-  type t = {
-    target: Target.t;
-    certification: Certification.t;
-  }
-  [@@deriving eq, ord, hash]
-
-  let entry_type = "loop_invariant_certificate"
-
-  let to_yaml' {target; certification} =
-    [
-      ("target", Target.to_yaml target);
-      ("certification", Certification.to_yaml certification);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ target = y |> find "target" >>= Target.of_yaml
-    and+ certification = y |> find "certification" >>= Certification.of_yaml in
-    {target; certification}
-end
-
-module PreconditionLoopInvariantCertificate =
-struct
-  include LoopInvariantCertificate
-  let entry_type = "precondition_loop_invariant_certificate"
-end
-
 module ViolationSequence =
 struct
 
@@ -791,8 +714,6 @@ struct
     | LoopInvariant of LoopInvariant.t
     | FlowInsensitiveInvariant of FlowInsensitiveInvariant.t
     | PreconditionLoopInvariant of PreconditionLoopInvariant.t
-    | LoopInvariantCertificate of LoopInvariantCertificate.t
-    | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
     | InvariantSet of InvariantSet.t
     | ViolationSequence of ViolationSequence.t
     | GhostInstrumentation of GhostInstrumentation.t
@@ -803,8 +724,6 @@ struct
     | LoopInvariant _ -> LoopInvariant.entry_type
     | FlowInsensitiveInvariant _ -> FlowInsensitiveInvariant.entry_type
     | PreconditionLoopInvariant _ -> PreconditionLoopInvariant.entry_type
-    | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type
-    | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type
     | InvariantSet _ -> InvariantSet.entry_type
     | ViolationSequence _ -> ViolationSequence.entry_type
     | GhostInstrumentation _ -> GhostInstrumentation.entry_type
@@ -814,8 +733,6 @@ struct
     | LoopInvariant x -> LoopInvariant.to_yaml' x
     | FlowInsensitiveInvariant x -> FlowInsensitiveInvariant.to_yaml' x
     | PreconditionLoopInvariant x -> PreconditionLoopInvariant.to_yaml' x
-    | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x
-    | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x
     | InvariantSet x -> InvariantSet.to_yaml' x
     | ViolationSequence x -> ViolationSequence.to_yaml' x
     | GhostInstrumentation x -> GhostInstrumentation.to_yaml' x
@@ -835,12 +752,6 @@ struct
     else if entry_type = PreconditionLoopInvariant.entry_type then
       let+ x = y |> PreconditionLoopInvariant.of_yaml in
       PreconditionLoopInvariant x
-    else if entry_type = LoopInvariantCertificate.entry_type then
-      let+ x = y |> LoopInvariantCertificate.of_yaml in
-      LoopInvariantCertificate x
-    else if entry_type = PreconditionLoopInvariantCertificate.entry_type then
-      let+ x = y |> PreconditionLoopInvariantCertificate.of_yaml in
-      PreconditionLoopInvariantCertificate x
     else if entry_type = InvariantSet.entry_type then
       let+ x = y |> InvariantSet.of_yaml in
       InvariantSet x
diff --git a/tests/util/yamlWitnessStripCommon.ml b/tests/util/yamlWitnessStripCommon.ml
