Fix YAML witness tests by distinguishing missing labels from empty labels

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 ({labels = []; _} as x) ->
+          | true, LocationInvariant ({labels = (None | Some []); _} as x) ->
             unassume_location_invariant ~i x
-          | true, LoopInvariant ({labels = []; _} as 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

src/witness/yamlWitness.ml

@@ -104,7 +104,7 @@ struct
           location;
           value = invariant;
           format = "c_expression";
-          labels = [];
+          labels = None;
         };
     }
 
@@ -114,7 +114,7 @@ struct
           location;
           value = invariant;
           format = "c_expression";
-          labels = [];
+          labels = None;
         };
     }
 
@@ -864,9 +864,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 ({labels = []; _} as x) ->
+          | true, LocationInvariant ({labels = (None | Some []); _} as x) ->
             validate_location_invariant x
-          | true, LoopInvariant ({labels = []; _} as x) ->
+          | true, LoopInvariant ({labels = (None | Some []); _} as x) ->
             validate_loop_invariant x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             incr cnt_disabled;

src/witness/yamlWitnessType.ml

@@ -275,7 +275,7 @@ struct
       location: Location.t;
       value: string;
       format: string;
-      labels: string list;
+      labels: string list option;
     }
     [@@deriving eq, ord, hash]
 
@@ -286,15 +286,18 @@ struct
         ("location", Location.to_yaml location);
         ("value", `String value);
         ("format", `String format);
-        ("labels", `A (List.map (fun label -> `String label) labels));
-      ]
+      ] @ 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
-      and+ labels = y |> find "labels" >>= list >>= list_map to_string in
+      and+ labels = y |> Yaml.Util.find "labels" >>= option_map (fun y -> y |> list >>= list_map to_string) in
       {location; value; format; labels}
   end
 
@@ -390,7 +393,7 @@ struct
       requires: string;
       ensures: string;
       format: string;
-      labels: string list;
+      labels: string list option;
     }
     [@@deriving eq, ord, hash]
 
@@ -402,16 +405,19 @@ struct
         ("requires", `String requires);
         ("ensures", `String ensures);
         ("format", `String format);
-        ("labels", `A (List.map (fun label -> `String label) labels));
-      ]
+      ] @ 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 |> find "labels" >>= list >>= list_map to_string in
+      and+ labels = y |> Yaml.Util.find "labels" >>= option_map (fun y -> y |> list >>= list_map to_string) in
       {location; requires; ensures; format; labels}
   end