13673
|
1 |
(* Title: HOL/MicroJava/Comp/TranslComp.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Martin Strecker
|
|
4 |
*)
|
|
5 |
|
|
6 |
(* Compiling MicroJava into MicroJVM -- Translation functions *)
|
|
7 |
|
|
8 |
theory TranslComp = TranslCompTp:
|
|
9 |
|
|
10 |
|
|
11 |
(* parameter java_mb only serves to define function index later *)
|
|
12 |
consts
|
|
13 |
compExpr :: "java_mb => expr => instr list"
|
|
14 |
compExprs :: "java_mb => expr list => instr list"
|
|
15 |
compStmt :: "java_mb => stmt => instr list"
|
|
16 |
|
|
17 |
|
|
18 |
|
|
19 |
(**********************************************************************)
|
|
20 |
(** code generation for expressions **)
|
|
21 |
|
|
22 |
primrec
|
|
23 |
(*class instance creation*)
|
|
24 |
"compExpr jmb (NewC c) = [New c]"
|
|
25 |
|
|
26 |
(*type cast*)
|
|
27 |
"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]"
|
|
28 |
|
|
29 |
|
|
30 |
(*literals*)
|
|
31 |
"compExpr jmb (Lit val) = [LitPush val]"
|
|
32 |
|
|
33 |
|
|
34 |
(* binary operation *)
|
|
35 |
"compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @
|
|
36 |
(case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
|
|
37 |
| Add => [IAdd])"
|
|
38 |
|
|
39 |
(*local variable*)
|
|
40 |
"compExpr jmb (LAcc vn) = [Load (index jmb vn)]"
|
|
41 |
|
|
42 |
|
|
43 |
(*assignement*)
|
|
44 |
"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]"
|
|
45 |
|
|
46 |
|
|
47 |
(*field access*)
|
|
48 |
"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
|
|
49 |
|
|
50 |
|
|
51 |
(*field assignement - expected syntax: {_}_.._:=_ *)
|
|
52 |
"compExpr jmb (FAss cn e1 fn e2 ) =
|
|
53 |
compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
|
|
54 |
|
|
55 |
|
|
56 |
(*method call*)
|
|
57 |
"compExpr jmb (Call cn e1 mn X ps) =
|
|
58 |
compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
|
|
59 |
|
|
60 |
|
|
61 |
(** code generation expression lists **)
|
|
62 |
|
|
63 |
"compExprs jmb [] = []"
|
|
64 |
|
|
65 |
"compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
|
|
66 |
|
|
67 |
|
|
68 |
|
|
69 |
primrec
|
|
70 |
(** code generation for statements **)
|
|
71 |
|
|
72 |
"compStmt jmb Skip = []"
|
|
73 |
|
|
74 |
"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
|
|
75 |
|
|
76 |
"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
|
|
77 |
|
|
78 |
"compStmt jmb (If(e) c1 Else c2) =
|
|
79 |
(let cnstf = LitPush (Bool False);
|
|
80 |
cnd = compExpr jmb e;
|
|
81 |
thn = compStmt jmb c1;
|
|
82 |
els = compStmt jmb c2;
|
|
83 |
test = Ifcmpeq (int(length thn +2));
|
|
84 |
thnex = Goto (int(length els +1))
|
|
85 |
in
|
|
86 |
[cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
|
|
87 |
|
|
88 |
"compStmt jmb (While(e) c) =
|
|
89 |
(let cnstf = LitPush (Bool False);
|
|
90 |
cnd = compExpr jmb e;
|
|
91 |
bdy = compStmt jmb c;
|
|
92 |
test = Ifcmpeq (int(length bdy +2));
|
|
93 |
loop = Goto (-(int((length bdy) + (length cnd) +2)))
|
|
94 |
in
|
|
95 |
[cnstf] @ cnd @ [test] @ bdy @ [loop])"
|
|
96 |
|
|
97 |
(**********************************************************************)
|
|
98 |
|
|
99 |
(*compiling methods, classes and programs*)
|
|
100 |
|
|
101 |
(*initialising a single variable*)
|
|
102 |
constdefs
|
|
103 |
load_default_val :: "ty => instr"
|
|
104 |
"load_default_val ty == LitPush (default_val ty)"
|
|
105 |
|
|
106 |
compInit :: "java_mb => (vname * ty) => instr list"
|
|
107 |
"compInit jmb == \<lambda> (vn,ty). [load_default_val ty, Store (index jmb vn)]"
|
|
108 |
|
|
109 |
compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode"
|
|
110 |
"compInitLvars jmb lvars == concat (map (compInit jmb) lvars)"
|
|
111 |
|
|
112 |
compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl"
|
|
113 |
"compMethod G C jmdl == let (sig, rT, jmb) = jmdl;
|
|
114 |
(pns,lvars,blk,res) = jmb;
|
|
115 |
mt = (compTpMethod G C jmdl);
|
|
116 |
bc = compInitLvars jmb lvars @
|
|
117 |
compStmt jmb blk @ compExpr jmb res @
|
|
118 |
[Return]
|
|
119 |
in (sig, rT, max_ssize mt, length lvars, bc, [])"
|
|
120 |
|
|
121 |
compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl"
|
|
122 |
"compClass G == \<lambda> (C,cno,fdls,jmdls). (C,cno,fdls, map (compMethod G C) jmdls)"
|
|
123 |
|
|
124 |
comp :: "java_mb prog => jvm_prog"
|
|
125 |
"comp G == map (compClass G) G"
|
|
126 |
|
|
127 |
end
|
|
128 |
|
|
129 |
|