benchrc : A way to describe bench

Makefile.in

@@ -455,7 +455,7 @@ endif
 # BENCH
 ###############
 
-BENCH_FILES = bench whybench
+BENCH_FILES = bench whybench benchrc
 
 BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
 

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

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 *)
 }
 
 

src/bench/benchrc.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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}

src/bench/benchrc.mli

+
+
+(**
+
+[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

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
 

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 *)
 

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
 

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

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