author | wenzelm |
Mon, 15 Nov 2010 17:40:38 +0100 | |
changeset 40547 | 05a82b4bccbc |
parent 16417 | 9bc16273c2d4 |
child 41589 | bbd861837ebc |
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 |
||
12911 | 7 |
header {* \isaheader{Instructions of the JVM} *} |
10057 | 8 |
|
9 |
||
16417 | 10 |
theory JVMInstructions imports JVMState begin |
9376 | 11 |
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
12 |
|
9376 | 13 |
datatype |
12519 | 14 |
instr = Load nat -- "load from local variable" |
15 |
| Store nat -- "store into local variable" |
|
16 |
| LitPush val -- "push a literal (constant)" |
|
17 |
| New cname -- "create object" |
|
18 |
| Getfield vname cname -- "Fetch field from object" |
|
19 |
| Putfield vname cname -- "Set field in object " |
|
20 |
| Checkcast cname -- "Check whether object is of given type" |
|
21 |
| Invoke cname mname "(ty list)" -- "inv. instance meth of an object" |
|
22 |
| Return -- "return from method" |
|
23 |
| Pop -- "pop top element from opstack" |
|
24 |
| Dup -- "duplicate top element of opstack" |
|
13676 | 25 |
| Dup_x1 -- "duplicate top element and push 2 down" |
26 |
| Dup_x2 -- "duplicate top element and push 3 down" |
|
12519 | 27 |
| Swap -- "swap top and next to top element" |
28 |
| IAdd -- "integer addition" |
|
29 |
| Goto int -- "goto relative address" |
|
30 |
| Ifcmpeq int -- "branch if int/ref comparison succeeds" |
|
31 |
| Throw -- "throw top of stack as exception" |
|
9376 | 32 |
|
33 |
types |
|
34 |
bytecode = "instr list" |
|
12519 | 35 |
exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" |
36 |
-- "start-pc, end-pc, handler-pc, exception type" |
|
37 |
exception_table = "exception_entry list" |
|
38 |
jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table" |
|
13676 | 39 |
-- "max stacksize, size of register set, instruction sequence, handler table" |
12519 | 40 |
jvm_prog = "jvm_method prog" |
9376 | 41 |
|
42 |
end |