From 250a5c949d321f34069c4afcffde1b046d0a4408 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 26 Apr 2022 16:19:48 +0200
Subject: [PATCH] [wp] fix decreases caller evaluation
---
src/plugins/wp/cfgAnnot.ml | 15 +++++++++++----
src/plugins/wp/normAtLabels.ml | 4 ++++
src/plugins/wp/normAtLabels.mli | 1 +
src/plugins/wp/tests/wp_acsl/decreases.i | 12 ++++++++++++
.../tests/wp_acsl/oracle/decreases.0.res.oracle | 16 ++++++++++++++--
.../tests/wp_acsl/oracle/decreases.1.res.oracle | 16 ++++++++++++++--
.../oracle/terminates_formulae.res.oracle | 4 +++-
.../wp_acsl/oracle_qualif/decreases.0.res.oracle | 15 ++++++++++-----
.../wp_acsl/oracle_qualif/decreases.1.res.oracle | 15 ++++++++++-----
.../oracle_qualif/terminates_formulae.res.oracle | 4 +++-
10 files changed, 82 insertions(+), 20 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 425f3df70fe..9e529fc7c44 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -91,6 +91,12 @@ let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
Some (id , implies ?assumes p)
else None
+let normalize_decreases (d, li) =
+ let module L = NormAtLabels in
+ let at_pre e = Logic_const.tat (e, BuiltinLabel Pre) in
+ let labels = L.labels_fct_pre in
+ (at_pre @@ L.preproc_term labels d, li)
+
let normalize_froms tk froms =
let module L = NormAtLabels in
let labels = L.labels_fct_assigns ~exit:(tk=Exits) in
@@ -246,12 +252,13 @@ let get_terminates_hyp kf =
let check_variant_relation = function
| (_, None) -> ()
- | (_, Some rel) ->
- Wp_parameters.hypothesis ~once:true
+ | ({ term_loc }, Some rel) ->
+ Wp_parameters.hypothesis
+ ~source:(fst term_loc) ~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
+ let defined t = WpPropId.mk_decrease_id kf Kglobal t, normalize_decreases t in
match Annotations.decreases ~populate:false kf with
| None -> None
| Some v -> check_variant_relation v ; Some (defined v)
@@ -348,7 +355,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| Writes froms -> Writes (normalize_froms Normal froms)
in
let terminates = get_terminates_hyp kf in
- let decreases = get_decreases_hyp kf in
+ let decreases = Option.map normalize_decreases @@ get_decreases_hyp kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 0033fe47bf1..4ae48410ed5 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -214,6 +214,10 @@ let preproc_annot labels p =
let visitor = new norm_at labels in
Visitor.visitFramacPredicate visitor p
+let preproc_term labels t =
+ let visitor = new norm_at labels in
+ Visitor.visitFramacTerm visitor t
+
(** @raise LabelError if there is a label in [p] that is incompatible
* with the [labels] translation *)
let preproc_assigns labels asgns =
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index dfa2f0962e4..73e5c5ca0be 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -42,6 +42,7 @@ val labels_stmt_assigns_l : kf:kernel_function -> stmt -> c_label option -> labe
val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
+val preproc_term : label_mapping -> term -> term
val preproc_annot : label_mapping -> predicate -> predicate
val preproc_assigns : label_mapping -> from list -> from list
val has_postassigns : assigns -> bool
diff --git a/src/plugins/wp/tests/wp_acsl/decreases.i b/src/plugins/wp/tests/wp_acsl/decreases.i
index b4d482fe2e6..c264819eb94 100644
--- a/src/plugins/wp/tests/wp_acsl/decreases.i
+++ b/src/plugins/wp/tests/wp_acsl/decreases.i
@@ -111,3 +111,15 @@ void mw2(unsigned x){
(void)fact(x); // no verification of decreases here
}
+
+// Recursion with side-effect
+
+int x ;
+
+//@ decreases x ;
+void se(void){
+ if (x > 0){
+ x -- ;
+ se();
+ }
+}
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 1c0241e1df5..d20b0623277 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,11 +2,14 @@
[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:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: 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:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
------------------------------------------------------------
@@ -240,3 +243,12 @@ Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: P_Wrong(x, to_uint32(x - 1)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function se
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 123
+Prove: true.
+
+------------------------------------------------------------
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 503c4176882..acfb72158d9 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,11 +2,14 @@
[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:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: 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:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
------------------------------------------------------------
@@ -257,3 +260,12 @@ Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: P_Wrong(x, to_uint32(x - 1)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function se
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 123
+Prove: true.
+
+------------------------------------------------------------
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 d9bd70618f7..d8eeb1c7538 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,7 +2,9 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:90: Warning:
+[wp:hypothesis] terminates_formulae.i:84: Warning:
+ 'Rel' relation must be well-founded
+[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
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 62e79688690..a87bf332421 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,14 +2,17 @@
[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:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: 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:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
-[wp] 26 goals scheduled
+[wp] 27 goals scheduled
[wp] [Qed] Goal typed_fact_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fact_variant : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_variant : Unsuccess
@@ -36,8 +39,9 @@
[wp] [Alt-Ergo] Goal typed_mw2_variant_part1 : Unsuccess (Degenerated)
[wp] [Alt-Ergo] Goal typed_mw2_variant_part2 : Valid
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
-[wp] Proved goals: 17 / 26
- Qed: 6
+[wp] [Qed] Goal typed_se_variant : Valid
+[wp] Proved goals: 18 / 27
+ Qed: 7
Alt-Ergo: 11 (unsuccess: 9)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -54,4 +58,5 @@
mt1 1 1 3 66.7%
mw2 - 1 2 50.0%
mw1 - - 1 0.0%
+ se 1 - 1 100%
------------------------------------------------------------
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 63e3fba1f74..541e824ca01 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,14 +2,17 @@
[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:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: 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:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
-[wp] 26 goals scheduled
+[wp] 27 goals scheduled
[wp] [Qed] Goal typed_fact_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fact_variant : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_variant : Unsuccess
@@ -36,8 +39,9 @@
[wp] [Alt-Ergo] Goal typed_mw2_variant_part1 : Unsuccess (Degenerated)
[wp] [Alt-Ergo] Goal typed_mw2_variant_part2 : Valid
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
-[wp] Proved goals: 18 / 26
- Qed: 7
+[wp] [Qed] Goal typed_se_variant : Valid
+[wp] Proved goals: 19 / 27
+ Qed: 8
Alt-Ergo: 11 (unsuccess: 8)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -54,4 +58,5 @@
mt1 1 1 3 66.7%
mw2 - 1 2 50.0%
mw1 - - 1 0.0%
+ se 1 - 1 100%
------------------------------------------------------------
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 cf90d39ba3f..cb8634fd614 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,7 +2,9 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:90: Warning:
+[wp:hypothesis] terminates_formulae.i:84: Warning:
+ 'Rel' relation must be well-founded
+[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
--
GitLab