[wp] fix corner cases for unreachability

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;

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

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
 
 (* -------------------------------------------------------------------------- *)