Merge pull request #1853 from goblint/yaml-witness-invariant-set-flow-insensitive

Move custom YAML witness `flow_insensitive_invariant` entries under `invariant_set`

Author: sim642

conf/svcomp-ghost.json

@@ -117,8 +117,10 @@
       "sv-comp-true-only": false,
       "format-version": "2.1",
       "entry-types": [
-        "flow_insensitive_invariant",
         "ghost_instrumentation"
+      ],
+      "invariant-types": [
+        "flow_insensitive_invariant"
       ]
     },
     "invariant": {

src/analyses/unassumeAnalysis.ml

@@ -222,6 +222,8 @@ struct
             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

src/config/options.schema.json

@@ -2763,8 +2763,8 @@
               "title": "witness.invariant.flow_insensitive-as",
               "description": "Emit flow-insensitive invariants as location invariants at certain locations.",
               "type": "string",
-              "enum": ["flow_insensitive_invariant", "location_invariant", "invariant_set-location_invariant"],
-              "default": "flow_insensitive_invariant"
+              "enum": ["invariant_set-flow_insensitive_invariant", "invariant_set-location_invariant"],
+              "default": "invariant_set-flow_insensitive_invariant"
             }
           },
           "additionalProperties": false
@@ -2805,7 +2805,6 @@
                 "enum": [
                   "location_invariant",
                   "loop_invariant",
-                  "flow_insensitive_invariant",
                   "precondition_loop_invariant",
                   "invariant_set",
                   "violation_sequence",
@@ -2824,7 +2823,8 @@
                 "type": "string",
                 "enum": [
                   "location_invariant",
-                  "loop_invariant"
+                  "loop_invariant",
+                  "flow_insensitive_invariant"
                 ]
               },
               "default": [

src/witness/yamlWitness.ml

@@ -80,14 +80,6 @@ struct
     metadata = metadata ~task ();
   }
 
-  (* non-standard extension *)
-  let flow_insensitive_invariant ~task ~(invariant): Entry.t = {
-    entry_type = FlowInsensitiveInvariant {
-        flow_insensitive_invariant = invariant;
-      };
-    metadata = metadata ~task ();
-  }
-
   (* non-standard extension *)
   let precondition_loop_invariant ~task ~location ~precondition ~(invariant): Entry.t = {
     entry_type = PreconditionLoopInvariant {
@@ -114,6 +106,14 @@ struct
       };
   }
 
