From 1fd955e101184eea25d5a1e1894eebeb161eb014 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 7 Jan 2022 09:53:42 +0100
Subject: [PATCH] [wp] Warns on user defined variant relations
---
src/plugins/wp/cfgAnnot.ml | 9 ++++++++-
src/plugins/wp/cfgWP.ml | 5 +++--
.../wp/tests/wp_acsl/oracle/decreases.0.res.oracle | 2 ++
.../wp/tests/wp_acsl/oracle/decreases.1.res.oracle | 2 ++
.../tests/wp_acsl/oracle/terminates_formulae.res.oracle | 2 ++
.../tests/wp_acsl/oracle_qualif/decreases.0.res.oracle | 2 ++
.../tests/wp_acsl/oracle_qualif/decreases.1.res.oracle | 2 ++
.../wp_acsl/oracle_qualif/terminates_formulae.res.oracle | 2 ++
8 files changed, 23 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index d6bc77f086a..12bdacececd 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -244,11 +244,17 @@ let get_terminates_hyp kf =
| Defined (_, p) -> false, p
| Assumed p -> true, p
+let check_variant_relation = function
+ | (_, None) -> ()
+ | (_, Some rel) ->
+ Wp_parameters.hypothesis ~once:true
+ "'%a' relation must be well-founded" Cil_printer.pp_logic_info rel
+
let get_decreases_goal kf =
let defined t = WpPropId.mk_decrease_id kf Kglobal t, t in
match Annotations.decreases ~populate:false kf with
| None -> None
- | Some v -> Some (defined v)
+ | Some v -> check_variant_relation v ; Some (defined v)
let get_decreases_hyp kf =
Annotations.decreases ~populate:false kf
@@ -475,6 +481,7 @@ let mk_variant_properties kf s ca v =
(vpos_id, vpos), (vdecr_id, vdecr)
let mk_variant_relation_property kf s ca v li =
+ check_variant_relation (v, Some li) ;
let vid = WpPropId.mk_var_id kf s ca in
let loc = v.term_loc in
let lcurr = Clabels.to_logic (Clabels.loop_current s) in
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index a0ce9b9ceb9..1bece5f01ae 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1153,11 +1153,12 @@ struct
Kernel_function.pretty kf
| (_, r), Some (_, r')
when not @@ Option.equal Logic_utils.is_same_logic_info r r' ->
+ let none : Pretty_utils.sformat = "<None>" in
Warning.error
"On call to %a, relation (%a) does not match caller (%a)"
Kernel_function.pretty kf
- (Pretty_utils.pp_opt Cil_printer.pp_logic_info) r
- (Pretty_utils.pp_opt Cil_printer.pp_logic_info) r'
+ (Pretty_utils.pp_opt ~none Cil_printer.pp_logic_info) r
+ (Pretty_utils.pp_opt ~none Cil_printer.pp_logic_info) r'
| (caller_d, rel), Some (callee_d,_ ) ->
let rel caller callee = match rel with
| None ->
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
index 767145c220c..1c0241e1df5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
index 337093493a9..503c4176882 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index 7f2d6c08cd7..d9bd70618f7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] terminates_formulae.i:90: Warning:
+ 'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
[wp] terminates_formulae.i:90: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
index a1c4020be5c..62e79688690 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
index 915be052f0a..63e3fba1f74 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
@@ -2,7 +2,9 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
+[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
[wp] decreases.i:105: Warning:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index 06ea7290c29..cf90d39ba3f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp:hypothesis] terminates_formulae.i:90: Warning:
+ 'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
[wp] terminates_formulae.i:90: Warning:
--
GitLab