1(*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
2    Author:     Gerwin Klein, Technische Universitaet Muenchen
3*)
4
5section \<open>Instructions of the JVM\<close>
6
7
8theory JVMInstructions imports JVMState begin
9
10
11datatype 
12  instr = Load nat                  \<comment> \<open>load from local variable\<close>
13        | Store nat                 \<comment> \<open>store into local variable\<close>
14        | LitPush val               \<comment> \<open>push a literal (constant)\<close>
15        | New cname                 \<comment> \<open>create object\<close>
16        | Getfield vname cname      \<comment> \<open>Fetch field from object\<close>
17        | Putfield vname cname      \<comment> \<open>Set field in object\<close>
18        | Checkcast cname           \<comment> \<open>Check whether object is of given type\<close>
19        | Invoke cname mname "(ty list)"  \<comment> \<open>inv. instance meth of an object\<close>
20        | Return                    \<comment> \<open>return from method\<close>
21        | Pop                       \<comment> \<open>pop top element from opstack\<close>
22        | Dup                       \<comment> \<open>duplicate top element of opstack\<close>
23        | Dup_x1                    \<comment> \<open>duplicate top element and push 2 down\<close>
24        | Dup_x2                    \<comment> \<open>duplicate top element and push 3 down\<close>
25        | Swap                      \<comment> \<open>swap top and next to top element\<close>
26        | IAdd                      \<comment> \<open>integer addition\<close>
27        | Goto int                  \<comment> \<open>goto relative address\<close>
28        | Ifcmpeq int               \<comment> \<open>branch if int/ref comparison succeeds\<close>
29        | Throw                     \<comment> \<open>throw top of stack as exception\<close>
30
31type_synonym
32  bytecode = "instr list"
33type_synonym
34  exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
35                  \<comment> \<open>start-pc, end-pc, handler-pc, exception type\<close>
36type_synonym
37  exception_table = "exception_entry list"
38type_synonym
39  jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
40   \<comment> \<open>max stacksize, size of register set, instruction sequence, handler table\<close>
41type_synonym
42  jvm_prog = "jvm_method prog" 
43
44end
45