[wp] smoke tests

src/plugins/wp/Changelog

@@ -28,6 +28,7 @@
 - WP	      [2019/17/04] Control splitting with -wp-max-split <n>
 - WP          [2019/12/04] Added option -wp-run-all-provers
 - WP          [2019/01/29] Emit a warning when no goal is generated
+- Wp          [2019/06/04] Checks for inconsistent requires (-wp-smoke-tests)
 - TIP         [2018/04/03] Create session directory only on demand
 - TIP         [2018/03/19] Specification of JSON script format
 - Wp          [2018/03/18] Additional lemma about remainder (mod)

src/plugins/wp/GuiGoal.ml

@@ -449,6 +449,13 @@ class pane (gprovers : GuiConfig.provers) =
                 cancel#set_enabled false ;
                 forward#set_enabled false ;
                 status#set_text "Non Proved Property" ;
+            | `Invalid ->
+                icon#set_icon GuiProver.wg_status ;
+                next#set_enabled false ;
+                prev#set_enabled false ;
+                cancel#set_enabled false ;
+                forward#set_enabled false ;
+                status#set_text "Invalid Smoke-test" ;
             | `Proved ->
                 icon#set_icon GuiProver.ok_status ;
                 next#set_enabled false ;

src/plugins/wp/GuiList.ml

@@ -70,7 +70,9 @@ let render_prover_result p =
           | `Proof -> icn_stock "gtk-edit"
           | `Saved -> icn_stock "gtk-file"
         end
-    | { verdict=r } , _ -> icon_of_verdict r
+    | result , _ ->
+        let smoke = Wpo.is_smoke_test w in
+        icon_of_verdict (VCS.verdict ~smoke result)
 
 class pane (gprovers:GuiConfig.provers) =
   let model = new model in

src/plugins/wp/GuiNavigator.ml

@@ -34,7 +34,7 @@ open GuiSource
 (* -------------------------------------------------------------------------- *)
 
 type scope = [ `All | `Module | `Select ]
-type filter = [ `ToProve | `Scripts | `All ]
+type filter = [ `ToProve | `Scripts | `Smoke | `All ]
 type card = [ `List | `Goal ]
 type focus =
   [ `All
@@ -105,7 +105,9 @@ class behavior
           ~values:[`All,"all" ; `Module,"module" ; `Select,"select"]
           ~default:`Module scope ;
         Cfg.config_values ~key:"wp.navigator.filter"
-          ~values:[`All,"all" ; `Scripts,"scripts" ;
+          ~values:[`All,"all" ;
+                   `Smoke,"smoketests" ;
+                   `Scripts,"scripts" ;
                    `ToProve,"toprove"]
           ~default:`ToProve filter ;
         filter#on_event self#reload ;
@@ -124,7 +126,9 @@ class behavior
     method reload () =
       begin
         list#reload ;
-        let to_prove g = not (Wpo.is_proved g || Wpo.reduce g) in
+        let to_prove g =
+          not (Wpo.is_smoke_test g) &&
+          not (Wpo.is_proved g || Wpo.reduce g) in
         let has_proof g =
           match ProofEngine.get g with
           | `None -> false
@@ -133,6 +137,7 @@ class behavior
           let ok =
             match filter#get with
             | `All -> true
+            | `Smoke -> Wpo.is_smoke_test g
             | `Scripts -> has_proof g
             | `ToProve -> to_prove g && (Wpo.is_unknown g || has_proof g)
           in if ok then list#add g
@@ -444,6 +449,7 @@ let make (main : main_window_extension_points) =
     let filter = new Widget.menu ~default:`ToProve ~options:[
       `ToProve , "Not Proved (yet)" ;
       `Scripts , "All Scripts" ;
+      `Smoke , "Smoke Tests" ;
       `All , "All Goals" ;
     ] () in
     let prev = new Widget.button ~icon:`GO_BACK ~tooltip:"Previous goal" () in
@@ -466,18 +472,6 @@ let make (main : main_window_extension_points) =
       pvrs#connect dp_chooser#run ;
     end ;
 
-    (* -------------------------------------------------------------------------- *)
-    (* --- Filter Popup                                                       --- *)
-    (* -------------------------------------------------------------------------- *)
-
-    begin
-      filter#set_render (function
-          | `All -> "All Results"
-          | `Scripts -> "All Scripts"
-          | `ToProve -> "Not Proved") ;
-      filter#set_items [ `ToProve ; `Scripts ; `All ] ;
-    end ;
-
     (* -------------------------------------------------------------------------- *)
     (* --- List/Goal view                                                     --- *)
     (* -------------------------------------------------------------------------- *)

