Skip to content

Commit

Permalink
Merge pull request #1240 from goblint/yaml-witness-2.0
Browse files Browse the repository at this point in the history 
Add support for YAML witness entry type `invariant_set`
  • Loading branch information
@sim642
sim642 authored Nov 17, 2023
2 parents ca46852 + a933266 commit 97ab0b6
Show file tree
Hide file tree
Showing 4 changed files with 316 additions and 8 deletions.
44 changes: 43 additions & 1 deletion src/analyses/unassumeAnalysis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200,14 +200,56 @@ 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
| true, LoopInvariant x ->
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
Expand Down
32 changes: 30 additions & 2 deletions src/common/util/options.schema.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.",
Expand All @@ -2430,15 +2440,33 @@
"flow_insensitive_invariant",
"precondition_loop_invariant",
"loop_invariant_certificate",
"precondition_loop_invariant_certificate"
"precondition_loop_invariant_certificate",
"invariant_set"
]
},
"default": [
"location_invariant",
"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": {
Expand Down
148 changes: 143 additions & 5 deletions src/witness/yamlWitness.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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_;
Expand Down Expand Up @@ -120,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
Expand All @@ -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
Expand Down Expand Up @@ -385,13 +411,81 @@ struct
entries
in

(* Generate invariant set *)
let (entries, invariants) =
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 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 (
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 invariants = List.rev invariants in
let entry = Entry.invariant_set ~task ~invariants in
(entry :: entries, List.length invariants)
)
else
(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 *)

M.msg_group Info ~category:Witness "witness generation summary" [
(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 ()
Expand Down Expand Up @@ -639,14 +733,58 @@ 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
| true, LoopInvariant x ->
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
Expand Down
Loading

0 comments on commit 97ab0b6

Please sign in to comment.