(* Title: HOL/Spec_Check/spec_check.ML
Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
Author: Christopher League
Specification-based testing of ML programs with random values.
*)
signature SPEC_CHECK =
sig
val gen_target : int Config.T
val gen_max : int Config.T
val examples : int Config.T
val sort_examples : bool Config.T
val show_stats : bool Config.T
val column_width : int Config.T
val style : string Config.T
type output_style = Context.generic -> string ->
{status : string option * Property.result * (Property.stats * string option list) -> unit,
finish: Property.stats * string option list -> unit}
val register_style : (string * output_style) -> theory -> theory
val checkGen : Context.generic ->
'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
val check_property : Proof.context -> string -> unit
end;
structure Spec_Check : SPEC_CHECK =
struct
(* configurations *)
val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
open Property
type ('a, 'b) reader = 'b -> ('a * 'b) option
type 'a rep = ('a -> string) option
type output_style = Context.generic -> string ->
{status: string option * Property.result * (Property.stats * string option list) -> unit,
finish: Property.stats * string option list -> unit}
fun limit context gen = Generator.limit (Config.get_generic context gen_max) gen
structure Style = Theory_Data
(
type T = output_style Symtab.table
val empty = Symtab.empty
val extend = I
fun merge data : T = Symtab.merge (K true) data
)
fun get_style context =
let val name = Config.get_generic context style
in case Symtab.lookup (Style.get (Context.theory_of context)) name of
SOME style => style context
| NONE => error ("No style called " ^ quote name ^ " found")
end
fun register_style (name, style) = Style.map (Symtab.update (name, style))
(* testing functions *)
fun cpsCheck context s0 shrink (next, show) (tag, prop) =
let
val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
val {status, finish} = get_style context tag
fun status' (obj, result, (stats, badobjs)) =
let
val badobjs' = if Property.failure result then obj :: badobjs else badobjs
val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
in badobjs' end
fun try_shrink (obj, result, stats') (stats, badobjs) =
let
fun is_failure s =
let val (result, stats') = Property.test prop (s, stats)
in if Property.failure result then SOME (s, result, stats') else NONE end
in
case get_first is_failure (shrink obj) of
SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
| NONE => status' (obj, result, (stats', badobjs))
end
fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
| iter (SOME (obj, stream), (stats, badobjs)) =
if #count stats >= Config.get_generic context gen_target then
finish (stats, map apply_show badobjs)
else
let
val (result, stats') = Property.test prop (obj, stats)
val badobjs' = if Property.failure result then
try_shrink (obj, result, stats') (stats, badobjs)
else
status' (obj, result, (stats', badobjs))
in iter (next stream, (stats', badobjs')) end
in
fn stream => iter (next stream, (s0, []))
end
fun check' context s0 = cpsCheck context s0 (fn _ => [])
fun check context = check' context Property.stats
fun checks context = cpsCheck context Property.stats
fun checkGen context (gen, show) (tag, prop) =
check' context {count=0, tags=[("__GEN", 0)]} (limit context gen, show) (tag, prop) Generator.stream
fun checkGenShrink context shrink (gen, show) (tag, prop) =
cpsCheck context {count=0, tags=[("__GEN", 0)]} shrink
(limit context gen, show) (tag, prop) Generator.stream
fun checkOne context show (tag, prop) obj =
check context (List.getItem, show) (tag, prop) [obj]
(*call the compiler and pass resulting type string to the parser*)
fun determine_type ctxt s =
let
val ret = Unsynchronized.ref "return"
val use_context : use_context = {
tune_source = ML_Parse.fix_ints,
name_space = ML_Env.name_space,
str_of_pos = Position.here oo Position.line_file,
print = fn r => ret := r,
error = error
}
val _ = ctxt |> Context.proof_map
(ML_Context.exec (fn () => Secure.use_text use_context (0, "generated code") true s))
in
Gen_Construction.parse_pred (!ret)
end;
(*call the compiler and run the test*)
fun run_test ctxt s =
let
val _ =
Context.proof_map
(ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code")
true s)) ctxt
in () end;
(*split input into tokens*)
fun input_split s =
let
fun dot c = c = #"."
fun space c = c = #" "
val (head, code) = Substring.splitl (not o dot) (Substring.full s)
in (String.tokens space (Substring.string head),
Substring.string (Substring.dropl dot code))
end;
(*create the function from the input*)
fun make_fun s =
let
val scan_param = Scan.one (fn s => s <> ";")
fun parameters s = Scan.repeat1 scan_param s
val p = $$ "ALL" |-- parameters
val (split, code) = input_split s
val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
val (params, _) = Scan.finite stop p split
in "fn (" ^ commas params ^ ") => " ^ code end;
(*read input and perform the test*)
fun gen_check_property check ctxt s =
let
val func = make_fun s
val (_, ty) = determine_type ctxt func
in run_test ctxt (check (Proof_Context.theory_of ctxt) "Check" (ty, func)) end;
val check_property = gen_check_property Gen_Construction.build_check
(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
(*perform test for specification function*)
fun gen_check_property_f check ctxt s =
let
val (name, ty) = determine_type ctxt s
in run_test ctxt (check (Proof_Context.theory_of ctxt) name (ty, s)) end;
val check_property_f = gen_check_property_f Gen_Construction.build_check
(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
end;
val check_property = Spec_Check.check_property;