Merge pull request #1848 from goblint/yaml-witness-2.1

sim642 · web-flow · commit a83cb1bb1e81 · 2025-10-30T16:59:25.000+02:00
Add YAML witness 2.1 parsing support
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
@@ -127,17 +127,26 @@ struct
         let validate_invariant i (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
           let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
           match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with
-          | true, LocationInvariant x ->
+          | true, LocationInvariant ({labels = (None | Some []); _} as x) ->
             unassume_location_invariant ~i x
-          | true, LoopInvariant x ->
+          | true, LoopInvariant ({labels = (None | Some []); _} as x) ->
             unassume_loop_invariant ~i x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             M.info_noloc ~category:Witness "disabled invariant of type %s" target_type
           | _ ->
             M.warn_noloc ~category:Witness "cannot unassume invariant of type %s" target_type
         in
 
-        List.iteri validate_invariant invariant_set.content
+        let validate_invariant_kind i (invariant_kind: YamlWitnessType.InvariantSet.InvariantKind.t) =
+          let target_type = YamlWitnessType.InvariantSet.InvariantKind.invariant_kind invariant_kind in
+          match invariant_kind with
+          | Invariant x ->
+            validate_invariant i x
+          | _ ->
+            M.warn_noloc ~category:Witness "cannot validate invariant of kind %s" target_type
+        in
+
+        List.iteri validate_invariant_kind invariant_set.content
       in
 
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -57,29 +57,34 @@ struct
       function_ = Some location_function;
     }
 
-  let location_invariant ~location ~(invariant): InvariantSet.Invariant.t = {
-    invariant_type = LocationInvariant {
-        location;
-        value = invariant;
-        format = "c_expression";
-      };
-  }
+  let location_invariant ~location ~(invariant): InvariantSet.InvariantKind.t =
+    Invariant {
+      invariant_type = LocationInvariant {
+          location;
+          value = invariant;
+          format = "c_expression";
+          labels = None;
+        };
+    }
 
-  let loop_invariant ~location ~(invariant): InvariantSet.Invariant.t = {
-    invariant_type = LoopInvariant {
-        location;
-        value = invariant;
-        format = "c_expression";
-      };
-  }
+  let loop_invariant ~location ~(invariant): InvariantSet.InvariantKind.t =
+    Invariant {
+      invariant_type = LoopInvariant {
+          location;
+          value = invariant;
+          format = "c_expression";
+          labels = None;
+        };
+    }
 
   (* non-standard extension *)
-  let flow_insensitive_invariant ~(invariant): InvariantSet.Invariant.t = {
-    invariant_type = FlowInsensitiveInvariant {
-        value = invariant;
-        format = "c_expression";
-      };
-  }
+  let flow_insensitive_invariant ~(invariant): InvariantSet.InvariantKind.t =
+    Invariant {
+      invariant_type = FlowInsensitiveInvariant {
+          value = invariant;
+          format = "c_expression";
+        };
+    }
 
   let invariant_set ~task ~(invariants): Entry.t = {
     entry_type = InvariantSet {
@@ -569,9 +574,9 @@ struct
         let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
           let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
           match invariant_type_enabled target_type, invariant.invariant_type with
-          | true, LocationInvariant x ->
+          | true, LocationInvariant ({labels = (None | Some []); _} as x) ->
             validate_location_invariant x
-          | true, LoopInvariant x ->
+          | true, LoopInvariant ({labels = (None | Some []); _} as x) ->
             validate_loop_invariant x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             incr cnt_disabled;
@@ -581,7 +586,17 @@ struct
             M.warn_noloc ~category:Witness "cannot validate invariant of type %s" target_type
         in
 
-        List.iter validate_invariant invariant_set.content
+        let validate_invariant_kind (invariant_kind: YamlWitnessType.InvariantSet.InvariantKind.t) =
+          let target_type = YamlWitnessType.InvariantSet.InvariantKind.invariant_kind invariant_kind in
+          match invariant_kind with
+          | Invariant x ->
+            validate_invariant x
+          | _ ->
+            incr cnt_unsupported;
+            M.warn_noloc ~category:Witness "cannot validate invariant of kind %s" target_type
+        in
+
+        List.iter validate_invariant_kind invariant_set.content
       in
 
       let validate_violation_sequence (violation_sequence: YamlWitnessType.ViolationSequence.t) =
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
@@ -159,24 +159,30 @@ struct
       location: Location.t;
       value: string;
       format: string;
+      labels: string list option;
     }
     [@@deriving eq, ord, hash]
 
     let invariant_type = "loop_invariant"
 
-    let to_yaml' {location; value; format} =
+    let to_yaml' {location; value; format; labels} =
       [
         ("location", Location.to_yaml location);
         ("value", `String value);
         ("format", `String format);
-      ]
+      ] @ match labels with
+      | Some labels -> [
+          ("labels", `A (List.map (fun label -> `String label) labels));
+        ]
+      | None -> []
 
     let of_yaml y =
       let open GobYaml in
       let+ location = y |> find "location" >>= Location.of_yaml
       and+ value = y |> find "value" >>= to_string
