[wp] (some) smoke fixes

src/plugins/wp/cfgAnnot.ml

@@ -126,13 +126,12 @@ let get_behavior kf
   let p_asgn, e_asgn =
     normalize_assigns kf ki exits bhv ~active bhv.b_assigns in
   let smokes =
-    if smoking then
-      if bhv.b_assumes = [] && bhv.b_requires = [] then [] else
-        let bname =
-          if Cil.is_default_behavior bhv then "default" else bhv.b_name in
-        let id = bname ^ "_requires" in
-        let doomed = Property.ip_requires_of_behavior kf Kglobal bhv in
-        [smoke kf ~id ~doomed ()]
+    if smoking && bhv.b_requires <> [] then
+      let bname =
+        if Cil.is_default_behavior bhv then "default" else bhv.b_name in
+      let id = bname ^ "_requires" in
+      let doomed = Property.ip_requires_of_behavior kf Kglobal bhv in
+      [smoke kf ~id ~doomed ()]
     else []
   in
   {
@@ -320,7 +319,7 @@ let get_code_assertions ?smoking kf stmt =
   | None -> ca
   | Some r ->
       if WpReached.smoking r stmt then
-        let s = smoke kf ~id:"deadcode" ~unreachable:stmt () in
+        let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
         { ca with code_verified = s :: ca.code_verified }
       else ca
 
@@ -333,6 +332,8 @@ type loop_contract = {
   loop_established: WpPropId.pred_info list;
   (* to be assumed for loop current *)
   loop_invariants: WpPropId.pred_info list;
+  (* to be proved after loop invariants *)
+  loop_smoke: WpPropId.pred_info list;
   (* to be verified after loop body *)
   loop_preserved: WpPropId.pred_info list;
   (* assigned by loop body *)
@@ -344,6 +345,7 @@ let reverse_loop_contract l = {
   loop_invariants = List.rev l.loop_invariants ;
   loop_preserved = List.rev l.loop_preserved ;
   loop_assigns = List.rev l.loop_assigns ;
+  loop_smoke = List.rev l.loop_smoke ;
 }
 
 let default_assigns stmt l =
@@ -403,11 +405,17 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
           loop_established = [] ;
           loop_invariants = [] ;
           loop_preserved = [] ;
+          loop_smoke = [] ;
           loop_assigns = [] ;
         }
     end)
 
-let get_loop_contract kf stmt = LoopContract.get (kf,stmt)
+let get_loop_contract ?(smoking=false) kf stmt =
+  let lc = LoopContract.get (kf,stmt) in
+  if smoking && not (WpReached.is_dead_code stmt) then
+    let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
+    { lc with loop_smoke = g :: lc.loop_smoke }
+  else lc
 
 (* -------------------------------------------------------------------------- *)
 (* --- Clear Tablesnts                                                    --- *)

src/plugins/wp/cfgAnnot.mli

@@ -72,16 +72,19 @@ val get_code_assertions :
 
 type loop_contract = {
   (** to be verified at loop entry *)
-  loop_established: pred_info list;
+  loop_established: WpPropId.pred_info list;
   (** to be assumed for loop current *)
-  loop_invariants: pred_info list;
+  loop_invariants: WpPropId.pred_info list;
+  (** to be proved after loop invariants *)
+  loop_smoke: WpPropId.pred_info list;
   (** to be verified after loop body *)
-  loop_preserved: pred_info list;
+  loop_preserved: WpPropId.pred_info list;
   (** assigned by loop body *)
-  loop_assigns: assigns_full_info list;
+  loop_assigns: WpPropId.assigns_full_info list;
 }
 
-val get_loop_contract : kernel_function -> stmt -> loop_contract
+val get_loop_contract : ?smoking:bool ->
+  kernel_function -> stmt -> loop_contract
 
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Call Contracts                                --- *)

src/plugins/wp/cfgCalculus.ml

@@ -98,10 +98,11 @@ let is_active_mode ~mode ~goal (p: Property.t) =
   | IPDecrease { id_ca = None } -> is_default_bhv mode
   | IPDecrease { id_ca = Some ca } -> is_selected_ca mode ~goal ca
   | IPComplete _ | IPDisjoint _ -> is_default_bhv mode
+  | IPOther _ -> true
   | IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _ ->
       (*TODO: is it in pass or not ? *) assert false
   | IPAxiomatic _ | IPAxiom _ | IPLemma _
-  | IPOther _ | IPExtended _ | IPBehavior _
+  | IPExtended _ | IPBehavior _
   | IPReachable _ | IPPropertyInstance _
     -> assert false (* n/a *)
 
@@ -220,7 +221,13 @@ struct
         W.switch env.we s value
           (List.map (fun (e,v) -> [e], wp env v) cases)
           (wp env default)
-    | Loop _ -> loop env a s (CfgAnnot.get_loop_contract env.mode.kf s)
+    | Loop _ ->
+        let m = env.mode in
+        let smoking =
+          is_default_bhv m &&
+          WpLog.SmokeTests.get () &&
+          WpLog.SmokeDeadloop.get () in
+        loop env a s (CfgAnnot.get_loop_contract ~smoking m.kf s)
     | Edges -> successors env a
 
   (* Compute loops *)
@@ -233,6 +240,7 @@ struct
       List.fold_right (use_assigns env) lc.loop_assigns @@
       W.label env.we None loop_current @@
       List.fold_right (use_property env) lc.loop_invariants @@
+      List.fold_right (prove_property env) lc.loop_smoke @@
       let q =
         List.fold_right (prove_property env) lc.loop_preserved @@
         List.fold_right (prove_assigns env) lc.loop_assigns @@
@@ -382,7 +390,7 @@ struct
       if body <> None &&
          is_default_bhv mode &&
          WpLog.SmokeTests.get () &&
-         WpLog.SmokeDeadcall.get ()
+         WpLog.SmokeDeadcode.get ()
       then Some (WpReached.reachability kf) else None in
     let env = {
       mode ; props ; body ; succ ; dead ;

src/plugins/wp/cfgInfos.ml

@@ -113,11 +113,12 @@ let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
   begin
     (selected_assigns ~prop b.b_assigns) ||
     (selected_allocates ~prop b.b_allocation) ||
+    (Wp_parameters.SmokeTests.get () && b.b_requires <> []) ||
     (List.exists (selected_postcond ~prop) b.b_post_cond)
   end
 
 let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
-  (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop) b
+  (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop b)
 
 (* -------------------------------------------------------------------------- *)
 (* --- Calls                                                              --- *)
@@ -225,10 +226,12 @@ let compile Key.{ kf ; bhv ; prop } =
            let ca = CfgAnnot.get_code_assertions kf stmt in
            let ca_pids = List.map fst ca.code_verified in
            let loop_pids = loop_contract_pids kf stmt in
-           if dead then begin
-             infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
-             infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
-           end else
+           if dead then
+             begin
+               infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
+               infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
+             end
+           else
              begin
                if not infos.annots &&
                   ( List.exists (selected ~bhv ~prop) ca_pids ||
@@ -239,6 +242,8 @@ let compile Key.{ kf ; bhv ; prop } =
              end
         ) cfg.stmt_table ;
     end body ;
+  (* Doomed *)
+  Bag.iter WpAnnot.set_unreachable infos.doomed ;
   (* Collected Infos *)
   infos
 

src/plugins/wp/wpAnnot.mli

@@ -34,6 +34,7 @@ open Cil_types
 
 val unreachable_proved : int ref
 val unreachable_failed : int ref
+val set_unreachable : WpPropId.prop_id -> unit
 
 type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns