why3bench : --redo-db rerun the proof_attempt which are

in the database given by -d
display only differences, --debug benchdb for other information.

Makefile.in

@@ -481,7 +481,7 @@ endif
 
 ifeq (@enable_bench@,yes)
 
-BENCH_FILES = bench benchrc whybench
+BENCH_FILES = bench benchrc benchdb whybench
 
 BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
 

src/bench/bench.ml

@@ -80,126 +80,104 @@ type proof_attempt_status =
 
 open Format
 
-let print_prover_answer fmt = function
-  | Db.Success -> fprintf fmt "Valid"
-    (* | Invalid -> fprintf fmt "Invalid" *)
-  | Db.Timeout -> fprintf fmt "Timeout"
-  | Db.Unknown -> fprintf fmt "Unknown"
-  | Db.Failure -> fprintf fmt "Failure"
-  | Db.Undone  -> fprintf fmt "Undone"
-
-let print_why_result fmt = function
-  | InternalFailure exn ->
-    Format.fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
-  | Done (pr,_) -> print_prover_answer fmt pr
-
-let print_pas fmt = function
-  | Runned sp -> fprintf fmt "Runned %a" print_why_result sp
-  | Cached (p,t) -> fprintf fmt "Cached (%a,%f)" print_prover_answer p t
-
 type callback = tool_id -> prob_id ->
     task -> int ->  proof_attempt_status -> unit
 
-let proof_status_to_db_result pr =
-  match pr with
-      | {pr_answer = Valid} -> (Db.Success,pr.pr_time)
-      | {pr_answer = Invalid} -> (Db.Unknown,pr.pr_time)
-      (* TODO add invalid in Db *)
-      | {pr_answer = Unknown _} -> (Db.Unknown,pr.pr_time)
-      | {pr_answer = Failure _ | HighFailure} -> (Db.Failure,pr.pr_time)
-      | {pr_answer = Timeout } -> (Db.Timeout,pr.pr_time)
-
 let debug_call = Debug.register_flag "call"
 let debug = Debug.register_flag "bench_core"
 
-open Worker
+
+module BenchUtil =
+struct
+
+  let print_proof_status fmt = function
+    | Db.Success -> fprintf fmt "Valid"
+  (* | Invalid -> fprintf fmt "Invalid" *)
+    | Db.Timeout -> fprintf fmt "Timeout"
+    | Db.Unknown -> fprintf fmt "Unknown"
+    | Db.Failure -> fprintf fmt "Failure"
+    | Db.Undone  -> fprintf fmt "Undone"
+
+  open Worker
 
 (* number of scheduled external proofs *)
-let coef_buf = 2
-let scheduled_proofs = ref 0
-let maximum_running_proofs = ref 2
+  let coef_buf = 2
+  let scheduled_proofs = ref 0
+  let maximum_running_proofs = ref 2
 
 (* they are protected by a lock *)
-let answers_queue = Queue.create ()
-let queue_lock = Mutex.create ()
-let queue_condition = Condition.create ()
+  let answers_queue = Queue.create ()
+  let queue_lock = Mutex.create ()
+  let queue_condition = Condition.create ()
 
 (** Before calling this function queue_lock must be locked *)
-let treat_result () =
-  let q_tmp = Queue.create () in
-  while not (Queue.is_empty answers_queue) do
-    Queue.transfer answers_queue q_tmp;
-    Mutex.unlock queue_lock;
-    let iter (result,callback) = decr scheduled_proofs; callback (result ()) in
-    Queue.iter iter q_tmp;
-    Queue.clear q_tmp;
-    Mutex.lock queue_lock
-  done
-
-let yield () =
-  Thread.yield ();
-  Mutex.lock queue_lock;
-  treat_result ();
-  Mutex.unlock queue_lock
-
-let new_external_proof =
-  let run_external (call_prover,callback) =
-    let r = Call_provers.wait_on_call (call_prover ()) in
+  let treat_result () =
+    let q_tmp = Queue.create () in
+    while not (Queue.is_empty answers_queue) do
+      Queue.transfer answers_queue q_tmp;
+      Mutex.unlock queue_lock;
+      let iter (result,callback) = decr scheduled_proofs; callback (result ())
+      in
+      Queue.iter iter q_tmp;
+      Queue.clear q_tmp;
+      Mutex.lock queue_lock
+    done
+
+  let yield () =
+    Thread.yield ();
+    Mutex.lock queue_lock;
+    treat_result ();
+    Mutex.unlock queue_lock
+
+  (** Wait for the last remaining tasks *)
+  let wait_remaining_task () =
     Mutex.lock queue_lock;
