author | wenzelm |
Tue, 16 Jan 2018 09:30:00 +0100 | |
changeset 67443 | 3abf6a722518 |
parent 62042 | 6c6ccf573479 |
permissions | -rw-r--r-- |
9376 | 1 |
(* Title: HOL/MicroJava/JVM/JVMInstructions.thy |
41589 | 2 |
Author: Gerwin Klein, Technische Universitaet Muenchen |
9376 | 3 |
*) |
4 |
||
61361 | 5 |
section \<open>Instructions of the JVM\<close> |
10057 | 6 |
|
7 |
||
16417 | 8 |
theory JVMInstructions imports JVMState begin |
9376 | 9 |
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
10 |
|
58310 | 11 |
datatype |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
12 |
instr = Load nat \<comment> \<open>load from local variable\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
13 |
| Store nat \<comment> \<open>store into local variable\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
14 |
| LitPush val \<comment> \<open>push a literal (constant)\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
15 |
| New cname \<comment> \<open>create object\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
16 |
| Getfield vname cname \<comment> \<open>Fetch field from object\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
17 |
| Putfield vname cname \<comment> \<open>Set field in object\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
18 |
| Checkcast cname \<comment> \<open>Check whether object is of given type\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
19 |
| Invoke cname mname "(ty list)" \<comment> \<open>inv. instance meth of an object\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
20 |
| Return \<comment> \<open>return from method\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
21 |
| Pop \<comment> \<open>pop top element from opstack\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
22 |
| Dup \<comment> \<open>duplicate top element of opstack\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
23 |
| Dup_x1 \<comment> \<open>duplicate top element and push 2 down\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
24 |
| Dup_x2 \<comment> \<open>duplicate top element and push 3 down\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
25 |
| Swap \<comment> \<open>swap top and next to top element\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
26 |
| IAdd \<comment> \<open>integer addition\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
27 |
| Goto int \<comment> \<open>goto relative address\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
28 |
| Ifcmpeq int \<comment> \<open>branch if int/ref comparison succeeds\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
29 |
| Throw \<comment> \<open>throw top of stack as exception\<close> |
9376 | 30 |
|
42463 | 31 |
type_synonym |
9376 | 32 |
bytecode = "instr list" |
42463 | 33 |
type_synonym |
12519 | 34 |
exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
35 |
\<comment> \<open>start-pc, end-pc, handler-pc, exception type\<close> |
42463 | 36 |
type_synonym |
12519 | 37 |
exception_table = "exception_entry list" |
42463 | 38 |
type_synonym |
12519 | 39 |
jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
40 |
\<comment> \<open>max stacksize, size of register set, instruction sequence, handler table\<close> |
42463 | 41 |
type_synonym |
12519 | 42 |
jvm_prog = "jvm_method prog" |
9376 | 43 |
|
44 |
end |