Theory JVMInstructions

(*  Title:      JinjaThreads/JVM/JVMInstructions.thy
    Author:     Gerwin Klein, Andreas Lochbihler
*)

header {* \isaheader{Instructions of the JVM} *}

theory JVMInstructions imports JVMState "../Common/BinOp" begin

datatype 
  instr = Load nat                  -- "load from local variable"
        | Store nat                 -- "store into local variable"
        | Push val                  -- "push a value (constant)"
        | New cname                 -- "create object"
        | NewArray ty               -- "create array for elements of given type"
        | ALoad                     -- "Load array element from heap to stack"
        | AStore                    -- "Set element in array"
        | ALength                   -- "Return the length of the array"
        | Getfield vname cname      -- "Fetch field from object"
        | Putfield vname cname      -- "Set field in object    "
        | Checkcast ty              -- "Check whether object is of given type"
        | Invoke mname nat          -- "inv. instance meth of an object"
        | Return                    -- "return from method"
        | Pop                       -- "pop top element from opstack"
        | BinOpInstr bop            -- "binary operator instruction"
        | Goto int                  -- "goto relative address"
        | IfFalse int               -- "branch if top of stack false"
        | ThrowExc                  -- "throw top of stack as exception"
        | MEnter                    -- "enter the monitor of object on top of the stack"
        | MExit                     -- "exit the monitor of object on top of the stack"

abbreviation IAdd :: instr
where "IAdd ≡ BinOpInstr Add"

abbreviation CmpEq :: instr
where "CmpEq ≡ BinOpInstr Eq"

abbreviation ISub :: instr
where "ISub ≡ BinOpInstr Subtract"

abbreviation IMult :: instr
where "IMult ≡ BinOpInstr Mult"

abbreviation IMod :: instr
where "IMod ≡ BinOpInstr Mod"

types
  bytecode = "instr list"

  ex_entry = "pc × pc × cname option × pc × nat" 
  -- "start-pc, end-pc, exception type (None = Any), handler-pc, remaining stack depth"

  ex_table = "ex_entry list"

  jvm_method = "nat × nat × bytecode × ex_table"
   -- "max stacksize"
   -- "number of local variables. Add 1 + no. of parameters to get no. of registers"
   -- "instruction sequence"
   -- "exception handler table"

  jvm_prog = "jvm_method prog" 

end