-    Queue.push (r,callback) answers_queue ;
-    Condition.signal queue_condition;
-    Mutex.unlock queue_lock in
-  let external_workers =
-    ManyWorkers.create maximum_running_proofs run_external in
-  fun (call_prover,callback) ->
-    ManyWorkers.add_work external_workers (call_prover,callback);
-    incr scheduled_proofs;
+    while !scheduled_proofs > 0 do
+      while Queue.is_empty answers_queue do
+        Condition.wait queue_condition queue_lock
+      done;
+      treat_result ();
+    done;
+    Mutex.unlock queue_lock
+
+  let new_external_proof =
+    let run_external (call_prover,callback) =
+      let r = Call_provers.wait_on_call (call_prover ()) in
+      Mutex.lock queue_lock;
+      Queue.push (r,callback) answers_queue ;
+      Condition.signal queue_condition;
+      Mutex.unlock queue_lock in
+    let external_workers =
+      ManyWorkers.create maximum_running_proofs run_external in
+    fun (call_prover,callback) ->
+      ManyWorkers.add_work external_workers (call_prover,callback);
+      incr scheduled_proofs;
     (** Stop the computation if too many external proof are scheduled *)
-    while !scheduled_proofs >= !maximum_running_proofs * coef_buf do
+      while !scheduled_proofs >= !maximum_running_proofs * coef_buf do
         Mutex.lock queue_lock;
         while Queue.is_empty answers_queue do
           Condition.wait queue_condition queue_lock
         done;
         treat_result ();
         Mutex.unlock queue_lock;
-    done
+      done
 
 
 (* from Gmain *)
-let task_checksum t =
-  fprintf str_formatter "%a@." Pretty.print_task t;
-  let s = flush_str_formatter () in
-  Digest.to_hex (Digest.string s)
-
-
-let apply_trans (task,db_goal) (trans,db_trans) =
-  let task = Trans.apply trans task in
-  match db_goal, db_trans with
-    | Some db_goal, Some db_trans ->
-      let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
-        with Not_found ->
-          Db.add_transformation db_goal db_trans
-      in
-      let md5 = task_checksum task in
-      let db_goal =
-        try
-          Mstr.find md5 (Db.subgoals transf)
-        with Not_found ->
-          Db.add_subgoal transf
-            (Task.task_goal task).Decl.pr_name.Ident.id_string
-            md5
-      in
-      (task,Some db_goal)
-    | _ -> ((task:task),None)
-
-let apply_transl (task,db_goal) (trans,db_trans) =
-  let tasks = Trans.apply trans task in
-  match db_goal, db_trans with
-    | Some db_goal, Some db_trans ->
-      let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
-        with Not_found -> Db.add_transformation db_goal db_trans
-      in
-      let map task =
+  let task_checksum t =
+    fprintf str_formatter "%a@." Pretty.print_task t;
+    let s = flush_str_formatter () in
+    Digest.to_hex (Digest.string s)
+
+
+  let apply_trans (task,db_goal) (trans,db_trans) =
+    let task = Trans.apply trans task in
+    match db_goal, db_trans with
+      | Some db_goal, Some db_trans ->
+        let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
+          with Not_found ->
+            Db.add_transformation db_goal db_trans
+        in
         let md5 = task_checksum task in
         let db_goal =
           try
@@ -209,18 +187,60 @@ let apply_transl (task,db_goal) (trans,db_trans) =
               (Task.task_goal task).Decl.pr_name.Ident.id_string
               md5
         in
