# Theory Compiler2

```(*  Title:      Jinja/Compiler/Compiler2.thy
Author:     Tobias Nipkow
*)

section ‹Compilation Stage 2›

theory Compiler2
imports PCompiler J1 "../JVM/JVMExec"
begin

primrec compE⇩2 :: "expr⇩1 ⇒ instr list"
and compEs⇩2 :: "expr⇩1 list ⇒ instr list" where
"compE⇩2 (new C) = [New C]"
| "compE⇩2 (Cast C e) = compE⇩2 e @ [Checkcast C]"
| "compE⇩2 (Val v) = [Push v]"
| "compE⇩2 (e⇩1 «bop» e⇩2) = compE⇩2 e⇩1 @ compE⇩2 e⇩2 @
(case bop of Eq ⇒ [CmpEq]
| "compE⇩2 (Var i) = [Load i]"
| "compE⇩2 (i:=e) = compE⇩2 e @ [Store i, Push Unit]"
| "compE⇩2 (e∙F{D}) = compE⇩2 e @ [Getfield F D]"
| "compE⇩2 (e⇩1∙F{D} := e⇩2) =
compE⇩2 e⇩1 @ compE⇩2 e⇩2 @ [Putfield F D, Push Unit]"
| "compE⇩2 (e∙M(es)) = compE⇩2 e @ compEs⇩2 es @ [Invoke M (size es)]"
| "compE⇩2 ({i:T; e}) = compE⇩2 e"
| "compE⇩2 (e⇩1;;e⇩2) = compE⇩2 e⇩1 @ [Pop] @ compE⇩2 e⇩2"
| "compE⇩2 (if (e) e⇩1 else e⇩2) =
(let cnd   = compE⇩2 e;
thn   = compE⇩2 e⇩1;
els   = compE⇩2 e⇩2;
test  = IfFalse (int(size thn + 2));
thnex = Goto (int(size els + 1))
in cnd @ [test] @ thn @ [thnex] @ els)"
| "compE⇩2 (while (e) c) =
(let cnd   = compE⇩2 e;
bdy   = compE⇩2 c;
test  = IfFalse (int(size bdy + 3));
loop  = Goto (-int(size bdy + size cnd + 2))
in cnd @ [test] @ bdy @ [Pop] @ [loop] @ [Push Unit])"
| "compE⇩2 (throw e) = compE⇩2 e @ [instr.Throw]"
| "compE⇩2 (try e⇩1 catch(C i) e⇩2) =
(let catch = compE⇩2 e⇩2
in compE⇩2 e⇩1 @ [Goto (int(size catch)+2), Store i] @ catch)"

| "compEs⇩2 []     = []"
| "compEs⇩2 (e#es) = compE⇩2 e @ compEs⇩2 es"

text‹Compilation of exception table. Is given start address of code
to compute absolute addresses necessary in exception table.›

primrec compxE⇩2  :: "expr⇩1      ⇒ pc ⇒ nat ⇒ ex_table"
and compxEs⇩2 :: "expr⇩1 list ⇒ pc ⇒ nat ⇒ ex_table" where
"compxE⇩2 (new C) pc d = []"
| "compxE⇩2 (Cast C e) pc d = compxE⇩2 e pc d"
| "compxE⇩2 (Val v) pc d = []"
| "compxE⇩2 (e⇩1 «bop» e⇩2) pc d =
compxE⇩2 e⇩1 pc d @ compxE⇩2 e⇩2 (pc + size(compE⇩2 e⇩1)) (d+1)"
| "compxE⇩2 (Var i) pc d = []"
| "compxE⇩2 (i:=e) pc d = compxE⇩2 e pc d"
| "compxE⇩2 (e∙F{D}) pc d = compxE⇩2 e pc d"
| "compxE⇩2 (e⇩1∙F{D} := e⇩2) pc d =
compxE⇩2 e⇩1 pc d @ compxE⇩2 e⇩2 (pc + size(compE⇩2 e⇩1)) (d+1)"
| "compxE⇩2 (e∙M(es)) pc d =
compxE⇩2 e pc d @ compxEs⇩2 es (pc + size(compE⇩2 e)) (d+1)"
| "compxE⇩2 ({i:T; e}) pc d = compxE⇩2 e pc d"
| "compxE⇩2 (e⇩1;;e⇩2) pc d =
compxE⇩2 e⇩1 pc d @ compxE⇩2 e⇩2 (pc+size(compE⇩2 e⇩1)+1) d"
| "compxE⇩2 (if (e) e⇩1 else e⇩2) pc d =
(let pc⇩1   = pc + size(compE⇩2 e) + 1;
pc⇩2   = pc⇩1 + size(compE⇩2 e⇩1) + 1
in compxE⇩2 e pc d @ compxE⇩2 e⇩1 pc⇩1 d @ compxE⇩2 e⇩2 pc⇩2 d)"
| "compxE⇩2 (while (b) e) pc d =
compxE⇩2 b pc d @ compxE⇩2 e (pc+size(compE⇩2 b)+1) d"
| "compxE⇩2 (throw e) pc d = compxE⇩2 e pc d"
| "compxE⇩2 (try e⇩1 catch(C i) e⇩2) pc d =
(let pc⇩1 = pc + size(compE⇩2 e⇩1)
in compxE⇩2 e⇩1 pc d @ compxE⇩2 e⇩2 (pc⇩1+2) d @ [(pc,pc⇩1,C,pc⇩1+1,d)])"

| "compxEs⇩2 [] pc d    = []"
| "compxEs⇩2 (e#es) pc d = compxE⇩2 e pc d @ compxEs⇩2 es (pc+size(compE⇩2 e)) (d+1)"

primrec max_stack :: "expr⇩1 ⇒ nat"
and max_stacks :: "expr⇩1 list ⇒ nat" where
"max_stack (new C) = 1"
| "max_stack (Cast C e) = max_stack e"
| "max_stack (Val v) = 1"
| "max_stack (e⇩1 «bop» e⇩2) = max (max_stack e⇩1) (max_stack e⇩2) + 1"
| "max_stack (Var i) = 1"
| "max_stack (i:=e) = max_stack e"
| "max_stack (e∙F{D}) = max_stack e"
| "max_stack (e⇩1∙F{D} := e⇩2) = max (max_stack e⇩1) (max_stack e⇩2) + 1"
| "max_stack (e∙M(es)) = max (max_stack e) (max_stacks es) + 1"
| "max_stack ({i:T; e}) = max_stack e"
| "max_stack (e⇩1;;e⇩2) = max (max_stack e⇩1) (max_stack e⇩2)"
| "max_stack (if (e) e⇩1 else e⇩2) =
max (max_stack e) (max (max_stack e⇩1) (max_stack e⇩2))"
| "max_stack (while (e) c) = max (max_stack e) (max_stack c)"
| "max_stack (throw e) = max_stack e"
| "max_stack (try e⇩1 catch(C i) e⇩2) = max (max_stack e⇩1) (max_stack e⇩2)"

| "max_stacks [] = 0"
| "max_stacks (e#es) = max (max_stack e) (1 + max_stacks es)"

lemma max_stack1: "1 ≤ max_stack e"

definition compMb⇩2 :: "expr⇩1 ⇒ jvm_method"
where
"compMb⇩2  ≡  λbody.
let ins = compE⇩2 body @ [Return];
xt = compxE⇩2 body 0 0
in (max_stack body, max_vars body, ins, xt)"

definition compP⇩2 :: "J⇩1_prog ⇒ jvm_prog"
where
"compP⇩2  ≡  compP compMb⇩2"

(*<*)
declare compP⇩2_def [simp]
(*>*)

lemma compMb⇩2 [simp]:
"compMb⇩2 e = (max_stack e, max_vars e, compE⇩2 e @ [Return], compxE⇩2 e 0 0)"