Handling errors
OCaml's equality
We've been using the symbol =
in OCaml for comparing values.
If you're coming from a language like Python or C,
you're probably used to this symbol being used for assignment instead
of comparison. Since assignment is a much less common operation in OCaml
(really only used when we're dealing with ref
s, like in gensym
),
this symbol is freed up for the more common use case.
But if you've played around (or made some typos), you may have noticed something:
OCaml also supports comparison with ==
. What's the difference?
The common =
implements structural equality. Two values are equal
if they are indistinguishable. So false = false
, [1; 2] = [1; 2]
,
and so on. But try evaluating [1; 2] == [1; 2]
in utop. It's false!
This double-equal ==
implements physical equality. Two values are
equal if they have identical runtime representations.
Think about what this means in our compiler. false
is always represented
with the same value, so (= false false)
should always be true, as
should (= false (= 1 2))
, etc. But what about something like
(= (pair 1 2) (pair 1 2))
? Each pair is represented at runtime by
a memory address. When we compile this expression, we put the pair (1, 2)
into memory twice; the first one has a different location than the second.
So the runtime representations are different and our comparison is false.
This is physical equality, and even gives a hint about how OCaml
represents [1; 2]
(it must be using memory!).
But notice that our interpreter is not implementing physical equality!
It thinks that (= (pair 1 2) (pair 1 2))
should evaluate to true
.
This is a divergence in behavior between or compiler and interpreter.
Dealing with it can be surprisingly tricky. We either need to implement
physical equality in the interpreter, or structural equality in the compiler.
For now, we'll cheat: let's restrict the interpreter to only consider
equality on natural numbers. Later, we'll come back and improve this.
interp.ml
| Prim2 (Eq, e1, e2) -> ( match (interp_exp env e1, interp_exp env e2) with | Number n1, Number n2 -> Boolean (n1 = n2) | _ -> raise (BadExpression exp) )
Error handling
Right now, here's how we're defining correctness for our compiler:
For all programs p
, if the interpreter produces a value when run on
p
, the compiler produces machine code that produces that same value.
These are the semantically valid programs.
But the interpreter doesn't produce a value for every program! On
(add1 false)
, for instance, the interpreter throws an exception.
This program is syntactically valid, but not semantically.
(Some programs don't even have corresponding ASTs;
we say that these are syntactically invalid and error out before reaching
the compiler or interpreter.)
For programs that are syntactically valid but semantically invalid,
we're currently making no claims about our
compiler's behavior. Maybe it will return an error of some kind–for
instance, on (add1 false)
we get an error from the runtime because it doesn't know how to
print the value.
But on some of these programs, our compiler will actually produce a
value (or really, produce a machine-code program that produces a value).
(add1 (sub1 false))
, for instance, produces false
in the compiler even though the
interpreter doesn't recognize it as a valid program.
Today, we'll fix this issue, modifying our compiler to handle these errors.
Modifying the runtime
First, we'll add an error-handling function to the runtime. We'll call this function from our compiled programs when an error occurs.
runtime.c
void error() { printf("ERROR"); exit(1); }
As usual, we'll need to recompile the runtime:
gcc -c runtime.c -o runtime.o
Modifying the compiler
First, we'll need to modify our compiler's output so that we can call
our new error
function:
compile.ml
let compile (program : expr) : string = [Global "entry"; Extern "error"; Label "entry"] @ compile_exp Symtab.empty (-8) program @ [Ret] |> List.map string_of_directive |> String.concat "\n"
That Extern "error"
directive is sort of the inverse of Global
: it
tells the assembler that our program will be linked against a program
that includes a definition for the error
label.
We'll jump to this label whenever we want to signal an error at runtime.
For instance, add1
should raise an error if its argument isn't a
number:
compile.ml
let rec compile_exp (tab : int symtab) (stack_index : int) (exp : expr) : directive list = match exp with (* some cases elided ... *) | Prim1 (Add1, arg) -> compile_exp tab stack_index arg @ [ Mov (Reg R8, Reg Rax) ; And (Reg R8, Imm num_mask) ; Cmp (Reg R8, Imm num_tag) ; Jnz "error" ] @ [Add (Reg Rax, operand_of_num 1)]
We raise an error by jumping to our error
function. In general calling
C functions will be more complex than this since we want to preserve our
heap pointer and values on our stack, but since the error
function
stops execution we don't need to worry about any of that.
We can extract these directives into a helper function:
compile.ml
let ensure_num (op : operand) : directive list = [ Mov (Reg R8, op) ; And (Reg R8, Imm num_mask) ; Cmp (Reg R8, Imm num_tag) ; Jnz "error" ]
(We should only call ensure_num
when we're not using the value in
r8
!)
We can use this to add error handling to functions that should take numbers:
compile.ml
let rec compile_exp (tab : int symtab) (stack_index : int) (exp : expr) : directive list = match exp with (* some cases elided ... *) | Prim1 (Add1, arg) -> compile_exp tab stack_index arg @ ensure_num (Reg Rax) @ [Add (Reg Rax, operand_of_num 1)] | Prim2 (Plus, e1, e2) -> compile_exp tab stack_index e1 @ ensure_num (Reg Rax) @ [Mov (stack_address stack_index, Reg Rax)] @ compile_exp tab (stack_index - 8) e2 @ (ensure_num (Reg Rax) @ [Mov (Reg R8, stack_address stack_index)] @ [Add (Reg Rax, Reg R8)]
and so on. We can write a similar function for pairs:
compile.ml
let ensure_pair (op : operand) : directive list = [ Mov (Reg R8, op) ; And (Reg R8, Imm heap_mask) ; Cmp (Reg R8, Imm pair_tag) ; Jnz "error" ]
Compiler correctness revisited
We can now make a stronger statement about compiler correctness:
For all programs p
, if the interpreter produces a value when run on
p
, the compiler produces machine code that produces that same value.
If the interpreter produces an error, the compiler will either produce
an error or produce a program that produces an error.
We can add support for erroring programs to our tester:
interp.ml
let interp_err (program : string) : string = try interp program with BadExpression _ -> "ERROR"
compile.ml
let compile_and_run_err (program : string) : string = try compile_and_run program with BadExpression _ -> "ERROR" let difftest (examples : string list) = let results = List.map (fun ex -> (compile_and_run_err ex, Interp.interp_err ex)) examples in List.for_all (fun (r1, r2) -> r1 = r2) results
We have one lingering problem: there are some programs that produce an
error in our compiler but not in our interpreter. An example is (if true 1 (add1 hello))
. Since the interpreter never evaluates (add1 hello)
, it
happily produces the value 1
. The compiler, however, will throw an
error at compile-time, since the variable hello
is undefined.
We could fix this by adding a check to the
interpreter to ensure that the programs it's trying to interpret are
well-formed (i.e., don't contain expressions like (add1 hello)
)
even if they aren't type-correct.