4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
5 |
6 Execution of the JVM |
6 Execution of the JVM |
7 *) |
7 *) |
8 |
8 |
9 JVMExec = LoadAndStore + Object + Method + Opstack + Control + |
9 JVMExec = JVMExecInstr + |
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 |
|
17 | MR meth_ret |
|
18 | OS op_stack |
|
19 | BR branch |
|
20 |
|
21 types |
|
22 bytecode = instr list |
|
23 jvm_prog = "(nat \\<times> bytecode)prog" |
|
24 |
10 |
25 consts |
11 consts |
26 exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option" |
12 exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option" |
27 |
13 |
28 (** exec is not recursive. recdef is just used because for pattern matching **) |
14 (** exec is not recursive. recdef is just used for pattern matching **) |
29 recdef exec "{}" |
15 recdef exec "{}" |
30 "exec (G, xp, hp, []) = None" |
16 "exec (G, xp, hp, []) = None" |
31 |
17 |
32 "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
18 "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
33 Some (case snd(snd(snd(the(method (G,C) sig)))) ! pc of |
19 (let |
34 LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc |
20 i = snd(snd(snd(the(method (G,C) sig)))) ! pc |
35 in |
21 in |
36 (None,hp,(stk',loc',C,sig,pc')#frs) |
22 Some (exec_instr i G hp stk loc C sig pc frs))" |
37 |
23 |
38 | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc |
24 "exec (G, Some xp, hp, frs) = None" |
39 in |
|
40 (xp',hp',(stk',loc,C,sig,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,C,sig,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,C,sig,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,C,sig,pc')#frs) |
|
53 |
|
54 | MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs') |
|
55 |
|
56 | OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc |
|
57 in |
|
58 (None,hp,(stk',loc,C,sig,pc')#frs) |
|
59 |
|
60 | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc |
|
61 in |
|
62 (None,hp,(stk',loc,C,sig,pc')#frs))" |
|
63 |
|
64 "exec (G, Some xp, hp, frs) = None" |
|
65 |
25 |
66 |
26 |
67 constdefs |
27 constdefs |
68 exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool" ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60) |
28 exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool" ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60) |
69 "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*" |
29 "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*" |