From 8c47b93028856dbfb8bcbdd8362c74b333372fcf Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 9 Jun 2021 10:42:28 +0200
Subject: [PATCH] [wp] Refacto CfgAnnot
---
src/plugins/wp/cfgAnnot.ml | 67 ++++++++++++-------
src/plugins/wp/cfgAnnot.mli | 4 +-
src/plugins/wp/cfgCalculus.ml | 2 +-
src/plugins/wp/cfgInfos.ml | 2 +-
.../terminates_call_options.0.res.oracle | 12 +++-
.../terminates_call_options.1.res.oracle | 4 ++
.../terminates_call_options.0.res.oracle | 15 +++--
.../terminates_call_options.1.res.oracle | 4 ++
.../tests/wp_acsl/terminates_call_options.c | 1 +
9 files changed, 77 insertions(+), 34 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 93e8cd53242..39d30a060ee 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -190,35 +190,54 @@ let wp_populate_terminates =
~correctness:[] (* TBC *)
~tuning:[] (* TBC *)
-let get_terminates kf =
+type terminates_clause =
+ | Defined of WpPropId.prop_id * predicate
+ | Assumed of predicate
+
+let get_terminates_clause kf =
+ (* Note:
+ * - user-defined terminates always returns Defined
+ * - generated "terminates \true" are:
+ * - first handled in a None case and returns Defined
+ * - then handled in a Some case (as user defined) and returns Defined *)
+ let defined p =
+ Defined (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p) in
+ let populate_true () =
+ 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 ;
+ defined p
+ in
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 when Kernel_function.is_in_libc kf ->
+ if not @@ Wp_parameters.TerminatesFCDeclarations.get ()
+ then Assumed Logic_const.pfalse
+ else if not @@ Kernel_function.is_definition kf
+ then Assumed Logic_const.ptrue
+ else populate_true ()
+ | None when Kernel_function.is_definition kf ->
+ if not @@ Wp_parameters.TerminatesDefinitions.get ()
+ then Assumed Logic_const.pfalse
+ else populate_true ()
| None ->
- None
+ if not @@ Wp_parameters.TerminatesExtDeclarations.get ()
+ then Assumed Logic_const.pfalse
+ else Assumed Logic_const.ptrue
| Some p ->
- Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
+ defined p
+
+let get_terminates_goal kf =
+ match get_terminates_clause kf with
+ | Assumed _ -> None
+ | Defined (id, p) -> Some (id, p)
let get_terminates_hyp kf =
- let to_default option =
- if option then Logic_const.ptrue else Logic_const.pfalse in
- match Annotations.terminates kf with
- | Some p ->
- false, normalize_terminates p
- | None when Kernel_function.is_in_libc kf ->
- false, to_default @@ Wp_parameters.TerminatesFCDeclarations.get ()
- | None when Kernel_function.is_definition kf ->
- true, to_default @@ Wp_parameters.TerminatesDefinitions.get ()
- | None ->
- true, to_default @@ Wp_parameters.TerminatesExtDeclarations.get ()
+ match get_terminates_clause kf with
+ | Defined (_, p) -> false, p
+ | Assumed p -> true, p
(* -------------------------------------------------------------------------- *)
(* --- Contracts --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 9b29f4bc05d..a6c4c5bcb36 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -56,7 +56,7 @@ val get_behavior_goals :
val get_complete_behaviors : kernel_function -> pred_info list
val get_disjoint_behaviors : kernel_function -> pred_info list
-val get_terminates : kernel_function -> pred_info option
+val get_terminates_goal : kernel_function -> pred_info option
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Assertions --- *)
@@ -105,7 +105,7 @@ type contract = {
contract_exit : pred_info list ;
contract_smoke : pred_info list ;
contract_assigns : assigns ;
- contract_terminates : bool * predicate ; (* boolean: default generated *)
+ contract_terminates : bool * predicate ; (* boolean: assumed terminates *)
}
val get_call_contract : ?smoking:stmt -> kernel_function -> stmt -> contract
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index ffc222e95de..41c62992ab8 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -414,7 +414,7 @@ struct
WpLog.SmokeTests.get () &&
WpLog.SmokeDeadcode.get ()
then CfgInfos.smoking infos else (fun _ -> false) in
- let terminates = CfgAnnot.get_terminates kf in
+ let terminates = CfgAnnot.get_terminates_goal kf in
let env = {
mode ; props ; body ;
succ ; dead ; terminates ;
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 9d3ed98ff63..78eed54a2d7 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -328,7 +328,7 @@ 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 CfgAnnot.get_terminates kf with
+ begin match CfgAnnot.get_terminates_goal kf with
| Some (id, _t)
when selected_terminates ~prop kf
&& infos.calls = Fset.empty
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
index 88e54b0226b..70f61d7719b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
@@ -6,6 +6,10 @@
Missing terminates clause on call to declaration, defaults to \false
[wp] tests/wp_acsl/terminates_call_options.c:28: Warning:
Missing terminates clause on call to definition, defaults to \false
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning:
+ Missing terminates clause on call to exit, defaults to \false
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning:
+ Missing terminates clause on call to div, defaults to \false
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
@@ -36,8 +40,14 @@ Prove: true.
Function libc_call
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call':
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (1/2):
Call Effect at line 37
Prove: false.
------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (2/2):
+Call Effect at line 38
+Prove: false.
+
+------------------------------------------------------------
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 6fdc59ea5b7..a48bad2bd1e 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
@@ -10,6 +10,10 @@
Missing terminates clause on call to declaration, defaults to \true
[wp] tests/wp_acsl/terminates_call_options.c:32: Warning:
Missing assigns clause (assigns 'everything' instead)
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning:
+ Missing terminates clause on call to exit, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning:
+ Missing terminates clause on call to div, defaults to \true
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
index 9b35ba85627..014de1caf3f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
@@ -6,18 +6,23 @@
Missing terminates clause on call to declaration, defaults to \false
[wp] tests/wp_acsl/terminates_call_options.c:28: Warning:
Missing terminates clause on call to definition, defaults to \false
-[wp] 4 goals scheduled
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning:
+ Missing terminates clause on call to exit, defaults to \false
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning:
+ Missing terminates clause on call to div, defaults to \false
+[wp] 5 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Alt-Ergo] Goal typed_call_declaration_terminates : Unsuccess
[wp] [Alt-Ergo] Goal typed_call_definition_terminates : Unsuccess
-[wp] [Alt-Ergo] Goal typed_libc_call_terminates : Unsuccess
-[wp] Proved goals: 1 / 4
+[wp] [Alt-Ergo] Goal typed_libc_call_terminates_part1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_libc_call_terminates_part2 : Unsuccess
+[wp] Proved goals: 1 / 5
Qed: 1
- Alt-Ergo: 0 (unsuccess: 3)
+ Alt-Ergo: 0 (unsuccess: 4)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
call_declaration - - 1 0.0%
call_definition - - 1 0.0%
- libc_call - - 1 0.0%
+ libc_call - - 2 0.0%
------------------------------------------------------------
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 66f71fa70b7..780952849c8 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
@@ -10,6 +10,10 @@
Missing terminates clause on call to declaration, defaults to \true
[wp] tests/wp_acsl/terminates_call_options.c:32: Warning:
Missing assigns clause (assigns 'everything' instead)
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning:
+ Missing terminates clause on call to exit, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:37: Warning:
+ Missing terminates clause on call to div, defaults to \true
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_call_options.c b/src/plugins/wp/tests/wp_acsl/terminates_call_options.c
index 47a083dc404..d26bc0ac61d 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_call_options.c
+++ b/src/plugins/wp/tests/wp_acsl/terminates_call_options.c
@@ -35,4 +35,5 @@ void no_spec_generates_goal(void){
//@ terminates \true ;
void libc_call(void){
(void) div(4,3);
+ exit(0);
}
--
GitLab