| author | kleing |
| Tue, 05 Dec 2000 14:08:22 +0100 | |
| changeset 10591 | 6d6cb845e841 |
| parent 10057 | 8c8d2d0d3ef8 |
| child 10897 | 697fab84709e |
| permissions | -rw-r--r-- |
| 9376 | 1 |
(* Title: HOL/MicroJava/JVM/JVMInstructions.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein |
|
4 |
Copyright 2000 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
| 10057 | 7 |
header {* Instructions of the JVM *}
|
8 |
||
9 |
||
10 |
theory JVMInstructions = JVMState: |
|
| 9376 | 11 |
|
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
12 |
|
| 9376 | 13 |
datatype |
14 |
instr = Load nat (* load from local variable *) |
|
15 |
| Store nat (* store into local variable *) |
|
16 |
| Bipush int (* push int *) |
|
17 |
| Aconst_null (* push null *) |
|
18 |
| New cname (* create object *) |
|
19 |
| Getfield vname cname (* Fetch field from object *) |
|
20 |
| Putfield vname cname (* Set field in object *) |
|
21 |
| Checkcast cname (* Check whether object is of given type *) |
|
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
22 |
| Invoke cname mname "(ty list)" (* inv. instance meth of an object *) |
| 10057 | 23 |
| Return (* return from method *) |
24 |
| Pop (* pop top element from opstack *) |
|
25 |
| Dup (* duplicate top element of opstack *) |
|
26 |
| Dup_x1 (* duplicate next to top element *) |
|
27 |
| Dup_x2 (* duplicate 3rd element *) |
|
28 |
| Swap (* swap top and next to top element *) |
|
29 |
| IAdd (* integer addition *) |
|
30 |
| Goto int (* goto relative address *) |
|
| 9376 | 31 |
| Ifcmpeq int (* Branch if int/ref comparison succeeds *) |
32 |
||
33 |
||
34 |
types |
|
35 |
bytecode = "instr list" |
|
| 10591 | 36 |
jvm_prog = "(nat \<times> nat \<times> bytecode) prog" |
| 9376 | 37 |
|
38 |
end |