Theory JVMInstructions

(*  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