From bf1dc9369aa866f65f7b1c0fedc89726dfd86013 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 7 Jun 2021 15:57:41 +0200
Subject: [PATCH] [wp] Populate terminates true
---
src/plugins/wp/cfgAnnot.ml | 31 +++++++++++++++----
src/plugins/wp/cfgInfos.ml | 9 +++---
.../terminates_call_options.1.res.oracle | 17 ++++++++--
.../terminates_call_options.1.res.oracle | 17 +++++++---
.../tests/wp_acsl/terminates_call_options.i | 4 +++
5 files changed, 60 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 16eb2e534cc..5c3aee79f13 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -183,10 +183,29 @@ let normalize_terminates p =
L.preproc_annot L.labels_fct_pre @@
Logic_const.pat (p.ip_content.tp_statement, BuiltinLabel Pre)
+let wp_populate_terminates =
+ Emitter.create
+ "Populate terminates"
+ [Emitter.Property_status]
+ ~correctness:[] (* TBC *)
+ ~tuning:[] (* TBC *)
+
let get_terminates kf =
- Option.map
- (fun p -> WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
- (Annotations.terminates kf)
+ match Annotations.terminates kf with
+ | None
+ when Kernel_function.is_definition kf &&
+ Wp_parameters.TerminatesDefinitions.get () ->
+ let p = Logic_const.new_predicate @@ Logic_const.ptrue in
+ Wp_parameters.warning
+ ~source:(fst @@ Kernel_function.get_location kf) ~once:true
+ "Missing terminates clause for %a, populates 'terminates \\true'"
+ Kernel_function.pretty kf ;
+ Annotations.add_terminates wp_populate_terminates kf p ;
+ Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
+ | None ->
+ None
+ | Some p ->
+ Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
let get_terminates_call kf =
match Annotations.terminates kf with
@@ -472,9 +491,9 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
WpStrategy.mk_variant_properties kf stmt ca term in
let intro_terminates (pid, v) =
pid,
- match Annotations.terminates kf with
- | Some t when Wp_parameters.TerminatesVariantHyp.get () ->
- Logic_const.pimplies (normalize_terminates t, v)
+ match get_terminates kf with
+ | Some (_,t) when Wp_parameters.TerminatesVariantHyp.get () ->
+ Logic_const.pimplies (t, v)
| _ -> v
in
{ l with loop_terminates = None ;
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 203ded1f820..9d3ed98ff63 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -113,7 +113,7 @@ let selected_clause ~prop name getter kf =
let selected_terminates ~prop kf =
match Annotations.terminates kf with
| None ->
- false
+ Wp_parameters.TerminatesDefinitions.get ()
| Some ip ->
let tk_name = "@terminates" in
let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
@@ -328,13 +328,12 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
(fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
infos.doomed ;
(* Trivial terminates *)
- begin match Annotations.terminates kf with
- | Some t
+ begin match CfgAnnot.get_terminates kf with
+ | Some (id, _t)
when selected_terminates ~prop kf
&& infos.calls = Fset.empty
&& infos.no_variant_loops = Sset.empty ->
- WpAnnot.set_trivially_terminates @@
- WpPropId.mk_terminates_id kf Kglobal t
+ WpAnnot.set_trivially_terminates id
| _ -> ()
end ;
(* Collected Infos *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
index 51f3303b866..f4391330dec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
@@ -2,10 +2,14 @@
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_call_options.i:17: Warning:
+ Missing terminates clause for definition, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_call_options.i:29: Warning:
+ Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.i:21: Warning:
Missing terminates clause on call to declaration, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.i:26: Warning:
- Missing terminates clause on call to definition, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.i:30: Warning:
+ Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
@@ -30,3 +34,12 @@ Goal Assigns nothing in 'definition':
Prove: true.
------------------------------------------------------------
+------------------------------------------------------------
+ Function no_spec_generates_goal
+------------------------------------------------------------
+
+Goal Termination-condition (generated) in 'no_spec_generates_goal':
+Effect at line 30
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
index 356e129f4e4..7dc2fa7d793 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
@@ -2,19 +2,26 @@
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_call_options.i:17: Warning:
+ Missing terminates clause for definition, populates 'terminates \true'
+[wp] tests/wp_acsl/terminates_call_options.i:29: Warning:
+ Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.i:21: Warning:
Missing terminates clause on call to declaration, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.i:26: Warning:
- Missing terminates clause on call to definition, defaults to \true
-[wp] 3 goals scheduled
+[wp] tests/wp_acsl/terminates_call_options.i:30: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 4 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates : Valid
[wp] [Qed] Goal typed_call_definition_terminates : Valid
-[wp] Proved goals: 3 / 3
- Qed: 3
+[wp] [Alt-Ergo] Goal typed_no_spec_generates_goal_terminates : Unsuccess
+[wp] Proved goals: 3 / 4
+ Qed: 3
+ Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
call_declaration 1 - 1 100%
call_definition 1 - 1 100%
+ no_spec_generates_goal - - 1 0.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_call_options.i b/src/plugins/wp/tests/wp_acsl/terminates_call_options.i
index 7aedc2aec4c..4f00e356794 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_call_options.i
+++ b/src/plugins/wp/tests/wp_acsl/terminates_call_options.i
@@ -25,3 +25,7 @@ void call_declaration(void){
void call_definition(void){
definition();
}
+
+void no_spec_generates_goal(void){
+ for(;;);
+}
--
GitLab