benchrc.ml 8.77 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
(*    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
22
open Why3
23 24 25 26
open Util
open Theory


27 28
type id_tool = (string * string)
type id_prob = (string * string * string)
29

30 31 32
type benchrc = { tools : tool list Mstr.t;
                 probs : prob list Mstr.t;
                 benchs : bench Mstr.t
33 34 35 36 37
               }

open Whyconf
open Rc

38
let absolute_filename dirname f =
François Bobot's avatar
François Bobot committed
39
  if f = "-" then f else
40 41 42 43 44
  if Filename.is_relative f then
    Filename.concat dirname f
  else
    f

45 46 47 48
let lookup_transf t =
  if Db.is_initialized () then Some (Db.transf_from_name t) else None


49
let read_tools absf wc map (name,section) =
50 51 52 53 54 55 56 57
  (* 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 *)
58
  let env = Env.create_env loadpath in
59 60
  (* transformations *)
  let transforms = get_stringl ~default:[] section "transform" in
61
  let lookup acc t = (Trans.lookup_transform t env, lookup_transf t)::acc in
62 63
  let transforms = List.fold_left lookup [] transforms in
  let transforms = List.rev transforms in
64 65
  (* use *)
  let use = get_stringl ~default:[] section "use" in
66
  let load_use s =
67 68 69
    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
70 71 72 73 74
    Env.find_theory env file th,
    if Db.is_initialized () then
      Some (Db.transf_from_name (Printf.sprintf "use %s" s))
    else None in
  let use = List.map load_use use in
75 76 77
  (* provers *)
  let provers = get_stringl ~default:[] section "prover" in
  let find_provers s =
78
    try let p = prover_by_id wc s in
79 80 81 82 83 84 85 86 87
        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
88
      ("driver",absf driver,command) :: provers
89 90 91 92
    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) =
93
    { tval = {Bench.tool_name = name; prover_name = n; tool_db =
94
        if Db.is_initialized () then Some (Db.prover_from_name n) else None};
95 96 97 98 99 100 101 102 103 104
      ttrans = transforms;
      tdriver = driver;
      tcommand = command;
      tenv = env;
      tuse = use;
      ttime = timelimit;
      tmem = memlimit
    } in
  Mstr.add name (List.map create_tool provers) map

105 106 107 108 109 110
let use_before_goal th = function
  | Some {Task.task_decl = tdecl; task_prev = task} ->
    Task.add_tdecl (Task.use_export task th) tdecl
  | _ -> assert false

let apply_use_before_goal (task,goal_id) (th_use,th_use_id) =
111
  let task = use_before_goal th_use task in
112 113 114 115
  let goal_id = match goal_id, th_use_id with
    | Some goal_id, Some th_use_id ->
      Some begin
        let transf =
116 117 118
          try Db.Htransf.find (Db.transformations goal_id) th_use_id
          with Not_found ->
            Db.add_transformation goal_id th_use_id  in
119 120
        let name2 = (Task.task_goal task).Decl.pr_name.Ident.id_string in
        let md5_2 = BenchUtil.task_checksum task in
121 122 123
        try Mstr.find md5_2 (Db.subgoals transf)
        with Not_found ->
          Db.add_subgoal transf name2 md5_2
124 125 126 127 128 129 130 131 132 133 134 135 136
      end
    | _,_ -> None in
  (task,goal_id)

let gen_from_file ~format ~prob_name ~file_path ~file_name env lth =
    try
      let theories =
        let file_name, cin = match file_path with
          | "-" -> "stdin", stdin
          | f   -> file_name, open_in f
        in
        let m = Env.read_channel ?format:format env file_name cin in
        close_in cin;
137
        Mstr.bindings m in
138 139 140 141
      let file_id = if Db.is_initialized () then
          let file_db = Sysutil.relativize_filename
            (Filename.dirname (Db.db_name ())) file_path in
          Some
142 143 144
          (try fst (List.find (fun (_,x) -> file_db = x) (Db.files ()))
           with Not_found ->
             Db.add_file file_db)
