Commit 5a3641ec authored by François Bobot's avatar François Bobot

new prover identification: remove id

       Remove the id in prover that is used only for command-line, use
       instead the name,version,alternative of the prover. One can
       also use regular expression (start with ^).

       "Alt-Ergo,0.92,with arrays" corresponds only to one prover
       "Alt-Ergo,^0\.9.*,with arrays" correspond to all the Alt-Ergo prover with arrays which version match "0\.9.*"
       "Alt-Ergo" is the same thing than "Alt-Ergo,^,^"
       "Alt-Ergo,0.92," corresponds only to one prover with the alternate fields empty
       "Alt-Ergo,,with arrays" corresponds to "Alt-Ergo,^,with arrays" since the version is never empty.

       Provers identification are case sensitive even if it is
       currently more complicated for the user because
       case-insensitiveness is not sufficient. Specifiying "alt-ergo"
       for "Alt-Ergo,^,^" is great, but not if there is more than one
       match. A more general system of shortcut would be more
       appropriate.
parent 043a5bcd
......@@ -87,10 +87,10 @@ bad_programs () {
valid_goals () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgml -L modules -t 10 -P alt-ergo $f | grep -q -v Valid; then
if $pgml -L modules -t 10 -P Alt-Ergo $f | grep -q -v Valid; then
echo "valid test $f failed!"
echo "$pgml -P alt-ergo $f"
$pgml -L modules -t 10 -P alt-ergo $f
$pgml -L modules -t 10 -P Alt-Ergo $f
exit 1
else
echo "ok"
......
......@@ -76,12 +76,15 @@ let main : Whyconf.main = Whyconf.get_main config
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
(* the [prover alt-ergo] section of the config file *)
(* One prover named Alt-Ergo in the config file *)
let alt_ergo : Whyconf.config_prover =
try
Whyconf.prover_by_id config "alt-ergo"
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
(** all the prover that have the name "Alt-Ergo" *)
let provers = Whyconf.filter_provers config fp in
snd (Whyconf.Mprover.choose provers)
with Whyconf.ProverNotFound _ ->
eprintf "Prover alt-ergo not installed or not configured@.";
eprintf "Prover Alt-Ergo not installed or not configured@.";
exit 0
(*
......
......@@ -56,7 +56,8 @@ let rec goal whyconf env path dbgoal wgoal =
let prover_name = Db.prover_name prover_id in
let driver, extra, command =
try
let p = Whyconf.prover_by_id whyconf prover_name in
let p = Whyconf.filter_one_prover whyconf
(Whyconf.parse_filter_prover prover_name) in
p.Whyconf.driver, p.Whyconf.extra_drivers,
String.concat " " (p.Whyconf.command :: p.Whyconf.extra_options)
with
......
......@@ -76,12 +76,9 @@ let read_tools absf wc map (name,section) =
(* provers *)
let provers = get_stringl ~default:[] section "prover" in
let find_provers s =
try let p = prover_by_id wc s in
s, p.driver, p.extra_drivers,
String.concat " " (p.command :: p.extra_options)
with
(* TODO add exceptions pehaps inside rc.ml in fact*)
| Not_found -> eprintf "Prover %s not found.@." s; exit 1 in
let p = filter_one_prover wc (parse_filter_prover s) in
s, p.driver, p.extra_drivers,
String.concat " " (p.command :: p.extra_options) in
let provers = List.map find_provers provers in
let provers =
try
......
......@@ -252,8 +252,8 @@ let () =
if !opt_list_provers then begin
opt_list := true;
let config = read_config !opt_config in
let print fmt prover pc = fprintf fmt "%s (%a)@\n"
pc.id print_prover prover in
let print fmt prover pc = fprintf fmt "%a (%a)@\n"
print_prover_parsable_format pc.prover print_prover prover in
let print fmt m = Mprover.iter (print fmt) m in
let provers = get_provers config in
printf "@[<hov 2>Known provers:@\n%a@]@." print provers
......@@ -343,7 +343,7 @@ let () =
let map_prover s =
let prover = prover_by_id config s in
let prover = filter_one_prover config (parse_filter_prover s) in
{ B.tval = {B.tool_name = "cmdline"; prover_name = s; tool_db = None};
ttrans = [Trans.identity,None];
tdriver = load_driver env prover.driver prover.extra_drivers;
......
......@@ -3,7 +3,7 @@ Require Export ZArith.
Open Scope Z_scope.
Require Export List.
Ltac ae := why3 "alt-ergo".
Ltac ae := why3 "Alt-Ergo".
Section S0.
Variable a:Set->Set.
......
......@@ -63,7 +63,17 @@ let get_prover s =
try
Hashtbl.find provers s
with Not_found ->
let cp = Whyconf.prover_by_id config s in
let filter_prover = Whyconf.parse_filter_prover s in
let cp = try Whyconf.filter_one_prover config filter_prover
with Whyconf.ProverAmbiguity (wc,fp,provers) ->
let provers = Mprover.filter (fun _ p -> not p.interactive) provers in
if Mprover.is_num_elt 1 provers then
snd (Mprover.choose provers)
else if Mprover.is_empty provers then
raise (Whyconf.ProverNotFound (wc,fp))
else
raise (Whyconf.ProverAmbiguity (wc,fp,provers))
in
let drv = Driver.load_driver env cp.driver cp.extra_drivers in
Hashtbl.add provers s (cp, drv);
cp, drv
......@@ -1097,6 +1107,9 @@ let tr_top_decl = function
| _, Lib.ClosedSection _
| _, Lib.FrozenState _ -> ()
let pr_fp fp =
pr_str (Pp.string_of_wnl Whyconf.print_filter_prover_no_regexp fp)
let why3tac ?(timelimit=timelimit) s gl =
(* print_dep Format.err_formatter; *)
let concl_type = pf_type_of gl (pf_concl gl) in
......@@ -1126,14 +1139,31 @@ let why3tac ?(timelimit=timelimit) s gl =
| NotFO ->
if debug then Printexc.print_backtrace stderr; flush stderr;
error "Not a first order goal"
| Whyconf.ProverNotFound (_, s) ->
| Whyconf.ProverNotFound (_, fp) ->
let pl =
Mprover.fold (fun _ p l -> if not p.interactive then p.id :: l else l)
Mprover.fold (fun prover p l -> if not p.interactive
then (Pp.string_of_wnl Whyconf.print_prover prover) :: l
else l)
(get_provers config) [] in
let msg = pr_str "No such prover `" ++ pr_str s ++ pr_str "'." ++
let msg = pr_str "No such prover `"
++ pr_fp fp
++ pr_str "'." ++
pr_spc () ++ pr_str "Available provers are:" ++ pr_fnl () ++
prlist (fun s -> pr_str s ++ pr_fnl ()) (List.rev pl) in
errorlabstrm "Whyconf.ProverNotFound" msg
| Whyconf.ProverAmbiguity (_, fp,provers) ->
let pl = Mprover.keys provers in
let pl = List.map (Pp.string_of_wnl Whyconf.print_prover) pl in
let msg = pr_str "More than one prover corresponding to `" ++
pr_fp fp ++ pr_str "'." ++
pr_spc () ++ pr_str "Corresponding provers are:" ++ pr_fnl () ++
prlist (fun s -> pr_str s ++ pr_fnl ()) (List.rev pl) in
errorlabstrm "Whyconf.ProverAmbiguity" msg
| Whyconf.ParseFilterProver s ->
let msg = pr_str "Syntax error prover identification '" ++
pr_str s ++ pr_str "' : name[,version[,alternative]|,,alternative]" in
errorlabstrm "Whyconf.ParseFilterProver" msg
| e ->
Printexc.print_backtrace stderr; flush stderr;
Format.eprintf "@[exception: %a@]@." Exn_printer.exn_printer e;
......
......@@ -88,8 +88,7 @@ let prover_keys =
let load_prover kind (id,section) =
check_exhaustive section prover_keys;
let reg_map = List.rev_map
(fun s -> if s.[0] = '^' then Str.regexp s else Str.regexp_string s) in
let reg_map = List.rev_map why3_regexp_of_string in
{ kind = kind;
prover_id = id;
prover_name = get_string section "name";
......@@ -218,9 +217,7 @@ let ask_prover_version env exec_name version_switch =
Hashtbl.replace env.prover_output (exec_name,version_switch) res;
res
let check_version version schema =
Str.string_match schema version 0
&& Str.match_end () = String.length version
let check_version version schema = Str.string_match schema version 0
let known_version env exec_name =
Hashtbl.replace env.prover_unknown_version exec_name None
......@@ -256,19 +253,7 @@ let add_prover_with_uniq_id prover provers =
(** find an unique prover triplet *)
let prover_id = find_prover_altern provers prover.Wc.prover in
let prover = {prover with Wc.prover = prover_id} in
(** find an unique id *)
let test id _ p = p.Wc.id = id in
if not (Mprover.exists (test prover.Wc.id) provers)
then Mprover.add prover.Wc.prover prover provers
else
let rec aux i =
let prover_id = sprintf "%s_%i" prover.Wc.id i in
if not (Mprover.exists (test prover_id) provers)
then Mprover.add prover.Wc.prover
{prover with id = prover_id} provers
else aux (i+1) in
aux 2
Mprover.add prover_id prover provers
let detect_exec env main data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
......@@ -319,7 +304,6 @@ let detect_exec env main data acc exec_name =
prover_altern = data.prover_altern} in
let prover_config =
{prover = prover;
id = data.prover_id;
command = c;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor;
......@@ -412,11 +396,7 @@ let add_prover_binary config id path =
Wc.prover_altern =
Util.concat_non_empty " " [p.prover.Wc.prover_altern;alt] } in
find_prover_altern provers prover_id in
let p_new = {p with prover = prover_id} in
let alt = sanitizer char_to_alnumus char_to_alnumus
(get_suffix p.prover.Wc.prover_altern
prover_id.Wc.prover_altern) in
let p_new = { p_new with id = p.id ^ "-" ^ alt } in
add_prover_with_uniq_id p_new provers in
let p = {p with prover = prover_id} in
add_prover_with_uniq_id p provers in
let provers = Mprover.fold fold detected provers in
set_provers config provers
This diff is collapsed.
......@@ -45,7 +45,8 @@ val read_config : string option -> config
the built-in default_config with default configuration filename *)
val merge_config : config -> string -> config
(** [merge_config config filename] merge the content of [filename] into [config] *)
(** [merge_config config filename] merge the content of [filename]
into [config]( *)
val save_config : config -> unit
(** [save_config config] save the configuration *)
......@@ -96,6 +97,8 @@ type prover =
(** record of necessary data for a given external prover *)
val print_prover : Format.formatter -> prover -> unit
val print_prover_parsable_format : Format.formatter -> prover -> unit
(** Printer for prover *)
module Prover : Util.OrderedHash with type t = prover
module Mprover : Stdlib.Map.S with type key = prover
......@@ -106,7 +109,6 @@ module Hprover : Hashtbl.S with type key = prover
type config_prover = {
prover : prover; (* unique name for session *)
id : string; (* unique name for command line *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
in_place: bool; (* verification should be performed in-place *)
......@@ -127,12 +129,6 @@ val set_provers : config -> config_prover Mprover.t -> config
val is_prover_known : config -> prover -> bool
(** test if a prover is detected *)
exception ProverNotFound of config * string
val prover_by_id : config -> string -> config_prover
(** return the configuration of the prover if found, otherwise return
ProverNotFound *)
type config_editor = {
editor_name : string;
editor_command : string;
......@@ -173,6 +169,44 @@ val get_policies : config -> prover_upgrade_policy Mprover.t
val set_policies : config -> prover_upgrade_policy Mprover.t -> config
(** filter prover *)
type filter_prover
val mk_filter_prover :
?version:string -> ?altern:string -> name:string -> filter_prover
val print_filter_prover :
Format.formatter -> filter_prover -> unit
val print_filter_prover_no_regexp :
Format.formatter -> filter_prover -> unit
val parse_filter_prover : string -> filter_prover
(** parse the string representing a filter_prover:
- "name,version,altern"
- "name,version" -> "name,version,^.*"
- "name,,altern" -> "name,^.*,altern"
- "name" -> "name,^.*,^.*"
regexp must start with ^. Partial match will be used.
*)
val filter_prover : filter_prover -> prover -> bool
(** test if the prover match the filter prover *)
val filter_provers : config -> filter_prover -> config_prover Mprover.t
(** test if the prover match the filter prover *)
exception ProverNotFound of config * filter_prover
exception ProverAmbiguity of config * filter_prover * config_prover Mprover.t
exception ParseFilterProver of string
val filter_one_prover : config -> filter_prover -> config_prover
(** find the uniq prover that verify the filter. If it doesn't exists
raise ProverNotFound or raise ProverAmbiguity *)
val why3_regexp_of_string : string -> Str.regexp
(** {2 For accesing other parts of the configuration } *)
(** Access to the Rc.t *)
......
......@@ -265,9 +265,8 @@ let () = try
opt_list := true;
let config = read_config !opt_config in
let config = List.fold_left merge_config config !opt_extra in
let print fmt prover pc = fprintf fmt "%s (%a)@\n"
pc.id print_prover prover in
let print fmt m = Mprover.iter (print fmt) m in
let print = Pp.print_iter2 Mprover.iter Pp.newline Pp.nothing
print_prover Pp.nothing in
let provers = get_provers config in
printf "@[<hov 2>Known provers:@\n%a@]@." print provers
end;
......@@ -328,9 +327,11 @@ let () = try
if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main);
begin match !opt_prover with
| Some s ->
let prover = Whyconf.prover_by_id config s in
opt_command := Some (String.concat " " (prover.command :: prover.extra_options));
opt_driver := Some (prover.driver, prover.extra_drivers)
let filter_prover = Whyconf.parse_filter_prover s in
let prover = Whyconf.filter_one_prover config filter_prover in
opt_command :=
Some (String.concat " " (prover.command :: prover.extra_options));
opt_driver := Some (prover.driver, prover.extra_drivers)
| None ->
()
end;
......@@ -547,7 +548,8 @@ let do_input env drv = function
let () =
try
let env = Env.create_env !opt_loadpath in
let drv = Util.option_map (fun (f,ef) -> load_driver env f ef) !opt_driver in
let drv =
Util.option_map (fun (f,ef) -> load_driver env f ef) !opt_driver in
Queue.iter (do_input env drv) opt_queue;
if !opt_token_count then
Format.printf "Total: %d annot/%d programs, ratio = %.3f@."
......
......@@ -52,6 +52,7 @@ module type S =
val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
(** Added into why stdlib version *)
val is_num_elt : int -> 'a t -> bool
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
......@@ -115,6 +116,7 @@ module type S =
val fold2: (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val translate : (elt -> elt) -> t -> t
val add_new : exn -> elt -> t -> t
val is_num_elt : int -> t -> bool
end
module Set : Set
......@@ -610,6 +612,11 @@ module Make(Ord: OrderedType) = struct
| Some _ -> raise e
| None -> Some v) x m
let is_num_elt n m =
try
fold (fun _ _ n -> if n < 0 then raise Exit else n-1) m n = 0
with Exit -> false
module type Set =
sig
type elt = key
......@@ -645,6 +652,7 @@ module Make(Ord: OrderedType) = struct
val fold2: (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val translate : (elt -> elt) -> t -> t
val add_new : exn -> elt -> t -> t
val is_num_elt : int -> t -> bool
end
module Set =
......@@ -688,6 +696,7 @@ module Make(Ord: OrderedType) = struct
let fold2 f = fold2_union (fun k _ _ acc -> f k acc)
let translate = translate
let add_new e x s = add_new e x () s
let is_num_elt n m = is_num_elt n m
end
end
......
......@@ -179,6 +179,9 @@ module type S =
(** {3} Added into why stdlib version *)
val is_num_elt : int -> 'a t -> bool
(** check if the map has the given number of elements *)
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
(** [change f x m] returns a map containing the same bindings as
[m], except the binding of [x] in [m] is changed from [y] to
......@@ -186,7 +189,9 @@ module type S =
binding of [x] becomes [f None].
[change f x m] corresponds to a more efficient way to do
[add x (try f (Some (find x m)) with Not_found -> f None) m] *)
[match (try f (Some (find x m)) with Not_found -> f None) with
| None -> m
| Some v -> add x v] *)
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
(** [union f m1 m2] computes a map whose keys is a subset of keys
......@@ -409,6 +414,10 @@ module type S =
val add_new : exn -> elt -> t -> t
(** [add_new e x s] adds [x] to [s] if [s] does not contain [x],
and raises [e] otherwise. *)
val is_num_elt : int -> t -> bool
(** check if the map has the given number of elements *)
end
module Set : Set
......
......@@ -179,12 +179,7 @@ let read_to_prover config =
match !opt_to_prover with
| None -> None
| Some fpr ->
try Some (prover_of_filter_prover config fpr)
with ProverNotFound (_,id) ->
eprintf
"The prover %s is not found in the configuration file %s@."
id (get_conf_file config);
exit 1
Some (prover_of_filter_prover config fpr)
let run ~action () =
......
......@@ -95,25 +95,24 @@ let read_update_session ~allow_obsolete env config fname =
(** filter *)
type filter_prover =
| Prover of Whyconf.prover
| ProverId of string
| Prover of Whyconf.prover
| FilterProver of Whyconf.filter_prover
let filter_prover = Stack.create ()
let read_opt_prover s =
let sl = Util.split_string_rev s ',' in
(* reverse order *)
let prover =
match sl with
| [altern;version;name] ->
Prover {C.prover_name = name; prover_version = version;
prover_altern = altern}
| [version;name] ->
Prover {C.prover_name = name; prover_version = version;
prover_altern = ""}
| [id] -> ProverId id
| _ -> raise (Arg.Bad "--filter-prover [name,version[,alternative]|id]")
in prover
try
let l = Util.split_string_rev s ',' in
match l with
| [altern;version;name] when List.for_all (fun s -> s.[0] <> '^') l ->
Prover {Whyconf.prover_name = name;
prover_version = version;
prover_altern = altern}
| _ -> FilterProver (Whyconf.parse_filter_prover s)
with Whyconf.ParseFilterProver _ ->
raise (Arg.Bad
"--filter-prover name[,version[,alternative]|,,alternative] \
regexp must start with ^")
let add_filter_prover s = Stack.push (read_opt_prover s) filter_prover
......@@ -155,20 +154,28 @@ type filters =
verified_goal : filter_three;
}
let provers_of_filter_prover whyconf = function
| Prover p -> C.Sprover.singleton p
| FilterProver fp ->
C.Mprover.map (Util.const ()) (C.filter_provers whyconf fp)
let prover_of_filter_prover whyconf = function
| Prover p -> p
| ProverId id -> (C.prover_by_id whyconf id).C.prover
| Prover p -> p
| FilterProver fp ->
(C.filter_one_prover whyconf fp).C.prover
let read_filter_spec whyconf : filters * bool =
let should_exit = ref false in
let s = ref C.Sprover.empty in
let iter p =
try
s := C.Sprover.add (prover_of_filter_prover whyconf p) !s
with C.ProverNotFound (_,id) ->
s := C.Sprover.union (provers_of_filter_prover whyconf p) !s
with C.ProverNotFound (_,fp) ->
Format.eprintf
"The prover %s is not found in the configuration file %s@."
id (Whyconf.get_conf_file whyconf);
"The prover %a is not found in the configuration file %s@."
Whyconf.print_filter_prover fp
(Whyconf.get_conf_file whyconf);
should_exit := true in
Stack.iter iter filter_prover;
{provers = !s;
......
......@@ -61,12 +61,11 @@ val read_update_session :
Why3.Whyconf.config -> string -> unit Why3.Session.env_session * bool
(** {2 Spec for filtering } *)
type filter_prover =
| Prover of Whyconf.prover
| ProverId of string
type filter_prover
val read_opt_prover : string -> filter_prover
val prover_of_filter_prover : config -> filter_prover -> prover
val prover_of_filter_prover : config -> filter_prover -> Why3.Whyconf.prover
val provers_of_filter_prover : config -> filter_prover -> Why3.Whyconf.Sprover.t
type filters
......
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