Merge branch 'feature/wp/extend-assumes-smoke' into 'master'

Do not miss assumes in smoke tests

See merge request frama-c/frama-c!3215

src/plugins/wp/cfgAnnot.ml

@@ -116,11 +116,20 @@ let get_behavior_goals kf ?(smoking=false) ?(exits=false) bhv =
   let post_cond = normalize_post ~goal:true kf bhv in
   let p_asgn, e_asgn = normalize_fct_assigns kf ~exits bhv bhv.b_assigns in
   let smokes =
-    if smoking && bhv.b_requires <> [] then
+    let do_assumes =
+      Wp_parameters.SmokeDeadassumes.get() && bhv.b_assumes <> [] in
+    if smoking && (bhv.b_requires <> [] || do_assumes) 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
+      let id, doomed =
+        if bhv.b_requires <> []
+        then
+          bname ^ "_requires",
+          Property.ip_requires_of_behavior kf Kglobal bhv
+        else
+          bname ^ "_assumes",
+          Property.ip_assumes_of_behavior kf Kglobal bhv
+      in
       [smoke kf ~id ~doomed ()]
     else []
   in

src/plugins/wp/tests/wp_plugin/doomed_pre.i

+/* run.config
+   OPT: -wp-smoke-tests
+*/
+
+/* run.config_qualif
+   OPT: -wp-smoke-tests
+*/
+
+//@ requires a < 0 && a > 0 ;
+void requires(int a){}
+
+/*@ requires a < 0 ;
+    behavior B:
+      assumes a > 0 ;
+*/
+void reqs_assumes(int a){}
+
+/*@ requires a < 0 ;
+    behavior B:
+      assumes a > 0 ;
+      assumes a > 1 ;
+*/
+void reqs_2_2_assumes(int a){}
+
+/*@ requires a < 0 ;
+    behavior B:
+      assumes a > 0 ;
+      assumes a < -42 ;
+*/
+void reqs_1_2_assumes(int a){}
+
+/*@ requires a >= 0 ;
+    behavior B:
+      assumes a > 10 ;
+      assumes a < 10 ;
+*/
+void reqs_combined_assumes(int a){}
+
+/*@ behavior B:
+      assumes a < 0 && a > 0 ; // not detected
+*/
+void only_assumes(int a){}
+
+/*@ behavior B:
+      assumes  a > 0 ;
+      requires a < 0 ;
+*/
+void bhv_requires_assumes(int a){}
+
+/*@ requires a < 0 ;
+    behavior B1:
+      assumes a > 0 ;
+    behavior B2:
+      assumes a > 1 ;
+*/
+void reqs_massumes(int a){}

src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/doomed_pre.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function bhv_requires_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_requires in 'bhv_requires_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_1_2_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_1_2_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_1_2_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_1_2_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_2_2_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_2_2_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_2_2_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_2_2_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_combined_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_combined_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: 0 <= a. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_combined_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_combined_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_massumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_massumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_massumes with behavior B1
+------------------------------------------------------------
+
+Goal Wp_smoke_B1_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_massumes with behavior B2
+------------------------------------------------------------
+
+Goal Wp_smoke_B2_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function requires
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'requires':
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/doomed_pre.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 13 goals scheduled
+[wp] [Failed] Smoke-test typed_requires_wp_smoke_default_requires
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:10: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:16: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:23: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:30: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_combined_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_combined_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:37: Warning: Failed smoke-test
+[wp] [Failed] Smoke-test typed_bhv_requires_assumes_wp_smoke_B_requires
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:48: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_massumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B1_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B2_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] Proved goals:    5 / 13
+  Qed:             0  (failed: 8)
+  Alt-Ergo:        5
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  requires                  -        -        1       0.0%
+  reqs_assumes              -        1        2      50.0%
+  reqs_2_2_assumes          -        1        2      50.0%
+  reqs_1_2_assumes          -        1        2      50.0%
+  reqs_combined_assumes     -        1        2      50.0%
+  bhv_requires_assumes      -        -        1       0.0%
+  reqs_massumes             -        1        3      33.3%
+------------------------------------------------------------

src/plugins/wp/wpReached.ml

@@ -318,8 +318,45 @@ let reachability = FRmap.memo
 (* --- Doome Status                                                       --- *)
 (* -------------------------------------------------------------------------- *)
 
+module Invalid_behaviors = struct
+  module String_set = Datatype.String.Set
+
+  include State_builder.Hashtbl(Kernel_function.Hashtbl)(String_set)
+      (struct
+        let name = "Wp.WpReached.Invalid_behavior"
+        let dependencies = [Ast.self]
+        let size = 32
+      end)
+
+  let add kf bhv =
+    let set =
+      try find kf
+      with Not_found -> String_set.empty
+    in
+    add kf (String_set.add bhv.b_name set)
+
+  let mem kf bhv =
+    try String_set.mem bhv.b_name (find kf)
+    with Not_found -> false
+end
+
 let set_invalid emitter tgt =
-  Property_status.emit emitter ~hyps:[] tgt Property_status.False_if_reachable
+  let open Property_status in
+  match tgt with
+  (* For invalid assumes, introduce "ensures false" in behavior on need *)
+  | Property.IPPredicate { ip_kind = PKAssumes(bhv) ; ip_kf ; ip_pred } ->
+      if not (Invalid_behaviors.mem ip_kf bhv) then begin
+        Invalid_behaviors.add ip_kf bhv ;
+        let pred_name = [ "Wp" ; "SmokeTest" ] in
+        let pred_loc = ip_pred.ip_content.tp_statement.pred_loc in
+        let p = { Logic_const.pfalse with pred_loc ; pred_name } in
+        let p = Logic_const.(new_predicate p) in
+        let pid = Property.ip_of_ensures ip_kf Kglobal bhv (Normal, p) in
+        Annotations.add_ensures emitter ip_kf ~behavior:bhv.b_name [Normal, p];
+        emit emitter ~hyps:[] pid False_if_reachable
+      end
+  | p ->
+      emit emitter ~hyps:[] p False_if_reachable
 
 let set_doomed emitter pid =
   List.iter (set_invalid emitter) (WpPropId.doomed_if_valid pid) ;

src/plugins/wp/wp_parameters.ml

@@ -400,6 +400,13 @@ module SmokeTests =
     let help = "Smoke-tests : look for inconsistent contracts (best effort)"
   end)
 
+let () = Parameter_customize.set_group wp_strategy
+module SmokeDeadassumes =
+  True(struct
+    let option_name = "-wp-smoke-dead-assumes"
+    let help = "When generating smoke tests, look for dead assumes"
+  end)
+
 let () = Parameter_customize.set_group wp_strategy
 module SmokeDeadcode =
   True(struct

src/plugins/wp/wp_parameters.mli

@@ -153,6 +153,7 @@ module ReportName: Parameter_sig.String
 module MemoryContext: Parameter_sig.Bool
 module CheckMemoryContext: Parameter_sig.Bool
 module SmokeTests: Parameter_sig.Bool
+module SmokeDeadassumes: Parameter_sig.Bool
 module SmokeDeadloop: Parameter_sig.Bool
 module SmokeDeadcode: Parameter_sig.Bool
 module SmokeDeadcall: Parameter_sig.Bool