145 146 147
        else None in
      let map (th_name,th) =
        let theory_id = option_map (fun file_id ->
148 149 150
          try Mstr.find th_name (Db.theories file_id)
          with Not_found ->
            Db.add_theory file_id th_name
151 152 153 154 155 156
        ) file_id in
        (* TODO make DB aware of the env *)
        let tasks = Task.split_theory th None None in
        let map task =
          let goal_id = option_map (fun theory_id ->
            let name = (Task.task_goal task).Decl.pr_name.Ident.id_string in
157 158
            try Mstr.find name (Db.goals theory_id)
            with Not_found ->
159
              Db.add_goal theory_id name (BenchUtil.task_checksum task)
160 161 162 163 164 165 166 167 168
          ) theory_id in
          let (task,goal_id) = List.fold_left apply_use_before_goal
            (task,goal_id) lth in
          {prob_name = prob_name;prob_file = file_name; prob_theory = th_name;
           prob_db = goal_id}, task in
        List.rev_map map tasks in
      list_flatten_rev (List.rev_map map theories)
    with exn -> eprintf "%a@." Exn_printer.exn_printer exn; exit 1

169
let read_probs absf map (name,section) =
170 171 172
  (* transformations *)
  let transforms = get_stringl ~default:[] section "transform" in
  let gen_trans env =
173 174
    let lookup acc t =
      ((try Trans.singleton (Trans.lookup_transform t env) with
175 176
          Trans.UnknownTrans _ -> Trans.lookup_transform_l t env),
       lookup_transf t)::acc
177
    in
178 179
    let transforms = List.fold_left lookup [] transforms in
    List.rev transforms
180 181 182 183 184
  in
  (* format *)
  let format = get_stringo section "format" in
  (* files *)
  let files = get_stringl ~default:[] section "file" in
185 186
  Mstr.add name
    (List.rev_map
187 188 189 190
       (fun file ->
         { ptask   = gen_from_file ~format ~prob_name:name
             ~file_path:(absf file) ~file_name:file;
           ptrans   = gen_trans}) files)
191
    map
192

François Bobot's avatar
François Bobot committed
193
let read_bench absf mtools mprobs map (name,section) =
194 195
  let tools = get_stringl section "tools" in
  let lookup s =
196 197
    try Mstr.find s mtools
    with Not_found -> eprintf "Undefined tools %s@." s;
198 199 200 201
      exit 1 in
  let tools = list_flatten_rev (List.map lookup tools) in
  let probs = get_stringl section "probs" in
  let lookup s =
202 203
    try Mstr.find s mprobs
    with Not_found -> eprintf "Undefined probs %s@." s;
204
      exit 1 in
205
  let probs = list_flatten_rev (List.map lookup probs) in
François Bobot's avatar
François Bobot committed
206 207 208 209 210 211 212 213 214 215 216 217 218 219
  let averages = get_stringl ~default:[] section "average" in
  let outputs = List.fold_left
    (cons (fun s -> Average (absf s)))
    [] averages in
  let timelines = get_stringl ~default:[] section "timeline" in
  let outputs = List.fold_left
    (cons (fun s -> Timeline (absf s)))
    outputs timelines in
  let csvs = get_stringl ~default:[] section "csv" in
  let outputs = List.fold_left
    (cons (fun s -> Csv (absf s)))
    outputs csvs in
  Mstr.add name
    { bname = name; btools = tools; bprobs = probs; boutputs = outputs} map
220 221 222 223


let read_file wc f =
  let rc = from_file f in
224
  let absf = absolute_filename (Filename.dirname f) in
225
  let tools = get_family rc "tools" in
226
  let tools = List.fold_left (read_tools absf wc) Mstr.empty tools in
227
  let probs = get_family rc "probs" in
228
  let probs = List.fold_left (read_probs absf) Mstr.empty probs in
229
  let benchs = get_family rc "bench" in
François Bobot's avatar
François Bobot committed
230
  let benchs = List.fold_left (read_bench absf tools probs)
231
    Mstr.empty benchs in
232 233 234
  {tools = tools;
   probs = probs;
   benchs = benchs}