smoke detector added to the replayer

The smoke detector try to detect when a goal is proved
because the context is self contradicting.

The way it is configured in session is not very pretty.

Makefile.in

@@ -131,7 +131,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		encoding_explicit encoding_guard encoding_sort \
 		encoding_instantiate simplify_array filter_trigger \
 		introduction abstraction close_epsilon lift_epsilon \
-		eval_match instantiate_predicate
+		eval_match instantiate_predicate smoke_detector
 
 LIB_PRINTER = print_number alt_ergo why3printer smtv1 smtv2 \
 		coq tptp simplify gappa cvc3 yices

doc/manpages.tex

@@ -487,9 +487,12 @@ not and you have to use the IDE to update it.
 \begin{itemize}
 \item The exit code is 0 if no difference was detected, 1 if there
   was. Other exit codes mean some failure in running the replay.
-\item option \texttt{-s}: suppresses the output of the final tree view
-\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath
-\item option \texttt{-force}: force writing a new session file even if some proofs did not replay correctly.
+\item option \texttt{-s}: suppresses the output of the final tree view.
+\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath.
+\item option \texttt{-force}: force writing a new session file even if
+  some proofs did not replay correctly.
+\item option \texttt{-smoke-detector \{none|top|deep\}} try to detect
+  if the context is self-contradicting.
 \item option \texttt{-latex \textsl{<dir>}}: produce a summary of
   the replay under the form of a tabular environment in LaTeX, one
   tabular for each theory, one per file, in directory \texttt{\textsl{<dir>}}.
@@ -499,6 +502,46 @@ not and you have to use the IDE to update it.
 %   the replay in HTML syntax.
 \end{itemize}
 
+\paragraph{Smoke Detector}
+ The smoke detector try to detect if the context is self-contradicting
+ and, thus, that anything can be proved in this context. The smoke
+ detector can't be run on outdated session and doesn't modify the session.
+ It has three possible configurations :
+ \begin{itemize}
+ \item \texttt{none} : don't run the smoke detector
+ \item \texttt{top} : The negation of each proved goals
+   tries to be proved with the same timeout and the same prover which
+   prove the goal.
+\begin{verbatim}
+[ ... ]
+
+Goal G : forall x:int. q x -> (p1 x \/ p2 x)
+\end{verbatim}
+becomes
+\begin{verbatim}
+[ ... ]
+
+Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
+\end{verbatim}
+ \item \texttt{deep} : The same technique as \texttt{top} but the
+   negation is pushed under the universal quantification (without
+   changing them) and under the implication. The previous example becomes
+\begin{verbatim}
+[ ... ]
+
+Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
+\end{verbatim}
+ \end{itemize}
+
+The name of the goals which triggered the smoke detector are printed :
+\begin{verbatim}
+   goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
+\end{verbatim}
+Moreover \texttt{Smoke detected} (exit code 1) is printed at the end if the smoke
+detector has been trigged, or \texttt{No smoke detected} (exit code 0)
+otherwise.
+
+
 \paragraph{Customizing LaTeX output}
 
 The generated LaTeX files contain some macros that must be defined

src/ide/replay.ml

@@ -29,6 +29,13 @@ let opt_latex = ref ""
 let opt_latex2 = ref ""
 let opt_html = ref ""
 let opt_force = ref false
