From e5e0f11a2985c910ddef7d2e34f3857eacccab3e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 1 Feb 2021 09:51:21 +0100
Subject: [PATCH] [wp] fix corner cases for unreachability
---
src/plugins/wp/wpAnnot.ml | 25 +++++++++----------
src/plugins/wp/wpReached.ml | 48 ++++++++++++++++++++++++------------
src/plugins/wp/wpReached.mli | 8 +++---
3 files changed, 48 insertions(+), 33 deletions(-)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index c27e5f587c1..2a3326280b0 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -238,7 +238,7 @@ module HdefAnnotBhv = Cil2cfg.HE (struct type t = (stmt * int) end)
type strategy_info = {
kf : Kernel_function.t;
cfg : Cil2cfg.t;
- reached : WpReached.reached option ;
+ reachability : WpReached.reachability option ;
cur_bhv : asked_bhv;
asked_bhvs : asked_bhv list;
asked_prop : asked_prop;
@@ -915,7 +915,7 @@ let get_loop_annots config vloop s =
let add_stmt_deadcode_smoke config acc s =
if cur_fct_default_bhv config
then
- match config.reached with
+ match config.reachability with
| Some r when WpReached.smoking r s ->
WpStrategy.add_prop_dead_code acc config.kf s
| _ -> acc
@@ -1298,6 +1298,8 @@ let process_unreached_annots cfg =
let do_annot s _ a acc =
List.fold_left add_id acc (WpPropId.mk_code_annot_ids kf s a)
in
+ let do_stmt s acc =
+ Annotations.fold_code_annot (do_annot s) s acc in
let do_node acc n =
debug
"process annotations of unreachable node %a@."
@@ -1312,13 +1314,13 @@ let process_unreached_annots cfg =
ignore Visitor.(visitFramacKf (visitor :> frama_c_visitor) kf) ;
visitor#acc
| Cil2cfg.Vcall (s, _, call, _) ->
- Annotations.fold_code_annot (do_annot s) s acc @
+ do_stmt s acc @
preconditions_at_call s call
| Cil2cfg.Vstmt s
| Cil2cfg.VblkIn (Cil2cfg.Bstmt s, _)
| Cil2cfg.VblkOut (Cil2cfg.Bstmt s, _)
| Cil2cfg.Vtest (true, s, _) | Cil2cfg.Vloop (_, s) | Cil2cfg.Vswitch (s,_)
- -> Annotations.fold_code_annot (do_annot s) s acc
+ -> do_stmt s acc
| Cil2cfg.Vtest (false, _, _) | Cil2cfg.Vloop2 _
| Cil2cfg.VblkIn _ | Cil2cfg.VblkOut _ | Cil2cfg.Vend -> acc
in
@@ -1330,11 +1332,6 @@ let process_unreached_annots cfg =
(* Everything must go through here. *)
(*----------------------------------------------------------------------------*)
-let get_cfg kf model =
- if Wp_parameters.RTE.get () then WpRTE.generate model kf ;
- let cfg = Cil2cfg.get kf in
- let _ = process_unreached_annots cfg in cfg
-
let build_configs assigns kf model behaviors ki property =
debug "[get_strategies] for behaviors names: %a@."
(Wp_error.pp_string_list ~sep:" " ~empty:"<none>")
@@ -1348,16 +1345,18 @@ let build_configs assigns kf model behaviors ki property =
debug
"[get_strategies] select stmt %d properties@." s.sid
in
- let cfg = get_cfg kf model in
- let reached =
+ if Wp_parameters.RTE.get () then WpRTE.generate model kf ;
+ let cfg = Cil2cfg.get kf in
+ let reachability =
if Wp_parameters.SmokeTests.get ()
&& Wp_parameters.SmokeDeadcode.get ()
- then Some (WpReached.reached kf)
+ then Some (WpReached.reachability kf)
else None in
+ process_unreached_annots cfg ;
let def_annot_bhv, bhvs = find_behaviors kf cfg ki behaviors in
if bhvs <> [] then debug "[get_strategies] %d behaviors" (List.length bhvs);
let mk_bhv_config bhv = {
- kf; reached; cfg;
+ kf; reachability; cfg;
cur_bhv = bhv;
asked_prop = property;
asked_bhvs = bhvs;
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index b21fa463f9f..3ef23a0bdbf 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -41,13 +41,14 @@ type node = {
mutable flow : flow ;
mutable prev : node list ;
mutable reached : bool option ;
+ mutable alive : bool option ;
}
let kid = ref 0
let node () =
incr kid ;
- { id = !kid ; prev = [] ; reached = None ; flow = F_goto }
+ { id = !kid ; prev = [] ; alive = None ; reached = None ; flow = F_goto }
(* -------------------------------------------------------------------------- *)
(* --- Unrolled Loop --- *)
@@ -83,7 +84,7 @@ let rec is_predicate cond p =
let is_dead_annot ca =
match ca.annot_content with
| APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
- false && is_unrolled_completely spec
+ is_unrolled_completely spec
| AAssert([],p)
| AInvariant([],_,p) ->
not p.tp_only_check && is_predicate false p.tp_statement
@@ -102,8 +103,8 @@ let is_dead_code stmt =
(* --- Compute CFG --- *)
(* -------------------------------------------------------------------------- *)
-type reached = node Stmt.Map.t
-type cfg = reached ref
+type reachability = node Stmt.Map.t
+type cfg = reachability ref (* working cfg during compilation *)
let of_stmt cfg s =
try Stmt.Map.find s !cfg with Not_found ->
@@ -133,11 +134,8 @@ type env = {
let rec stmt env s b =
let a = of_stmt env.cfg s in
- if is_dead_code s then
- a.flow <- F_dead
- else
- a.flow <- skind env a b s.skind ;
- a
+ let f = skind env a b s.skind in
+ a.flow <- if is_dead_code s then F_dead else f ; a
and skind env a b = function
| Instr i -> flow i (goto a b)
@@ -182,7 +180,12 @@ let rec reached node =
| Some r -> r
| None ->
node.reached <- Some true ; (* cut loops *)
- let r = List.for_all reached_after node.prev in
+ let r =
+ match node.flow with
+ | F_dead | F_entry -> true
+ | F_goto | F_effect | F_return | F_branch | F_call ->
+ List.for_all reached_after node.prev
+ in
node.reached <- Some r ; r
and reached_after node =
@@ -191,14 +194,26 @@ and reached_after node =
| F_effect | F_entry | F_dead -> true
| F_return | F_branch | F_call -> false
+let rec alive node =
+ match node.alive with
+ | Some a -> a
+ | None ->
+ match node.flow with
+ | F_dead -> false
+ | F_entry -> true
+ | _ ->
+ node.alive <- Some false ;
+ let a = List.exists alive node.prev in
+ node.alive <- Some a ; a
+
let smoking_node n =
match n.flow with
- | F_effect | F_call | F_return -> not (reached n)
+ | F_effect | F_call | F_return -> alive n && not (reached n)
| F_goto | F_branch | F_entry | F_dead -> false
(* returns true if the stmt requires a reachability smoke test *)
-let smoking nodes stmt =
- try Stmt.Map.find stmt nodes |> smoking_node
+let smoking reachability stmt =
+ try Stmt.Map.find stmt reachability |> smoking_node
with Not_found -> false
let compute kf =
@@ -262,7 +277,8 @@ let dump ~dir kf reached =
| UnspecifiedSequence _ -> Printf.sprintf "Seq. s%d" s.sid
| Throw _ | TryExcept _ | TryCatch _ | TryFinally _ ->
Printf.sprintf "Exn. s%d" s.sid
- in G.node dot (N.get n) [`Box;`Label label])
+ in G.node dot (N.get n)
+ [`Box;`Label (Printf.sprintf "s%d n%d: %s" s.sid n.id label)])
reached ;
G.run dot ;
G.close dot ;
@@ -276,7 +292,7 @@ let dump ~dir kf reached =
module FRmap = Kernel_function.Make_Table
(Datatype.Make
(struct
- type t = reached
+ type t = reachability
include Datatype.Serializable_undefined
let reprs = [Stmt.Map.empty]
let name = "WpReachable.reached"
@@ -289,7 +305,7 @@ module FRmap = Kernel_function.Make_Table
let dkey = Wp_parameters.register_category "reached"
-let reached = FRmap.memo
+let reachability = FRmap.memo
begin fun kf ->
let r = compute kf in
(if Wp_parameters.has_dkey dkey then
diff --git a/src/plugins/wp/wpReached.mli b/src/plugins/wp/wpReached.mli
index 2f7bc0283bc..0c9c6f46ee4 100644
--- a/src/plugins/wp/wpReached.mli
+++ b/src/plugins/wp/wpReached.mli
@@ -26,7 +26,7 @@
open Cil_types
-type reached
+type reachability
(** control flow graph dedicated to smoke tests *)
val is_predicate : bool -> predicate -> bool
@@ -39,14 +39,14 @@ val is_dead_annot : code_annotation -> bool
val is_dead_code : stmt -> bool
(** Checks whether the stmt has a dead-code annotation. *)
-val reached : Kernel_function.t -> reached
+val reachability : Kernel_function.t -> reachability
(** memoized reached cfg for function *)
-val smoking : reached -> Cil_types.stmt -> bool
+val smoking : reachability -> Cil_types.stmt -> bool
(** Returns whether a stmt need a smoke tests to avoid being unreachable.
This is restricted to assignments, returns and calls not dominated
another smoking statement. *)
-val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> reached -> unit
+val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> reachability -> unit
(* -------------------------------------------------------------------------- *)
--
GitLab