From 22cfca3f05bab065477a8b8eb1e4971b140e7edc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 8 Dec 2010 09:25:46 +0100 Subject: [PATCH] benchrc : A way to describe bench --- Makefile.in | 2 +- src/bench/bench.ml | 5 +- src/bench/bench.mli | 3 +- src/bench/benchrc.ml | 166 ++++++++++++++++++++++++++++++++++++++++++ src/bench/benchrc.mli | 68 +++++++++++++++++ src/bench/whybench.ml | 3 +- src/util/rc.mli | 6 ++ src/util/rc.mll | 22 ++++-- src/util/util.ml | 13 ++++ src/util/util.mli | 5 ++ 10 files changed, 282 insertions(+), 11 deletions(-) create mode 100644 src/bench/benchrc.ml create mode 100644 src/bench/benchrc.mli diff --git a/Makefile.in b/Makefile.in index f690f4323..81e68af3b 100644 --- a/Makefile.in +++ b/Makefile.in @@ -455,7 +455,7 @@ endif # BENCH ############### -BENCH_FILES = bench whybench +BENCH_FILES = bench whybench benchrc BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES)) diff --git a/src/bench/bench.ml b/src/bench/bench.ml index 4bffaf73c..1e47fb5a6 100644 --- a/src/bench/bench.ml +++ b/src/bench/bench.ml @@ -40,7 +40,7 @@ type 'a tool = { type 'a prob = { ptask : env -> task -> ('a * task) list; (** needed for tenv *) - ptrans : task list trans; + ptrans : env -> task list trans; } type ('a,'b) result = {tool : 'a; @@ -103,7 +103,8 @@ let call s callback tool prob = (** Apply trans *) let iter_task (pval,task) = MTask.start s; - let trans = Trans.compose_l prob.ptrans (Trans.singleton tool.ttrans) in + let trans = Trans.compose_l (prob.ptrans tool.tenv) + (Trans.singleton tool.ttrans) in apply_transformation_l ~callback:(trans_cb pval) trans task in (** Split *) let ths = prob.ptask tool.tenv tool.tuse in diff --git a/src/bench/bench.mli b/src/bench/bench.mli index e4e345fb7..e122931cf 100644 --- a/src/bench/bench.mli +++ b/src/bench/bench.mli @@ -40,7 +40,8 @@ type 'a tool = { type 'a prob = { ptask : env -> task -> ('a * task) list; (** needed for tenv and tuse *) - ptrans : task list trans; + ptrans : env -> task list trans; (** perhaps should be merged in + ptask *) } diff --git a/src/bench/benchrc.ml b/src/bench/benchrc.ml new file mode 100644 index 000000000..cac538e69 --- /dev/null +++ b/src/bench/benchrc.ml @@ -0,0 +1,166 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010- *) +(* Francois Bobot *) +(* Jean-Christophe Filliatre *) +(* Johannes Kanig *) +(* 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. *) +(* *) +(**************************************************************************) + +open Format +open Bench +open Why +open Util +open Theory + +type output = + (** on stdout *) + |Average + |Timeline + (** In a file *) + |Csv + +type bench = + { + (* tool_name, prover_name *) + btools : (string * string) tool list; + (* prob_name, file_name, theory name *) + bprobs : (string * string * string) prob list; + boutputs : output list; + } + +type benchrc = { tools : (string * string) tool list Mstr.t; + probs : (string * string * string) prob Mstr.t; + benchs : bench Mstr.t; + } + +open Whyconf +open Rc + +let read_tools wc map (name,section) = + (* loadpath *) + let wc_main = get_main wc in + let loadpath = get_stringl ~default:[] section "loadpath" in + let loadpath = List.append loadpath (Whyconf.loadpath wc_main) in + (* limit *) + let timelimit = get_int ~default:(timelimit wc_main) section "timelimit" in + let memlimit = get_int ~default:(memlimit wc_main) section "memlimit" in + (* env *) + let env = Env.create_env (Lexer.retrieve loadpath) in + (* transformations *) + let transforms = get_stringl ~default:[] section "transform" in + let lookup acc t = Trans.compose (Trans.lookup_transform t env) acc in + let transforms = List.fold_left lookup Trans.identity transforms + in + (* use *) + let use = get_stringl ~default:[] section "use" in + let load_use task s = + let file,th = match Util.split_string_rev s '.' with + | [] | [_] -> eprintf "Bad theory qualifier %s" s; exit 1 + | a::l -> List.rev l,a in + let th = Env.find_theory env file th in + Task.use_export task th in + let use = List.fold_left load_use None use in + (* provers *) + let provers = get_stringl ~default:[] section "prover" in + let find_provers s = + try let p = Mstr.find s (get_provers wc) in + s,p.driver ,p.command + with + (* TODO add exceptions pehaps inside rc.ml in fact*) + | Not_found -> eprintf "Prover %s not found.@." s; exit 1 in + let provers = List.map find_provers provers in + let provers = + try + let driver = get_string section "driver" in + let command = get_string section "command" in + ("driver",driver,command) :: provers + with MissingField _ -> provers in + let load_driver (n,d,c) = n,Driver.load_driver env d,c in + let provers = List.map load_driver provers in + let create_tool (n,driver,command) = + { tval = name,n ; + ttrans = transforms; + tdriver = driver; + tcommand = command; + tenv = env; + tuse = use; + ttime = timelimit; + tmem = memlimit + } in + Mstr.add name (List.map create_tool provers) map + +let read_probs map (name,section) = + (* transformations *) + let transforms = get_stringl ~default:[] section "transform" in + let gen_trans env = + let lookup acc t = Trans.compose_l + (try Trans.singleton (Trans.lookup_transform t env) with + Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) acc + in + let transforms = List.fold_left lookup Trans.identity_l transforms in + transforms + in + (* format *) + let format = get_stringo section "format" in + (* files *) + let files = get_stringl ~default:[] section "file" in + let gen env task = + let fwhy () = + let read_one fname = + let cin = open_in fname in + let m = Env.read_channel ?format:format env fname cin in + close_in cin; + let ths = Mnm.bindings m in + List.rev_map (fun (n,th) -> ((name,fname,n),th)) ths + in + let map (name,th) = name,Task.split_theory th None task in + let fold acc (n,l) = + List.rev_append (List.rev_map (fun v -> (n,v)) l) acc in + files |> List.map read_one |> list_flatten_rev + |> List.rev_map map |> List.fold_left fold [] in + Scheduler.do_why_sync fwhy () in + Mstr.add name { ptask = gen; ptrans = gen_trans} map + +let read_bench mtools mprobs map (name,section) = + let tools = get_stringl section "tools" in + let lookup s = + try Mstr.find s mtools with Not_found -> eprintf "Undefined tools %s@." s; + exit 1 in + let tools = list_flatten_rev (List.map lookup tools) in + let probs = get_stringl section "probs" in + let lookup s = + try Mstr.find s mprobs with Not_found -> eprintf "Undefined probs %s@." s; + exit 1 in + let probs = List.map lookup probs in + let outputs = get_stringl ~default:[] section "probs" in + let check = function + | "average" -> Average + | "timeline" -> Timeline + | "csv" -> Csv + | s -> eprintf "Unknown output %s" s; exit 1 in + let outputs = List.map check outputs in + Mstr.add name { btools = tools; bprobs = probs; boutputs = outputs} map + + +let read_file wc f = + let rc = from_file f in + let tools = get_family rc "tools" in + let tools = List.fold_left (read_tools wc) Mstr.empty tools in + let probs = get_family rc "probs" in + let probs = List.fold_left read_probs Mstr.empty probs in + let benchs = get_family rc "bench" in + let benchs = List.fold_left (read_bench tools probs) Mstr.empty benchs in + {tools = tools; + probs = probs; + benchs = benchs} diff --git a/src/bench/benchrc.mli b/src/bench/benchrc.mli new file mode 100644 index 000000000..bde6c7af1 --- /dev/null +++ b/src/bench/benchrc.mli @@ -0,0 +1,68 @@ + + +(** + +[probs "myprobs"] + file = "examples/monbut.why" #relatives to the rc file + file = "examples/monprogram.mlw" + theory = "monprogram.T" + goal = "monbut.T.G" + + transform = "split_goal" #applied in the order + transform = "..." + transform = "..." + +[tools "mytools"] +prover = cvc3 +prover = altergo +#or only one +driver = "..." +command = "..." + +loadpath = "..." #added to the one in why.conf +loadpath = "..." + +timelimit = 30 +memlimit = 300 + +use = "toto.T" #use the theory toto (allow to add metas) + +transform = "simplify_array" #only 1 to 1 + +[bench "mybench"] +tools = "mytools" +tools = ... +probs = "myprobs" +probs = ... +output = "csv" +output = "average" +output = "timeline" +*) + +open Bench +open Why +open Util + +type output = + (** on stdout *) + |Average + |Timeline + (** In a file *) + |Csv + + +type bench = + { + (* tool_name, prover_name *) + btools : (string * string) tool list; + (* prob_name, file_name, theory name *) + bprobs : (string * string * string) prob list; + boutputs : output list; + } + +type benchrc = { tools : (string * string) tool list Mstr.t; + probs : (string * string * string) prob Mstr.t; + benchs : bench Mstr.t + } + +val read_file : Whyconf.config -> string -> benchrc diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml index c49d1d91d..6519b0a48 100644 --- a/src/bench/whybench.ml +++ b/src/bench/whybench.ml @@ -331,9 +331,8 @@ let () = (* let memo = Trans.store (fun task -> gen env task) in *) (* Trans.apply memo) in *) let gen _ _ = tlist in - let gen env task = Scheduler.do_why_sync (gen env) task in { B.ptask = gen; - ptrans = transl; + ptrans = fun _ -> transl; }::acc in probs := Queue.fold fold_prob [] opt_queue diff --git a/src/util/rc.mli b/src/util/rc.mli index 4c3f2f72b..ee55d717f 100644 --- a/src/util/rc.mli +++ b/src/util/rc.mli @@ -104,6 +104,8 @@ val get_int : ?default:int -> section -> string -> int @raise Multiple_value if the key appears multiple time. *) +val get_into : section -> string -> int option + val get_intl : ?default:int list -> section -> string -> int list (** [get_intl ~default section key] one key to many value @@ -131,6 +133,8 @@ val get_bool : ?default:bool -> section -> string -> bool val get_booll : ?default:bool list -> section -> string -> bool list (** Same as {!get_intl} but on bool *) +val get_boolo : section -> string -> bool option + val set_bool : section -> string -> bool -> section (** Same as {!set_int} but on bool *) @@ -144,6 +148,8 @@ val get_string : ?default:string -> section -> string -> string val get_stringl : ?default:string list -> section -> string -> string list (** Same as {!get_intl} but on string *) +val get_stringo : section -> string -> string option + val set_string : section -> string -> string -> section (** Same as {!set_int} but on string *) diff --git a/src/util/rc.mll b/src/util/rc.mll index d6183d54c..447faf212 100644 --- a/src/util/rc.mll +++ b/src/util/rc.mll @@ -148,18 +148,26 @@ let set_family t sname sections = let set (arg,section) = (Some arg,section) in Mstr.add sname (List.map set sections) t +let get_value read section key = + let l = Mstr.find key section in + match l with + | [] -> assert false + | [v] -> read key v + | v1::v2::_ -> raise (DuplicateField (key,v1,v2)) + let get_value read ?default section key = try - let l = Mstr.find key section in - match l with - | [] -> assert false - | [v] -> read key v - | v1::v2::_ -> raise (DuplicateField (key,v1,v2)) + get_value read section key with Not_found -> match default with | None -> raise (MissingField key) | Some v -> v +let get_valueo read section key = + try + Some (get_value read section key) + with Not_found -> None + let get_valuel read ?default section key = try let l = Mstr.find key section in @@ -196,16 +204,20 @@ let wstring s = RCstring s let get_int = get_value rint let get_intl = get_valuel rint +let get_into = get_valueo rint + let set_int = set_value wint let set_intl = set_valuel wint let get_bool = get_value rbool let get_booll = get_valuel rbool +let get_boolo = get_valueo rbool let set_bool = set_value wbool let set_booll = set_valuel wbool let get_string = get_value rstring let get_stringl = get_valuel rstring +let get_stringo = get_valueo rstring let set_string = set_value wstring let set_stringl = set_valuel wstring diff --git a/src/util/util.ml b/src/util/util.ml index ebef3d5e7..d5d1f090a 100644 --- a/src/util/util.ml +++ b/src/util/util.ml @@ -118,6 +118,9 @@ let list_compare cmp l1 l2 = match l1,l2 with | a1::l1, a2::l2 -> let c = cmp a1 a2 in if c = 0 then compare l1 l2 else c +let list_flatten_rev fl = + List.fold_left (fun acc l -> List.rev_append l acc) [] fl + (* boolean fold accumulators *) exception FoldSkip @@ -129,6 +132,16 @@ let any_fn pr _ t = pr t && raise FoldSkip let ttrue _ = true let ffalse _ = false +(* useful function on string *) +let split_string_rev s c = + let rec aux acc i = + try + let j = String.index_from s i c in + aux ((String.sub s i (j-i))::acc) (j + 1) + with Not_found -> (String.sub s i (String.length s - i))::acc + | Invalid_argument _ -> ""::acc in + aux [] 0 + (* Set and Map on ints and strings *) module Int = struct type t = int let compare = Pervasives.compare end diff --git a/src/util/util.mli b/src/util/util.mli index f747f6564..1db119ebc 100644 --- a/src/util/util.mli +++ b/src/util/util.mli @@ -89,6 +89,8 @@ val list_fold_product_l : val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int +val list_flatten_rev : 'a list list -> 'a list + (* boolean fold accumulators *) exception FoldSkip @@ -105,6 +107,9 @@ val ffalse : 'a -> bool val ttrue : 'a -> bool (** [ttrue] constant function [true] *) +(* useful function on string *) +val split_string_rev : string -> char -> string list + (* Set and Map on ints and strings *) module Mint : Map.S with type key = int -- GitLab