+let opt_smoke = ref Session.SD_None
+
+let set_opt_smoke = function
+  | "none" -> opt_smoke := Session.SD_None
+  | "top" ->  opt_smoke := Session.SD_Top
+  | "deep" ->  opt_smoke := Session.SD_Deep
+  | _ -> assert false
 
 let spec = Arg.align [
   ("-I",
@@ -37,6 +44,9 @@ let spec = Arg.align [
   ("-force",
    Arg.Set opt_force,
    " enforce saving of session even if replay failed") ;
+  ("-smoke-detector",
+   Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
+   " try to detect if the context is self-contradicting") ;
   ("-s",
    Arg.Clear opt_stats,
    " do not print statistics") ;
@@ -75,6 +85,12 @@ let () =
     exit 0
   end
 
+let () =
+  if !opt_smoke <> Session.SD_None && !opt_force then begin
+    Format.printf "You can't force when detecting smoke@.";
+    exit 1
+  end
+
 let fname = match !file with
   | None ->
       Arg.usage spec usage_str;
@@ -524,8 +540,13 @@ let print_report (g,p,r) =
   printf "   goal '%s', prover '%s': " g p;
   match r with
   | M.Wrong_result(new_res,old_res) ->
-      printf "%a instead of %a@."
-        print_result new_res print_result old_res
+    begin match !opt_smoke with
+      | Session.SD_None ->
+        printf "%a instead of %a@."
+          print_result new_res print_result old_res
+      | _ ->
+        printf "Smoke detected!!!@."
+    end
   | M.No_former_result ->
       printf "no former result available@."
   | M.CallFailed msg ->
@@ -533,22 +554,7 @@ let print_report (g,p,r) =
   | M.Prover_not_installed ->
       printf "not installed@."
 
-let () =
-  try
-    eprintf "Opening session...@?";
-    let found_obs =
-      M.open_session ~allow_obsolete:true
-        ~env ~config ~init ~notify project_dir
-    in
-    if found_obs then
-      eprintf "[Warning] session is obsolete@.";
-    M.maximum_running_proofs :=
-      Whyconf.running_provers_max (Whyconf.get_main config);
-    eprintf " done@.";
-    if !opt_latex <> "" then print_latex_statistics 1 !opt_latex
-    else
-    if !opt_latex2 <> "" then print_latex_statistics 2 !opt_latex2
-    else
+let add_to_check_no_smoke found_obs =
       let callback report =
         eprintf "@.";
 	let files,n,m =
@@ -584,9 +590,56 @@ session NOT updated)@." n m
             eprintf "Replay failed.@.";
             exit 1
     in
-    M.check_all ~callback;
-    try main_loop ()
-    with Exit -> eprintf "main replayer exited unexpectedly@."
+    M.check_all ~callback
+
+let add_to_check_smoke () =
+  let callback report =
+    eprintf "@.";
+    match report with
+      | [] ->
+        eprintf "No smoke detected.@.";
+        exit 0
+      | _ ->
+        List.iter print_report report;
+        eprintf "Smoke detected.@.";
+        exit 1
+  in
+  M.check_all ~callback
+
+let add_to_check found_obs =
+  match !opt_smoke with
+    | Session.SD_None -> add_to_check_no_smoke found_obs;
+    | _ -> assert (not found_obs); add_to_check_smoke ()
+
+
+let () =
+  try
+    eprintf "Opening session...@?";
+    let found_obs =
+      M.open_session ~allow_obsolete:true
+        ~env ~config ~init ~notify project_dir
+    in
+    if found_obs then begin
+      if !opt_smoke <> Session.SD_None then begin
+        eprintf
+          "[Error] I can't run the smoke detector if the session is obsolete";
+        exit 1
+      end;
+      eprintf "[Warning] session is obsolete@.";
+    end;
+    M.maximum_running_proofs :=
+      Whyconf.running_provers_max (Whyconf.get_main config);
+    M.smoke_detector := !opt_smoke;
+    eprintf " done@.";
+    if !opt_latex <> "" then print_latex_statistics 1 !opt_latex
+    else
+    if !opt_latex2 <> "" then print_latex_statistics 2 !opt_latex2
+    else
+      begin
+        add_to_check found_obs;
+        try main_loop ()
+        with Exit -> eprintf "main replayer exited unexpectedly@."
+      end
   with
     | M.OutdatedSession ->
         eprintf "The session database '%s' is outdated, cannot replay@."

src/ide/session.ml

@@ -104,6 +104,11 @@ type proof_attempt_status =
   | InternalFailure of exn (** external proof aborted by internal error *)
   | Unedited (** interactive prover yet no proof script *)
 
+type smoke_detector =
+  | SD_None (** no smoke detector *)
+  | SD_Top  (** smoke_detector *)
+  | SD_Deep (** smoke_detector_deep *)
+
 (***************************)
 (*     main functor        *)
 (***************************)
@@ -225,6 +230,8 @@ let transformations g = g.transformations
 let external_proofs g = g.external_proofs
 let goal_expanded g = g.goal_expanded
 
+let smoke_detector = ref SD_None
+
 let get_task g =
   match g.task with
     | None ->
@@ -1733,7 +1740,8 @@ let same_result r1 r2 =
     | Call_provers.Failure _, Call_provers.Failure _-> true
     | _ -> false
 
-let check_external_proof g a =
+(** When no smoke *)
+let check_external_proof_not_smoked g a =
   (* check that the state is not Scheduled or Running *)
   if running a then ()
   else
@@ -1781,6 +1789,62 @@ let check_external_proof g a =
             (get_task g)
     end
 
+(** When some smoke method is used *)
+let check_external_proof_smoked g a =
+  (* check that the state is not Scheduled or Running *)
+  match a.proof_state with
+    | Done ({Call_provers.pr_answer = Call_provers.Valid } as old_res)
+        when not (running a)->
+      begin
+        incr proofs_to_do;
+        match a.prover with
+          | Undetected_prover s ->
+            push_report g s Prover_not_installed;
+            incr proofs_done;
+            set_proof_state ~obsolete:false a Undone
+          | Detected_prover p ->
+            let p_name = p.prover_name ^ " " ^ p.prover_version in
+            let callback result =
+              match result with
+                | Scheduled | Running | Interrupted -> ()
+                | Undone | Unedited -> assert false
+                | InternalFailure msg ->
+                  push_report g p_name (CallFailed msg);
+                  incr proofs_done;
+                  set_proof_state ~obsolete:false a result
+                | Done new_res ->
+                  begin
+                    match new_res.Call_provers.pr_answer with
+                      | Call_provers.Valid ->
+                        push_report g p_name (Wrong_result(new_res,old_res))
+                      | _ -> ()
+                  end;
+                  incr proofs_done;
+                  set_proof_state ~obsolete:false a result
+            in
+            let old = if a.edited_as = "" then None else
+                begin
+                  let f = Filename.concat !project_dir a.edited_as in
+                  (Some (open_in f))
+                end
+            in
+            let task =  match !smoke_detector with
+              | SD_None -> assert false
+              | SD_Top -> Trans.apply Smoke_detector.top (get_task g)
+              | SD_Deep -> Trans.apply Smoke_detector.deep (get_task g) in
+            schedule_proof_attempt
+              ~debug:false ~timelimit:a.timelimit ~memlimit:0
+              ?old ~command:p.command ~driver:p.driver
+              ~callback
+              task
+      end
+    | _ -> ()
+
+let check_external_proof g a =
+  match !smoke_detector with
+    | SD_None -> check_external_proof_not_smoked g a
+    | _ -> check_external_proof_smoked g a
+
 let rec check_goal_and_children g =
   Hashtbl.iter (fun _ a -> check_external_proof g a) g.external_proofs;
   Hashtbl.iter

src/ide/session.mli

@@ -64,6 +64,14 @@ type proof_attempt_status = private
     | InternalFailure of exn (** external proof aborted by internal error *)
     | Unedited (** interactive prover yet no proof script *)
 
+(** {2 Smoke detector} *)
+
+type smoke_detector =
+  | SD_None (** No smoke detector *)
+  | SD_Top  (** Negation added at the top of the goals *)
+  | SD_Deep
+(** Negation added under implication and universal quantification *)
+
 (** {2 Observers signature} *)
 
 module type OBSERVER = sig
@@ -304,6 +312,9 @@ module Make(O: OBSERVER) : sig
     (** [clean a] removes failed attempts below [a] where
         there at least one successful attempt or transformation *)
 
+  val smoke_detector : smoke_detector ref
+    (** Define if the smoke detector is used *)
+
 end
 
 

src/transform/smoke_detector.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Smoke detector try to find if the axiomatisation is self-contradicting.
+
+   The second smoke detector add the negation under the implication and
+   universal quantification (replace implication by conjunction).
+*)
+
+open Ident
+open Term
+open Decl
+open Task
+
+let create app =
+  Trans.goal (fun pr t -> [create_prop_decl Pgoal pr (app t)])
+
+let top = create t_not
+
+let rec neg f = match f.t_node with
+  | Tbinop (Timplies,f1,f2) -> t_and f1 (neg f2)
+  | Tquant (Tforall,fq) ->
+      let vsl,_trl,f = t_open_quant fq in
+      t_forall_close vsl _trl (neg f)
+  | Tlet (t,fb) ->
+      let vs,f = t_open_bound fb in
+      t_let_close vs t (neg f)
+  | _ -> t_not f
+
+let deep = create neg
+
+let () = List.iter (fun (name,trans) -> Trans.register_transform name trans)
+  ["smoke_detector_top",top;
+   "smoke_detector_deep",deep]
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. byte"
+End:
+*)

src/transform/smoke_detector.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+val top : Task.task Trans.trans
+val deep : Task.task Trans.trans