Commit 979cf05c authored by Sylvain Dailler's avatar Sylvain Dailler

Add debug keep_vcs: allow to use a given filename to save prover files.

It is now possible to give an optional argument to schedule_proof_attempt
so that (when in debug mode) the file given is used to store the generated
input file of the prover. In non debug mode, the file given to
schedule_proof_attempt is used but removed after the call to the prover.

Currently, no file is ever given to schedule_proof_attempt but this can be
used by people using Why3 as a backend.
parent 3e91bbc5
......@@ -16,6 +16,8 @@ let debug = Debug.register_info_flag "call_prover"
~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
and@ keep@ temporary@ files."
let keep_vcs = Debug.register_info_flag "keep_vcs" ~desc:"Keep@ intermediate@ prover@ files."
type reason_unknown =
| Resourceout
| Other
......@@ -343,15 +345,15 @@ let handle_answer answer =
let id = answer.Prove_client.id in
let save = Hashtbl.find saved_data id in
Hashtbl.remove saved_data id;
if Debug.test_noflag debug then begin
Sys.remove save.vc_file;
if save.inplace then Sys.rename (backup_file save.vc_file) save.vc_file
if Debug.test_noflag debug && Debug.test_noflag keep_vcs then begin
Sys.remove save.vc_file;
if save.inplace then Sys.rename (backup_file save.vc_file) save.vc_file
end;
let out = read_and_delete_file answer.Prove_client.out_file in
let ret = answer.Prove_client.exit_code in
let printer_mapping = save.printer_mapping in
let ans = parse_prover_run save.res_parser
answer.Prove_client.time out ret save.limit ~printer_mapping in
answer.Prove_client.time out ret save.limit ~printer_mapping in
id, Some ans
| Prove_client.Started id ->
id, None
......@@ -447,7 +449,7 @@ let rec wait_on_call = function
| ServerCall id as pc ->
begin match query_result_buffer id with
| ProverFinished r -> r
| _ ->
| _ ->
fetch_new_results ~blocking:true;
wait_on_call pc
end
......@@ -456,14 +458,18 @@ let rec wait_on_call = function
editor_result ret
let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
?(inplace=false) buffer =
~gen_new_file ?(inplace=false) buffer =
let fin,cin =
if inplace then begin
let filename = Sysutil.absolutize_filename (Sys.getcwd ()) filename in
Sys.rename filename (backup_file filename);
filename, open_out filename
end else
Filename.open_temp_file "why_" ("_" ^ filename) in
if gen_new_file then
Filename.open_temp_file "why_" ("_" ^ filename)
else
begin
let filename = Sysutil.absolutize_filename (Sys.getcwd ()) filename in
if inplace then
Sys.rename filename (backup_file filename);
filename, open_out filename
end
in
Buffer.output_buffer cin buffer; close_out cin;
call_on_file ~command ~limit ~res_parser ~printer_mapping ~inplace fin
......
......@@ -149,6 +149,7 @@ val call_on_buffer :
res_parser : prover_result_parser ->
filename : string ->
printer_mapping : Printer.printer_mapping ->
gen_new_file : bool ->
?inplace : bool ->
Buffer.t -> prover_call
(** Call a prover on the task printed in the {!type: Buffer.t} given.
......@@ -163,7 +164,12 @@ val call_on_buffer :
@param inplace : it is used to make a save of the file on which the
prover was called. It is renamed as %f.save if inplace=true and the command
[actualcommand] fails *)
[actualcommand] fails
@param gen_new_file: When set, this generates a new temp file to run the
prover on. Otherwise it reuses the filename already given.
*)
type prover_update =
| NoUpdates
......
......@@ -254,10 +254,10 @@ let file_of_task drv input_file theory_name task =
let file_of_theory drv input_file th =
get_filename drv input_file th.th_name.Ident.id_string "null"
let call_on_buffer ~command ~limit
?inplace ~filename ~printer_mapping drv buffer =
let call_on_buffer ~command ~limit ~gen_new_file ?inplace ~filename
~printer_mapping drv buffer =
Call_provers.call_on_buffer
~command ~limit ~res_parser:drv.drv_res_parser
~command ~limit ~gen_new_file ~res_parser:drv.drv_res_parser
~filename ~printer_mapping ?inplace buffer
(** print'n'prove *)
......@@ -325,35 +325,60 @@ let print_theory ?old drv fmt th =
let task = Task.use_export None th in
print_task ?old drv fmt task
let file_name_of_task ?old ?inplace drv task =
let file_name_of_task ?old ?inplace ?interactive drv task =
match old, inplace with
| Some fn, Some true -> fn
| Some fn, Some true ->
(* Example: Isabelle. No file should be generated, it should be done
in_place and we keep the same file. *)
false, fn
| Some fn, _ when interactive <> Some true ->
(* Example: cvc4. If a file is provided, it means it was passed to
schedule_proof_attempt via its save_to argument. So we ask to erase
and regenerate the file (the advantage is that we decide the location
of the file).
*)
false, fn
| Some _, _ ->
(* Example: Coq.
For Coq, the interactively edited file should be kept (not erased)
and a new temp file is generated using the old one.
*)
let pr = Task.task_goal task in
let fn = match pr.pr_name.id_loc with
| Some loc -> let fn,_,_,_ = Loc.get loc in Filename.basename fn
| None -> "" in
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
true, get_filename drv fn "T" pr.pr_name.id_string
| _ ->
(* Example: cvc4 without ?save_to argument
No file were provided. We have to generate a new one.
*)
let pr = Task.task_goal task in
let fn = match pr.pr_name.id_loc with
| Some loc -> let fn,_,_,_ = Loc.get loc in Filename.basename fn
| None -> "" in
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
get_filename drv fn "T" pr.pr_name.id_string
true, get_filename drv fn "T" pr.pr_name.id_string
let prove_task_prepared ~command ~limit ?old ?inplace drv task =
let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
let gen_new_file, filename =
file_name_of_task ?old ?inplace ?interactive drv task in
let old_channel = Opt.map open_in old in
let filename = file_name_of_task ?old ?inplace drv task in
let printer_mapping = print_task_prepared ?old:old_channel drv fmt task in
pp_print_flush fmt ();
Opt.iter close_in old_channel;
let res =
call_on_buffer ~command ~limit
call_on_buffer ~command ~limit ~gen_new_file
?inplace ~filename ~printer_mapping drv buf in
Buffer.reset buf;
res
let prove_task ~command ~limit ?(cntexample=false) ?old
?inplace drv task =
?inplace ?interactive drv task =
let task = prepare_task ~cntexample drv task in
prove_task_prepared ~command ~limit ?old ?inplace drv task
prove_task_prepared ~command ~limit ?interactive ?old ?inplace drv task
(* exception report *)
......
......@@ -37,6 +37,7 @@ val file_of_theory : driver -> string -> Theory.theory -> string
val call_on_buffer :
command : string ->
limit : Call_provers.resource_limit ->
gen_new_file : bool ->
?inplace : bool ->
filename : string ->
printer_mapping : Printer.printer_mapping ->
......@@ -59,6 +60,7 @@ val prove_task :
?cntexample : bool ->
?old : string ->
?inplace : bool ->
?interactive : bool ->
driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
......@@ -73,6 +75,7 @@ val prove_task_prepared :
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
?interactive : bool ->
driver -> Task.task -> Call_provers.prover_call
......
......@@ -366,10 +366,11 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
Debug.dprintf debug_sched "[build_prover_call] Script file = %a@."
(Pp.print_option Pp.string) proof_script;
let inplace = config_pr.Whyconf.in_place in
let interactive = config_pr.Whyconf.interactive in
try
let call =
Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace ~command
~limit driver task
~limit ~interactive driver task
in
let pa = (c.controller_session,id,pr,callback,false,call,ores) in
Hashtbl.replace prover_tasks_in_progress call pa
......@@ -496,7 +497,7 @@ let run_timeout_handler () =
S.timeout ~ms:default_delay_ms timeout_handler;
end
let schedule_proof_attempt c id pr
let schedule_proof_attempt c id pr ?save_to
~counterexmp ~limit ~callback ~notification =
let ses = c.controller_session in
let callback panid s =
......@@ -534,12 +535,16 @@ let schedule_proof_attempt c id pr
let interactive = config_pr.Whyconf.interactive in
let use_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let limit = adapt_limits ~interactive ~use_steps limit a in
let script = Opt.map (fun s ->
let script =
if save_to = None then
Opt.map (fun s ->
Debug.dprintf debug_sched "Script file = %s@." s;
Filename.concat (get_dir ses) s) a.proof_script
else
save_to
in
limit, old_res, script
with Not_found | Session_itp.BadID -> limit,None,None
with Not_found | Session_itp.BadID -> limit,None,save_to
in
let panid = graft_proof_attempt ~limit ses id pr in
Queue.add (c,id,pr,adaptlimit,proof_script,callback panid,counterexmp,ores)
......@@ -740,7 +745,7 @@ let run_strategy_on_goal
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
schedule_proof_attempt c g p ~counterexmp ~limit ~callback ~notification
schedule_proof_attempt c g p ?save_to:None ~counterexmp ~limit ~callback ~notification
| Itransform(trname,pcsuccess) ->
let callback ntr =
callback_tr trname [] ntr;
......@@ -856,7 +861,7 @@ let rec copy_rec ~notification ~callback_pa ~callback_tr c from_any to_any =
*)
| APn from_pn, APn to_pn ->
let from_pa_list = get_proof_attempts s from_pn in
List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn ~counterexmp:false
List.iter (fun x -> schedule_pa_with_same_arguments ?save_to:None c x to_pn ~counterexmp:false
~callback:callback_pa ~notification) from_pa_list;
let from_tr_list = get_transformations s from_pn in
let callback x tr args st = callback_tr tr args st;
......@@ -952,7 +957,7 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
try
if pr' <> pr then callback id (UpgradeProver pr');
let _ = get_task c.controller_session parid in
schedule_proof_attempt c parid pr' ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt ?save_to:None c parid pr' ~counterexmp:false ~limit ~callback ~notification
with Not_found ->
callback id Detached
......@@ -1151,7 +1156,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
Call_provers.print_prover_result res
end
in
schedule_proof_attempt c pn prover ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt ?save_to:None c pn prover ~counterexmp:false ~limit ~callback ~notification
| _ -> assert false
end
in
......@@ -1231,7 +1236,7 @@ later on. We do has if proof fails. *)
in
Debug.dprintf
debug "[Bisect] running the prover on subtask@.";
schedule_proof_attempt c pn prover ~counterexmp:false ~limit ~callback ~notification
schedule_proof_attempt ?save_to:None c pn prover ~counterexmp:false ~limit ~callback ~notification
| _ -> assert false
end
in
......
......@@ -197,6 +197,7 @@ val schedule_proof_attempt :
controller ->
proofNodeID ->
Whyconf.prover ->
?save_to:string ->
counterexmp:bool ->
limit:Call_provers.resource_limit ->
callback:(proofAttemptID -> proof_attempt_status -> unit) ->
......@@ -206,7 +207,10 @@ val schedule_proof_attempt :
time limit [timelimit]; the function [callback] will be called each
time the proof attempt status changes. Typically at Scheduled, then
Running, then Done. If there is already a proof attempt with [p] it
is updated. *)
is updated.
[save_to] is used to give a location for the file generated for the prover
( *.smt2). With debug flag keep_vcs, the file are saved at this location.
*)
val schedule_edition :
controller ->
......
......@@ -1055,7 +1055,7 @@ end
let prover = p.Whyconf.prover in
let callback = callback_update_tree_proof d.cont in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
List.iter (fun id -> C.schedule_proof_attempt d.cont id prover ~counterexmp
List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id prover ~counterexmp
~limit ~callback ~notification:(notify_change_proved d.cont))
unproven_goals
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment