author | nipkow |
Wed, 01 Dec 1999 18:22:28 +0100 | |
changeset 8045 | 816f566c414f |
parent 8034 | 6fc37b5c5e98 |
child 9376 | c32c5696ec2a |
permissions | -rw-r--r-- |
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 |
||
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
32 |
"exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
33 |
Some (case snd(snd(snd(the(method (G,C) sig)))) ! pc of |
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
34 |
LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc |
8011 | 35 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
36 |
(None,hp,(stk',loc',C,sig,pc')#frs) |
8011 | 37 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
38 |
| CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc |
8011 | 39 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
40 |
(xp',hp',(stk',loc,C,sig,pc')#frs) |
8011 | 41 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
42 |
| MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc |
8011 | 43 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
44 |
(xp',hp',(stk',loc,C,sig,pc')#frs) |
8011 | 45 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
46 |
| CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc |
8011 | 47 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
48 |
(xp',hp,(stk',loc,C,sig,pc')#frs) |
8011 | 49 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
50 |
| MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc |
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
51 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
52 |
(xp',hp,frs'@(stk',loc,C,sig,pc')#frs) |
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
53 |
|
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
54 |
| MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs') |
8011 | 55 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
56 |
| OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc |
8011 | 57 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
58 |
(None,hp,(stk',loc,C,sig,pc')#frs) |
8011 | 59 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
60 |
| BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc |
8011 | 61 |
in |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
62 |
(None,hp,(stk',loc,C,sig,pc')#frs))" |
8011 | 63 |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
64 |
"exec (G, Some xp, hp, frs) = None" |
8011 | 65 |
|
66 |
||
67 |
constdefs |
|
68 |
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}^*" |
|
70 |
||
71 |
end |