1 (* fuzz the tables and matchers generated *)
6 val create
: ?capacity
:int -> unit -> 'a t
7 val reset
: 'a t
-> unit
9 val get
: 'a t
-> int -> 'a
10 val set
: 'a t
-> int -> 'a
-> unit
11 val push
: 'a t
-> 'a
-> unit
15 ; mutable data
: 'a array
}
16 let mk_array n
= Array.make n
(Obj.magic
0)
17 let create ?
(capacity
= 10) () =
18 if capacity
< 0 then invalid_arg
"Buffer.make";
19 {size
= 0; data
= mk_array capacity
}
20 let reset b
= b
.size
<- 0
23 if n
>= size b
then invalid_arg
"Buffer.get";
26 if n
>= size b
then invalid_arg
"Buffer.set";
29 let cap = Array.length b
.data
in
30 if size b
= cap then begin
31 let data = mk_array (2 * cap + 1) in
32 Array.blit b
.data 0 data 0 cap;
40 let binop_state n op s1 s2
=
41 let key = K
(op
, s1
, s2
) in
42 try StateMap.find
key n
.statemap
43 with Not_found
-> atom_state n Tmp
47 | Binop
of op
* id
* id
48 | Leaf
of atomic_pattern
54 let pp_term fmt
(ta
, id
) =
55 let fpf x
= Format.fprintf fmt x
in
57 match ta
.(id
).data with
58 | Leaf
(Con c
) -> fpf "%Ld" c
59 | Leaf AnyCon
-> fpf "$%d" id
60 | Leaf Tmp
-> fpf "%%%d" id
61 | Binop
(op
, id1
, id2
) ->
62 fpf "@[(%s@%d:%d @[<hov>%a@ %a@])@]"
63 (show_op op
) id ta
.(id
).state
.id
67 (* A term pool is a deduplicated set of term
68 * that maintains nodes numbering using the
69 * statemap passed at creation time *)
70 module TermPool
= struct
72 { terms
: term
Buffer.t
73 ; hcons
: (term_data
, id
) Hashtbl.t
77 { terms
= Buffer.create ()
78 ; hcons
= Hashtbl.create 100
81 Buffer.reset tp
.terms
;
82 Hashtbl.clear tp
.hcons
84 let size tp
= Buffer.size tp
.terms
85 let term tp id
= Buffer.get tp
.terms id
88 let data = Leaf atm
in
89 match Hashtbl.find tp
.hcons
data with
91 | exception Not_found
->
92 let id = Buffer.size tp
.terms
in
93 let state = atom_state tp
.numbr atm
in
94 Buffer.push tp
.terms
{id; data; state};
95 Hashtbl.add tp
.hcons
data id;
97 let mk_binop tp op t1 t2
=
98 let data = Binop
(op
, t1
.id, t2
.id) in
99 match Hashtbl.find tp
.hcons
data with
101 | exception Not_found
->
102 let id = Buffer.size tp
.terms
in
104 binop_state tp
.numbr op t1
.state t2
.state
106 Buffer.push tp
.terms
{id; data; state};
107 Hashtbl.add tp
.hcons
data id;
110 let rec add_pattern tp
= function
111 | Bnr
(op
, p1
, p2
) ->
112 let t1 = add_pattern tp p1
in
113 let t2 = add_pattern tp p2
in
115 | Atm atm
-> mk_leaf tp atm
116 | Var
(_
, atm
) -> add_pattern tp
(Atm atm
)
118 let explode_term tp
id =
119 let rec aux tms n
id =
120 let t = term tp
id in
122 | Leaf _
-> (n
, {t with id = n
} :: tms
)
123 | Binop
(op
, id1
, id2
) ->
124 let n1, tms
= aux tms n id1
in
126 let n2, tms
= aux tms
n id2
in
128 (n, { t with data = Binop
(op
, n1, n2)
131 let n, tms
= aux [] 0 id in
132 Array.of_list
(List.rev tms
), n
137 (* uniform pick in a list *)
143 if R.int (n + 1) = 0 then
149 | [] -> invalid_arg
"list_pick"
150 | x
:: l
-> aux 1 l x
152 let term_pick ~numbr
=
154 if numbr
.ops = [] then
156 (StateMap.fold
(fun k _
ops ->
158 | K
(op
, _
, _
) -> op
:: ops)
159 numbr
.statemap
[] |> setify
);
163 (* exponential probability for leaves to
164 * avoid skewing towards shallow terms *)
165 let atm_prob = 0.75 ** float_of_int depth
in
166 if R.float 1.0 <= atm_prob || ops = [] then
167 let atom, st
= list_pick numbr
.atoms
in
170 let op = list_pick ops in
171 let s1, t1 = gen (depth
- 1) in
172 let s2, t2 = gen (depth
- 1) in
173 ( binop_state numbr
op s1 s2
175 in fun ~depth
-> gen depth
179 let rec pattern_depth = function
181 1 + max
(pattern_depth p1
) (pattern_depth p2
)
183 | Var
(_
, atm
) -> pattern_depth (Atm atm
)
186 1e2
*. float_of_int a
/. float_of_int b
188 let progress ?
(width
= 50) msg pct
=
189 Format.eprintf
"\x1b[2K\r%!";
190 let progress_bar fmt
=
192 let fwidth = float_of_int width
in
193 1 + int_of_float
(pct
*. fwidth /. 1e2
)
195 Format.fprintf fmt
" %s%s %.0f%%@?"
196 (String.concat
"" (List.init
n (fun _
-> "▒")))
197 (String.make
(max
0 (width
- n)) '
-'
)
200 Format.kfprintf
progress_bar
201 Format.err_formatter msg
203 let fuzz_numberer rules numbr
=
204 (* pick twice the max pattern depth so we
205 * have a chance to find non-trivial numbers
206 * for the atomic patterns in the rules *)
208 List.fold_left
(fun depth r
->
209 max
depth (pattern_depth r
.pattern
))
212 (* fuzz until the term pool we are constructing
213 * is no longer growing fast enough; or we just
214 * went through sufficiently many iterations *)
215 let max_iter = 1_000_000 in
216 let low_insert_rate = 1e-2 in
217 let tp = TermPool.create numbr
in
218 let rec loop new_stats i
=
219 let (_
, _
, insert_rate
) = new_stats
in
220 if insert_rate
<= low_insert_rate then () else
221 if i
>= max_iter then () else
222 (* periodically update stats *)
224 let (num
, cnt
, rate
) = new_stats in
225 if num
land 1023 = 0 then
227 0.5 *. (rate +. float_of_int cnt
/. 1023.)
229 progress " insert_rate=%.1f%%"
230 (i
%% max_iter) (rate *. 1e2
);
234 (* create a term and check that its number is
235 * accurate wrt the rules *)
236 let st, term = term_pick ~numbr ~
depth in
238 List.filter_map
(fun cu
->
240 | Top
("$" | "%") -> None
241 | Top name
-> Some name
246 List.filter_map
(fun r
->
247 if pattern_match r
.pattern
term then
252 if state_matched <> rule_matched then begin
255 let pp_sep fmt
() = fprintf fmt
",@ " in
256 pp_print_list ~
pp_sep pp_print_string
258 eprintf
"@.@[<v2>fuzz error for %s"
260 eprintf
"@ @[state matched: %a@]"
261 pp_str_list state_matched;
262 eprintf
"@ @[rule matched: %a@]"
263 pp_str_list rule_matched;
267 if state_matched = [] then
268 loop new_stats (i
+ 1)
270 (* add to the term pool *)
271 let old_size = TermPool.size tp in
272 let _ = TermPool.add_pattern tp term in
274 let (num
, cnt
, rate) = new_stats in
275 if TermPool.size tp <> old_size then
276 (num
+ 1, cnt
+ 1, rate)
280 loop new_stats (i
+ 1)
284 "@.@[ generated %.3fMiB of test terms@]@."
285 (float_of_int
(Obj.reachable_words
(Obj.repr
tp))
289 let rec run_matcher stk m
(ta
, id as t) =
290 let state id = ta
.(id).state.id in
291 match m
.Action.node
with
292 | Action.Switch cases
->
294 try List.assoc
(state id) cases
295 with Not_found
-> failwith
"no switch case"
298 | Action.Push
(sym
, m) ->
300 match ta
.(id).data with
301 | Leaf
_ -> failwith
"push on leaf"
302 | Binop
(_, l, r
) -> (l, r
)
304 if sym
&& state l > state r
305 then run_matcher (l :: stk
) m (ta
, r
)
306 else run_matcher (r
:: stk
) m (ta
, l)
307 | Action.Pop
m -> begin
309 | id :: stk
-> run_matcher stk
m (ta
, id)
310 | [] -> failwith
"pop on empty stack"
312 | Action.Set
(v
, m) ->
313 (v
, id) :: run_matcher stk
m t
316 let rec term_match p
(ta
, id) =
318 match x
with None
-> None
| Some x
-> f x
321 match ta
.(id).data with
322 | Leaf a'
-> pattern_match
(Atm a
) (Atm a'
)
323 | Binop
_ -> pattern_match
(Atm a
) (Atm Tmp
)
326 | Var
(v
, a
) when atom_match a
->
328 | Atm a
when atom_match a
-> Some
[]
329 | (Atm
_ | Var
_) -> None
330 | Bnr
(op, pl
, pr
) -> begin
331 match ta
.(id).data with
332 | Binop
(op'
, idl
, idr
) when op'
= op ->
333 term_match pl
(ta
, idl
) |>> fun l1
->
334 term_match pr
(ta
, idr
) |>> fun l2
->
339 let test_matchers tp numbr rules
=
340 let {statemap
= sm
; states
= sa
; _} = numbr
in
343 let htbl = Hashtbl.create (Array.length sa
) in
344 List.map
(fun r
-> (r
.name
, r
.pattern
)) rules
|>
346 List.iter
(fun (r
, ps
) ->
347 total := !total + List.length ps
;
348 let pm = (ps
, lr_matcher sm sa rules r
) in
349 sa
|> Array.iter
(fun s
->
350 if List.mem
(Top r
) s
.point
then
351 Hashtbl.add
htbl s
.id pm));
354 let seen = Hashtbl.create !total in
355 for id = 0 to TermPool.size tp - 1 do
356 if id land 1023 = 0 ||
357 id = TermPool.size tp - 1 then begin
360 (id %% TermPool.size tp)
361 (Hashtbl.length
seen %% !total)
363 let t = TermPool.explode_term tp id in
364 Hashtbl.find_all
matchers
365 (TermPool.term tp id).state.id |>
366 List.iter
(fun (ps
, m) ->
367 let norm = List.fast_sort compare
in
369 match norm (run_matcher [] m t) with
370 | asn
-> `Match
(List.exists
(fun p
->
371 match term_match p
t with
374 if asn
= norm asn'
then begin
375 Hashtbl.replace
seen p
();
378 | exception e
-> `RunFailure e
380 if ok <> `Match
true then begin
385 ~
pp_sep:(fun fmt
() -> fprintf fmt
";@ ")
387 fprintf fmt
"@[%s←%d@]" v d
)
391 eprintf
"@.@[<v2>matcher error for";
392 eprintf
"@ @[%a@]" pp_term t;
395 eprintf
"@ @[exception: %s@]"
396 (Printexc.to_string e
)
397 | `Match
(* false *) _ ->
398 let asn = run_matcher [] m t in
399 eprintf
"@ @[assignment: %a@]"
401 eprintf
"@ @[<v2>could not match";
404 (show_pattern p
)) ps
;