[wp] smoke requires

src/plugins/wp/cfgAnnot.ml

@@ -22,6 +22,13 @@
 
 open Cil_types
 
+(* -------------------------------------------------------------------------- *)
+(* --- Smoke Tests                                                        --- *)
+(* -------------------------------------------------------------------------- *)
+
+let smoke kf ~id ?doomed ?unreachable () =
+  WpPropId.mk_smoke kf ~id ?doomed ?unreachable () , Logic_const.pfalse
+
 (* -------------------------------------------------------------------------- *)
 (* --- Memoization                                                        --- *)
 (* -------------------------------------------------------------------------- *)
@@ -40,6 +47,7 @@ end
 type behavior = {
   bhv_assumes: WpPropId.pred_info list ;
   bhv_requires: WpPropId.pred_info list ;
+  bhv_smokes: WpPropId.pred_info list ;
   bhv_ensures: WpPropId.pred_info list ;
   bhv_exits: WpPropId.pred_info list ;
   bhv_post_assigns: WpPropId.assigns_full_info ;
@@ -110,16 +118,27 @@ let normalize_assigns kf ki has_exit bhv ~active = function
 let get_requires kf ki bhv =
   List.map (normalize_pre kf ki bhv) bhv.b_requires
 
-let get_behavior kf ki ~exits ~active bhv =
+let get_behavior kf
+    ?(ki=Kglobal) ?(smoking=false) ?(exits=false) ?(active=[]) bhv =
   let pre_cond = normalize_pre kf ki bhv in
   let post_cond tk (kind,ip) =
     if kind = tk then Some (normalize_post kf ki bhv tk ip) else None in
   let p_asgn, e_asgn =
-    normalize_assigns kf ki exits bhv ~active bhv.b_assigns
+    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 ()]
+    else []
   in
   {
     bhv_assumes = List.map pre_cond bhv.b_assumes;
     bhv_requires = List.map pre_cond bhv.b_requires;
+    bhv_smokes = smokes;
     bhv_ensures = List.filter_map (post_cond Normal) bhv.b_post_cond ;
     bhv_exits = List.filter_map (post_cond Exits) bhv.b_post_cond ;
     bhv_post_assigns = p_asgn ;

src/plugins/wp/cfgAnnot.mli

@@ -35,6 +35,7 @@ open WpPropId
 type behavior = {
   bhv_assumes: pred_info list ;
   bhv_requires: pred_info list ;
+  bhv_smokes: pred_info list ;
   bhv_ensures: pred_info list ;
   bhv_exits: pred_info list ;
   bhv_post_assigns: assigns_full_info ;
@@ -42,11 +43,13 @@ type behavior = {
 }
 
 val get_requires : kernel_function -> kinstr -> funbehavior -> pred_info list
+
 val get_behavior :
-  kernel_function -> kinstr -> exits:bool -> active:string list ->
+  kernel_function ->
+  ?ki:kinstr -> ?smoking:bool -> ?exits:bool -> ?active:string list ->
   funbehavior -> behavior
 
-val get_preconditions : goal:bool ->kernel_function -> pred_info list
+val get_preconditions : goal:bool -> kernel_function -> pred_info list
 val get_complete_behaviors : kernel_function -> pred_info list
 val get_disjoint_behaviors : kernel_function -> pred_info list
 

src/plugins/wp/cfgCalculus.ml

@@ -321,26 +321,24 @@ struct
     I.process_global_init env.we env.mode.kf @@
     W.scope env.we [] SC_Global w
 
-  let do_preconditions env ~formals bhvs w =
+  let do_preconditions env ~formals (b : CfgAnnot.behavior) w =
     let kf = env.mode.kf in
     let init = WpStrategy.is_main_init kf in
-    let behaviors =
+    let side_behaviors =
       if init || WpLog.PrecondWeakening.get () then []
       else CfgAnnot.get_preconditions ~goal:false kf in
-    let defaults = default_requires env.mode kf in
-    let requires = bhvs.CfgAnnot.bhv_requires in
-    let initreqs = if init then requires else [] in
-    let assumes = bhvs.CfgAnnot.bhv_assumes in
+    let requires_init = if init then b.bhv_requires else [] in
     (* pre-state *)
     W.label env.we None Clabels.pre @@
     (* frame-in *)
     W.scope env.we formals SC_Frame_in @@
     (* pre-conditions *)
-    List.fold_right (use_property env) defaults @@
-    List.fold_right (use_property env) assumes @@
-    List.fold_right (prove_property env) initreqs @@
-    List.fold_right (use_property env) requires @@
-    List.fold_right (use_property env) behaviors w
+    List.fold_right (use_property env) (default_requires env.mode kf) @@
+    List.fold_right (use_property env) b.bhv_assumes @@
+    List.fold_right (prove_property env) requires_init @@
+    List.fold_right (use_property env) b.bhv_requires @@
+    List.fold_right (prove_property env) b.bhv_smokes @@
+    List.fold_right (use_property env) side_behaviors w
 
   let do_post env ~formals (b : CfgAnnot.behavior) w =
     W.scope env.we formals SC_Frame_out @@
@@ -380,7 +378,8 @@ struct
     } in
     let formals = Kf.get_formals kf in
     let exits = not @@ Kf.Set.is_empty @@ CfgInfos.calls infos in
-    let bhv = CfgAnnot.get_behavior kf Kglobal ~exits ~active:[] mode.bhv in
+    let smoking = WpLog.SmokeTests.get () in
+    let bhv = CfgAnnot.get_behavior kf ~smoking ~exits mode.bhv in
     begin
       W.close env.we @@
       do_global_init env @@