|
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 |
|
17 | MR |
|
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 |
|
54 | MR \\<Rightarrow> (let frs' = exec_mr stk frs in |
|
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 |