From 476795e22774535cfb38820011cd261b1df58218 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 14:07:27 +0200 Subject: [PATCH 01/10] Add YAML invariant_set entry type (issue #1238) --- src/witness/yamlWitnessType.ml | 100 +++++++++++++++++++++++++++++++++ 1 file changed, 100 insertions(+) diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 3390c1e3ab..c68b1a45c9 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -242,6 +242,100 @@ struct {location; loop_invariant; precondition} end +module InvariantSet = +struct + module LoopInvariant = + struct + type t = { + location: Location.t; + value: string; + format: string; + } + + let invariant_type = "loop_invariant" + + let to_yaml' {location; value; format} = + [ + ("location", Location.to_yaml location); + ("value", `String value); + ("format", `String format); + ] + + 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} + end + + module LocationInvariant = + struct + include LoopInvariant + + let invariant_type = "location_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 + + let invariant_type = function + | LocationInvariant _ -> LocationInvariant.invariant_type + | LoopInvariant _ -> LoopInvariant.invariant_type + + let to_yaml' = function + | LocationInvariant x -> LocationInvariant.to_yaml' x + | LoopInvariant x -> LoopInvariant.to_yaml' x + + let of_yaml y = + let open GobYaml in + let* invariant_type = y |> find "type" >>= to_string in + if invariant_type = LocationInvariant.invariant_type then + let+ x = y |> LocationInvariant.of_yaml in + LocationInvariant x + else if invariant_type = LoopInvariant.invariant_type then + let+ x = y |> LoopInvariant.of_yaml in + LoopInvariant x + else + Error (`Msg "type") + end + + module Invariant = + struct + type t = { + invariant_type: InvariantType.t; + } + + let to_yaml {invariant_type} = + `O ([ + ("type", `String (InvariantType.invariant_type invariant_type)); + ] @ InvariantType.to_yaml' invariant_type) + + let of_yaml y = + let open GobYaml in + let+ invariant_type = y |> InvariantType.of_yaml in + {invariant_type} + end + + type t = { + content: Invariant.t list; + } + + let entry_type = "invariant_set" + + let to_yaml' {content} = + [("content", `A (List.map Invariant.to_yaml content))] + + let of_yaml y = + let open GobYaml in + let+ content = y |> list >>= list_map Invariant.of_yaml in + {content} +end + module Target = struct type t = { @@ -326,6 +420,7 @@ struct | PreconditionLoopInvariant of PreconditionLoopInvariant.t | LoopInvariantCertificate of LoopInvariantCertificate.t | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t + | InvariantSet of InvariantSet.t let entry_type = function | LocationInvariant _ -> LocationInvariant.entry_type @@ -334,6 +429,7 @@ struct | PreconditionLoopInvariant _ -> PreconditionLoopInvariant.entry_type | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type + | InvariantSet _ -> InvariantSet.entry_type let to_yaml' = function | LocationInvariant x -> LocationInvariant.to_yaml' x @@ -342,6 +438,7 @@ struct | PreconditionLoopInvariant x -> PreconditionLoopInvariant.to_yaml' x | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x + | InvariantSet x -> InvariantSet.to_yaml' x let of_yaml y = let open GobYaml in @@ -364,6 +461,9 @@ struct else if entry_type = PreconditionLoopInvariantCertificate.entry_type then let+ x = y |> PreconditionLoopInvariantCertificate.of_yaml in PreconditionLoopInvariantCertificate x + else if entry_type = InvariantSet.entry_type then + let+ x = y |> InvariantSet.of_yaml in + InvariantSet x else Error (`Msg "entry_type") end From f25051c5e6b55220e572d9a536f8b2e1ccba450a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 14:31:04 +0200 Subject: [PATCH 02/10] Add options for YAML invariant_set --- src/common/util/options.schema.json | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 40669ff729..a51c5c59cf 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2430,7 +2430,8 @@ "flow_insensitive_invariant", "precondition_loop_invariant", "loop_invariant_certificate", - "precondition_loop_invariant_certificate" + "precondition_loop_invariant_certificate", + "invariant_set" ] }, "default": [ @@ -2438,7 +2439,24 @@ "loop_invariant", "flow_insensitive_invariant", "loop_invariant_certificate", - "precondition_loop_invariant_certificate" + "precondition_loop_invariant_certificate", + "invariant_set" + ] + }, + "invariant-types": { + "title": "witness.yaml.invariant-types", + "description": "YAML witness invariant types to output/input.", + "type": "array", + "items": { + "type": "string", + "enum": [ + "location_invariant", + "loop_invariant" + ] + }, + "default": [ + "location_invariant", + "loop_invariant" ] }, "path": { From 4a329b0373462cc3bc266d21d4f693ccc424abfb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 14:31:33 +0200 Subject: [PATCH 03/10] Add YAML invariant_set generation --- src/witness/yamlWitness.ml | 93 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 9e8ebeff51..c83d5b48be 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -91,6 +91,29 @@ struct metadata = metadata ~task (); } + let location_invariant' ~location ~(invariant): InvariantSet.Invariant.t = { + invariant_type = LocationInvariant { + location; + value = invariant; + format = "c_expression"; + }; + } + + let loop_invariant' ~location ~(invariant): InvariantSet.Invariant.t = { + invariant_type = LoopInvariant { + location; + value = invariant; + format = "c_expression"; + }; + } + + let invariant_set ~task ~(invariants): Entry.t = { + entry_type = InvariantSet { + content = invariants; + }; + metadata = metadata ~task (); + } + let target ~uuid ~type_ ~(file_name): Target.t = { uuid; type_; @@ -134,6 +157,9 @@ let yaml_entries_to_file yaml_entries file = let entry_type_enabled entry_type = List.mem entry_type (GobConfig.get_string_list "witness.yaml.entry-types") +let invariant_type_enabled invariant_type = + List.mem invariant_type (GobConfig.get_string_list "witness.yaml.invariant-types") + module Make (R: ResultQuery.SpecSysSol2) = struct open R @@ -385,6 +411,73 @@ struct entries in + (* Generate invariant set *) + let entries = + if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then ( + let invariants = [] in + + (* Generate location invariants *) + let invariants = + if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( + NH.fold (fun n local acc -> + let loc = Node.location n in + if is_invariant_node n then ( + let lvals = local_lvals n local in + match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Node.find_fundec n).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = CilType.Exp.show inv in + let invariant = Entry.location_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else + acc + ) (Lazy.force nh) invariants + ) + else + invariants + in + + (* Generate loop invariants *) + let invariants = + if entry_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( + NH.fold (fun n local acc -> + let loc = Node.location n in + if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( + match R.ask_local_node n ~local (Invariant Invariant.default_context) with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Node.find_fundec n).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = CilType.Exp.show inv in + let invariant = Entry.loop_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else + acc + ) (Lazy.force nh) invariants + ) + else + invariants + in + + let entry = Entry.invariant_set ~task ~invariants in + entry :: entries + ) + else + entries + in + let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *) M.msg_group Info ~category:Witness "witness generation summary" [ From fcd18652628e74bcaec601614f0852d13be4ea13 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 14:58:07 +0200 Subject: [PATCH 04/10] Add YAML invariant_set validation --- src/witness/yamlWitness.ml | 46 +++++++++++++++++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index c83d5b48be..c66938961b 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -732,6 +732,48 @@ struct None in + let validate_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) = + + let validate_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = + let loc = loc_of_location location_invariant.location in + let inv = location_invariant.value in + + match Locator.find_opt locator loc with + | Some lvars -> + ignore (validate_lvars_invariant ~entry_certificate:None ~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.InvariantSet.LoopInvariant.t) = + let loc = loc_of_location loop_invariant.location in + let inv = loop_invariant.value in + + match Locator.find_opt loop_locator loc with + | Some lvars -> + ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv) + | None -> + incr cnt_error; + M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv; + in + + 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 -> + validate_location_invariant x + | true, LoopInvariant x -> + validate_loop_invariant x + | false, (LocationInvariant _ | LoopInvariant _) -> + incr cnt_disabled; + M.info_noloc ~category:Witness "disabled invariant of type %s" target_type; + in + + List.iter validate_invariant invariant_set.content; + None + in + match entry_type_enabled target_type, entry.entry_type with | true, LocationInvariant x -> validate_location_invariant x @@ -739,7 +781,9 @@ struct validate_loop_invariant x | true, PreconditionLoopInvariant x -> validate_precondition_loop_invariant x - | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _) -> + | true, InvariantSet x -> + validate_invariant_set x + | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) -> incr cnt_disabled; M.info_noloc ~category:Witness "disabled entry of type %s" target_type; None From e13bb5c3131f066fc1b793269a15c04c56cc9dbd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 15:02:39 +0200 Subject: [PATCH 05/10] Add YAML invariant_set unassume --- src/analyses/unassumeAnalysis.ml | 44 +++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 43707acd1e..5895f242c9 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -200,6 +200,46 @@ struct 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 (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = + let loc = loc_of_location location_invariant.location in + let inv = location_invariant.value in + let msgLoc: M.Location.t = CilLocation loc in + + match Locator.find_opt 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.InvariantSet.LoopInvariant.t) = + let loc = loc_of_location loop_invariant.location in + let inv = loop_invariant.value 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 validate_invariant (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 -> + unassume_location_invariant x + | true, LoopInvariant x -> + unassume_loop_invariant x + | false, (LocationInvariant _ | LoopInvariant _) -> + M.info_noloc ~category:Witness "disabled invariant of type %s" target_type + in + + List.iter validate_invariant invariant_set.content + in + match YamlWitness.entry_type_enabled target_type, entry.entry_type with | true, LocationInvariant x -> unassume_location_invariant x @@ -207,7 +247,9 @@ struct unassume_loop_invariant x | true, PreconditionLoopInvariant x -> unassume_precondition_loop_invariant x - | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _) -> + | true, InvariantSet x -> + unassume_invariant_set x + | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) -> M.info_noloc ~category:Witness "disabled entry of type %s" target_type | _ -> M.info_noloc ~category:Witness "cannot unassume entry of type %s" target_type From 90e962f53ebf4eb92ef88c5fcf8c6401f118299c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 15:15:10 +0200 Subject: [PATCH 06/10] Reverse YAML invariant_set content --- src/witness/yamlWitness.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index c66938961b..a580b319db 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -471,6 +471,7 @@ struct invariants in + let invariants = List.rev invariants in let entry = Entry.invariant_set ~task ~invariants in entry :: entries ) From ca84014548d7d585162b0afc9842dc78c2f72cef Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 7 Nov 2023 15:15:22 +0200 Subject: [PATCH 07/10] Fix YAML invariant_set parsing --- src/witness/yamlWitnessType.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index c68b1a45c9..f9bcf3235f 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -332,7 +332,7 @@ struct let of_yaml y = let open GobYaml in - let+ content = y |> list >>= list_map Invariant.of_yaml in + let+ content = y |> find "content" >>= list >>= list_map Invariant.of_yaml in {content} end From f7c022fcfbf53f9b0673dcd78a69f9beb176643a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Nov 2023 12:38:50 +0200 Subject: [PATCH 08/10] Account for invariant_set size when esitmating YAML witness buffer --- src/witness/yamlWitness.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index a580b319db..2c0340a997 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -143,12 +143,12 @@ struct } end -let yaml_entries_to_file yaml_entries file = +let yaml_entries_to_file ?(invariants=0) yaml_entries file = let yaml = `A yaml_entries in (* Yaml_unix.to_file_exn file yaml *) (* to_file/to_string uses a fixed-size buffer... *) (* estimate how big it should be + extra in case empty *) - let text = match Yaml.to_string ~len:(List.length yaml_entries * 4096 + 2048) yaml with + let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 4096 + 2048) yaml with | Ok text -> text | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m) in @@ -412,7 +412,7 @@ struct in (* Generate invariant set *) - let entries = + let (entries, invariants) = if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then ( let invariants = [] in @@ -473,10 +473,10 @@ struct let invariants = List.rev invariants in let entry = Entry.invariant_set ~task ~invariants in - entry :: entries + (entry :: entries, List.length invariants) ) else - entries + (entries, 0) in let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *) @@ -485,7 +485,7 @@ struct (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None); ]; - yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) + yaml_entries_to_file ~invariants yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) let write () = Timing.wrap "yaml witness" write () From d884744ccb793eb4e0c21fdb507e876932efcc9f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Nov 2023 12:43:33 +0200 Subject: [PATCH 09/10] Add option witness.yaml.format-version --- src/common/util/options.schema.json | 10 ++++++++++ src/witness/yamlWitness.ml | 2 +- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index a51c5c59cf..5993c5b1e4 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2418,6 +2418,16 @@ "type": "boolean", "default": false }, + "format-version": { + "title": "witness.yaml.format-version", + "description": "YAML witness format version", + "type": "string", + "enum": [ + "0.1", + "2.0" + ], + "default": "0.1" + }, "entry-types": { "title": "witness.yaml.entry-types", "description": "YAML witness entry types to output/input.", diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 2c0340a997..019ee67813 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -25,7 +25,7 @@ struct let uuid = Uuidm.v4_gen uuid_random_state () in let creation_time = TimeUtil.iso8601_now () in { - format_version = "0.1"; + format_version = GobConfig.get_string "witness.yaml.format-version"; uuid = Uuidm.to_string uuid; creation_time; producer; From a933266b4a6fbf8a47937d657401dc6e14b378f6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Nov 2023 13:08:52 +0200 Subject: [PATCH 10/10] Fix invariant_set loop_invariant option check --- src/witness/yamlWitness.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 019ee67813..f8532a1551 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -446,7 +446,7 @@ struct (* Generate loop invariants *) let invariants = - if entry_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( + if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( NH.fold (fun n local acc -> let loc = Node.location n in if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then (