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