Quelle  JVMInstructions.thy

(*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
  Author: Gerwin Klein, Technische Universitaet Muenchen
*)

section ‹Instructions of the JVM›


theory JVMInstructions imports JVMState begin


datatype 
  instr = Load nat                  🍋 ‹load from local variable›
        | Store nat                 🍋 ‹store into local variable›
        | LitPush val               🍋 ‹push a literal (constant)›
        | New cname                 🍋 ‹create object›
        | Getfield vname cname      🍋 ‹Fetch field from object›
        | Putfield vname cname      🍋 ‹Set field in object›
        | Checkcast cname           🍋 ‹Check whether object is of given type›
        | Invoke cname mname "(ty list)"  🍋 ‹inv. instance meth of an object›
        | Return                    🍋 ‹return from method›
        | Pop                       🍋 ‹pop top element from opstack›
        | Dup                       🍋 ‹duplicate top element of opstack›
        | Dup_x1                    🍋 ‹duplicate top element and push 2 down›
        | Dup_x2                    🍋 ‹duplicate top element and push 3 down›
        | Swap                      🍋 ‹swap top and next to top element›
        | IAdd                      🍋 ‹integer addition›
        | Goto int                  🍋 ‹goto relative address›
        | Ifcmpeq int               🍋 ‹branch if int/ref comparison succeeds›
        | Throw                     🍋 ‹throw top of stack as exception›

type_synonym
  bytecode = "instr list"
type_synonym
  exception_entry = "p_count × p_count × p_count × cname" 
                  🍋 ‹start-pc, end-pc, handler-pc, exception type›
type_synonym
  exception_table = "exception_entry list"
type_synonym
  jvm_method = "nat × nat × bytecode × exception_table"
   🍋 ‹max stacksize, size of register set, instruction sequence, handler table›
type_synonym
  jvm_prog = "jvm_method prog" 

end