+  (* non-standard extension *)
+  let flow_insensitive_invariant' ~(invariant): InvariantSet.Invariant.t = {
+    invariant_type = FlowInsensitiveInvariant {
+        value = invariant;
+        format = "c_expression";
+      };
+  }
+
   let invariant_set ~task ~(invariants): Entry.t = {
     entry_type = InvariantSet {
         content = invariants;
@@ -338,40 +338,6 @@ struct
         ) (Lazy.force invariant_global_nodes) acc
     in
 
-    (* Generate flow-insensitive invariants *)
-    let entries =
-      if entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type then (
-        GHT.fold (fun g v acc ->
-            match g with
-            | `Left g -> (* global unknown from analysis Spec *)
-              begin match R.ask_global (InvariantGlobal (Obj.repr g)), GobConfig.get_string "witness.invariant.flow_insensitive-as" with
-                | `Lifted inv, "flow_insensitive_invariant" ->
-                  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.flow_insensitive_invariant ~task ~invariant in
-                      incr cnt_flow_insensitive_invariant;
-                      entry :: acc
-                    ) acc invs
-                | `Lifted inv, "location_invariant" ->
-                  fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
-                      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
-                | `Lifted _, _
-                | `Bot, _ | `Top, _ -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *)
-                  acc
-              end
-            | `Right _ -> (* global unknown for FromSpec contexts *)
-              acc
-          ) gh entries
-      )
-      else
-        entries
-    in
-
     (* Generate flow-insensitive entries (ghost instrumentation) *)
     let entries =
       if entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type then (
@@ -502,12 +468,12 @@ struct
 
     (* Generate invariant set *)
     let entries =
-      if entry_type_enabled YamlWitnessType.InvariantSet.entry_type || entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type && GobConfig.get_string "witness.invariant.flow_insensitive-as" = "invariant_set-location_invariant" then (
+      if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then (
         let invariants = [] in
 
         (* Generate location invariants *)
         let invariants =
-          if entry_type_enabled YamlWitnessType.InvariantSet.entry_type && invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then (
+          if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_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
@@ -537,7 +503,7 @@ struct
 
         (* Generate loop invariants *)
         let invariants =
-          if entry_type_enabled YamlWitnessType.InvariantSet.entry_type && invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
+          if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
             LH.fold (fun loc ns acc ->
                 if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? *)
                   let inv = List.fold_left (fun acc n ->
@@ -568,21 +534,31 @@ struct
             invariants
         in
 
-        (* Generate flow-insensitive invariants as location invariants *)
+        (* Generate flow-insensitive invariants *)
         let invariants =
-          if entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type && GobConfig.get_string "witness.invariant.flow_insensitive-as" = "invariant_set-location_invariant" then (
+          if invariant_type_enabled YamlWitnessType.InvariantSet.FlowInsensitiveInvariant.invariant_type then (
             GHT.fold (fun g v acc ->
                 match g with
                 | `Left g -> (* global unknown from analysis Spec *)
-                  begin match R.ask_global (InvariantGlobal (Obj.repr g)) with
-                    | `Lifted inv ->
+                  begin match R.ask_global (InvariantGlobal (Obj.repr g)), GobConfig.get_string "witness.invariant.flow_insensitive-as" with
+                    | `Lifted inv, "invariant_set-flow_insensitive_invariant" ->
+                      let invs = WitnessUtil.InvariantExp.process_exp inv in
+                      List.fold_left (fun acc inv ->
+                          let invariant = CilType.Exp.show inv in
+                          let invariant = Entry.flow_insensitive_invariant' ~invariant in
+                          incr cnt_flow_insensitive_invariant;
+                          invariant :: acc
+                        ) acc invs
+                    | `Lifted inv, "invariant_set-location_invariant" ->
+                      (* TODO: fold_flow_insensitive_as_location is now only used here, inline/move? *)
                       fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
                           let invariant = CilType.Exp.show inv in
                           let invariant = Entry.location_invariant' ~location ~invariant in
                           incr cnt_location_invariant;
                           invariant :: acc
                         ) acc
-                    | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *)
+                    | `Lifted _, _
+                    | `Bot, _ | `Top, _ -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *)
                       acc
                   end
                 | `Right _ -> (* global unknown for FromSpec contexts *)
@@ -866,7 +842,10 @@ struct
             validate_loop_invariant x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             incr cnt_disabled;
-            M.info_noloc ~category:Witness "disabled invariant of type %s" target_type;
+            M.info_noloc ~category:Witness "disabled invariant of type %s" target_type
+          | _ ->
+            incr cnt_unsupported;
+            M.warn_noloc ~category:Witness "cannot validate invariant of type %s" target_type
         in
 
         List.iter validate_invariant invariant_set.content

src/witness/yamlWitnessType.ml

@@ -221,26 +221,6 @@ struct
     {location; location_invariant}
 end
 
-module FlowInsensitiveInvariant =
-struct
-  type t = {
-    flow_insensitive_invariant: Invariant.t;
-  }
-  [@@deriving eq, ord, hash]
-
-  let entry_type = "flow_insensitive_invariant"
-
-  let to_yaml' {flow_insensitive_invariant} =
-    [
-      ("flow_insensitive_invariant", Invariant.to_yaml flow_insensitive_invariant);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ flow_insensitive_invariant = y |> find "flow_insensitive_invariant" >>= Invariant.of_yaml in
-    {flow_insensitive_invariant}
-end
-
 module PreconditionLoopInvariant =
 struct
   type t = {
@@ -302,21 +282,47 @@ struct
     let invariant_type = "location_invariant"
   end
 
+  module FlowInsensitiveInvariant =
+  struct
+    type t = {
+      value: string;
+      format: string;
+    }
+    [@@deriving eq, ord, hash]
+
+    let invariant_type = "flow_insensitive_invariant"
+
+    let to_yaml' {value; format} =
+      [
+        ("value", `String value);
+        ("format", `String format);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ value = y |> find "value" >>= to_string
+      and+ format = y |> find "format" >>= to_string in
+      {value; format}
+  end
+
   (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
   module InvariantType =
   struct
     type t =
       | LocationInvariant of LocationInvariant.t
       | LoopInvariant of LoopInvariant.t
+      | FlowInsensitiveInvariant of FlowInsensitiveInvariant.t
     [@@deriving eq, ord, hash]
 
     let invariant_type = function
       | LocationInvariant _ -> LocationInvariant.invariant_type
       | LoopInvariant _ -> LoopInvariant.invariant_type
+      | FlowInsensitiveInvariant _ -> FlowInsensitiveInvariant.invariant_type
 
     let to_yaml' = function
       | LocationInvariant x -> LocationInvariant.to_yaml' x
       | LoopInvariant x -> LoopInvariant.to_yaml' x
+      | FlowInsensitiveInvariant x -> FlowInsensitiveInvariant.to_yaml' x
 
     let of_yaml y =
       let open GobYaml in
@@ -327,6 +333,9 @@ struct
       else if invariant_type = LoopInvariant.invariant_type then
         let+ x = y |> LoopInvariant.of_yaml in
         LoopInvariant x
+      else if invariant_type = FlowInsensitiveInvariant.invariant_type then
+        let+ x = y |> FlowInsensitiveInvariant.of_yaml in
+        FlowInsensitiveInvariant x
       else
         Error (`Msg "type")
   end
