Add YAML witness loop_transition_invariant and location_transition_invariant parsing support

Author: sim642

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/witness/yamlWitness.ml

@@ -866,7 +866,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

@@ -302,21 +302,41 @@ 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
+
   (* 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
+      | LoopTransitionInvariant of LoopTransitionInvariant.t
+      | LocationTransitionInvariant of LocationTransitionInvariant.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
 
     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
 
     let of_yaml y =
       let open GobYaml in
@@ -327,6 +347,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
         Error (`Msg "type")
   end

tests/util/yamlWitnessStripCommon.ml

@@ -25,6 +25,10 @@ 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}
       in
       {invariant_type}
     in