Theory Compiler2

(*  Title:      JinjaDCI/Compiler/Compiler2.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   TUM 2003, UIUC 2019-20

    Based on the Jinja theory Compiler/Compiler2.thy by Tobias Nipkow
*)

section ‹ Compilation Stage 2 ›

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

lemma bop_expr_length_aux [simp]:
 "length (case bop of Eq ⇒ [CmpEq] | Add ⇒ [IAdd]) = Suc 0"
 by(cases bop, simp+)

primrec compE2 :: "expr1 ⇒ instr list"
  and compEs2 :: "expr1 list ⇒ instr list" where
  "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∙F{D}) = compE2 e @ [Getfield F D]"
| "compE2 (C∙sF{D}) = [Getstatic C F D]"
| "compE2 (e1∙F{D} := e2) =
       compE2 e1 @ compE2 e2 @ [Putfield F D, Push Unit]"
| "compE2 (C∙sF{D} := e2) =
       compE2 e2 @ [Putstatic C F D, Push Unit]"
| "compE2 (e∙M(es)) = compE2 e @ compEs2 es @ [Invoke M (size es)]"
| "compE2 (C∙sM(es)) = compEs2 es @ [Invokestatic C 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)"
| "compE2 (INIT C (Cs,b) ← e) = []"
| "compE2 (RI(C,e);Cs ← e') = []"

| "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. ›

primrec compxE2  :: "expr1      ⇒ pc ⇒ nat ⇒ ex_table"
  and compxEs2 :: "expr1 list ⇒ pc ⇒ nat ⇒ ex_table" where
  "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∙F{D}) pc d = compxE2 e pc d"
| "compxE2 (C∙sF{D}) pc d = []"
| "compxE2 (e1∙F{D} := e2) pc d =
   compxE2 e1 pc d @ compxE2 e2 (pc + size(compE2 e1)) (d+1)"
| "compxE2 (C∙sF{D} := e2) pc d = compxE2 e2 pc d"
| "compxE2 (e∙M(es)) pc d =
   compxE2 e pc d @ compxEs2 es (pc + size(compE2 e)) (d+1)"
| "compxE2 (C∙sM(es)) pc d = compxEs2 es pc d"
| "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)])"
| "compxE2 (INIT C (Cs, b) ← e) pc d = []"
| "compxE2 (RI(C, e);Cs ← e') pc d = []"

| "compxEs2 [] pc d    = []"
| "compxEs2 (e#es) pc d = compxE2 e pc d @ compxEs2 es (pc+size(compE2 e)) (d+1)"

primrec max_stack :: "expr1 ⇒ nat"
  and max_stacks :: "expr1 list ⇒ nat" where
  "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∙F{D}) = max_stack e"
| "max_stack (C∙sF{D}) = 1"
| "max_stack (e1∙F{D} := e2) = max (max_stack e1) (max_stack e2) + 1"
| "max_stack (C∙sF{D} := e2) = max_stack e2"
| "max_stack (e∙M(es)) = max (max_stack e) (max_stacks es) + 1"
| "max_stack (C∙sM(es)) = 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': "¬sub_RI e ⟹ 1 ≤ max_stack e"
(*<*)by(induct e) (simp_all add:max_def)(*>*)

lemma compE2_not_Nil': "¬sub_RI e ⟹ compE2 e ≠ []"
(*<*)by(induct e) auto(*>*)

lemma compE2_nRet: "⋀i. i ∈ set (compE2 e1) ⟹ i ≠ Return"
 and "⋀i. i ∈ set (compEs2 es1) ⟹ i ≠ Return"
 by(induct rule: compE2.induct compEs2.induct, auto simp: nth_append split: bop.splits)


definition compMb2 :: "staticb ⇒ expr1 ⇒ jvm_method"
where
  "compMb2  ≡  λb 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"

(*<*)
declare compP2_def [simp]
(*>*)

lemma compMb2 [simp]:
  "compMb2 b e = (max_stack e, max_vars e,
                   compE2 e @ [Return], compxE2 e 0 0)"
(*<*)by (simp add: compMb2_def)(*>*)

end