(* Title: Jinja/Compiler/Compiler2.thy
ID: $Id: Compiler2.html 1910 2004-05-19 04:46:04Z kleing $
Author: Tobias Nipkow
Copyright TUM 2003
*)
header {* \isaheader{Compilation Stage 2} *}
theory Compiler2 = PCompiler + J1 + JVMExec:
consts
compE2 :: "expr1 => instr list"
compEs2 :: "expr1 list => instr list"
primrec
"compE2 (new C) = [New C]"
"compE2 (Cast C e) = compE2 e @ [Checkcast C]"
"compE2 (Val v) = [Push v]"
"compE2 (e1 «bop» e2) = compE2 e1 @ compE2 e2 @
(case bop of Eq => [CmpEq]
| Add => [IAdd])"
"compE2 (Var i) = [Load i]"
"compE2 (i:=e) = compE2 e @ [Store i, Push Unit]"
"compE2 (e\<bullet>F{D}) = compE2 e @ [Getfield F D]"
"compE2 (e1\<bullet>F{D} := e2) =
compE2 e1 @ compE2 e2 @ [Putfield F D, Push Unit]"
"compE2 (e\<bullet>M(es)) = compE2 e @ compEs2 es @ [Invoke M (size es)]"
"compE2 ({i:T; e}) = compE2 e"
"compE2 (e1;;e2) = compE2 e1 @ [Pop] @ compE2 e2"
"compE2 (if (e) e1 else e2) =
(let cnd = compE2 e;
thn = compE2 e1;
els = compE2 e2;
test = IfFalse (int(size thn + 2));
thnex = Goto (int(size els + 1))
in cnd @ [test] @ thn @ [thnex] @ els)"
"compE2 (while (e) c) =
(let cnd = compE2 e;
bdy = compE2 c;
test = IfFalse (int(size bdy + 3));
loop = Goto (-int(size bdy + size cnd + 2))
in cnd @ [test] @ bdy @ [Pop] @ [loop] @ [Push Unit])"
"compE2 (throw e) = compE2 e @ [instr.Throw]"
"compE2 (try e1 catch(C i) e2) =
(let catch = compE2 e2
in compE2 e1 @ [Goto (int(size catch)+2), Store i] @ catch)"
"compEs2 [] = []"
"compEs2 (e#es) = compE2 e @ compEs2 es"
text{* Compilation of exception table. Is given start address of code
to compute absolute addresses necessary in exception table. *}
consts
compxE2 :: "expr1 => pc => nat => ex_table"
compxEs2 :: "expr1 list => pc => nat => ex_table"
primrec
"compxE2 (new C) pc d = []"
"compxE2 (Cast C e) pc d = compxE2 e pc d"
"compxE2 (Val v) pc d = []"
"compxE2 (e1 «bop» e2) pc d =
compxE2 e1 pc d @ compxE2 e2 (pc + size(compE2 e1)) (d+1)"
"compxE2 (Var i) pc d = []"
"compxE2 (i:=e) pc d = compxE2 e pc d"
"compxE2 (e\<bullet>F{D}) pc d = compxE2 e pc d"
"compxE2 (e1\<bullet>F{D} := e2) pc d =
compxE2 e1 pc d @ compxE2 e2 (pc + size(compE2 e1)) (d+1)"
"compxE2 (e\<bullet>M(es)) pc d =
compxE2 e pc d @ compxEs2 es (pc + size(compE2 e)) (d+1)"
"compxE2 ({i:T; e}) pc d = compxE2 e pc d"
"compxE2 (e1;;e2) pc d =
compxE2 e1 pc d @ compxE2 e2 (pc+size(compE2 e1)+1) d"
"compxE2 (if (e) e1 else e2) pc d =
(let pc1 = pc + size(compE2 e) + 1;
pc2 = pc1 + size(compE2 e1) + 1
in compxE2 e pc d @ compxE2 e1 pc1 d @ compxE2 e2 pc2 d)"
"compxE2 (while (b) e) pc d =
compxE2 b pc d @ compxE2 e (pc+size(compE2 b)+1) d"
"compxE2 (throw e) pc d = compxE2 e pc d"
"compxE2 (try e1 catch(C i) e2) pc d =
(let pc1 = pc + size(compE2 e1)
in compxE2 e1 pc d @ compxE2 e2 (pc1+2) d @ [(pc,pc1,C,pc1+1,d)])"
"compxEs2 [] pc d = []"
"compxEs2 (e#es) pc d = compxE2 e pc d @ compxEs2 es (pc+size(compE2 e)) (d+1)"
consts
max_stack :: "expr1 => nat"
max_stacks :: "expr1 list => nat"
primrec
"max_stack (new C) = 1"
"max_stack (Cast C e) = max_stack e"
"max_stack (Val v) = 1"
"max_stack (e1 «bop» e2) = max (max_stack e1) (max_stack e2) + 1"
"max_stack (Var i) = 1"
"max_stack (i:=e) = max_stack e"
"max_stack (e\<bullet>F{D}) = max_stack e"
"max_stack (e1\<bullet>F{D} := e2) = max (max_stack e1) (max_stack e2) + 1"
"max_stack (e\<bullet>M(es)) = max (max_stack e) (max_stacks es) + 1"
"max_stack ({i:T; e}) = max_stack e"
"max_stack (e1;;e2) = max (max_stack e1) (max_stack e2)"
"max_stack (if (e) e1 else e2) =
max (max_stack e) (max (max_stack e1) (max_stack e2))"
"max_stack (while (e) c) = max (max_stack e) (max_stack c)"
"max_stack (throw e) = max_stack e"
"max_stack (try e1 catch(C i) e2) = max (max_stack e1) (max_stack e2)"
"max_stacks [] = 0"
"max_stacks (e#es) = max (max_stack e) (1 + max_stacks es)"
lemma max_stack1: "1 ≤ max_stack e"
(*<*)by(induct e) (simp_all add:max_def)(*>*)
constdefs
compMb2 :: "expr1 => jvm_method"
"compMb2 ≡ λbody.
let ins = compE2 body @ [Return];
xt = compxE2 body 0 0
in (max_stack body, max_vars body, ins, xt)"
compP2 :: "J1_prog => jvm_prog"
"compP2 ≡ compP compMb2"
(*<*)
declare compP2_def [simp]
(*>*)
lemma compMb2 [simp]:
"compMb2 e = (max_stack e, max_vars e, compE2 e @ [Return], compxE2 e 0 0)"
(*<*)by (simp add: compMb2_def)(*>*)
end
lemma max_stack1:
1 <= max_stack e
lemma compMb2:
compMb2 e = (max_stack e, max_vars e, compE2 e @ [Return], compxE2 e 0 0)