@@ -712,7 +721,6 @@ struct
   type t =
     | LocationInvariant of LocationInvariant.t
     | LoopInvariant of LoopInvariant.t
-    | FlowInsensitiveInvariant of FlowInsensitiveInvariant.t
     | PreconditionLoopInvariant of PreconditionLoopInvariant.t
     | InvariantSet of InvariantSet.t
     | ViolationSequence of ViolationSequence.t
@@ -722,7 +730,6 @@ struct
   let entry_type = function
     | LocationInvariant _ -> LocationInvariant.entry_type
     | LoopInvariant _ -> LoopInvariant.entry_type
-    | FlowInsensitiveInvariant _ -> FlowInsensitiveInvariant.entry_type
     | PreconditionLoopInvariant _ -> PreconditionLoopInvariant.entry_type
     | InvariantSet _ -> InvariantSet.entry_type
     | ViolationSequence _ -> ViolationSequence.entry_type
@@ -731,7 +738,6 @@ struct
   let to_yaml' = function
     | LocationInvariant x -> LocationInvariant.to_yaml' x
     | LoopInvariant x -> LoopInvariant.to_yaml' x
-    | FlowInsensitiveInvariant x -> FlowInsensitiveInvariant.to_yaml' x
     | PreconditionLoopInvariant x -> PreconditionLoopInvariant.to_yaml' x
     | InvariantSet x -> InvariantSet.to_yaml' x
     | ViolationSequence x -> ViolationSequence.to_yaml' x
@@ -746,9 +752,6 @@ struct
     else if entry_type = LoopInvariant.entry_type then
       let+ x = y |> LoopInvariant.of_yaml in
       LoopInvariant x
-    else if entry_type = FlowInsensitiveInvariant.entry_type then
-      let+ x = y |> FlowInsensitiveInvariant.of_yaml in
-      FlowInsensitiveInvariant x
     else if entry_type = PreconditionLoopInvariant.entry_type then
       let+ x = y |> PreconditionLoopInvariant.of_yaml in
       PreconditionLoopInvariant x