8011
|
1 |
(* Title: HOL/MicroJava/JVM/JVMExec.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Cornelia Pusch
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
|
|
6 |
Execution of the JVM
|
|
7 |
*)
|
|
8 |
|
|
9 |
JVMExec = LoadAndStore + Object + Method + Opstack + Control +
|
|
10 |
|
|
11 |
datatype
|
|
12 |
instr = LS load_and_store
|
|
13 |
| CO create_object
|
|
14 |
| MO manipulate_object
|
|
15 |
| CH check_object
|
|
16 |
| MI meth_inv
|
8032
|
17 |
| MR meth_ret
|
8011
|
18 |
| OS op_stack
|
|
19 |
| BR branch
|
|
20 |
|
|
21 |
types
|
|
22 |
bytecode = instr list
|
|
23 |
jvm_prog = "(nat \\<times> bytecode)prog"
|
|
24 |
|
|
25 |
consts
|
|
26 |
exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
|
|
27 |
|
|
28 |
(** exec is not recursive. recdef is just used because for pattern matching **)
|
|
29 |
recdef exec "{}"
|
|
30 |
"exec (G, xp, hp, []) = None"
|
|
31 |
|
|
32 |
"exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) =
|
|
33 |
Some (case snd(snd(snd(the(cmethd (G,cn) ml)))) ! pc of
|
|
34 |
LS ins \\<Rightarrow> (let (stk',loc',pc') = exec_las ins stk loc pc
|
|
35 |
in
|
|
36 |
(None,hp,(stk',loc',cn,ml,pc')#frs))
|
|
37 |
|
|
38 |
| CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
|
|
39 |
in
|
|
40 |
(xp',hp',(stk',loc,cn,ml,pc')#frs))
|
|
41 |
|
|
42 |
| MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
|
|
43 |
in
|
|
44 |
(xp',hp',(stk',loc,cn,ml,pc')#frs))
|
|
45 |
|
|
46 |
| CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
|
|
47 |
in
|
|
48 |
(xp',hp,(stk',loc,cn,ml,pc')#frs))
|
|
49 |
|
|
50 |
| MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
|
|
51 |
in
|
|
52 |
(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
|
|
53 |
|
8032
|
54 |
| MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
|
8011
|
55 |
(None,hp,frs'))
|
|
56 |
|
|
57 |
| OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
|
|
58 |
in
|
|
59 |
(None,hp,(stk',loc,cn,ml,pc')#frs))
|
|
60 |
|
|
61 |
| BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
|
|
62 |
in
|
|
63 |
(None,hp,(stk',loc,cn,ml,pc')#frs)))"
|
|
64 |
|
|
65 |
"exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
|
|
66 |
|
|
67 |
|
|
68 |
constdefs
|
|
69 |
exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool" ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
|
|
70 |
"G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
|
|
71 |
|
|
72 |
end
|