Remove YAML witness 0.1 entry types

sim642 · sim642 · commit 86c6c608a065 · 2025-10-28T18:44:52.000+02:00
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
@@ -113,30 +113,6 @@ struct
           M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv
       in
 
-      let unassume_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) =
-        let loc = YamlWitness.loc_of_location location_invariant.location in
-        let inv = location_invariant.location_invariant.string in
-        let msgLoc: M.Location.t = CilLocation loc in
-
-        match Locator.find_opt location_locator loc with
-        | Some nodes ->
-          unassume_nodes_invariant ~loc ~nodes inv
-        | None ->
-          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
-      in
-
-      let unassume_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) =
-        let loc = YamlWitness.loc_of_location loop_invariant.location in
-        let inv = loop_invariant.loop_invariant.string in
-        let msgLoc: M.Location.t = CilLocation loc in
-
-        match Locator.find_opt loop_locator loc with
-        | Some nodes ->
-          unassume_nodes_invariant ~loc ~nodes inv
-        | None ->
-          M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
-      in
-
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
         let unassume_location_invariant ~i (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
@@ -180,13 +156,9 @@ struct
       in
 
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
-      | true, LocationInvariant x ->
-        unassume_location_invariant x
-      | true, LoopInvariant x ->
-        unassume_loop_invariant x
       | true, InvariantSet x ->
         unassume_invariant_set x
-      | false, (LocationInvariant _ | LoopInvariant _ | InvariantSet _) ->
+      | false, InvariantSet _ ->
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type
       | _ ->
         M.warn_noloc ~category:Witness "cannot unassume entry of type %s" target_type
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -2803,8 +2803,6 @@
               "items": {
                 "type": "string",
                 "enum": [
-                  "location_invariant",
-                  "loop_invariant",
                   "invariant_set",
                   "violation_sequence",
                   "ghost_instrumentation"
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
@@ -63,23 +63,9 @@ struct
     type_ = "assertion";
     format = "C";
   }
+  (* TODO: remove above? *)
 
-  let location_invariant ~task ~location ~(invariant): Entry.t = {
-    entry_type = LocationInvariant {
-        location;
-        location_invariant = invariant;
-      };
-    metadata = metadata ~task ();
-  }
-
-  let loop_invariant ~task ~location ~(invariant): Entry.t = {
-    entry_type = LoopInvariant {
-        location;
-        loop_invariant = invariant;
-      };
-    metadata = metadata ~task ();
-  }
-
+  (* TODO: remove primes from name *)
   let location_invariant' ~location ~(invariant): InvariantSet.Invariant.t = {
     invariant_type = LocationInvariant {
         location;
@@ -245,69 +231,6 @@ struct
     let cnt_flow_insensitive_invariant = ref 0 in
     (* TODO: precondition invariants? *)
 
-    (* Generate location invariants (without precondition) *)
-    let entries =
-      if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
-        LH.fold (fun loc ns acc ->
-            let inv = List.fold_left (fun acc n ->
-                let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
-                let lvals = local_lvals n local in
-                Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-              ) (Invariant.bot ()) ns
-            in
-            match inv with
-            | `Lifted inv ->
-              let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
-              let location_function = fundec.svar.vname in
-              let location = Entry.location ~location:loc ~location_function in
-              let invs = WitnessUtil.InvariantExp.process_exp inv in
-              List.fold_left (fun acc inv ->
-                  let invariant = Entry.invariant (CilType.Exp.show inv) in
-                  let entry = Entry.location_invariant ~task ~location ~invariant in
-                  incr cnt_location_invariant;
-                  entry :: acc
-                ) acc invs
-            | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
-              acc
-          ) (Lazy.force location_nodes) entries
-      )
-      else
-        entries
-    in
-
-    (* Generate loop invariants (without precondition) *)
-    let entries =
-      if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then (
-        LH.fold (fun loc ns acc ->
-            if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? needs both loop_invariant entry enabled and witness.invariant.loop-head option enabled *)
-              let inv = List.fold_left (fun acc n ->
-                  let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
-                  Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-                ) (Invariant.bot ()) ns
-              in
-              match inv with
-              | `Lifted inv ->
-                let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
-                let location_function = fundec.svar.vname in
-                let location = Entry.location ~location:loc ~location_function in
-                let invs = WitnessUtil.InvariantExp.process_exp inv in
-                List.fold_left (fun acc inv ->
-                    let invariant = Entry.invariant (CilType.Exp.show inv) in
-                    let entry = Entry.loop_invariant ~task ~location ~invariant in
-                    incr cnt_loop_invariant;
-                    entry :: acc
-                  ) acc invs
-              | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
-                acc
-            )
-            else
-              acc
-          ) (Lazy.force loop_nodes) entries
-      )
-      else
-        entries
-    in
-
     let invariant_global_nodes = lazy (R.ask_global InvariantGlobalNodes) in
 
     let fold_flow_insensitive_as_location ~inv f acc =
@@ -627,30 +550,6 @@ struct
           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
-
-        match Locator.find_opt location_locator loc with
-        | Some lvars ->
-          validate_lvars_invariant ~loc ~lvars inv
-        | None ->
-          incr cnt_error;
-          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
-
-        match Locator.find_opt loop_locator loc with
-        | Some lvars ->
-          validate_lvars_invariant ~loc ~lvars inv
-        | None ->
-          incr cnt_error;
-          M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv
-      in
-
       let validate_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
         let validate_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
@@ -705,15 +604,11 @@ struct
       in
 
       match entry_type_enabled target_type, entry.entry_type with
-      | true, LocationInvariant x ->
-        validate_location_invariant x
-      | true, LoopInvariant x ->
-        validate_loop_invariant x
       | true, InvariantSet x ->
         validate_invariant_set x
       | true, ViolationSequence x ->
         validate_violation_sequence x
-      | false, (LocationInvariant _ | LoopInvariant _ | InvariantSet _ | ViolationSequence _) ->
+      | false, (InvariantSet _ | ViolationSequence _) ->
         incr cnt_disabled;
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type
       | _ ->
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
@@ -174,52 +174,7 @@ struct
     and+ format = y |> find "format" >>= to_string in
     {string; type_; format}
 end
-
-module LoopInvariant =
-struct
-  type t = {
-    location: Location.t;
-    loop_invariant: Invariant.t;
-  }
-  [@@deriving eq, ord, hash]
-
-  let entry_type = "loop_invariant"
-
-  let to_yaml' {location; loop_invariant} =
-    [
-      ("location", Location.to_yaml location);
-      ("loop_invariant", Invariant.to_yaml loop_invariant);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ location = y |> find "location" >>= Location.of_yaml
-    and+ loop_invariant = y |> find "loop_invariant" >>= Invariant.of_yaml in
-    {location; loop_invariant}
-end
-
-module LocationInvariant =
-struct
-  type t = {
-    location: Location.t;
-    location_invariant: Invariant.t;
-  }
-  [@@deriving eq, ord, hash]
-
-  let entry_type = "location_invariant"
-
-  let to_yaml' {location; location_invariant} =
-    [
-      ("location", Location.to_yaml location);
-      ("location_invariant", Invariant.to_yaml location_invariant);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ location = y |> find "location" >>= Location.of_yaml
-    and+ location_invariant = y |> find "location_invariant" >>= Invariant.of_yaml in
-    {location; location_invariant}
-end
+(* TODO: remove above things? *)
 
 module InvariantSet =
 struct
@@ -693,37 +648,25 @@ end
 module EntryType =
 struct
   type t =
-    | LocationInvariant of LocationInvariant.t
-    | LoopInvariant of LoopInvariant.t
     | InvariantSet of InvariantSet.t
     | ViolationSequence of ViolationSequence.t
     | GhostInstrumentation of GhostInstrumentation.t
   [@@deriving eq, ord, hash]
 
   let entry_type = function
-    | LocationInvariant _ -> LocationInvariant.entry_type
-    | LoopInvariant _ -> LoopInvariant.entry_type
     | InvariantSet _ -> InvariantSet.entry_type
     | ViolationSequence _ -> ViolationSequence.entry_type
     | GhostInstrumentation _ -> GhostInstrumentation.entry_type
 
   let to_yaml' = function
-    | LocationInvariant x -> LocationInvariant.to_yaml' x
-    | LoopInvariant x -> LoopInvariant.to_yaml' x
     | InvariantSet x -> InvariantSet.to_yaml' x
     | ViolationSequence x -> ViolationSequence.to_yaml' x
     | GhostInstrumentation x -> GhostInstrumentation.to_yaml' x
 
   let of_yaml y =
     let open GobYaml in
     let* entry_type = y |> find "entry_type" >>= to_string in
-    if entry_type = LocationInvariant.entry_type then
-      let+ x = y |> LocationInvariant.of_yaml in
-      LocationInvariant x
-    else if entry_type = LoopInvariant.entry_type then
-      let+ x = y |> LoopInvariant.of_yaml in
-      LoopInvariant x
-    else if entry_type = InvariantSet.entry_type then
+    if entry_type = InvariantSet.entry_type then
       let+ x = y |> InvariantSet.of_yaml in
       InvariantSet x
     else if entry_type = ViolationSequence.entry_type then
diff --git a/tests/util/yamlWitnessStripCommon.ml b/tests/util/yamlWitnessStripCommon.ml
@@ -57,10 +57,6 @@ struct
     in
     let entry_type: EntryType.t =
       match entry_type with
-      | LocationInvariant x ->
-        LocationInvariant {x with location = location_strip_file_hash x.location}
-      | LoopInvariant x ->
-        LoopInvariant {x with location = location_strip_file_hash x.location}
       | 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. *)
       | ViolationSequence x ->
