1 (* Title: Tools/Spec_Check/spec_check.ML |
|
2 Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen |
|
3 Author: Christopher League |
|
4 |
|
5 Specification-based testing of ML programs with random values. |
|
6 *) |
|
7 |
|
8 signature SPEC_CHECK = |
|
9 sig |
|
10 val gen_target : int Config.T |
|
11 val gen_max : int Config.T |
|
12 val examples : int Config.T |
|
13 val sort_examples : bool Config.T |
|
14 val show_stats : bool Config.T |
|
15 val column_width : int Config.T |
|
16 val style : string Config.T |
|
17 |
|
18 type output_style = Proof.context -> string -> |
|
19 {status : string option * Property.result * (Property.stats * string option list) -> unit, |
|
20 finish: Property.stats * string option list -> unit} |
|
21 |
|
22 val register_style : string -> output_style -> theory -> theory |
|
23 |
|
24 val checkGen : Proof.context -> |
|
25 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit |
|
26 |
|
27 val check_property : Proof.context -> string -> unit |
|
28 end; |
|
29 |
|
30 structure Spec_Check : SPEC_CHECK = |
|
31 struct |
|
32 |
|
33 (* configurations *) |
|
34 |
|
35 val gen_target = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_target\<close> (K 100) |
|
36 val gen_max = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_max\<close> (K 400) |
|
37 val examples = Attrib.setup_config_int \<^binding>\<open>spec_check_examples\<close> (K 5) |
|
38 |
|
39 val sort_examples = Attrib.setup_config_bool \<^binding>\<open>spec_check_sort_examples\<close> (K true) |
|
40 val show_stats = Attrib.setup_config_bool \<^binding>\<open>spec_check_show_stats\<close> (K true) |
|
41 val column_width = Attrib.setup_config_int \<^binding>\<open>spec_check_column_width\<close> (K 22) |
|
42 val style = Attrib.setup_config_string \<^binding>\<open>spec_check_style\<close> (K "Perl") |
|
43 |
|
44 type ('a, 'b) reader = 'b -> ('a * 'b) option |
|
45 type 'a rep = ('a -> string) option |
|
46 |
|
47 type output_style = Proof.context -> string -> |
|
48 {status: string option * Property.result * (Property.stats * string option list) -> unit, |
|
49 finish: Property.stats * string option list -> unit} |
|
50 |
|
51 fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen |
|
52 |
|
53 structure Style = Theory_Data |
|
54 ( |
|
55 type T = output_style Symtab.table |
|
56 val empty = Symtab.empty |
|
57 val extend = I |
|
58 fun merge data : T = Symtab.merge (K true) data |
|
59 ) |
|
60 |
|
61 fun get_style ctxt = |
|
62 let val name = Config.get ctxt style in |
|
63 (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of |
|
64 SOME style => style ctxt |
|
65 | NONE => error ("No style called " ^ quote name ^ " found")) |
|
66 end |
|
67 |
|
68 fun register_style name style = Style.map (Symtab.update (name, style)) |
|
69 |
|
70 |
|
71 (* testing functions *) |
|
72 |
|
73 fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) = |
|
74 let |
|
75 val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f |
|
76 |
|
77 val {status, finish} = get_style ctxt tag |
|
78 fun status' (obj, result, (stats, badobjs)) = |
|
79 let |
|
80 val badobjs' = if Property.failure result then obj :: badobjs else badobjs |
|
81 val _ = status (apply_show obj, result, (stats, map apply_show badobjs')) |
|
82 in badobjs' end |
|
83 |
|
84 fun try_shrink (obj, result, stats') (stats, badobjs) = |
|
85 let |
|
86 fun is_failure s = |
|
87 let val (result, stats') = Property.test prop (s, stats) |
|
88 in if Property.failure result then SOME (s, result, stats') else NONE end |
|
89 in |
|
90 case get_first is_failure (shrink obj) of |
|
91 SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs) |
|
92 | NONE => status' (obj, result, (stats', badobjs)) |
|
93 end |
|
94 |
|
95 fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs) |
|
96 | iter (SOME (obj, stream), (stats, badobjs)) = |
|
97 if #count stats >= Config.get ctxt gen_target then |
|
98 finish (stats, map apply_show badobjs) |
|
99 else |
|
100 let |
|
101 val (result, stats') = Property.test prop (obj, stats) |
|
102 val badobjs' = if Property.failure result then |
|
103 try_shrink (obj, result, stats') (stats, badobjs) |
|
104 else |
|
105 status' (obj, result, (stats', badobjs)) |
|
106 in iter (next stream, (stats', badobjs')) end |
|
107 in |
|
108 fn stream => iter (next stream, (s0, [])) |
|
109 end |
|
110 |
|
111 fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => []) |
|
112 fun check ctxt = check' ctxt Property.stats |
|
113 fun checks ctxt = cpsCheck ctxt Property.stats |
|
114 |
|
115 fun checkGen ctxt (gen, show) (tag, prop) = |
|
116 check' ctxt {count = 0, tags = [("__GEN", 0)]} |
|
117 (limit ctxt gen, show) (tag, prop) Generator.stream |
|
118 |
|
119 fun checkGenShrink ctxt shrink (gen, show) (tag, prop) = |
|
120 cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink |
|
121 (limit ctxt gen, show) (tag, prop) Generator.stream |
|
122 |
|
123 fun checkOne ctxt show (tag, prop) obj = |
|
124 check ctxt (List.getItem, show) (tag, prop) [obj] |
|
125 |
|
126 (*call the compiler and pass resulting type string to the parser*) |
|
127 fun determine_type ctxt s = |
|
128 let |
|
129 val return = Unsynchronized.ref "return" |
|
130 val context : ML_Compiler0.context = |
|
131 {name_space = #name_space ML_Env.context, |
|
132 print_depth = SOME 1000000, |
|
133 here = #here ML_Env.context, |
|
134 print = fn r => return := r, |
|
135 error = #error ML_Env.context} |
|
136 val _ = |
|
137 Context.setmp_generic_context (SOME (Context.Proof ctxt)) |
|
138 (fn () => |
|
139 ML_Compiler0.ML context |
|
140 {line = 0, file = "generated code", verbose = true, debug = false} s) () |
|
141 in |
|
142 Gen_Construction.parse_pred (! return) |
|
143 end; |
|
144 |
|
145 (*call the compiler and run the test*) |
|
146 fun run_test ctxt s = |
|
147 Context.setmp_generic_context (SOME (Context.Proof ctxt)) |
|
148 (fn () => |
|
149 ML_Compiler0.ML ML_Env.context |
|
150 {line = 0, file = "generated code", verbose = false, debug = false} s) (); |
|
151 |
|
152 (*split input into tokens*) |
|
153 fun input_split s = |
|
154 let |
|
155 fun dot c = c = #"." |
|
156 fun space c = c = #" " |
|
157 val (head, code) = Substring.splitl (not o dot) (Substring.full s) |
|
158 in |
|
159 (String.tokens space (Substring.string head), |
|
160 Substring.string (Substring.dropl dot code)) |
|
161 end; |
|
162 |
|
163 (*create the function from the input*) |
|
164 fun make_fun s = |
|
165 let |
|
166 val scan_param = Scan.one (fn s => s <> ";") |
|
167 fun parameters s = Scan.repeat1 scan_param s |
|
168 val p = $$ "ALL" |-- parameters |
|
169 val (split, code) = input_split s |
|
170 val stop = Scan.stopper (fn _ => ";") (fn s => s = ";"); |
|
171 val (params, _) = Scan.finite stop p split |
|
172 in "fn (" ^ commas params ^ ") => " ^ code end; |
|
173 |
|
174 (*read input and perform the test*) |
|
175 fun gen_check_property check ctxt s = |
|
176 let |
|
177 val func = make_fun s |
|
178 val (_, ty) = determine_type ctxt func |
|
179 in run_test ctxt (check ctxt "Check" (ty, func)) end; |
|
180 |
|
181 val check_property = gen_check_property Gen_Construction.build_check |
|
182 (*val check_property_safe = gen_check_property Gen_Construction.safe_check*) |
|
183 |
|
184 (*perform test for specification function*) |
|
185 fun gen_check_property_f check ctxt s = |
|
186 let |
|
187 val (name, ty) = determine_type ctxt s |
|
188 in run_test ctxt (check ctxt name (ty, s)) end; |
|
189 |
|
190 val check_property_f = gen_check_property_f Gen_Construction.build_check |
|
191 (*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*) |
|
192 |
|
193 end; |
|
194 |
|
195 fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s; |
|
196 |
|