-      and+ format = y |> find "format" >>= to_string in
-      {location; value; format}
+      and+ format = y |> find "format" >>= to_string
+      and+ labels = y |> Yaml.Util.find "labels" >>= option_map (fun y -> y |> list >>= list_map to_string) in
+      {location; value; format; labels}
   end
 
   module LocationInvariant =
@@ -186,6 +192,20 @@ struct
     let invariant_type = "location_invariant"
   end
 
+  module LoopTransitionInvariant =
+  struct
+    include LoopInvariant
+
+    let invariant_type = "loop_transition_invariant"
+  end
+
+  module LocationTransitionInvariant =
+  struct
+    include LoopTransitionInvariant
+
+    let invariant_type = "location_transition_invariant"
+  end
+
   module FlowInsensitiveInvariant =
   struct
     type t = {
@@ -215,17 +235,23 @@ struct
     type t =
       | LocationInvariant of LocationInvariant.t
       | LoopInvariant of LoopInvariant.t
+      | LoopTransitionInvariant of LoopTransitionInvariant.t
+      | LocationTransitionInvariant of LocationTransitionInvariant.t
       | FlowInsensitiveInvariant of FlowInsensitiveInvariant.t
     [@@deriving eq, ord, hash]
 
     let invariant_type = function
       | LocationInvariant _ -> LocationInvariant.invariant_type
       | LoopInvariant _ -> LoopInvariant.invariant_type
+      | LoopTransitionInvariant _ -> LoopTransitionInvariant.invariant_type
+      | LocationTransitionInvariant _ -> LocationTransitionInvariant.invariant_type
       | FlowInsensitiveInvariant _ -> FlowInsensitiveInvariant.invariant_type
 
     let to_yaml' = function
       | LocationInvariant x -> LocationInvariant.to_yaml' x
       | LoopInvariant x -> LoopInvariant.to_yaml' x
+      | LoopTransitionInvariant x -> LoopTransitionInvariant.to_yaml' x
+      | LocationTransitionInvariant x -> LocationTransitionInvariant.to_yaml' x
       | FlowInsensitiveInvariant x -> FlowInsensitiveInvariant.to_yaml' x
 
     let of_yaml y =
@@ -237,6 +263,12 @@ struct
       else if invariant_type = LoopInvariant.invariant_type then
         let+ x = y |> LoopInvariant.of_yaml in
         LoopInvariant x
+      else if invariant_type = LoopTransitionInvariant.invariant_type then
+        let+ x = y |> LoopTransitionInvariant.of_yaml in
+        LoopTransitionInvariant x
+      else if invariant_type = LocationTransitionInvariant.invariant_type then
+        let+ x = y |> LocationTransitionInvariant.of_yaml in
+        LocationTransitionInvariant x
       else if invariant_type = FlowInsensitiveInvariant.invariant_type then
         let+ x = y |> FlowInsensitiveInvariant.of_yaml in
         FlowInsensitiveInvariant x
@@ -251,6 +283,8 @@ struct
     }
     [@@deriving eq, ord, hash]
 