-        (task,Some db_goal) in
-      List.map map tasks
-    | _ -> List.map (fun task -> (task:task),None) tasks
+        (task,Some db_goal)
+      | _ -> ((task:task),None)
+
+  let apply_transl (task,db_goal) (trans,db_trans) =
+    let tasks = Trans.apply trans task in
+    match db_goal, db_trans with
+      | Some db_goal, Some db_trans ->
+        let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
+          with Not_found -> Db.add_transformation db_goal db_trans
+        in
+        let map task =
+          let md5 = task_checksum task in
+          let db_goal =
+            try
+              Mstr.find md5 (Db.subgoals transf)
+            with Not_found ->
+              Db.add_subgoal transf
+                (Task.task_goal task).Decl.pr_name.Ident.id_string
+                md5
+          in
+          (task,Some db_goal) in
+        List.map map tasks
+      | _ -> List.map (fun task -> (task:task),None) tasks
+
+
+  let rec apply_transll trl acc (task,db_goal) =
+    match trl with
+      | [] -> (task,db_goal)::acc
+      | tr::trl ->
+        let tl = apply_transl (task,db_goal) tr in
+        List.fold_left (apply_transll trl) acc tl
+
+  let proof_status_to_db_result pr =
+    match pr with
+      | {pr_answer = Valid} -> (Db.Success,pr.pr_time)
+      | {pr_answer = Invalid} -> (Db.Unknown,pr.pr_time)
+      (* TODO add invalid in Db *)
+      | {pr_answer = Unknown _} -> (Db.Unknown,pr.pr_time)
+      | {pr_answer = Failure _ | HighFailure} -> (Db.Failure,pr.pr_time)
+      | {pr_answer = Timeout } -> (Db.Timeout,pr.pr_time)
+
 
+end
 
-let rec apply_transll trl acc (task,db_goal) =
-  match trl with
-    | [] -> (task,db_goal)::acc
-    | tr::trl ->
-      let tl = apply_transl (task,db_goal) tr in
-      List.fold_left (apply_transll trl) acc tl
 
+let print_why_result fmt = function
+  | InternalFailure exn ->
+    Format.fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
+  | Done (pr,_) -> BenchUtil.print_proof_status fmt pr
+
+let print_pas fmt = function
+  | Runned sp -> fprintf fmt "Runned %a" print_why_result sp
+  | Cached (p,t) -> fprintf fmt "Cached (%a,%f)"
+    BenchUtil.print_proof_status p t
 
 let call callback tool prob =
   (** Prove goal *)
@@ -230,7 +250,7 @@ let call callback tool prob =
       let call_prover : Call_provers.pre_prover_call =
         Driver.prove_task ~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
           ~command:(tool.tcommand) (tool.tdriver) task in
-      new_external_proof (call_prover,cb)
+      BenchUtil.new_external_proof (call_prover,cb)
     with e ->
       Format.eprintf "%a@." Exn_printer.exn_printer e;
       callback pval i task (Runned (InternalFailure e)) in
@@ -245,7 +265,7 @@ let call callback tool prob =
         in
         let (proof_status,time,_,_) = Db.status_and_time proof_attempt in
         Debug.dprintf debug "Database has (%a,%f) for the goal@."
-          print_prover_answer proof_status time;
+          BenchUtil.print_proof_status proof_status time;
         begin
           if proof_status = Db.Success ||
             (proof_status = Db.Timeout && time > (float tool.ttime -. 0.1))
@@ -256,7 +276,7 @@ let call callback tool prob =
               Debug.dprintf debug "@.time = %f %i@.@."
                 time tool.ttime;
               let cb res =
-                let (status,time) = proof_status_to_db_result res in
+                let (status,time) = BenchUtil.proof_status_to_db_result res in
                 callback pval i task (Runned (Done (status,time)));
                 Db.set_status proof_attempt status time
               in
@@ -265,16 +285,18 @@ let call callback tool prob =
         end
       | _ ->
         let cb res =
-          let (status,time) = proof_status_to_db_result res in
+          let (status,time) = BenchUtil.proof_status_to_db_result res in
           callback pval i task (Runned (Done (status,time))) in
         new_external_proof pval i cb task
   in
   (** Apply trans *)
   let iter_task (pval,task) =
     let translist = prob.ptrans tool.tenv in
