Tiny parser for strategies

A simple, assembly-like syntax for strategies is introduced.
The code for a strategy is now a single string, in the field
'code' of a 'strategy' entry of a configuration file.
See share/strategies.conf for examples.
parent e5442abb
......@@ -181,6 +181,7 @@ pvsbin/
# /src/session
/src/session/xml.ml
/src/session/compress.ml
/src/session/strategy_parser.ml
# /src/tools
/src/tools/why3wc.ml
......
......@@ -110,6 +110,7 @@ LIBGENERATED = src/util/config.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml \
src/session/compress.ml src/session/xml.ml \
src/session/strategy_parser.ml \
lib/ocaml/why3__BigInt_compat.ml
LIB_UTIL = config bigInt util opt lists strings \
......@@ -155,7 +156,8 @@ LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/printer/, $(LIB_PRINTER)) \
$(addprefix src/whyml/, $(LIB_WHYML))
LIB_SESSION = compress xml termcode session session_tools session_scheduler
LIB_SESSION = compress xml termcode session session_tools strategy \
strategy_parser session_scheduler
LIBSESSIONMODULES = $(addprefix src/session/, $(LIB_SESSION))
......
......@@ -2,28 +2,32 @@
name = "Mini Blaster"
desc = "A@ simple@ blaster"
shortcut = "b"
l0 = "c Alt-Ergo,0.95.2, 1 1000"
l1 = "c CVC4,1.4, 1 1000"
l2 = "t split_goal_wp 0"
l3 = "c Alt-Ergo,0.95.2, 10 4000"
l4 = "c CVC4,1.4, 10 4000"
code = "
start:
c Alt-Ergo,0.95.2, 1 1000
c CVC4,1.4, 1 1000
t split_goal_wp start
c Alt-Ergo,0.95.2, 10 4000
c CVC4,1.4, 10 4000"
[strategy]
desc = "Mega@ Blaster@ of@ the@ death@ who@ kills"
l0 = "c Alt-Ergo,0.95.2, 1 1000"
l1 = "c CVC4,1.4, 1 1000"
l2 = "t split_goal_wp 6"
l3 = "t introduce_premises 4"
l4 = "t inline_goal 0"
l5 = "g 11"
l6 = "c Alt-Ergo,0.95.2, 1 1000"
l7 = "c CVC4,1.4, 1 1000"
l8 = "t introduce_premises 9"
l9 = "t inline_goal 0"
l10 = "t split_goal_wp 6"
l11 = "c Alt-Ergo,0.95.2, 5 2000"
l12 = "c CVC4,1.4, 5 2000"
l13 = "c Alt-Ergo,0.95.2, 30 4000"
l14 = "c CVC4,1.4, 30 4000"
name = "Mega Blaster"
desc = "Mega@ Blaster@ of@ the@ death"
code = "
L0:c Alt-Ergo,0.95.2, 1 1000
c CVC4,1.4, 1 1000
t split_goal_wp L6
t introduce_premises L4
L4:t inline_goal L0
g L11
L6:c Alt-Ergo,0.95.2, 1 1000
c CVC4,1.4, 1 1000
t introduce_premises L9
L9:t inline_goal L0
t split_goal_wp L6
L11:
c Alt-Ergo,0.95.2, 5 2000
c CVC4,1.4, 5 2000
c Alt-Ergo,0.95.2, 30 4000
c CVC4,1.4, 30 4000"
......@@ -133,7 +133,7 @@ type config_editor = {
type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_code : string array;
strategy_code : string;
strategy_shortcut : string;
}
......@@ -468,22 +468,14 @@ let load_strategy strategies section =
try
let name = get_string section "name" in
let desc = get_string section "desc" in
let shortcut = get_string ~default:"" section "shortcut" in
let desc = Scanf.format_from_string desc "" in
let code = ref [] and i = ref 0 in
try
while true do
let instr = get_string section ("l" ^ (string_of_int !i)) in
code := instr :: !code;
incr i
done;
assert false
with MissingField _ ->
Mstr.add
name
let shortcut = get_string ~default:"" section "shortcut" in
let code = get_string section "code" in
Mstr.add
name
{ strategy_name = name;
strategy_desc = desc;
strategy_code = Array.of_list (List.rev !code);
strategy_code = code;
strategy_shortcut = shortcut;
}
strategies
......
......@@ -182,7 +182,7 @@ val set_policies : config -> prover_upgrade_policy Mprover.t -> config
type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_code : string array;
strategy_code : string;
strategy_shortcut : string;
}
......
......@@ -1414,10 +1414,10 @@ let () =
add_gui_item add_item_provers
let split_strategy =
[| M.Itransform(split_transformation,1) |]
[| Strategy.Itransform(split_transformation,1) |]
let inline_strategy =
[| M.Itransform(inline_transformation,1) |]
[| Strategy.Itransform(inline_transformation,1) |]
let test_strategy () =
let config = gconfig.Gconfig.config in
......@@ -1430,11 +1430,11 @@ let test_strategy () =
Whyconf.filter_one_prover config fp
in
[|
M.Icall_prover(altergo.Whyconf.prover,1,1000);
M.Icall_prover(cvc4.Whyconf.prover,1,1000);
M.Itransform(split_transformation,0); (* goto 0 on success *)
M.Icall_prover(altergo.Whyconf.prover,10,4000);
M.Icall_prover(cvc4.Whyconf.prover,10,4000);
Strategy.Icall_prover(altergo.Whyconf.prover,1,1000);
Strategy.Icall_prover(cvc4.Whyconf.prover,1,1000);
Strategy.Itransform(split_transformation,0); (* goto 0 on success *)
Strategy.Icall_prover(altergo.Whyconf.prover,10,4000);
Strategy.Icall_prover(cvc4.Whyconf.prover,10,4000);
|]
(*
......@@ -1497,13 +1497,13 @@ let strategies () =
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let len = Array.length code in
let code = Strategy_parser.parse (env_session()) code in
let shortcut = load_shortcut st.Whyconf.strategy_shortcut in
let code = Array.map (M.parse_instr (env_session()) len) code in
Format.eprintf "[GUI] Strategy '%s' loaded.@." name;
(name, st.Whyconf.strategy_desc,code, shortcut) :: acc
with M.SyntaxError msg ->
Format.eprintf "[GUI warning] Loading strategy '%s' failed: %s@." name msg;
(name, st.Whyconf.strategy_desc, code, shortcut) :: acc
with Strategy_parser.SyntaxError msg ->
Format.eprintf
"[GUI warning] Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
......
......@@ -917,100 +917,7 @@ let rec clean = function
let convert_unknown_prover =
Session_tools.convert_unknown_prover ~keygen:O.create
(** {2 User-defined strategies} *)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
exception SyntaxError of string
let parse_instr env max s =
match Strings.split ' ' s with
| [] -> raise (SyntaxError "unexpected empty instruction")
| ["g";n] ->
let g =
try int_of_string n
with Failure _ ->
raise
(SyntaxError
("unable to parse goto argument '" ^ n ^ "' as an integer"))
in
if g < 0 || g > max then
raise
(SyntaxError ("goto index " ^ n ^ " is invalid"));
Igoto g
| "g" :: _ ->
raise (SyntaxError "'g' expects exactly one argument")
| ["c";p;t;m] ->
let p =
try
let fp = Whyconf.parse_filter_prover p in
Whyconf.filter_one_prover env.whyconf fp
with
| Whyconf.ProverNotFound _ ->
raise
(SyntaxError
("Prover " ^ p ^ " not installed or not configured"))
| Whyconf.ProverAmbiguity _ ->
raise
(SyntaxError
("Prover description " ^ p ^ " is ambiguous"))
in
let timelimit =
try int_of_string t
with Failure _ ->
raise
(SyntaxError
("unable to parse timelimit argument '" ^ t ^ "'"))
in
if timelimit <= 0 then
raise
(SyntaxError ("timelimit " ^ t ^ " is invalid"));
let memlimit =
try int_of_string m
with Failure _ ->
raise
(SyntaxError
("unable to parse memlimit argument '" ^ m ^ "'"))
in
if memlimit <= 0 then
raise
(SyntaxError ("memlimit " ^ m ^ " is invalid"));
Icall_prover(p.Whyconf.prover,timelimit,memlimit)
| "c" :: _ ->
raise (SyntaxError "'c' expects exactly three arguments")
| ["t";t;n] ->
let () =
try
let _ = Trans.lookup_transform t env.env in
()
with Trans.UnknownTrans _ ->
try
let _ = Trans.lookup_transform_l t env.env in
()
with Trans.UnknownTrans _->
raise (SyntaxError ("transformation '" ^ t ^ "' is unknown"))
in
let g =
try int_of_string n
with Failure _ ->
raise
(SyntaxError
("unable to parse argument '" ^ n ^ "' as an integer"))
in
if g < 0 || g > max then
raise
(SyntaxError ("index " ^ n ^ " is invalid"));
Itransform(t,g)
| "t" :: _ ->
raise (SyntaxError "'t' expects exactly one argument")
| s :: _ ->
raise (SyntaxError ("unknown instruction '" ^ s ^ "'"))
type strategy = instruction array
open Strategy
let rec exec_strategy es sched pc strat g =
if pc < 0 || pc >= Array.length strat then
......
......@@ -296,42 +296,14 @@ module Make(O: OBSERVER) : sig
val convert_unknown_prover : O.key env_session -> unit
(** Same as {!Session_tools.convert_unknown_prover} *)
(** {2 User-defined strategies} *)
(** A strategy is defined by a program declared under a simple
assembly-like form: instructions are indexed by integers
starting from 0 (the initial instruction counter). An
instruction is either
1) a call to a prover, with given time and mem limits
. on success, the program execution ends
. on any other result, the program execution continues on the next index
2) a application of a transformation
. on success, the execution continues to a explicitly given index
. on failure, execution continues on the next index
3) a goto instruction.
the execution halts when reaching a non-existing state
*)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
type strategy = instruction array
exception SyntaxError of string
val parse_instr : O.key Session.env_session -> int -> string -> instruction
val run_strategy_on_goal:
O.key Session.env_session -> t ->
strategy -> O.key Session.goal -> unit
Strategy.t -> O.key Session.goal -> unit
val run_strategy:
O.key Session.env_session -> t ->
context_unproved_goals_only:bool ->
strategy -> O.key Session.any -> unit
Strategy.t -> O.key Session.any -> unit
end
......
open Why3
(** {2 User-defined strategies} *)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
type t = instruction array
open Why3
(** {2 User-defined strategies} *)
(** A strategy is defined by a program declared under a simple
assembly-like form: instructions are indexed by integers
starting from 0 (the initial instruction counter). An
instruction is either
1) a call to a prover, with given time and mem limits
. on success, the program execution ends
. on any other result, the program execution continues on the next index
2) a application of a transformation
. on success, the execution continues to a explicitly given index
. on failure, execution continues on the next index
3) a goto instruction.
the execution halts when reaching a non-existing state
*)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
type t = instruction array
open Why3
exception SyntaxError of string
val parse : 'a Session.env_session -> string -> Strategy.t
{
open Why3
open Session
open Strategy
exception SyntaxError of string
let error f =
Printf.kbprintf
(fun b ->
let s = Buffer.contents b in Buffer.clear b; raise (SyntaxError s))
(Buffer.create 1024)
f
type label = {
mutable defined: int option;
temporary: int;
}
type 'a code = {
env: 'a Session.env_session;
mutable instr: instruction array;
mutable next: int;
labels: (string, label) Hashtbl.t; (* label name -> label *)
mutable temp: int;
}
let create_code env = {
env = env;
instr = Array.make 10 (Igoto 0);
next = 0; temp = 0;
labels = Hashtbl.create 17;
}
let enlarge_code code =
let old = code.instr in
let n = Array.length old in
code.instr <- Array.make (2 * n) (Igoto 0);
Array.blit old 0 code.instr 0 n
let add_instr code i =
let n = code.next in
if n = Array.length code.instr then enlarge_code code;
code.instr.(n) <- i;
code.next <- n + 1
let temp code =
let t = code.temp in code.temp <- t + 1; t
let define_label code l =
let n = code.next in
try
let lab = Hashtbl.find code.labels l in
if lab.defined = None then lab.defined <- Some n
else error "duplicate label %s" l
with Not_found ->
let lab = { defined = Some n; temporary = temp code } in
Hashtbl.add code.labels l lab
let find_label code l =
try
let lab = Hashtbl.find code.labels l in lab.temporary
with Not_found ->
let t = temp code in
Hashtbl.add code.labels l { defined = None; temporary = t };
t
let prover code p =
try
let fp = Whyconf.parse_filter_prover p in
Whyconf.filter_one_prover code.env.whyconf fp
with
| Whyconf.ProverNotFound _ ->
error "Prover %S not installed or not configured" p
| Whyconf.ProverAmbiguity _ ->
error "Prover description %s is ambiguous" p
let integer msg s =
try int_of_string s
with Failure _ -> error "unabel to parse %s argument '%s'" msg s
let transform code t =
try
ignore (Trans.lookup_transform t code.env.Session.env)
with Trans.UnknownTrans _ ->
try
ignore (Trans.lookup_transform_l t code.env.Session.env)
with Trans.UnknownTrans _->
error "transformation %S is unknown" t
}
let space = [' ' '\t' '\r' '\n']
let ident = [^ ' ' '\t' '\r' '\n' ':' '#']+
let integer = ['0'-'9']+
let goto = 'g' | "goto"
let call = 'c' | "call"
let transform = 't' | "transform"
rule scan code = parse
| space+
{ scan code lexbuf }
| '#' [^ '\n']* ('\n' | eof)
{ scan code lexbuf }
| ident as id ':'
{ define_label code id;
scan code lexbuf }
| goto space+ (ident as id)
{ add_instr code (Igoto (find_label code id));
scan code lexbuf }
| call space+ (ident as p) space+ (integer as t) space+ (integer as m)
{ let p = prover code p in
let t = integer "timelimit" t in
if t <= 0 then error "timelimit %d is invalid" t;
let m = integer "memlimit" m in
if m <= 0 then error "memlimit %d is invalid" m;
add_instr code (Icall_prover (p.Whyconf.prover, t, m));
scan code lexbuf }
| transform space+ (ident as t) space+ (ident as l)
{ transform code t;
add_instr code (Itransform (t, find_label code l));
scan code lexbuf }
| _ as c
{ let i = Lexing.lexeme_start lexbuf in
error "syntax error on character '%c' at position %d" c i }
| eof
{ () }
{
let parse env s =
let code = create_code env in
scan code (Lexing.from_string s);
let label = Array.create code.temp 0 in
let fill name lab = match lab.defined with
| None -> error "label '%s' is undefined" name
| Some n -> label.(lab.temporary) <- n in
Hashtbl.iter fill code.labels;
let solve = function
| Icall_prover _ as i -> i
| Itransform (t, n) -> Itransform (t, label.(n))
| Igoto n -> Igoto label.(n) in
Array.map solve (Array.sub code.instr 0 code.next)
}
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