From 159e2efc44e8d8cfc43f2e2a6cbf83101109c5c8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 2 Feb 2021 11:56:27 +0100
Subject: [PATCH] [wp] Partial refactoring of main compute procedure
---
src/plugins/wp/cfgCalculus.ml | 76 +++++++++++--------
src/plugins/wp/tests/wp/exit_post_scope.i | 9 +++
.../wp/oracle/exit_post_scope.res.oracle | 19 +++++
.../oracle_qualif/exit_post_scope.res.oracle | 15 ++++
4 files changed, 89 insertions(+), 30 deletions(-)
create mode 100644 src/plugins/wp/tests/wp/exit_post_scope.i
create mode 100644 src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 77b150a71b9..36dbc16b796 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -134,12 +134,7 @@ struct
cfg: Cfg.automaton ;
}
- let rec has_reachable_call cfg v =
- let env = { table = Vhash.create 32 ; cfg } in
- try reachable_call_by_cfg env v ; false
- with Found_call -> true
-
- and reachable_call_by_cfg env a =
+ let rec reachable_call_by_cfg env a =
try Vhash.find env.table a
with Not_found ->
Vhash.add env.table a () ;
@@ -151,6 +146,11 @@ struct
| Instr ((Local_init(_,ConsInit _, _)| Call _), _) -> raise Found_call
| _ -> ()
+ let has_reachable_call cfg v =
+ let env = { table = Vhash.create 32 ; cfg } in
+ try reachable_call_by_cfg env v ; false
+ with Found_call -> true
+
end
(* --- Traversal Environment --- *)
@@ -185,7 +185,7 @@ struct
match a with
| NoAssignsInfo -> assert false
| AssignsAny ad ->
- Wp_parameters.warning ~current:true ~once:true
+ WpLog.warning ~current:true ~once:true
"Missing assigns clause (assigns 'everything' instead)" ;
W.use_assigns env.we None ad w
| AssignsLocations(ap,ad) -> W.use_assigns env.we (Some ap) ad w
@@ -367,40 +367,56 @@ struct
if not @@ WpStrategy.is_main_init kf then Extlib.id
else List.fold_right (prove_property env) ps
in
+ let do_preconditions env w =
+ List.fold_right (use_property env) req @@
+ List.fold_right (use_property env) bhv.bhv_assumes @@
+ prove_if_main env bhv.bhv_requires @@
+ List.fold_right (use_property env) bhv.bhv_requires @@
+ List.fold_right (use_property env) (behaviors kf) w
+ in
+ let do_complete_disjoint env w =
+ List.fold_right (prove_property env) (complete mode kf) @@
+ List.fold_right (prove_property env) (disjoint mode kf) w
+ in
+ let do_function_body env w =
+ Vhash.add env.wp env.cfg.return_point (Some w) ;
+ wp env env.cfg.entry_point
+ in
+ let do_post_exit env w =
+ let w_exit =
+ W.scope env.we xs SC_Frame_out @@
+ W.label env.we None Clabels.at_exit @@
+ List.fold_right (prove_property env) bhv.bhv_exits @@
+ if not has_exit then w else prove_assigns env bhv.bhv_exit_assigns w
+ in
+ let w_post =
+ W.scope env.we xs SC_Frame_out @@
+ W.label env.we None Clabels.post @@
+ List.fold_right (prove_property env) bhv.bhv_ensures @@
+ prove_assigns env bhv.bhv_post_assigns w
+ in
+ env.wk <- w_exit ;
+ w_post
+ in
env.we ,
(* global init *)
W.close env.we @@
I.process_global_init env.we kf @@
W.scope env.we [] SC_Global @@
+
(* pre-state *)
W.label env.we None Clabels.pre @@
- List.fold_right (use_property env) req @@
- List.fold_right (use_property env) bhv.bhv_assumes @@
- prove_if_main env bhv.bhv_requires @@
- List.fold_right (use_property env) bhv.bhv_requires @@
- List.fold_right (use_property env) (behaviors kf) @@
- List.fold_right (prove_property env) (complete mode kf) @@
- List.fold_right (prove_property env) (disjoint mode kf) @@
(* frame-in *)
W.scope env.we xs SC_Frame_in @@
- (* function body *)
- begin fun w ->
- Vhash.add env.wp env.cfg.return_point (Some w) ;
- wp env env.cfg.entry_point
- end @@
- (* frame-out *)
- W.scope env.we xs SC_Frame_out @@
- (* Post-conds*)
- W.label env.we None Clabels.post @@
- begin fun w ->
- env.wk <-
- List.fold_right (prove_property env) bhv.bhv_exits @@
- if not has_exit then w else prove_assigns env bhv.bhv_exit_assigns w ;
- List.fold_right (prove_property env) bhv.bhv_ensures @@
- prove_assigns env bhv.bhv_post_assigns w
- end @@
+ do_preconditions env @@
+ do_complete_disjoint env @@
+ do_function_body env @@
+
+ (* NOTE: do_post_exit performs frame-out on both post and exit *)
+ (* Post-conds*)
+ do_post_exit env @@
(* wp-end *)
W.empty
diff --git a/src/plugins/wp/tests/wp/exit_post_scope.i b/src/plugins/wp/tests/wp/exit_post_scope.i
new file mode 100644
index 00000000000..4cfdafaf8c5
--- /dev/null
+++ b/src/plugins/wp/tests/wp/exit_post_scope.i
@@ -0,0 +1,9 @@
+void bar(void);
+
+/*@
+ ensures \valid(&f);
+ exits \valid(&f);
+*/
+void foo(int f){
+ bar();
+}
diff --git a/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle b/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
new file mode 100644
index 00000000000..84a6cd87562
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/exit_post_scope.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/exit_post_scope.i:7: Warning:
+ Neither code nor specification for function bar, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function foo
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp/exit_post_scope.i, line 4) in 'foo':
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp/exit_post_scope.i, line 5) in 'foo':
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
new file mode 100644
index 00000000000..cd113ca71f9
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
@@ -0,0 +1,15 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/exit_post_scope.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/exit_post_scope.i:7: Warning:
+ Neither code nor specification for function bar, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_foo_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_foo_exits : Unsuccess
+[wp] Proved goals: 0 / 2
+ Alt-Ergo: 0 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ foo - - 2 0.0%
+------------------------------------------------------------
--
GitLab