-    let tasks = apply_transll translist [] (task,pval.prob_db) in
+    let tasks = BenchUtil.apply_transll translist [] (task,pval.prob_db) in
     let tasks = List.map
-      (fun task -> List.fold_left apply_trans task tool.ttrans) tasks in
+      (fun task -> List.fold_left BenchUtil.apply_trans task tool.ttrans)
+      tasks
+    in
     let iter i task = call pval i task; succ i in
     ignore (List.fold_left iter 0 (List.rev tasks)) in
   (** Split *)
@@ -297,15 +319,7 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
                | Cached (res,time) -> Done (res,time)
             } in
     call cb tool prob);
-  (** Wait for the last remaining tasks *)
-  Mutex.lock queue_lock;
-  while !scheduled_proofs > 0 do
-    while Queue.is_empty answers_queue do
-      Condition.wait queue_condition queue_lock
-    done;
-    treat_result ();
-  done;
-  Mutex.unlock queue_lock
+  BenchUtil.wait_remaining_task ()
 
 let any ?callback toolprob =
   let l = ref [] in
@@ -498,7 +512,7 @@ answer output time
       match r with
         | Done (answer,time) ->
           fprintf fmt "%a, %.3f" (*"%a, %S, %.3f"*)
-            print_prover_answer answer (*r.result.pr_output*)
+            BenchUtil.print_proof_status answer (*r.result.pr_output*)
             time
         | InternalFailure _ -> fprintf fmt "InternalFailure, \"\""
 in

src/bench/bench.mli

@@ -26,11 +26,49 @@ open Driver
 open Call_provers
 open Scheduler
 
-
-val maximum_running_proofs: int ref
+module BenchUtil : sig
+  val maximum_running_proofs: int ref
 (** bound on the number of prover processes running in parallel.
     default is 2 *)
 
