12.1 Compiler Wrap up: Correctness & PBT
Compiler Correctness
With our completed compiler, we can begin stating our correctness criteria in OCaml. At a high level, we want to say that any closed Calc expression that evaluates to a value can also be compiled to a StackLang program that produces a semantically equivalent value.
Here, eval_opt and execute_opt will convert runtime errors into option types, and conv will convert a calc_value v to its representative integer (our values in StackLang). Let's define our new helper functions.
let eval_succeeds (e : CalcLang.expr) : bool =
try
let _ = CalcLang.eval StrMap.empty e in
true
with Failure _ -> false
let conv v =
match v with
| Nat v -> v
| Bool v -> if v then 1 else 0
Our proposition can now be stated in OCaml as follows:
let (==>) a thk = if a then thk () else true
let compiler_correct (e : CalcLang.expr) =
(eval_succeeds e) ==> (fun () -> Stack.(execute (compile e)) = conv CalcLang.(eval StrMap.empty e))
We have stated properties like this in prior lectures throughout our discussion of programming languages, both at a high-level with a written statement or a low-level in code. All of these prior statements, as well as this code above, is in our implementatino for the lecture and have been property checked. Let's walk through how this works, next.
Property checking compiler correctness.
We can start with the forall function we have seen in prior classes.
let rec forall gen prop num =
if num <= 0 then None
else let x = gen () in
if prop x then forall gen prop (num - 1) else Some x
To actually generate expressions we can use Random.int to select which AST constructor to build.
let mkvar i : string = "x" ^ (string_of_int i)
let gen_expr () : CalcLang.expr =
let open CalcLang in
let rec go depth i =
let max_k = if depth <= 0 then 2 else 6 in
match Random.int max_k with
| 0 -> Value (Nat (Random.int 10))
| 1 -> Value (Bool (Random.bool ()))
| 2 -> Var (mkvar i)
| 3 -> Let (mkvar (i+1), go (depth-1) i, go (depth-1) (i+1))
| 4 ->
let op = (match Random.int 6 with
| 0 -> Add | 1 -> Mul | 2 -> And | 3 -> Or | 4 -> LT | 5 -> EQ
| n -> failwith ("invalid random selector: " ^ string_of_int n)
) in
App (op, [go (depth-1) i; go (depth-1) i])
| 5 -> ITE (go (depth-1) i, go (depth-1) i, go (depth-1) i)
| n -> failwith ("invalid random selector: " ^ string_of_int n)
in go 5 0
Finally, we can property check our statement in the usual way:
let _ =
let samples = 1000000 in
match forall gen_expr prop_compiler_correct samples with
| Some ctr -> print_endline "calclang->stacklang: failed"
| None -> print_endline ("✓ calclang->stacklang: " ^ string_of_int samples ^ " checks pass")
But how thorough are our property checks?
(* -------------------------------------------------------------------- *)
(* PBT stuff *)
(* -------------------------------------------------------------------- *)
let rec forall gen prop num = if num <= 0 then None else
let x = gen () in
if prop x then forall gen prop (num - 1) else Some x
module Stats = Map.Make(String);;
exception Na of string
let forall_stats ?(trials : int = 1000) (gen : unit -> 'a) (prop : 'a -> bool) : 'a option =
let total_label = "total trials" in
let bump_stat what stats =
let bump count_opt =
match count_opt with
| Some i -> Some (i + 1)
| None -> Some 1 in
Stats.update what bump stats in
let bump_total stats = bump_stat total_label stats in
let print_stats =
Stats.iter (fun what count -> print_endline (what ^ ": " ^ string_of_int count)) in
let rec loop n (stats : int Stats.t) =
if n <= 0 then (None, stats) else
let x = gen () in
let stats' = bump_total stats in
match prop x with
| true -> loop (n - 1) stats'
| false -> (Some x, stats')
| exception (Na what) -> loop (n - 1) (bump_stat what stats')
in
let res, stats = loop trials Stats.empty in
if not (Stats.is_empty stats) then print_stats stats;
res
let assume (desc : string) (cond : bool) : unit =
if not cond then raise (Na ("not " ^ desc))
let gen_pair f g () =
(f (), g())
let gen_var () : string = "x" ^ (string_of_int (Random.int 10))
let gen_expr () : expr =
let rec go depth =
(* when depth reaches 0 we only generate leaf nodes *)
let max_k = if depth <= 0 then 2 else 6 in
match Random.int max_k with
| 0 -> Val (Nat (Random.int 10))
| 1 -> Val (Bool (Random.bool ()))
| 2 -> Var (gen_var ())
| 3 -> let id = gen_var () in Let (id, go (depth-1), go (depth-1))
| 4 -> (match Random.int 4 with
| 0 -> let x = go (depth-1) in
If (go (depth-1), x, x)
| _ -> If (go (depth-1), go (depth-1), go (depth-1) )
)
| 5 ->
let op = (match Random.int 6 with
| 0 -> Add | 1 -> Mul | 2 -> And | 3 -> Or | 4 -> LT | 5 -> EQ
| n -> failwith ("invalid random selector: " ^ string_of_int n)
) in
App (op, [go (depth-1); go (depth-1)])
| n -> failwith ("invalid random selector: " ^ string_of_int n)
in go 5
let rec depth e =
match e with
| Val _ | Var _ -> 1
| Let (_, e1, e2) -> 1 + max (depth e1) (depth e2)
| If (g, t, f) -> 1 + max (depth g) (max (depth t) (depth f))
| App (_, args) -> 1 + List.fold_left (fun acc expr -> max acc (depth expr)) 0 args
(* -------------------------------------------------------------------- *)
(* PBT stuff done *)
(* -------------------------------------------------------------------- *)
let rec gen_typeof_nat (st : kind) = fun () ->
let e = gen_expr() in
if typeof StrMap.empty e = Some (TNat st)
then e
else gen_typeof_nat st ()
let type_safe (e : expr) : bool =
match typeof StrMap.empty e with
| None -> false
| Some _ -> true
let wont_crash (f : unit -> 'a) : bool =
try
let _ = f () in true
with | _ -> false
(* ∀ e : expr, well-typed e -> e wont crash *)
let prop_sound (e : expr) : bool =
assume "well-typed" (type_safe e && depth e > 1);
wont_crash (fun () -> eval e)
let () =
let samples = 10000 in
match forall_stats ~trials:samples gen_expr prop_sound with
| Some ctr -> print_endline "fail"
| None -> print_endline (string_of_int samples ^ " checks pass")