src/plugins/wp/GuiProver.ml

@@ -23,7 +23,7 @@
 let no_status = `Share "theme/default/never_tried.png"
 let ok_status = `Share "theme/default/surely_valid.png"
 let ko_status = `Share "theme/default/unknown.png"
-let wg_status = `Share "theme/default/invalid.png"
+let wg_status = `Share "theme/default/surely_invalid.png"
 
 let filter = function
   | VCS.Qed | VCS.Tactical | VCS.NativeCoq -> false

src/plugins/wp/ProofEngine.ml

@@ -205,12 +205,14 @@ let children n =
 (* --- State & Status                                                     --- *)
 (* -------------------------------------------------------------------------- *)
 
-type status = [ `Main | `Proved | `Pending of int ]
+type status = [ `Main | `Proved | `Invalid | `Pending of int ]
 
 let status t : status =
   match t.root with
   | None ->
-      if Wpo.is_proved t.main then `Proved else `Main
+      if Wpo.is_proved t.main
+      then if Wpo.is_smoke_test t.main then `Invalid else `Proved
+      else `Main
   | Some root ->
       match root.script with
       | Opened | Script _ -> `Main

src/plugins/wp/ProofEngine.mli

@@ -35,7 +35,7 @@ val validate : ?incomplete:bool -> tree -> unit
 
 (** Leaves are numbered from 0 to n-1 *)
 
-type status = [ `Main | `Proved | `Pending of int ]
+type status = [ `Main | `Invalid | `Proved | `Pending of int ]
 type current = [ `Main | `Internal of node | `Leaf of int * node ]
 type position = [ `Main | `Node of node | `Leaf of int ]
 

src/plugins/wp/ProverErgo.ml

@@ -341,8 +341,6 @@ let re_unsat = Str.regexp p_unsat
 class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
   object(ergo)
 
-    initializer ignore pid
-
     inherit ProverTask.command (Wp_parameters.AltErgo.get ())
 
     val mutable files = []
@@ -437,7 +435,8 @@ class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
       if not gui then begin
         ergo#add_positive
           ~name:"-steps-bound" ~value:(VCS.get_stepout config) ;
-        ergo#timeout (VCS.get_timeout config) ;
+        let smoke = WpPropId.is_smoke_test pid in
+        ergo#timeout (VCS.get_timeout ~smoke config) ;
       end ;
       ergo#validate_time ergo#time ;
       ergo#validate_pattern ~logs:`ERR re_error ergo#error ;

src/plugins/wp/ProverScript.ml

@@ -167,7 +167,7 @@ struct
 
   let pending env =
     match ProofEngine.status env.tree with
-    | `Main | `Proved -> 0 | `Pending n -> n
+    | `Main | `Invalid | `Proved -> 0 | `Pending n -> n
 
   let setup_backtrack env node depth =
     if env.backtrack > 0 then

src/plugins/wp/ProverTask.ml

@@ -133,8 +133,11 @@ let location file line = {
   Lexing.pos_cnum = 0 ;
 }
 
-let timeout = function
-  | None -> Wp_parameters.Timeout.get ()
+let timeout ~smoke = function
+  | None ->
+      if smoke
+      then Wp_parameters.SmokeTimeout.get ()
+      else Wp_parameters.Timeout.get ()
   | Some t -> t
 
 let stepout = function

src/plugins/wp/ProverTask.mli

@@ -54,7 +54,7 @@ val p_until_space : string (** No space group pattern "\\([^ \t\n]*\\)" *)
 
 val location : string -> int -> Lexing.position
 
-val timeout : int option -> int
+val timeout : smoke:bool -> int option -> int
 val stepout : int option -> int
 type logs = [ `OUT | `ERR | `BOTH ]
 

src/plugins/wp/VCS.ml