+  val new_external_proof :
+    Call_provers.pre_prover_call * (Call_provers.prover_result -> unit)
+    -> unit
+  (** [new_external_proof pre_prover_call callback] *)
+
+  val wait_remaining_task : unit -> unit
+  (** Wait the completion of the remaining task started by
+      new_external_proof *)
+
+  val task_checksum : Task.task -> string
+
+  val apply_trans :
+    task * Db.goal option ->
+    task trans * Db.transf_id option ->
+    task * Db.goal option
+  (** [apply_transl trans goal] *)
+
+  val apply_transl :
+    task * Db.goal option ->
+    task list trans * Db.transf_id option ->
+    (task * Db.goal option) list
+  (** [apply_transl transl goal] *)
+
+  val apply_transll :
+    (task list trans * Db.transf_id option) list ->
+    (task * Db.goal option) list ->
+    task * Db.goal option ->
+    (task * Db.goal option) list
+  (** [apply_transll transllist acc goal] *)
+
+  val proof_status_to_db_result :
+    Call_provers.prover_result -> Db.proof_status * float
+
+  val print_proof_status :
+    Format.formatter -> Db.proof_status -> unit
+
+end
+
 type tool_id = {
   tool_name : string;
   prover_name : string;
@@ -82,8 +120,6 @@ type proof_attempt_status =
 
 val print_pas : Format.formatter -> proof_attempt_status -> unit
 
-val task_checksum : Task.task -> string
-
 type callback = tool_id -> prob_id ->
     task -> int -> proof_attempt_status -> unit
 

src/bench/benchdb.ml

+(** run benchs from the database *)
+
+open Format
+open Why
+open Util
+module BenchUtil = Bench.BenchUtil
+
+let load_driver = Env.Wenv.memoize 2 (fun env ->
+  memo_string 10 (Driver.load_driver env))
+
+let debug = Debug.register_flag "benchdb"
+
+type path =
+  | Pgoal of string
+  | Ptrans of string
+
+let print_path fmt = function
+  | Pgoal s -> Format.fprintf fmt "the goal %s" s
+  | Ptrans s -> Format.fprintf fmt "the transformation %s" s
+
+let print_paths fmt (wf,thname,pathl) =
+  Format.fprintf fmt "%a of theory %s in file %s"
+    (Pp.print_list (fun fmt () -> fprintf fmt "@ of@ ") print_path) pathl
+    thname wf
+
+let concat_path p (wf,thname,pathl) = (wf,thname,p::pathl)
+
+let rec goal whyconf env path dbgoal wgoal =
+  (** external proof *)
+  let db_proofs = Db.external_proofs dbgoal in
+  let iter prover_id proof_attempt =
+    try
+      let (proof_status,time,obsolete,edited_as) =
+        Db.status_and_time proof_attempt in
+      if obsolete then () else
+      let prover_name = Db.prover_name prover_id in
+      let driver,command =
+        try
+          let p = Mstr.find prover_name (Whyconf.get_provers whyconf) in
+          p.Whyconf.driver ,p.Whyconf.command
+        with
+      (* TODO add exceptions pehaps inside rc.ml in fact*)
+          | Not_found ->
+            Debug.dprintf debug "Error : Prover %s not found.@." prover_name;
+            raise Exit
+      in
+      let cb res =
+        let (res_status,_res_time) = BenchUtil.proof_status_to_db_result res in
+        if proof_status <> res_status then
+          printf "Diff : %a instead of %a in %a@."
+            BenchUtil.print_proof_status proof_status
+            BenchUtil.print_proof_status res_status
+            print_paths path
+        else
+          Debug.dprintf debug "Same : %a for %a@."
+            BenchUtil.print_proof_status proof_status
+            print_paths path
+      in
+      let old = if edited_as = "" then None else
+          begin
+            eprintf "Info: proving using edited file %s@." edited_as;
+            (Some (open_in edited_as))
+          end
+      in
+      let call_prover : Call_provers.pre_prover_call =
+        Driver.prove_task
+          ~timelimit:(truncate (ceil (time*.1.1)))
+          ~command (load_driver env driver) ?old wgoal in
+      BenchUtil.new_external_proof (call_prover,cb)
+    with Exit -> ()
+  in
+  Db.Hprover.iter iter db_proofs;
+  (** with transformations *)
+  let db_trans = Db.transformations dbgoal in
+  let iter dbtrans_id dbtrans =
+    let name = Db.transf_name dbtrans_id in
+    try
+      let wtransf = try Trans.singleton (Trans.lookup_transform name env)
+        with Trans.UnknownTrans _ -> Trans.lookup_transform_l name env
+      in
+      transf whyconf env (concat_path (Ptrans name) path) dbtrans wtransf wgoal
+    with Trans.UnknownTrans _ ->
+      Debug.dprintf debug "Error : Transformation %s not found.@." name
+  in
+  Db.Htransf.iter iter db_trans
+
+and transf whyconf env path dbtransf wtransf wgoal =
+  try
+    let wgoals = Trans.apply wtransf wgoal in
+    let dbgoals = Db.subgoals dbtransf in
+    let iter wgoal =
+      let checksum = BenchUtil.task_checksum wgoal in
+      try
+        let dbgoal = Mstr.find checksum dbgoals in
+        let gname = (Task.task_goal wgoal).Decl.pr_name.Ident.id_string in
+        goal whyconf env (concat_path (Pgoal gname) path) dbgoal wgoal
+      with Not_found ->
+        Debug.dprintf debug
+          "Error : Goal with checksum %s@ not found in@ %a.@."
+          checksum print_paths path
+    in
+    List.iter iter wgoals
+  with e ->
+    Debug.dprintf debug "Error : Execption %a@ in %a not found.@."
+      Exn_printer.exn_printer e print_paths path
+
+let theory whyconf env wf thname dbth wth =
+  let wgoals = Task.split_theory wth None None in
+  let dbgoals = Db.goals dbth in
+  let iter wgoal =
+    let gname = (Task.task_goal wgoal).Decl.pr_name.Ident.id_string in
+    try
+      let dbgoal = Mstr.find gname dbgoals in
+      goal whyconf env (wf,thname,[Pgoal gname]) dbgoal wgoal
+    with Not_found ->
+      Debug.dprintf debug
+        "Error : No sketch of proof for the goal %s of theory %s in file %s.@."
+        gname thname wf
+  in
+  List.iter iter wgoals
+
+let file whyconf env (dbf,wf) =
+  let wths = Env.read_file env
+    (Filename.concat (Filename.dirname (Db.db_name ())) wf) in
+  let dbths = Db.theories dbf in
+  let iter thname wth =
+    try
+      let dbth = Mstr.find thname dbths in
+      theory whyconf env wf thname dbth wth
+    with Not_found ->
+      Debug.dprintf debug
+        "Error : No sketch of proof for the theory %s of file %s.@."
+        thname wf
+  in
+  Theory.Mnm.iter iter wths
+
+
+let db whyconf env =
+  assert (Db.is_initialized ());
+  List.iter (file whyconf env) (Db.files ());
+  BenchUtil.wait_remaining_task ()

src/bench/benchdb.mli

+(** run benchs from the database *)
+
+open Why
+
+val db : Whyconf.config -> Env.env -> unit

src/bench/benchrc.ml

@@ -117,7 +117,7 @@ let apply_use_before_goal (task,goal_id) (th_use,th_use_id) =
           with Not_found ->
             Db.add_transformation goal_id th_use_id  in
         let name2 = (Task.task_goal task2).Decl.pr_name.Ident.id_string in
-        let md5_2 = task_checksum task2 in
+        let md5_2 = BenchUtil.task_checksum task2 in
         try Mstr.find md5_2 (Db.subgoals transf)
         with Not_found ->
           Db.add_subgoal transf name2 md5_2
@@ -154,7 +154,7 @@ let gen_from_file ~format ~prob_name ~file_path ~file_name env lth =
             let name = (Task.task_goal task).Decl.pr_name.Ident.id_string in
             try Mstr.find name (Db.goals theory_id)
             with Not_found ->
-              Db.add_goal theory_id name (task_checksum task)
+              Db.add_goal theory_id name (BenchUtil.task_checksum task)
           ) theory_id in
           let (task,goal_id) = List.fold_left apply_use_before_goal
             (task,goal_id) lth in

