diff --git a/src/Tools/ROOT b/src/Tools/ROOT --- a/src/Tools/ROOT +++ b/src/Tools/ROOT @@ -1,15 +1,20 @@ chapter Tools session Tools = Pure + theories Code_Generator +session Spec_Check in Spec_Check = Pure + + theories + Spec_Check + Examples + session SML in SML = Pure + theories Examples session Haskell in Haskell = Pure + theories Haskell theories [condition = ISABELLE_GHC_STACK] Test diff --git a/src/Tools/Spec_Check/Examples.thy b/src/Tools/Spec_Check/Examples.thy new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/Examples.thy @@ -0,0 +1,83 @@ +theory Examples +imports Spec_Check +begin + +section \List examples\ + +ML_command \ +check_property "ALL xs. rev xs = xs"; +\ + +ML_command \ +check_property "ALL xs. rev (rev xs) = xs"; +\ + + +section \AList Specification\ + +ML_command \ +(* map_entry applies the function to the element *) +check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)"; +\ + +ML_command \ +(* update always results in an entry *) +check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k"; +\ + +ML_command \ +(* update always writes the value *) +check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v"; +\ + +ML_command \ +(* default always results in an entry *) +check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k"; +\ + +ML_command \ +(* delete always removes the entry *) +check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)"; +\ + +ML_command \ +(* default writes the entry iff it didn't exist *) +check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))"; +\ + +section \Examples on Types and Terms\ + +ML_command \ +check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t"; +\ + +ML_command \ +check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t"; +\ + + +text \One would think this holds:\ + +ML_command \ +check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)" +\ + +text \But it only holds with this precondition:\ + +ML_command \ +check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)" +\ + +section \Some surprises\ + +ML_command \ +check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)" +\ + + +ML_command \ +val thy = \<^theory>; +check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true" +\ + +end diff --git a/src/Tools/Spec_Check/README b/src/Tools/Spec_Check/README new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/README @@ -0,0 +1,47 @@ +This is a Quickcheck tool for Isabelle/ML. + +Authors + + Lukas Bulwahn + Nicolai Schaffroth + +Quick Usage + + - Import Spec_Check.thy in your development + - Look at examples in Examples.thy + - write specifications with the ML invocation + check_property "ALL x. P x" + +Notes + +Our specification-based testing tool originated from Christopher League's +QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle +provides a rich and uniform ML platform (called Isabelle/ML), this +testing tools is very different than the one for a typical ML developer. + +1. Isabelle/ML provides common data structures, which we can use in the +tool's implementation for storing data and printing output. + +2. The implementation in Isabelle that will be checked with this tool +commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int), +but they do not use other integer types in ML, such as ML's Int.int, +Word.word and others. + +3. As Isabelle can run heavily in parallel, we avoid reference types. + +4. Isabelle has special naming conventions and documentation of source +code is only minimal to avoid parroting. + +Next steps: + - Remove all references and store the neccessary random seed in the + Isabelle's context. + - Simplify some existing random generators. + The original ones from Christopher League are so complicated to + support many integer types uniformly. + +License + + The source code originated from Christopher League's QCheck, which is + licensed under the 2-clause BSD license. The current source code is + licensed under the compatible 3-clause BSD license of Isabelle. + diff --git a/src/Tools/Spec_Check/Spec_Check.thy b/src/Tools/Spec_Check/Spec_Check.thy new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/Spec_Check.thy @@ -0,0 +1,13 @@ +theory Spec_Check +imports Pure +begin + +ML_file \random.ML\ +ML_file \property.ML\ +ML_file \base_generator.ML\ +ML_file \generator.ML\ +ML_file \gen_construction.ML\ +ML_file \spec_check.ML\ +ML_file \output_style.ML\ + +end \ No newline at end of file diff --git a/src/Tools/Spec_Check/base_generator.ML b/src/Tools/Spec_Check/base_generator.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/base_generator.ML @@ -0,0 +1,201 @@ +(* Title: Tools/Spec_Check/base_generator.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Basic random generators. +*) + +signature BASE_GENERATOR = +sig + +type rand +type 'a gen = rand -> 'a * rand +type ('a, 'b) co = 'a -> 'b gen -> 'b gen + +val new : unit -> rand +val range : int * int -> rand -> int * rand +type ('a, 'b) reader = 'b -> ('a * 'b) option + +val lift : 'a -> 'a gen +val select : 'a vector -> 'a gen +val choose : 'a gen vector -> 'a gen +val choose' : (int * 'a gen) vector -> 'a gen +val selectL : 'a list -> 'a gen +val chooseL : 'a gen list -> 'a gen +val chooseL' : (int * 'a gen) list -> 'a gen +val filter : ('a -> bool) -> 'a gen -> 'a gen + +val zip : ('a gen * 'b gen) -> ('a * 'b) gen +val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen +val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen +val map : ('a -> 'b) -> 'a gen -> 'b gen +val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen +val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen +val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen + +val flip : bool gen +val flip' : int * int -> bool gen + +val list : bool gen -> 'a gen -> 'a list gen +val option : bool gen -> 'a gen -> 'a option gen +val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen + +val variant : (int, 'b) co +val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen +val cobool : (bool, 'b) co +val colist : ('a, 'b) co -> ('a list, 'b) co +val coopt : ('a, 'b) co -> ('a option, 'b) co + +type stream +val start : rand -> stream +val limit : int -> 'a gen -> ('a, stream) reader + +end + +structure Base_Generator : BASE_GENERATOR = +struct + +(* random number engine *) + +type rand = real + +val a = 16807.0 +val m = 2147483647.0 + +fun nextrand seed = + let + val t = a * seed + in + t - m * real (floor (t / m)) + end + +val new = nextrand o Time.toReal o Time.now + +fun range (min, max) = + if min > max then raise Domain (* TODO: raise its own error *) + else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r) + +fun split r = + let + val r = r / a + val r0 = real (floor r) + val r1 = r - r0 + in + (nextrand r0, nextrand r1) + end + +(* generators *) + +type 'a gen = rand -> 'a * rand +type ('a, 'b) reader = 'b -> ('a * 'b) option + +fun lift obj r = (obj, r) + +local (* Isabelle does not use vectors? *) + fun explode ((freq, gen), acc) = + List.tabulate (freq, fn _ => gen) @ acc +in + fun choose v r = + let val (i, r) = range(0, Vector.length v - 1) r + in Vector.sub (v, i) r end + fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v)) + fun select v = choose (Vector.map lift v) +end + +fun chooseL l = choose (Vector.fromList l) +fun chooseL' l = choose' (Vector.fromList l) +fun selectL l = select (Vector.fromList l) + +fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2))) + +fun zip3 (g1, g2, g3) = + zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3)) + +fun zip4 (g1, g2, g3, g4) = + zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4)) + +fun map f g = apfst f o g + +fun map2 f = map f o zip +fun map3 f = map f o zip3 +fun map4 f = map f o zip4 + +fun filter p gen r = + let + fun loop (x, r) = if p x then (x, r) else loop (gen r) + in + loop (gen r) + end + +val flip = selectL [true, false] +fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)] + +fun list flip g r = + case flip r of + (true, r) => ([], r) + | (false, r) => + let + val (x,r) = g r + val (xs,r) = list flip g r + in (x::xs, r) end + +fun option flip g r = + case flip r of + (true, r) => (NONE, r) + | (false, r) => map SOME g r + +fun vector tabulate (int, elem) r = + let + val (n, r) = int r + val p = Unsynchronized.ref r + fun g _ = + let + val (x,r) = elem(!p) + in x before p := r end + in + (tabulate(n, g), !p) + end + +type stream = rand Unsynchronized.ref * int + +fun start r = (Unsynchronized.ref r, 0) + +fun limit max gen = + let + fun next (p, i) = + if i >= max then NONE + else + let val (x, r) = gen(!p) + in SOME(x, (p, i+1)) before p := r end + in + next + end + +type ('a, 'b) co = 'a -> 'b gen -> 'b gen + +fun variant v g r = + let + fun nth (i, r) = + let val (r1, r2) = split r + in if i = 0 then r1 else nth (i-1, r2) end + in + g (nth (v, r)) + end + +fun arrow (cogen, gen) r = + let + val (r1, r2) = split r + fun g x = fst (cogen x gen r1) + in (g, r2) end + +fun cobool false = variant 0 + | cobool true = variant 1 + +fun colist _ [] = variant 0 + | colist co (x::xs) = variant 1 o co x o colist co xs + +fun coopt _ NONE = variant 0 + | coopt co (SOME x) = variant 1 o co x + +end + diff --git a/src/Tools/Spec_Check/gen_construction.ML b/src/Tools/Spec_Check/gen_construction.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/gen_construction.ML @@ -0,0 +1,179 @@ +(* Title: Tools/Spec_Check/gen_construction.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Constructing generators and pretty printing function for complex types. +*) + +signature GEN_CONSTRUCTION = +sig + val register : string * (string * string) -> theory -> theory + type mltype + val parse_pred : string -> string * mltype + val build_check : Proof.context -> string -> mltype * string -> string + (*val safe_check : string -> mltype * string -> string*) + val string_of_bool : bool -> string + val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string +end; + +structure Gen_Construction : GEN_CONSTRUCTION = +struct + +(* Parsing ML types *) + +datatype mltype = Var | Con of string * mltype list | Tuple of mltype list; + +(*Split string into tokens for parsing*) +fun split s = + let + fun split_symbol #"(" = "( " + | split_symbol #")" = " )" + | split_symbol #"," = " ," + | split_symbol #":" = " :" + | split_symbol c = Char.toString c + fun is_space c = c = #" " + in String.tokens is_space (String.translate split_symbol s) end; + +(*Accept anything that is not a recognized symbol*) +val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;")); + +(*Turn a type list into a nested Con*) +fun make_con [] = raise Empty + | make_con [c] = c + | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]); + +(*Parse a type*) +fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s + +and parse_type_arg s = (parse_tuple || parse_type_single) s + +and parse_type_single s = (parse_con || parse_type_basic) s + +and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s + +and parse_list s = + ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s + +and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s + +and parse_con s = ((parse_con_nest + || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl) + || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl)) + >> (make_con o rev)) s + +and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s + +and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s + +and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single) + >> (fn (t, tl) => Tuple (t :: tl))) s; + +(*Parse entire type + name*) +fun parse_function s = + let + val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":") + val (name, ty) = p (split s) + val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); + val (typ, _) = Scan.finite stop parse_type ty + in (name, typ) end; + +(*Create desired output*) +fun parse_pred s = + let + val (name, Con ("->", t :: _)) = parse_function s + in (name, t) end; + +(* Construct Generators and Pretty Printers *) + +(*copied from smt_config.ML *) +fun string_of_bool b = if b then "true" else "false" + +fun string_of_ref f r = f (!r) ^ " ref"; + +val initial_content = Symtab.make + [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")), + ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")), + ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")), + ("unit", ("gen_unit", "fn () => \"()\"")), + ("int", ("Generator.int", "string_of_int")), + ("real", ("Generator.real", "string_of_real")), + ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")), + ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")), + ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")), + ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")), + ("term", ("Generator.term 10", "ML_Syntax.print_term"))] + +structure Data = Theory_Data +( + type T = (string * string) Symtab.table + val empty = initial_content + val extend = I + fun merge data : T = Symtab.merge (K true) data +) + +fun data_of ctxt tycon = + (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of + SOME data => data + | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)) + +val generator_of = fst oo data_of +val printer_of = snd oo data_of + +fun register (ty, data) = Data.map (Symtab.update (ty, data)) + +(* +fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table); +*) + +fun combine dict [] = dict + | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts) + +fun compose_generator _ Var = "Generator.int" + | compose_generator ctxt (Con (s, types)) = + combine (generator_of ctxt s) (map (compose_generator ctxt) types) + | compose_generator ctxt (Tuple t) = + let + fun tuple_body t = space_implode "" + (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^ + compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t)))) + fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a)) + in + "fn r0 => let " ^ tuple_body t ^ + "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" + end; + +fun compose_printer _ Var = "Int.toString" + | compose_printer ctxt (Con (s, types)) = + combine (printer_of ctxt s) (map (compose_printer ctxt) types) + | compose_printer ctxt (Tuple t) = + let + fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a)) + fun tuple_body t = space_implode " ^ \", \" ^ " + (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n) + (t ~~ (1 upto (length t)))) + in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end; + +(*produce compilable string*) +fun build_check ctxt name (ty, spec) = + "Spec_Check.checkGen (Context.the_local_context ()) (" + ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\"" + ^ name ^ "\", Property.pred (" ^ spec ^ "));"; + +(*produce compilable string - non-eqtype functions*) +(* +fun safe_check name (ty, spec) = + let + val default = + (case AList.lookup (op =) (!gen_table) "->" of + NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"") + | SOME entry => entry) + in + (gen_table := + AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table); + build_check name (ty, spec) before + gen_table := AList.update (op =) ("->", default) (!gen_table)) + end; +*) + +end; + diff --git a/src/Tools/Spec_Check/generator.ML b/src/Tools/Spec_Check/generator.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/generator.ML @@ -0,0 +1,235 @@ +(* Title: Tools/Spec_Check/generator.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Random generators for Isabelle/ML's types. +*) + +signature GENERATOR = sig + include BASE_GENERATOR + (* text generators *) + val char : char gen + val charRange : char * char -> char gen + val charFrom : string -> char gen + val charByType : (char -> bool) -> char gen + val string : (int gen * char gen) -> string gen + val substring : string gen -> substring gen + val cochar : (char, 'b) co + val costring : (string, 'b) co + val cosubstring : (substring, 'b) co + (* integer generators *) + val int : int gen + val int_pos : int gen + val int_neg : int gen + val int_nonpos : int gen + val int_nonneg : int gen + val coint : (int, 'b) co + (* real generators *) + val real : real gen + val real_frac : real gen + val real_pos : real gen + val real_neg : real gen + val real_nonpos : real gen + val real_nonneg : real gen + val real_finite : real gen + (* function generators *) + val function_const : 'c * 'b gen -> ('a -> 'b) gen + val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen + val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen + val unit : unit gen + val ref' : 'a gen -> 'a Unsynchronized.ref gen + (* more generators *) + val term : int -> term gen + val typ : int -> typ gen + + val stream : stream +end + +structure Generator : GENERATOR = +struct + +open Base_Generator + +val stream = start (new()) + +type 'a gen = rand -> 'a * rand +type ('a, 'b) co = 'a -> 'b gen -> 'b gen + +(* text *) + +type char = Char.char +type string = String.string +type substring = Substring.substring + + +val char = map Char.chr (range (0, Char.maxOrd)) +fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi)) + +fun charFrom s = + choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i)))) + +fun charByType p = filter p char + +val string = vector CharVector.tabulate + +fun substring gen r = + let + val (s, r') = gen r + val (i, r'') = range (0, String.size s) r' + val (j, r''') = range (0, String.size s - i) r'' + in + (Substring.substring (s, i, j), r''') + end + +fun cochar c = + if Char.ord c = 0 then variant 0 + else variant 1 o cochar (Char.chr (Char.ord c div 2)) + +fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s + +fun costring s = cosubstring (Substring.full s) + +(* integers *) +val digit = charRange (#"0", #"9") +val nonzero = string (lift 1, charRange (#"1", #"9")) +fun digits' n = string (range (0, n-1), digit) +fun digits n = map2 op^ (nonzero, digits' n) + +val maxDigits = 64 +val ratio = 49 + +fun pos_or_neg f r = + let + val (s, r') = digits maxDigits r + in (f (the (Int.fromString s)), r') end + +val int_pos = pos_or_neg I +val int_neg = pos_or_neg Int.~ +val zero = lift 0 + +val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)] +val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)] +val int = chooseL [int_nonneg, int_nonpos] + +fun coint n = + if n = 0 then variant 0 + else if n < 0 then variant 1 o coint (~ n) + else variant 2 o coint (n div 2) + +(* reals *) +val digits = string (range(1, Real.precision), charRange(#"0", #"9")) + +fun real_frac r = + let val (s, r') = digits r + in (the (Real.fromString s), r') end + +val {exp=minExp,...} = Real.toManExp Real.minPos +val {exp=maxExp,...} = Real.toManExp Real.posInf + +val ratio = 99 + +fun mk r = + let + val (a, r') = digits r + val (b, r'') = digits r' + val (e, r''') = range (minExp div 4, maxExp div 4) r'' + val x = String.concat [a, ".", b, "E", Int.toString e] + in + (the (Real.fromString x), r''') + end + +val real_pos = chooseL' (List.map ((pair 1) o lift) + [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)]) + +val real_neg = map Real.~ real_pos + +val real_zero = Real.fromInt 0 +val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)] +val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)] + +val real = chooseL [real_nonneg, real_nonpos] + +val real_finite = filter Real.isFinite real + +(*alternate list generator - uses an integer generator to determine list length*) +fun list' int gen = vector List.tabulate (int, gen); + +(* more function generators *) + +fun function_const (_, gen2) r = + let + val (v, r') = gen2 r + in (fn _ => v, r') end; + +fun function_strict size (gen1, gen2) r = + let + val (def, r') = gen2 r + val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r' + in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end; + +fun function_lazy (gen1, gen2) r = + let + val (initial1, r') = gen1 r + val (initial2, internal) = gen2 r' + val seed = Unsynchronized.ref internal + val table = Unsynchronized.ref [(initial1, initial2)] + fun new_entry k = + let + val (new_val, new_seed) = gen2 (!seed) + val _ = seed := new_seed + val _ = table := AList.update (op =) (k, new_val) (!table) + in new_val end + in + (fn v1 => + case AList.lookup (op =) (!table) v1 of + NONE => new_entry v1 + | SOME v2 => v2, r') + end; + +(* unit *) + +fun unit r = ((), r); + +(* references *) + +fun ref' gen r = + let val (value, r') = gen r + in (Unsynchronized.ref value, r') end; + +(* types and terms *) + +val sort_string = selectL ["sort1", "sort2", "sort3"]; +val type_string = selectL ["TCon1", "TCon2", "TCon3"]; +val tvar_string = selectL ["a", "b", "c"]; + +val const_string = selectL ["c1", "c2", "c3"]; +val var_string = selectL ["x", "y", "z"]; +val index = selectL [0, 1, 2, 3]; +val bound_index = selectL [0, 1, 2, 3]; + +val sort = list (flip' (1, 2)) sort_string; + +fun typ n = + let + fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m))) + val tfree = map TFree (zip (tvar_string, sort)) + val tvar = map TVar (zip (zip (tvar_string, index), sort)) + in + if n = 0 then chooseL [tfree, tvar] + else chooseL [type' (n div 2), tfree, tvar] + end; + +fun term n = + let + val const = map Const (zip (const_string, typ 10)) + val free = map Free (zip (var_string, typ 10)) + val var = map Var (zip (zip (var_string, index), typ 10)) + val bound = map Bound bound_index + fun abs m = map Abs (zip3 (var_string, typ 10, term m)) + fun app m = map (op $) (zip (term m, term m)) + in + if n = 0 then chooseL [const, free, var, bound] + else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)] + end; + +end diff --git a/src/Tools/Spec_Check/output_style.ML b/src/Tools/Spec_Check/output_style.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/output_style.ML @@ -0,0 +1,113 @@ +(* Title: Tools/Spec_Check/output_style.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Output styles for presenting Spec_Check's results. +*) + +structure Output_Style : sig end = +struct + +(* perl style *) + +val perl_style = + Spec_Check.register_style "Perl" + (fn ctxt => fn tag => + let + val target = Config.get ctxt Spec_Check.gen_target + val namew = Config.get ctxt Spec_Check.column_width + val sort_examples = Config.get ctxt Spec_Check.sort_examples + val show_stats = Config.get ctxt Spec_Check.show_stats + val limit = Config.get ctxt Spec_Check.examples + + val resultw = 8 + val countw = 20 + val allw = namew + resultw + countw + 2 + + val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I + + fun result ({count = 0, ...}, _) _ = "dubious" + | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" + | result ({count, tags}, badobjs) true = + if not (null badobjs) then "FAILED" + else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" + else "ok" + + fun ratio (0, _) = "(0/0 passed)" + | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" + | ratio (count, n) = + "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)" + + fun update (stats, badobjs) donep = + "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^ + StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^ + StringCvt.padRight #" " countw (ratio (#count stats, length badobjs)) + + fun status (_, result, (stats, badobjs)) = + if Property.failure result then warning (update (stats, badobjs) false) else () + + fun prtag count (tag, n) first = + if String.isPrefix "__" tag then ("", first) + else + let + val ratio = round ((real n / real count) * 100.0) + in + (((if first then "" else StringCvt.padRight #" " allw "\n") ^ + StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag), + false) + end + + fun prtags ({count, tags} : Property.stats) = + if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else "" + + fun err badobjs = + let + fun iter [] _ = () + | iter (e :: es) k = + (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^ + StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e); + iter es (k + 1)) + in + iter (maybe_sort (take limit (map_filter I badobjs))) 0 + end + + fun finish (stats, badobjs) = + if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats) + else (warning (update (stats, badobjs) true); err badobjs) + in + {status = status, finish = finish} + end) + +val _ = Theory.setup perl_style; + + +(* CM style: meshes with CM output; highlighted in sml-mode *) + +val cm_style = + Spec_Check.register_style "CM" + (fn ctxt => fn tag => + let + fun pad wd = StringCvt.padLeft #"0" wd o Int.toString + val gen_target = Config.get ctxt Spec_Check.gen_target + val _ = writeln ("[testing " ^ tag ^ "... ") + fun finish ({count, ...} : Property.stats, badobjs) = + (case (count, badobjs) of + (0, []) => warning ("no valid cases generated]") + | (n, []) => writeln ( + if n >= gen_target then "ok]" + else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]") + | (_, es) => + let + val wd = size (string_of_int (length es)) + fun each (NONE, _) = () + | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) + in + (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ()) + end) + in + {status = K (), finish = finish} + end) + +val _ = Theory.setup cm_style; + +end diff --git a/src/Tools/Spec_Check/property.ML b/src/Tools/Spec_Check/property.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/property.ML @@ -0,0 +1,77 @@ +(* Title: Tools/Spec_Check/property.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Conditional properties that can track argument distribution. +*) + +signature PROPERTY = +sig + +type 'a pred = 'a -> bool +type 'a prop +val pred : 'a pred -> 'a prop +val pred2 : ('a * 'b) pred -> 'b -> 'a prop +val implies : 'a pred * 'a prop -> 'a prop +val ==> : 'a pred * 'a pred -> 'a prop +val trivial : 'a pred -> 'a prop -> 'a prop +val classify : 'a pred -> string -> 'a prop -> 'a prop +val classify' : ('a -> string option) -> 'a prop -> 'a prop + +(*Results*) +type result = bool option +type stats = { tags : (string * int) list, count : int } +val test : 'a prop -> 'a * stats -> result * stats +val stats : stats +val success : result pred +val failure : result pred + +end + +structure Property : PROPERTY = +struct + +type result = bool option +type stats = { tags : (string * int) list, count : int } +type 'a pred = 'a -> bool +type 'a prop = 'a * stats -> result * stats + +fun success (SOME true) = true + | success _ = false + +fun failure (SOME false) = true + | failure _ = false + +fun apply f x = (case try f x of NONE => SOME false | some => some) +fun pred f (x,s) = (apply f x, s) +fun pred2 f z = pred (fn x => f (x, z)) + +fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s) + +fun ==> (p1, p2) = implies (p1, pred p2) + +fun wrap trans p (x,s) = + let val (result,s) = p (x,s) + in (result, trans (x, result, s)) end + +fun classify' f = + wrap (fn (x, result, {tags, count}) => + { tags = + if is_some result then + (case f x of + NONE => tags + | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags) + else tags, + count = count }) + +fun classify p tag = classify' (fn x => if p x then SOME tag else NONE) + +fun trivial cond = classify cond "trivial" + +fun test p = + wrap (fn (_, result, {tags, count}) => + { tags = tags, count = if is_some result then count + 1 else count }) p + +val stats = { tags = [], count = 0 } + +end diff --git a/src/Tools/Spec_Check/random.ML b/src/Tools/Spec_Check/random.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/random.ML @@ -0,0 +1,46 @@ +(* Title: Tools/Spec_Check/random.ML + Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen + Author: Christopher League + +Random number engine. +*) + +signature RANDOM = +sig + type rand + val new : unit -> rand + val range : int * int -> rand -> int * rand + val split : rand -> rand * rand +end + +structure Random : RANDOM = +struct + +type rand = real + +val a = 16807.0 +val m = 2147483647.0 + +fun nextrand seed = + let + val t = a * seed + in + t - m * real(floor(t/m)) + end + +val new = nextrand o Time.toReal o Time.now + +fun range (min, max) = + if min > max then raise Domain (* TODO: raise its own error *) + else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r) + +fun split r = + let + val r = r / a + val r0 = real(floor r) + val r1 = r - r0 + in + (nextrand r0, nextrand r1) + end + +end diff --git a/src/Tools/Spec_Check/spec_check.ML b/src/Tools/Spec_Check/spec_check.ML new file mode 100644 --- /dev/null +++ b/src/Tools/Spec_Check/spec_check.ML @@ -0,0 +1,196 @@ +(* Title: Tools/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 = Proof.context -> 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 : Proof.context -> + '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") + +type ('a, 'b) reader = 'b -> ('a * 'b) option +type 'a rep = ('a -> string) option + +type output_style = Proof.context -> string -> + {status: string option * Property.result * (Property.stats * string option list) -> unit, + finish: Property.stats * string option list -> unit} + +fun limit ctxt gen = Generator.limit (Config.get ctxt 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 ctxt = + let val name = Config.get ctxt style in + (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of + SOME style => style ctxt + | NONE => error ("No style called " ^ quote name ^ " found")) + end + +fun register_style name style = Style.map (Symtab.update (name, style)) + + +(* testing functions *) + +fun cpsCheck ctxt 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 ctxt 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 ctxt 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' ctxt s0 = cpsCheck ctxt s0 (fn _ => []) +fun check ctxt = check' ctxt Property.stats +fun checks ctxt = cpsCheck ctxt Property.stats + +fun checkGen ctxt (gen, show) (tag, prop) = + check' ctxt {count = 0, tags = [("__GEN", 0)]} + (limit ctxt gen, show) (tag, prop) Generator.stream + +fun checkGenShrink ctxt shrink (gen, show) (tag, prop) = + cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink + (limit ctxt gen, show) (tag, prop) Generator.stream + +fun checkOne ctxt show (tag, prop) obj = + check ctxt (List.getItem, show) (tag, prop) [obj] + +(*call the compiler and pass resulting type string to the parser*) +fun determine_type ctxt s = + let + val return = Unsynchronized.ref "return" + val context : ML_Compiler0.context = + {name_space = #name_space ML_Env.context, + print_depth = SOME 1000000, + here = #here ML_Env.context, + print = fn r => return := r, + error = #error ML_Env.context} + val _ = + Context.setmp_generic_context (SOME (Context.Proof ctxt)) + (fn () => + ML_Compiler0.ML context + {line = 0, file = "generated code", verbose = true, debug = false} s) () + in + Gen_Construction.parse_pred (! return) + end; + +(*call the compiler and run the test*) +fun run_test ctxt s = + Context.setmp_generic_context (SOME (Context.Proof ctxt)) + (fn () => + ML_Compiler0.ML ML_Env.context + {line = 0, file = "generated code", verbose = false, debug = false} s) (); + +(*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 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 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; + +fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s; +