@@ -170,8 +170,11 @@ let current () = {
 
 let default = { valid = false ; timeout = None ; stepout = None }
 
-let get_timeout = function
-  | { timeout = None } -> Wp_parameters.Timeout.get ()
+let get_timeout ~smoke = function
+  | { timeout = None } ->
+      if smoke
+      then Wp_parameters.SmokeTimeout.get ()
+      else Wp_parameters.Timeout.get ()
   | { timeout = Some t } -> t
 
 let get_stepout = function
@@ -210,6 +213,16 @@ let is_verdict r = match r.verdict with
 let is_valid = function { verdict = Valid } -> true | _ -> false
 let is_computing = function { verdict=Computing _ } -> true | _ -> false
 
+let verdict ~smoke r =
+  if smoke then
+    match r.verdict with
+    | (Failed | NoResult | Checked | Computing _) as r -> r
+    | Valid -> Invalid
+    | Invalid | Unknown | Timeout | Stepout -> Valid
+  else r.verdict
+
+let is_proved ~smoke r = (verdict ~smoke r = Valid)
+
 let configure r =
   let valid = (r.verdict = Valid) in
   let timeout =

src/plugins/wp/VCS.mli

@@ -68,7 +68,7 @@ type config = {
 val current : unit -> config (** Current parameters *)
 val default : config (** all None *)
 
-val get_timeout : config -> int (** 0 means no-timeout *)
+val get_timeout : smoke:bool -> config -> int (** 0 means no-timeout *)
 val get_stepout : config -> int (** 0 means no-stepout *)
 
 (** {2 Results} *)
@@ -112,6 +112,10 @@ val is_auto : prover -> bool
 val is_verdict : result -> bool
 val is_valid: result -> bool
 val is_computing: result -> bool
+val is_proved: smoke:bool -> result -> bool
+
+val verdict: smoke:bool -> result -> verdict
+
 val configure : result -> config
 val autofit : result -> bool (** Result that fits the default configuration *)
 

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -913,6 +913,38 @@ weakest precondition calculus.
   (default is: \texttt{yes}).
 \end{description}
 
+\subsection{Smoke Tests}
+
+During modular deductive verification, inconsistencies in function requirements
+can be difficult to detect untill you actually call it.
+Although, such inconsistencies make its post-conditions provable, while its pre-conditions
+would never be provable.
+
+The \textsf{WP} plug-in can generate smoke-tests to detect such inconsistencies.
+Basically, it consists in checking if \verb+\false+ is provable under the requirements
+or assumptions of a behavior, or under the invariants of a loop.
+
+This is best-effort verification : if at least one prover succeed in proving \verb+\false+,
+an inconsistency is detected. Otherwized, the test is not conclusive, and you can never be sure
+that your annotations are free of inconsistencies.
+
+In case any smoke-test fails, a ``\textit{False if reachable}'' status is put on the
+inconsistent requirements, or on the loop with inconsistent invariants, and finally,
+\textsf{WP} generates a user error.
+
+\begin{description}
+\item[\tt -wp-(no)-smoke-tests] generates checks to detect inconsistent
+  annotations.
+\item[\tt -wp-(no)-smoke-timeout] timeout to be used for trying to prove \verb+\false+
+  on smoke-tests (default is \verb+2+ seconds).
+\end{description}
+
+When reporting prover results for smoke-tests, the \textsf{WP} displays
+``Failed'' when some prover succeed in discharing the \verb+\false+ proof-obligation
+and ``Passed'' when all the provers result are unknown or interrupted.
+In the final prover statistics, the interrupted smoke tests are \emph{not} reported, since
+they are considered valid tests.
+
 \subsection{Trigger Generation}
 \label{triggers}
 
@@ -1016,6 +1048,8 @@ Support for \textsf{Why-3 IDE} is no longer provided.
   on proved goals when available (default is: \texttt{no}).
 \item[\tt -wp-timeout <n>] sets the timeout (in seconds) for the calls
   to the decision prover (defaults to 10 seconds).
+\item[\tt -wp-smoke-timeout <n>] sets the timeout (in seconds) for smoke tests
+  (see \verb+-wp-smoke-tests+, defaults to 5 seconds).
 \item[\tt -wp-time-extra <n>] additional time allocated to provers when
   replaying a script. This is used to cope with variable machine load.
   Default is \verb+5s+.

src/plugins/wp/prover.ml

@@ -35,10 +35,12 @@ let dispatch ?(config=VCS.default) mode prover wpo =
     | Qed | Tactical -> Task.return VCS.no_result
     | NativeAltErgo -> ProverErgo.prove ~config ~mode wpo
     | NativeCoq -> ProverCoq.prove mode wpo
-    | Why3 prover -> ProverWhy3.prove
-                       ~timeout:(VCS.get_timeout config)
-                       ~steplimit:(VCS.get_stepout config)
-                       ~prover wpo
+    | Why3 prover ->
+        let smoke = Wpo.is_smoke_test wpo in
+        ProverWhy3.prove
+          ~timeout:(VCS.get_timeout ~smoke config)
+          ~steplimit:(VCS.get_stepout config)
+          ~prover wpo
   end
 
 let started ?start wpo =

src/plugins/wp/register.ml

@@ -25,6 +25,7 @@ open Factory
 let dkey_main = Wp_parameters.register_category "main"
 let dkey_raised = Wp_parameters.register_category "raised"
 let dkey_shell = Wp_parameters.register_category "shell"
+let wkey_smoke = Wp_parameters.register_warn_category "smoke"
 
 (* --------- Command Line ------------------- *)
 
@@ -347,12 +348,14 @@ let do_wpo_stat goal prover res =
   let s = get_pstat prover in
   let open VCS in
   if res.cached then s.incache <- succ s.incache ;
-  match res.verdict with
-  | Checked | NoResult | Computing _ | Invalid | Unknown ->
+  let smoke = Wpo.is_smoke_test goal in
+  let verdict = VCS.verdict ~smoke res in
+  match verdict with
+  | Checked | NoResult | Computing _ | Unknown ->
       s.unknown <- succ s.unknown
   | Stepout | Timeout ->
       s.interrupted <- succ s.interrupted
-  | Failed ->
+  | Failed | Invalid ->
       s.failed <- succ s.failed
   | Valid ->
       if not (Wpo.is_tactic goal) then
@@ -379,6 +382,49 @@ let do_wpo_result goal prover res =
       do_wpo_stat goal prover res ;
     end
 
+let do_wpo_failed goal =
+  match Wpo.get_results goal with
+  | [p,r] ->
+      Wp_parameters.result "[%a] Goal %s : %a%a"
+        VCS.pp_prover p (Wpo.get_gid goal)
+        VCS.pp_result r pp_warnings goal
+  | pres ->
+      Wp_parameters.result "[Failed] Goal %s%t" (Wpo.get_gid goal)
+        begin fun fmt ->
+          pp_warnings fmt goal ;
+          List.iter
+            (fun (p,r) ->
+               Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
+                 (VCS.title_of_prover p) VCS.pp_result r
+            ) pres ;
+        end
+
+let do_wpo_smoke goal =
+  let results = Wpo.get_results goal in
+  let verdicts = List.filter (fun (_,r) -> VCS.is_verdict r) results in
+  let proved,unproved = List.partition (fun (_,r) -> VCS.is_valid r) verdicts in
+  let pp_provers fmt = function
+    | [] -> ()
+    | (p,_)::prs ->
+        VCS.pp_prover fmt p ;
+        List.iter (fun (p,_) -> Format.fprintf fmt ", %a" VCS.pp_prover p) prs
+  in
+  if proved <> [] then
+    let loc = Property.location (Wpo.get_target goal) in
+    Wp_parameters.warning ~wkey:wkey_smoke ~source:(fst loc)
+      "Smoke-test %s : Failed (%a)"
+      (Wpo.get_gid goal) pp_provers proved
+  else
+  if unproved <> [] then
+    Wp_parameters.feedback ~ontty:`Silent
+      "Smoke-test %s : Passed (%a)"
+      (Wpo.get_gid goal) pp_provers unproved
+  else
+    let loc = Property.location (Wpo.get_target goal) in
+    Wp_parameters.warning ~source:(fst loc)
+      "Smoke-test %s : Non-conclusive (no-result)"
+      (Wpo.get_gid goal)
+
 let do_wpo_success goal s =
   if not (Wp_parameters.Check.get ()) then
     if Wp_parameters.Generate.get () then
@@ -387,36 +433,22 @@ let do_wpo_success goal s =
       | Some prover ->
           Wp_parameters.feedback ~ontty:`Silent
             "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
+    else
+    if Wpo.is_smoke_test goal then
+      do_wpo_smoke goal
     else
       match s with
-      | None ->
-          begin
-            match Wpo.get_results goal with
-            | [p,r] ->
-                Wp_parameters.result "[%a] Goal %s : %a%a"
-                  VCS.pp_prover p (Wpo.get_gid goal)
-                  VCS.pp_result r pp_warnings goal
-            | pres ->
-                Wp_parameters.result "[Failed] Goal %s%t" (Wpo.get_gid goal)
-                  begin fun fmt ->
-                    pp_warnings fmt goal ;
-                    List.iter
-                      (fun (p,r) ->
-                         Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
-                           (VCS.title_of_prover p) VCS.pp_result r
-                      ) pres ;
-                  end
-          end
-      | Some (VCS.Tactical as p) ->
+      | None -> do_wpo_failed goal
+      | Some (VCS.Tactical as script) ->
           Wp_parameters.feedback ~ontty:`Silent
             "[%a] Goal %s : Valid"
-            VCS.pp_prover p (Wpo.get_gid goal)
-      | Some p ->
-          let r = Wpo.get_result goal p in
+            VCS.pp_prover script (Wpo.get_gid goal)
+      | Some prover ->
+          let result = Wpo.get_result goal prover in
           Wp_parameters.feedback ~ontty:`Silent
             "[%a] Goal %s : %a"
-            VCS.pp_prover p (Wpo.get_gid goal)
-            VCS.pp_result r
+            VCS.pp_prover prover (Wpo.get_gid goal)
+            VCS.pp_result result
 
 let do_report_time fmt s =
   begin

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

+/* run.config
+   OPT:
+   OPT: -wp-smoke-tests
+ */
+
+/* run.config_qualif
+   OPT: -wp-smoke-tests
+*/
+
+/*@ axiomatic CFG {
+  predicate ASSUMES(integer x,integer y);
+  predicate REQUIRES(integer x,integer y);
+  predicate ENSURES(integer x,integer y);
+  }*/
+
+/*@
+  requires REQUIRES(0,x);
+  requires x < 0 ;
+  behavior A:
+    assumes  ASSUMES(1,x);
+    requires REQUIRES(1,x);
+    requires 2 < x ;
+  behavior B:
+    assumes  ASSUMES(2,x);
+    requires REQUIRES(2,x);
+ */
+int foo(int x)
+{
+  x++;
+  return x;
+}
+
+
+/*@ requires x > 0; ensures \result == x+1 ; */
+int bar(int x)
+{
+  return x+1;
+}
+
+/*@ requires x > 0; requires x < -4 ; ensures \result == x-1 ; */
+int buzz(int x)
+{
+  return x-1;
+}

src/plugins/wp/tests/wp_plugin/doomed.report

+@CONSOLE
+@ZERO "   -"
+        &30:   Qed Ergo Failed
+@PROPERTY
+  %name &30: %qed %alt-ergo %failed
+@END
+@TAIL
+-------------------------------------------------------------
+Success:  %prop%%
+   Total  :  %prop:total properties
+   Valid  :  %prop:valid
+   Failed :  %prop:failed
+-------------------------------------------------------------

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

+/* run.config
+   OPT: -wp-smoke-tests
+ */
+
+/* run.config_qualif
+   OPT: -wp-smoke-tests
+*/
+
+/*@ axiomatic CFG {
+  predicate P(integer x);
+  predicate Q(integer x);
+  predicate R(integer x);
+  axiom init: P(0) && Q(0) && R(0);
+  axiom loop1: \forall integer n; P(n) ==> Q(n+1);
+  axiom loop2: \forall integer n; Q(n) ==> R(n+1);
+  axiom loop3: \forall integer n; R(n) ==> !P(n);
+  }*/
+
+
+int foo(int x)
+{
+  int n = 0;
+  /*@
+    loop invariant A: P(n);
+    loop invariant B: Q(n);
+    loop invariant C: R(n);
+    loop assigns n ;
+  */
+  while (x>0) {
+    n++;
+  }
+  return n;
+}

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

+/* run.config
+   OPT: -wp-smoke-tests
+ */
+
+/* run.config_qualif
+   OPT: -wp-smoke-tests
+*/
+
+/*@ axiomatic CFG {
+  predicate P(integer x);
+  }*/
+
+
+int foo(int x)
+{
+  int n = 0;
+  /*@
+    loop invariant A: P(n);
+    loop invariant B: !P(n);
+    loop assigns n ;
+  */
+  while (x>0) {
+    n++;
+  }
+  return n;
+}