From d847cc19d1215596b3a44a8cf86d77857a4b2385 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 17 Dec 2021 17:10:20 +0100
Subject: [PATCH] [wp] Weaken check invariant - no they have the expected
behavior
---
src/plugins/wp/cfgAnnot.ml | 12 +-
src/plugins/wp/cfgAnnot.mli | 7 +-
src/plugins/wp/cfgCalculus.ml | 32 +++--
src/plugins/wp/cfgDump.ml | 11 +-
src/plugins/wp/cfgWP.ml | 8 +-
src/plugins/wp/mcfg.mli | 3 +-
src/plugins/wp/tests/wp/cfg_loop_deps.i | 26 ++++
.../tests/wp/oracle/cfg_loop_deps.res.oracle | 135 ++++++++++++++++++
.../oracle/generalized_checks.res.oracle | 3 +-
.../generalized_checks.res.oracle | 10 +-
10 files changed, 219 insertions(+), 28 deletions(-)
create mode 100644 src/plugins/wp/tests/wp/cfg_loop_deps.i
create mode 100644 src/plugins/wp/tests/wp/oracle/cfg_loop_deps.res.oracle
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 1103f2c2fe5..6e114cdf7e7 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -468,8 +468,13 @@ let mk_variant_properties kf s ca v =
let vdecr = Logic_const.prel ~loc (Rlt, v, vcurr) in
(vpos_id, vpos), (vdecr_id, vdecr)
+type loop_hypothesis =
+ | NoHyp
+ | Check of WpPropId.prop_id
+ | Always of WpPropId.prop_id
+
type loop_invariant = {
- loop_hyp : WpPropId.prop_id option ;
+ loop_hyp : loop_hypothesis ;
loop_est : WpPropId.prop_id option ;
loop_ind : WpPropId.prop_id option ;
loop_pred : Cil_types.predicate ;
@@ -509,10 +514,11 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
let g_est, g_ind = WpPropId.mk_loop_inv kf stmt ca in
let admit = Logic_utils.use_predicate inv.tp_kind in
let verif = Logic_utils.verify_predicate inv.tp_kind in
+ let loop_hyp = if admit then Always g_hyp else Check g_hyp in
let use flag id = if flag then Some id else None in
let inv =
{ loop_pred = normalize_pred inv.tp_statement ;
- loop_hyp = use admit g_hyp ;
+ loop_hyp ;
loop_est = use verif g_est ;
loop_ind = use verif g_ind ; }
in
@@ -536,7 +542,7 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
let mk_inv (i, p) =
let i, p = intro_terminates @@ normalize_annot (i, p) in
{ loop_pred = p ;
- loop_hyp = None ; loop_est = None ; loop_ind = Some i }
+ loop_hyp = NoHyp ; loop_est = None ; loop_ind = Some i }
in
{ l with loop_terminates = None ;
loop_invariants =
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index f3311ca1a52..53c1c4659e4 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -78,8 +78,13 @@ val get_stmt_assigns : kernel_function -> stmt -> assigns_full_info list
(* --- Property Accessors : Loop Contracts --- *)
(* -------------------------------------------------------------------------- *)
+type loop_hypothesis =
+ | NoHyp
+ | Check of WpPropId.prop_id
+ | Always of WpPropId.prop_id
+
type loop_invariant = {
- loop_hyp : WpPropId.prop_id option ;
+ loop_hyp : loop_hypothesis ;
loop_est : WpPropId.prop_id option ;
loop_ind : WpPropId.prop_id option ;
loop_pred : Cil_types.predicate ;
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 198ae795cbc..4fba7b07405 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -182,8 +182,8 @@ struct
then W.add_assigns env.we ai w
else w
- let use_property env (p : WpPropId.pred_info) w =
- if is_selected ~goal:false env p then W.add_hyp env.we p w else w
+ let use_property ?for_pid env (p : WpPropId.pred_info) w =
+ if is_selected ~goal:false env p then W.add_hyp ?for_pid env.we p w else w
let prove_property env (p : WpPropId.pred_info) w =
if is_selected ~goal:true env p then W.add_goal env.we p w else w
@@ -259,18 +259,28 @@ struct
| None, _ | _, None -> w (* no terminates goal or nothing to prove *)
| Some t, Some prop -> prove_subproperty env t prop s FromCode w
in
- let if_some_id op env id p w =
- match id with None -> w | Some id -> op env (id, p) w in
- let loop_current_hyp env CfgAnnot.{ loop_hyp ; loop_pred } =
- if_some_id use_property env loop_hyp loop_pred
+ let prove_invariant env pid pred w =
+ match pid with None -> w | Some pid -> prove_property env (pid, pred) w
in
- let established env CfgAnnot.{ loop_hyp ; loop_est ; loop_pred } w =
- if_some_id prove_property env loop_est loop_pred @@
- if_some_id use_property env loop_hyp loop_pred w
+ let assume_invariant env (hyp: CfgAnnot.loop_hypothesis) pred ind w =
+ match hyp with
+ | NoHyp -> w
+ | Check pid -> use_property ?for_pid:ind env (pid, pred) w
+ | Always pid -> use_property env (pid, pred) w
+ in
+ let established env CfgAnnot.{ loop_hyp; loop_ind; loop_est; loop_pred } w =
+ prove_invariant env loop_est loop_pred @@
+ assume_invariant env loop_hyp loop_pred loop_ind w
+ in
+ let loop_current_hyp env CfgAnnot.{ loop_hyp ; loop_ind ; loop_pred } w =
+ assume_invariant env loop_hyp loop_pred loop_ind w
in
let preserved env CfgAnnot.{ loop_hyp ; loop_ind ; loop_pred } w =
- if_some_id prove_property env loop_ind loop_pred @@
- if_some_id use_property env loop_hyp loop_pred w
+ prove_invariant env loop_ind loop_pred @@
+ begin match loop_hyp with
+ | CfgAnnot.Always pid -> use_property env (pid, loop_pred)
+ | _ -> Extlib.id (* we never assume this one for checks *)
+ end w
in
insert_terminates @@
List.fold_right (established env) lc.loop_invariants @@
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index c15ac2a858f..c38b30c4127 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -89,12 +89,17 @@ let new_env ?lvars kf : t_env = ignore lvars ; kf
let add_axiom _p _l = ()
-let add_hyp _env (pid,pred) k =
+let add_hyp ?for_pid _env (pid,pred) k =
+ ignore(for_pid);
let u = node () in
if Wp_parameters.debug_atleast 1 then
- Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u Printer.pp_predicate pred
+ Format.fprintf !out " %a [ color=green , label=\"Assume %a%a\"] ;@."
+ pretty u Printer.pp_predicate pred
+ (Pretty_utils.pp_opt ~pre:" for" WpPropId.pretty) for_pid
else
- Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+ Format.fprintf !out " %a [ color=green , label=\"Assume %a%a\"] ;@."
+ pretty u WpPropId.pp_propid pid
+ (Pretty_utils.pp_opt ~pre:" for" WpPropId.pretty) for_pid ;
link u k ; u
let add_goal env (pid,pred) k =
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 7c5edf076e1..97c136c1d4f 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -484,7 +484,7 @@ struct
let add_axiom _id _l = ()
- let add_hyp wenv (hpid,predicate) wp = in_wenv wenv wp
+ let add_hyp ?for_pid wenv (hpid,predicate) wp = in_wenv wenv wp
(fun env wp ->
let outcome = Warning.catch
~severe:false ~effect:"Skip hypothesis"
@@ -493,7 +493,11 @@ struct
| Warning.Result(warn,p) -> warn , [p]
| Warning.Failed warn -> warn , []
in
- let vcs = gmap (assume_vc ~hpid ~warn hs) wp.vcs in
+ let assume_vc target vcs = match for_pid with
+ | Some id when not @@ PropId.equal id (TARGET.prop_id target) -> vcs
+ | _ -> Splitter.map (assume_vc ~hpid ~warn hs) vcs
+ in
+ let vcs = Gmap.mapi assume_vc wp.vcs in
{ wp with vcs = vcs })
let add_goal wenv (gpid,predicate) wp = in_wenv wenv wp
diff --git a/src/plugins/wp/mcfg.mli b/src/plugins/wp/mcfg.mli
index 3ecd5a5f9a2..3afad69feed 100644
--- a/src/plugins/wp/mcfg.mli
+++ b/src/plugins/wp/mcfg.mli
@@ -65,7 +65,8 @@ module type S = sig
val new_env : ?lvars:Cil_types.logic_var list -> kernel_function -> t_env
val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
- val add_hyp : t_env -> WpPropId.pred_info -> t_prop -> t_prop
+ val add_hyp :
+ ?for_pid:WpPropId.prop_id -> t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_subgoal : t_env -> WpPropId.pred_info -> ?deps:Property.Set.t ->
predicate -> stmt -> WpPropId.effect_source -> t_prop -> t_prop
diff --git a/src/plugins/wp/tests/wp/cfg_loop_deps.i b/src/plugins/wp/tests/wp/cfg_loop_deps.i
new file mode 100644
index 00000000000..4d034c136d2
--- /dev/null
+++ b/src/plugins/wp/tests/wp/cfg_loop_deps.i
@@ -0,0 +1,26 @@
+/* run.config_qualif
+ DONTRUN:
+*/
+
+/*@ axiomatic Ax {
+ predicate P(integer i);
+ predicate Q(integer i);
+ predicate R(integer i);
+ predicate S(integer i);
+ predicate W(integer i);
+ }
+*/
+
+int x ;
+
+void function(void){
+ int i = 0;
+ /*@ loop invariant IP: P(i) ;
+ @ check loop invariant IQ: Q(i);
+ @ admit loop invariant IR: R(i);
+ @ loop invariant IS: S(i);
+ @ loop assigns i ; */
+ while(i < 10) i++ ;
+
+ //@ check W(i);
+}
diff --git a/src/plugins/wp/tests/wp/oracle/cfg_loop_deps.res.oracle b/src/plugins/wp/tests/wp/oracle/cfg_loop_deps.res.oracle
new file mode 100644
index 00000000000..31ebbb9df49
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/cfg_loop_deps.res.oracle
@@ -0,0 +1,135 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/cfg_loop_deps.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function function
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'IP' (file tests/wp/cfg_loop_deps.i, line 18):
+Let x = 1 + i.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(x).
+ (* Invariant 'IP' *)
+ Have: P_P(0).
+ (* Invariant 'IR' *)
+ Have: P_R(0).
+ (* Invariant 'IS' *)
+ Have: P_S(0).
+ (* Invariant 'IP' *)
+ Have: P_P(i).
+ (* Invariant 'IR' *)
+ Have: P_R(i).
+ (* Invariant 'IS' *)
+ Have: P_S(i).
+ (* Then *)
+ Have: i <= 9.
+}
+Prove: P_P(x).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'IP' (file tests/wp/cfg_loop_deps.i, line 18):
+Prove: P_P(0).
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'IQ' (file tests/wp/cfg_loop_deps.i, line 19):
+Let x = 1 + i.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(x).
+ (* Invariant 'IP' *)
+ Have: P_P(0).
+ (* Invariant 'IQ' *)
+ Have: P_Q(0).
+ (* Invariant 'IR' *)
+ Have: P_R(0).
+ (* Invariant 'IS' *)
+ Have: P_S(0).
+ (* Invariant 'IP' *)
+ Have: P_P(i).
+ (* Invariant 'IQ' *)
+ Have: P_Q(i).
+ (* Invariant 'IR' *)
+ Have: P_R(i).
+ (* Invariant 'IS' *)
+ Have: P_S(i).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant 'IP' *)
+ Have: P_P(x).
+}
+Prove: P_Q(x).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'IQ' (file tests/wp/cfg_loop_deps.i, line 19):
+Assume { (* Invariant 'IP' *) Have: P_P(0). }
+Prove: P_Q(0).
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'IS' (file tests/wp/cfg_loop_deps.i, line 21):
+Let x = 1 + i.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(x).
+ (* Invariant 'IP' *)
+ Have: P_P(0).
+ (* Invariant 'IR' *)
+ Have: P_R(0).
+ (* Invariant 'IS' *)
+ Have: P_S(0).
+ (* Invariant 'IP' *)
+ Have: P_P(i).
+ (* Invariant 'IR' *)
+ Have: P_R(i).
+ (* Invariant 'IS' *)
+ Have: P_S(i).
+ (* Then *)
+ Have: i <= 9.
+ (* Invariant 'IP' *)
+ Have: P_P(x).
+ (* Invariant 'IR' *)
+ Have: P_R(x).
+}
+Prove: P_S(x).
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'IS' (file tests/wp/cfg_loop_deps.i, line 21):
+Assume {
+ (* Invariant 'IP' *)
+ Have: P_P(0).
+ (* Invariant 'IR' *)
+ Have: P_R(0).
+}
+Prove: P_S(0).
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp/cfg_loop_deps.i, line 25):
+Assume {
+ Type: is_sint32(i).
+ (* Invariant 'IP' *)
+ Have: P_P(0).
+ (* Invariant 'IR' *)
+ Have: P_R(0).
+ (* Invariant 'IS' *)
+ Have: P_S(0).
+ (* Invariant 'IP' *)
+ Have: P_P(i).
+ (* Invariant 'IR' *)
+ Have: P_R(i).
+ (* Invariant 'IS' *)
+ Have: P_S(i).
+ (* Else *)
+ Have: 10 <= i.
+}
+Prove: P_W(i).
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp/cfg_loop_deps.i, line 22):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
index 65a87c92522..8320e268cf4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -151,8 +151,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
-Assume { Type: is_sint32(i). (* Then *) Have: i <= 9. }
-Prove: false.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
index 99a33fee772..22b1cace818 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -20,13 +20,13 @@
[wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
[wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess
-[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved : Unsuccess
+[wp] [Qed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved : Valid
[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_established : Unsuccess
[wp] [Alt-Ergo] Goal typed_loop_check_implied_by_false_invariant : Unsuccess
[wp] [Qed] Goal typed_loop_loop_assigns : Valid
-[wp] Proved goals: 12 / 21
- Qed: 10
- Alt-Ergo: 2 (unsuccess: 9)
+[wp] Proved goals: 13 / 21
+ Qed: 11
+ Alt-Ergo: 2 (unsuccess: 8)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Th - - 2 0.0%
@@ -34,5 +34,5 @@
Functions WP Alt-Ergo Total Success
job 3 2 6 83.3%
caller 6 - 9 66.7%
- loop 1 - 4 25.0%
+ loop 2 - 4 50.0%
------------------------------------------------------------
--
GitLab