+    let invariant_kind = "invariant"
+
     let to_yaml {invariant_type} =
       `O [
         ("invariant", `O ([
@@ -265,19 +299,132 @@ struct
       {invariant_type}
   end
 
+  module FunctionContract =
+  struct
+    type t = {
+      location: Location.t;
+      requires: string;
+      ensures: string;
+      format: string;
+      labels: string list option;
+    }
+    [@@deriving eq, ord, hash]
+
+    let contract_type = "function_contract"
+
+    let to_yaml' {location; requires; ensures; format; labels} =
+      [
+        ("location", Location.to_yaml location);
+        ("requires", `String requires);
+        ("ensures", `String ensures);
+        ("format", `String format);
+      ] @ match labels with
+      | Some labels -> [
+          ("labels", `A (List.map (fun label -> `String label) labels));
+        ]
+      | None -> []
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ location = y |> find "location" >>= Location.of_yaml
+      and+ requires = y |> find "requires" >>= to_string
+      and+ ensures = y |> find "ensures" >>= to_string
+      and+ format = y |> find "format" >>= to_string
+      and+ labels = y |> Yaml.Util.find "labels" >>= option_map (fun y -> y |> list >>= list_map to_string) in
+      {location; requires; ensures; format; labels}
+  end
+
+  (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
+  module ContractType =
+  struct
+    type t =
+      | FunctionContract of FunctionContract.t
+    [@@deriving eq, ord, hash]
+
+    let contract_type = function
+      | FunctionContract _ -> FunctionContract.contract_type
+
+    let to_yaml' = function
+      | FunctionContract x -> FunctionContract.to_yaml' x
+
+    let of_yaml y =
+      let open GobYaml in
+      let* contract_type = y |> find "type" >>= to_string in
+      if contract_type = FunctionContract.contract_type then
+        let+ x = y |> FunctionContract.of_yaml in
+        FunctionContract x
+      else
+        Error (`Msg "type")
+  end
+
+  module Contract =
+  struct
+    type t = {
+      contract_type: ContractType.t;
+    }
+    [@@deriving eq, ord, hash]
+
+    let invariant_kind = "contract"
+
+    let to_yaml {contract_type} =
+      `O [
+        ("contract", `O ([
+             ("type", `String (ContractType.contract_type contract_type));
+           ] @ ContractType.to_yaml' contract_type)
+        )
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ contract_type = y |> find "contract" >>= ContractType.of_yaml in
+      {contract_type}
+  end
+
+  module InvariantKind =
+  struct
+    type t =
+      | Invariant of Invariant.t
+      | Contract of Contract.t
+    [@@deriving eq, ord, hash]
+
+    let invariant_kind = function
+      | Invariant _ -> Invariant.invariant_kind
+      | Contract _ -> Contract.invariant_kind
+
+    let to_yaml = function
+      | Invariant x -> Invariant.to_yaml x
+      | Contract x -> Contract.to_yaml x
+
+    let of_yaml y =
+      let open GobYaml in
+      let* entries = y |> entries in
+      match entries with
+      | [(invariant_kind, _)] ->
+        if invariant_kind = Invariant.invariant_kind then
+          let+ x = y |> Invariant.of_yaml in
+          Invariant x
+        else if invariant_kind = Contract.invariant_kind then
+          let+ x = y |> Contract.of_yaml in
+          Contract x
+        else
+          Error (`Msg "kind")
+      | _ ->
+        Error (`Msg "kind")
+  end
+
   type t = {
-    content: Invariant.t list;
+    content: InvariantKind.t list;
   }
   [@@deriving eq, ord, hash]
 
   let entry_type = "invariant_set"
 
   let to_yaml' {content} =
-    [("content", `A (List.map Invariant.to_yaml content))]
+    [("content", `A (List.map InvariantKind.to_yaml content))]
 
   let of_yaml y =
     let open GobYaml in
-    let+ content = y |> find "content" >>= list >>= list_map Invariant.of_yaml in
+    let+ content = y |> find "content" >>= list >>= list_map InvariantKind.of_yaml in
     {content}
 end
 
diff --git a/tests/util/yamlWitnessStripCommon.ml b/tests/util/yamlWitnessStripCommon.ml
@@ -25,11 +25,30 @@ struct
           LocationInvariant {x with location = location_strip_file_hash x.location}
         | LoopInvariant x ->
           LoopInvariant {x with location = location_strip_file_hash x.location}
+        | LoopTransitionInvariant x ->
+          LoopTransitionInvariant {x with location = location_strip_file_hash x.location}
+        | LocationTransitionInvariant x ->
+          LocationTransitionInvariant {x with location = location_strip_file_hash x.location}
         | FlowInsensitiveInvariant x ->
           FlowInsensitiveInvariant x (* no location to strip *)
       in
       {invariant_type}
     in
+    let contract_strip_file_hash ({contract_type}: InvariantSet.Contract.t): InvariantSet.Contract.t =
+      let contract_type: InvariantSet.ContractType.t =
+        match contract_type with
+        | FunctionContract x ->
+          FunctionContract {x with location = location_strip_file_hash x.location}
+      in
+      {contract_type}
+    in
+    let invariant_kind_strip_file_hash (invariant_kind: InvariantSet.InvariantKind.t): InvariantSet.InvariantKind.t =
+      match invariant_kind with
+      | Invariant x ->
+        Invariant (invariant_strip_file_hash x)
+      | Contract x ->
+        Contract (contract_strip_file_hash x)
+    in
     let waypoint_strip_file_hash ({waypoint_type}: ViolationSequence.Waypoint.t): ViolationSequence.Waypoint.t =
       let waypoint_type: ViolationSequence.WaypointType.t =
         match waypoint_type with
@@ -58,7 +77,7 @@ struct
     let entry_type: EntryType.t =
       match entry_type with
       | InvariantSet x ->
-        InvariantSet {content = List.sort InvariantSet.Invariant.compare (List.map invariant_strip_file_hash x.content)} (* Sort, so order is deterministic regardless of Goblint. *)
+        InvariantSet {content = List.sort InvariantSet.InvariantKind.compare (List.map invariant_kind_strip_file_hash x.content)} (* Sort, so order is deterministic regardless of Goblint. *)
       | ViolationSequence x ->
         ViolationSequence {content = List.map segment_strip_file_hash x.content}
       | GhostInstrumentation x ->
diff --git a/tests/util/yamlWitnessStripDiff.ml b/tests/util/yamlWitnessStripDiff.ml
