Up to index of Isabelle/HOL/JinjaThreads
theory Compiler2(* Title: JinjaThreads/Compiler/Compiler2.thy Author: Andreas Lochbihler, Tobias Nipkow *) header {* \isaheader{Compilation Stage 2} *} theory Compiler2 imports PCompiler J1 "../JVM/JVMExec" begin primrec compE2 :: "expr1 => instr list" and compEs2 :: "expr1 list => instr list" where "compE2 (new C) = [New C]" | "compE2 (newA T⌊e⌉) = compE2 e @ [NewArray T]" | "compE2 (Cast T e) = compE2 e @ [Checkcast T]" | "compE2 (Val v) = [Push v]" | "compE2 (e1 «bop» e2) = compE2 e1 @ compE2 e2 @ [BinOpInstr bop]" | "compE2 (Var i) = [Load i]" | "compE2 (i:=e) = compE2 e @ [Store i, Push Unit]" | "compE2 (a⌊i⌉) = compE2 a @ compE2 i @ [ALoad]" | "compE2 (a⌊i⌉ := e) = compE2 a @ compE2 i @ compE2 e @ [AStore, Push Unit]" | "compE2 (a•length) = compE2 a @ [ALength]" | "compE2 (e•F{D}) = compE2 e @ [Getfield F D]" | "compE2 (e1•F{D} := e2) = compE2 e1 @ compE2 e2 @ [Putfield F D, Push Unit]" | "compE2 (e•M(es)) = compE2 e @ compEs2 es @ [Invoke M (size es)]" | "compE2 ({i:T=vo; e}) = (case vo of None => [] | ⌊v⌋ => [Push v, Store i]) @ compE2 e" | "compE2 (syncV (o') e) = compE2 o' @ [Store V, Load V, MEnter] @ compE2 e @ [Load V, MExit, Goto 4, Load V, MExit, ThrowExc]" | "compE2 (insyncV (a) e) = [Goto 1]" -- "Define insync sensibly" | "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 @ [ThrowExc]" | "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 (newA T⌊e⌉) pc d = compxE2 e pc d" "compxE2 (Cast T 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 (a⌊i⌉) pc d = compxE2 a pc d @ compxE2 i (pc + size (compE2 a)) (d + 1)" "compxE2 (a⌊i⌉ := e) pc d = (let pc1 = pc + size (compE2 a); pc2 = pc1 + size (compE2 i) in compxE2 a pc d @ compxE2 i pc1 (d + 1) @ compxE2 e pc2 (d + 2))" "compxE2 (a•length) pc d = compxE2 a pc d" "compxE2 (e•F{D}) pc d = compxE2 e pc d" "compxE2 (e1•F{D} := e2) pc d = compxE2 e1 pc d @ compxE2 e2 (pc + size (compE2 e1)) (d + 1)" "compxE2 (e•M(es)) pc d = compxE2 e pc d @ compxEs2 es (pc + size(compE2 e)) (d+1)" "compxE2 ({i:T=vo; e}) pc d = compxE2 e (case vo of None => pc | ⌊v⌋ => Suc (Suc pc)) d" "compxE2 (syncV (o') e) pc d = (let pc1 = pc + size (compE2 o') + 3; pc2 = pc1 + size(compE2 e) in compxE2 o' pc d @ compxE2 e pc1 d @ [(pc1, pc2, None, Suc (Suc (Suc pc2)), d)])" "compxE2 (insyncV (a) 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,Some C,pc1+1,d)])" "compxEs2 [] pc d = []" "compxEs2 (e#es) pc d = compxE2 e pc d @ compxEs2 es (pc+size(compE2 e)) (d+1)" lemma compE2_neq_Nil [simp]: "compE2 e ≠ []" by(induct e) auto declare compE2_neq_Nil[symmetric, simp] lemma compEs2_append [simp]: "compEs2 (es @ es') = compEs2 es @ compEs2 es'" by(induct es) auto lemma compEs2_eq_Nil_conv [simp]: "compEs2 es = [] <-> es = []" by(cases es) auto lemma compEs2_map_Val: "compEs2 (map Val vs) = map Push vs" by(induct vs) auto lemma compE2_0th_neq_Invoke [simp]: "compE2 e ! 0 ≠ Invoke M n" by(induct e)(auto simp add: nth_append) declare compE2_0th_neq_Invoke[symmetric, simp] lemma compxEs2_append [simp]: "compxEs2 (es @ es') pc d = compxEs2 es pc d @ compxEs2 es' (length (compEs2 es) + pc) (length es + d)" by(induct es arbitrary: pc d)(auto simp add: add_ac) lemma compxEs2_map_Val [simp]: "compxEs2 (map Val vs) pc d = []" by(induct vs arbitrary: d pc) auto lemma compE2_blocks1 [simp]: "compE2 (blocks1 n Ts body) = compE2 body" by(induct n Ts body rule: blocks1.induct)(auto) lemma compxE2_blocks1 [simp]: "compxE2 (blocks1 n Ts body) = compxE2 body" by(induct n Ts body rule: blocks1.induct)(auto intro!: ext) lemma compE2_not_Return: "Return ∉ set (compE2 e)" and compEs2_not_Return: "Return ∉ set (compEs2 es)" by(induct e and es)(auto) primrec max_stack :: "expr1 => nat" and max_stacks :: "expr1 list => nat" where "max_stack (new C) = 1" | "max_stack (newA T⌊e⌉) = max_stack e" | "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 (a⌊i⌉) = max (max_stack a) (max_stack i + 1)" | "max_stack (a⌊i⌉ := e) = max (max (max_stack a) (max_stack i + 1)) (max_stack e + 2)" | "max_stack (a•length) = max_stack a" | "max_stack (e•F{D}) = max_stack e" | "max_stack (e1•F{D} := e2) = max (max_stack e1) (max_stack e2) + 1" | "max_stack (e•M(es)) = max (max_stack e) (max_stacks es) + 1" | "max_stack ({i:T=vo; e}) = max_stack e" | "max_stack (syncV (o') e) = max (max_stack o') (max_stack e + 1)" | "max_stack (insyncV (a) e) = 1" | "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)(*>*) lemma max_stacks_ge_length: "max_stacks es ≥ length es" by(induct es, auto) definition compMb2 :: "expr1 => jvm_method" where "compMb2 ≡ λbody. let ins = compE2 body @ [Return]; xt = compxE2 body 0 0 in (max_stack body, max_vars body, ins, xt)" definition compP2 :: "J1_prog => jvm_prog" where "compP2 ≡ compP compMb2" lemma compMb2: "compMb2 e = (max_stack e, max_vars e, (compE2 e @ [Return]), compxE2 e 0 0)" by (simp add: compMb2_def) end