Skip to content
Snippets Groups Projects
Commit 1cf513ad authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

[SAVer] Separated answer computation from answer printing.

parent 844b2017
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 120 additions and 113 deletions
src/verification.ml
+ 120
− 113
View file @ 1cf513ad
......@@ -55,128 +55,135 @@ let combine_prover_answers answers =
| Call_provers.Valid, r | r, Call_provers.Valid -> r
| _ -> acc)
let handle_task_saver task env dataset_csv command =
let answer_saver limit config task env prover dataset_csv =
let open Why3 in
let dataset_filename =
match dataset_csv with
| Some s -> s
| None -> failwith "Error, no dataset provided for SAVer."
let handle_task_saver task env dataset_csv command =
let dataset_filename =
match dataset_csv with
| Some s -> s
| None -> failwith "Error, no dataset provided for SAVer."
in
let goal = Task.task_goal_fmla task in
let eps, svm_filename =
match goal.t_node with
| Tquant (Tforall, b) -> (
let _, _, pred = Term.t_open_quant b in
let svm_t = Pmodule.read_module env [ "caisar" ] "SVM" in
let robust_to_predicate =
let open Theory in
ns_find_ls svm_t.mod_theory.th_export [ "robust_to" ]
in
match pred.t_node with
| Term.Tapp
( ls,
[
{ t_node = Tapp (svm_app_sym, _); _ };
_;
{ t_node = Tconst e; _ };
] ) ->
if Term.ls_equal ls robust_to_predicate
then
let eps = Fmt.str "%a" Constant.print_def e in
let svm_filename =
match Language.lookup_loaded_svms svm_app_sym with
| Some t -> t.filename
| None -> failwith "Svm file not found in environment."
in
(eps, svm_filename)
else failwith "Wrong predicate found."
(* no other predicate than robust_to is supported *)
| _ -> failwith "Unsupported by SAVer.")
| _ -> failwith "Unsupported by SAVer."
in
let svm_file = Filename.concat (Caml.Sys.getcwd ()) svm_filename in
let dataset_file = Filename.concat (Caml.Sys.getcwd ()) dataset_filename in
let command = Re__Core.replace_string svm ~by:svm_file command in
let command = Re__Core.replace_string dataset ~by:dataset_file command in
let command = Re__Core.replace_string epsilon ~by:eps command in
command
in
let command = Whyconf.get_complete_command ~with_steps:false prover in
let command = handle_task_saver task env dataset_csv command in
let res_parser =
{
Call_provers.prp_regexps =
[ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
prp_timeregexps = [];
prp_stepregexps = [];
prp_exitcodes = [];
prp_model_parser = Model_parser.lookup_model_parser "no_model";
}
in
let prover_call =
Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
~filename:"foo.txt" ~get_counterexmp:false ~gen_new_file:false
~printing_info:Printer.default_printing_info (Buffer.create 10)
in
let goal = Task.task_goal_fmla task in
let eps, svm_filename =
match goal.t_node with
| Tquant (Tforall, b) -> (
let _, _, pred = Term.t_open_quant b in
let svm_t = Pmodule.read_module env [ "caisar" ] "SVM" in
let robust_to_predicate =
let open Theory in
ns_find_ls svm_t.mod_theory.th_export [ "robust_to" ]
let prover_result = Call_provers.wait_on_call prover_call in
let answer =
match prover_result.pr_answer with
| Call_provers.HighFailure -> (
let pr_output = prover_result.pr_output in
let matcher =
Re__Pcre.regexp
"\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*\\d+\\s*(\\d+)\\s*\\d"
in
match pred.t_node with
| Term.Tapp
( ls,
[
{ t_node = Tapp (svm_app_sym, _); _ }; _; { t_node = Tconst e; _ };
] ) ->
if Term.ls_equal ls robust_to_predicate
then
let eps = Fmt.str "%a" Constant.print_def e in
let svm_filename =
match Language.lookup_loaded_svms svm_app_sym with
| Some t -> t.filename
| None -> failwith "Svm file not found in environment."
in
(eps, svm_filename)
else failwith "Wrong predicate found."
(* no other predicate than robust_to is supported *)
| _ -> failwith "Unsupported by SAVer.")
| _ -> failwith "Unsupported by SAVer."
match Re__Core.exec_opt matcher pr_output with
| Some g ->
if Int.of_string (Re__Core.Group.get g 1)
= Int.of_string (Re__Core.Group.get g 2)
then Call_provers.Valid
else Call_provers.Invalid
| None -> Call_provers.HighFailure
(* Any other answer than HighFailure should
* never happen as we do not define
* anything in SAVer's driver *))
| _ -> assert false
in
let svm_file = Filename.concat (Caml.Sys.getcwd ()) svm_filename in
let dataset_file = Filename.concat (Caml.Sys.getcwd ()) dataset_filename in
let command = Re__Core.replace_string svm ~by:svm_file command in
let command = Re__Core.replace_string dataset ~by:dataset_file command in
let command = Re__Core.replace_string epsilon ~by:eps command in
command
answer
let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
dataset_csv task =
let answer_generic limit config task driver
(prover : Why3.Whyconf.config_prover) =
let open Why3 in
if String.equal prover.prover.prover_name "SAVer"
then
let command = Whyconf.get_complete_command ~with_steps:false prover in
let command = handle_task_saver task env dataset_csv command in
let res_parser =
{
Call_provers.prp_regexps =
[ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
prp_timeregexps = [];
prp_stepregexps = [];
prp_exitcodes = [];
prp_model_parser = Model_parser.lookup_model_parser "no_model";
}
in
let task_prepared = Driver.prepare_task driver task in
let tasks =
(* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
if String.equal prover.prover.prover_name "Marabou"
then Trans.apply Split_goal.split_goal_full task_prepared
else [ task_prepared ]
in
let command = Whyconf.get_complete_command ~with_steps:false prover in
let nn_file =
match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
| Some [ MAstr nn_file ] -> nn_file
| Some _ -> assert false (* By construction of the meta. *)
| None -> invalid_arg (Fmt.str "No neural network model found in task")
in
let nn_file = Unix.realpath nn_file in
let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
let call_prover_on_task task_prepared =
let prover_call =
Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
~filename:"foo.txt" ~get_counterexmp:false ~gen_new_file:false
~printing_info:Printer.default_printing_info (Buffer.create 10)
Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
in
let prover_result = Call_provers.wait_on_call prover_call in
let answer =
match prover_result.pr_answer with
| Call_provers.HighFailure -> (
let pr_output = prover_result.pr_output in
let matcher =
Re__Pcre.regexp
"\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*\\d+\\s*(\\d+)\\s*\\d"
in
match Re__Core.exec_opt matcher pr_output with
| Some g ->
if Int.of_string (Re__Core.Group.get g 1)
= Int.of_string (Re__Core.Group.get g 2)
then Call_provers.Valid
else Call_provers.Invalid
| None -> Call_provers.HighFailure
(* Any other answer than HighFailure should
* never happen as we do not define
* anything in SAVer's driver *))
| _ -> assert false
in
Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
Call_provers.print_prover_answer answer
else
let task_prepared = Driver.prepare_task driver task in
let tasks =
(* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
if String.equal prover.prover.prover_name "Marabou"
then Trans.apply Split_goal.split_goal_full task_prepared
else [ task_prepared ]
in
let command = Whyconf.get_complete_command ~with_steps:false prover in
let nn_file =
match
Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared
with
| Some [ MAstr nn_file ] -> nn_file
| Some _ -> assert false (* By construction of the meta. *)
| None -> invalid_arg (Fmt.str "No neural network model found in task")
in
let nn_file = Unix.realpath nn_file in
let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
let call_prover_on_task task_prepared =
let prover_call =
Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
in
let prover_result = Call_provers.wait_on_call prover_call in
prover_result.pr_answer
in
let answers = List.map tasks ~f:call_prover_on_task in
let answer = combine_prover_answers answers in
Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
Call_provers.print_prover_answer answer
prover_result.pr_answer
in
let answers = List.map tasks ~f:call_prover_on_task in
let answer = combine_prover_answers answers in
answer
let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
dataset_csv task =
let open Why3 in
let prover_answer =
if String.equal prover.prover.prover_name "SAVer"
then answer_saver limit config task env prover dataset_csv
else answer_generic limit config task driver prover
in
Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
Call_provers.print_prover_answer prover_answer
let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
~dataset_csv file =
......
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