Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix YAML witness invariants for unrolled loops #1248

Merged
merged 6 commits into from
Nov 24, 2023
Merged

Fix YAML witness invariants for unrolled loops #1248

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
6f54991
Fix YAML witness invariants for unrolled loops (closes #1225)
sim642 Nov 17, 2023
eabb461
Merge branch 'yaml-witness-2.0' into yaml-witness-location-hack
sim642 Nov 17, 2023
952b90d
Fix bisect_ppx build
sim642 Nov 17, 2023
4ae3556
Fix missing unrolled iterations in YAML witness invariants
sim642 Nov 17, 2023
0fb479f
Refactor YAML witness fundec lookup
sim642 Nov 17, 2023
3c89ece
Fix YamlWitness indentation
sim642 Nov 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 43 additions & 1 deletion src/analyses/unassumeAnalysis.ml
View file
Open in desktop
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
Open in desktop
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
Loading