src/bench/whybench.ml

@@ -103,6 +103,7 @@ let opt_timelimit = ref None
 let opt_memlimit = ref None
 let opt_benchrc = ref []
 let opt_db = ref None
+let opt_redo = ref false
 
 let opt_print_theory = ref false
 let opt_print_namespace = ref false
@@ -145,6 +146,8 @@ let option_list = Arg.align [
       "<bench> Read one bench configuration file from <bench>";
   "-d", Arg.String (fun s -> opt_db := Some s),
   "<dir> the directory containing the database";
+  "--redo-db", Arg.Set opt_redo,
+  "Check that the proof attempts in the database (-d) give the same results";
   "--prover", Arg.String (fun s -> opt_prover := s::!opt_prover),
       " same as -P";
   "-F", Arg.String (fun s -> opt_parser := Some s),
@@ -222,7 +225,7 @@ let () =
 
   let main = get_main config in
   Whyconf.load_plugins main;
-  Bench.maximum_running_proofs := Whyconf.running_provers_max main;
+  Bench.BenchUtil.maximum_running_proofs := Whyconf.running_provers_max main;
   (** listings*)
 
   let opt_list = ref false in
@@ -318,9 +321,12 @@ let () =
       Debug.dprintf debug "database loaded@."
   end;
 
-  if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue) then
+  if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue)
+    && (not !opt_redo)
+  then
     begin
-      eprintf "At least one bench is required or one prover and one file.@.";
+      eprintf "At least one bench is required or one prover and one file or 
+      the verification of a database .@.";
       Arg.usage option_list usage_msg;
       exit 1
     end;
@@ -337,6 +343,15 @@ let () =
     !opt_metas) in
 
   let env = Lexer.create_env !opt_loadpath in
+
+  if !opt_redo then
+    begin if not (Db.is_initialized ()) then
+        begin eprintf "--redo-db need the option -d";
+          exit 1 end;
+      Benchdb.db config env
+    end;