From 16c650851439d48b362a4e9cb249b766bce09173 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 23 Mar 2020 17:06:07 +0100
Subject: [PATCH] [wp] fix open/close blocks
---
src/plugins/wp/calculus.ml | 9 ++--
src/plugins/wp/cil2cfg.ml | 54 +++++++++----------
src/plugins/wp/cil2cfg.mli | 4 +-
.../tests/wp_bts/oracle/issue_837.res.oracle | 3 +-
.../wp_bts/oracle_qualif/issue_837.res.oracle | 9 ++--
5 files changed, 38 insertions(+), 41 deletions(-)
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 1ff49f9195b..01e99eacd7f 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -605,11 +605,10 @@ module Cfg (W : Mcfg.S) = struct
wp_scope wenv formals Mcfg.SC_Function_after_POST obj
*)
in
- let res =
- let blks = Cil2cfg.blocks_closed_by_edge cfg e in
- let free_locals res b = wp_scope wenv b.blocals Mcfg.SC_Block_out res in
- List.fold_left free_locals res blks
- in
+ let Cil2cfg.{ b_closed ; b_opened } = Cil2cfg.block_scope_for_edge cfg e in
+ let do_block sc res b = wp_scope wenv b.blocals sc res in
+ let res = List.fold_left (do_block Mcfg.SC_Block_in) res b_opened in
+ let res = List.fold_left (do_block Mcfg.SC_Block_out) res b_closed in
debug "[compute_edge] before %a done@." Cil2cfg.pp_node v;
Cil.CurrentLoc.set old_loc;
res
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index b995b8212a4..8a8402eb871 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -626,36 +626,34 @@ let get_post_label cfg v =
| None -> None
| Some s -> Some (Clabels.stmt s)
-let blocks_closed_by_edge cfg e =
+type block_scope = { b_opened : block list ; b_closed : block list }
+
+let no_scope = { b_opened = [] ; b_closed = [] }
+
+let block_scope s s' =
+ try
+ {
+ b_opened = Kernel_function.blocks_opened_by_edge s s' ;
+ b_closed = Kernel_function.blocks_closed_by_edge s s' ;
+ }
+ with Not_found | Invalid_argument _ ->
+ debug "[blocks_closed_by_edge] not found sid:%d -> sid:%d@." s.sid s'.sid;
+ no_scope
+
+let block_scope_for_edge cfg e =
debug "[blocks_closed_by_edge] for %a...@." pp_edge e;
let v_before = edge_src e in
- let blocks = match node_type v_before with
- | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_) ->
- ignore (Ast.get ()); (* Since CIL Cfg computation is required and
- Ast.get () have to do this well. *)
- begin match s.succs with
- | [s'] -> (try Kernel_function.blocks_closed_by_edge s s'
- with Not_found as e -> debug "[blocks_closed_by_edge] not found sid:%d -> sid:%d@."
- s.sid s'.sid;
- raise e)
- | [] | _ :: _ ->
- let s' = get_edge_next_stmt cfg e in
- match s' with
- | None -> []
- | Some s' ->
- debug
- "[blocks_closed_by_edge] found sid:%d -> sid:%d@."
- s.sid s'.sid;
- try Kernel_function.blocks_closed_by_edge s s'
- with Invalid_argument _ -> []
- end
- | _ -> (* TODO ? *) []
- in
- let v_after = edge_dst e in
- let blocks = match node_type v_after with
- | VblkOut (Bfct, b) -> b::blocks
- | _ -> blocks
- in blocks
+ match node_type v_before with
+ | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_) ->
+ begin match s.succs with
+ | [s'] -> block_scope s s'
+ | [] | _ :: _ ->
+ let s' = get_edge_next_stmt cfg e in
+ match s' with
+ | None -> no_scope
+ | Some s' -> block_scope s s'
+ end
+ | _ -> (* TODO ? *) no_scope
let has_exit cfg =
try
diff --git a/src/plugins/wp/cil2cfg.mli b/src/plugins/wp/cil2cfg.mli
index f0c16fe47c0..5df3e524af0 100644
--- a/src/plugins/wp/cil2cfg.mli
+++ b/src/plugins/wp/cil2cfg.mli
@@ -107,7 +107,9 @@ val get_switch_edges : t -> node -> (exp list * edge) list * edge
but gives the edge to VcallOut first and the edge to Vexit second. *)
val get_call_out_edges : t -> node -> edge * edge
-val blocks_closed_by_edge : t -> edge -> block list
+type block_scope = { b_opened : block list ; b_closed : block list }
+
+val block_scope_for_edge : t -> edge -> block_scope
val is_back_edge : edge -> bool
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
index 2c7f2a6b78d..d1e95f07802 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
@@ -60,7 +60,6 @@ Prove: true.
Goal Assigns nothing in 'foo' (4/4):
Effect at line 6
-Assume { Type: is_sint32(a). (* Residual *) When: a != 0. }
-Prove: (ta_tmp_0=false).
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
index a619021a1b9..1e55e4e4da4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
@@ -12,12 +12,11 @@
[wp] [Qed] Goal typed_foo_assigns_part1 : Valid
[wp] [Qed] Goal typed_foo_assigns_part2 : Valid
[wp] [Qed] Goal typed_foo_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assigns_part4 : Unsuccess
-[wp] Proved goals: 8 / 9
- Qed: 8
- Alt-Ergo: 0 (unsuccess: 1)
+[wp] [Qed] Goal typed_foo_assigns_part4 : Valid
+[wp] Proved goals: 9 / 9
+ Qed: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- foo 3 - 4 75.0%
+ foo 4 - 4 100%
bar 5 - 5 100%
------------------------------------------------------------
--
GitLab