Add YAML witness invariant labels parsing support

Author: sim642

src/analyses/unassumeAnalysis.ml

@@ -216,9 +216,9 @@ 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 = []; _} as x) ->
             unassume_location_invariant ~i x
-          | true, LoopInvariant x ->
+          | true, LoopInvariant ({labels = []; _} as x) ->
             unassume_loop_invariant ~i x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             M.info_noloc ~category:Witness "disabled invariant of type %s" target_type

src/witness/yamlWitness.ml

@@ -103,6 +103,7 @@ struct
         location;
         value = invariant;
         format = "c_expression";
+        labels = [];
       };
   }
 
@@ -111,6 +112,7 @@ struct
         location;
         value = invariant;
         format = "c_expression";
+        labels = [];
       };
   }
 
@@ -860,9 +862,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 = []; _} as x) ->
             validate_location_invariant x
-          | true, LoopInvariant x ->
+          | true, LoopInvariant ({labels = []; _} as x) ->
             validate_loop_invariant x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             incr cnt_disabled;

src/witness/yamlWitnessType.ml

@@ -275,24 +275,27 @@ struct
       location: Location.t;
       value: string;
       format: string;
+      labels: string list;
     }
     [@@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);
+        ("labels", `A (List.map (fun label -> `String label) labels));
       ]
 
     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 |> find "labels" >>= list >>= list_map to_string in
+      {location; value; format; labels}
   end
 
   module LocationInvariant =