Theory JVMInstructions

(*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
    ID:         $Id: JVMInstructions.thy,v 1.5.2.5 2002/08/06 10:39:06 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen
*)

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

theory JVMInstructions 
imports JVMState BinOP begin

text{* Apply Binary Operation *}

consts
 "applyBinOp" :: "[PrimOp,val,val] => val"


primrec
   "applyBinOp Equal b1 b2 = (if (the_Intg(b1) = the_Intg(b2)) then Intg 1 else Intg 0)"
   "applyBinOp NotEqual b1 b2 = (if (the_Intg(b1) ≠ the_Intg(b2)) then Intg 1 else Intg 0)"
   "applyBinOp GreaterEqual b1 b2 = (if (the_Intg(b1) ≥ the_Intg(b2)) then Intg 1 else Intg 0)"
   "applyBinOp GreaterThan b1 b2 = (if (the_Intg(b1) > the_Intg(b2)) then Intg 1 else Intg 0)"
   "applyBinOp LessThan b1 b2 = (if (the_Intg(b1) < the_Intg(b2)) then Intg 1 else Intg 0)"
   "applyBinOp LessEqual b1 b2 = (if (the_Intg(b1) ≤ the_Intg(b2)) then Intg 1 else Intg 0)"
   "applyBinOp Add b1 b2 = Intg (the_Intg(b1) + the_Intg(b2))"
   "applyBinOp Substract b1 b2 = Intg (the_Intg(b1) - the_Intg(b2))"
   "applyBinOp Times b1 b2 = Intg (the_Intg(b1) * the_Intg(b2))"
   "applyBinOp Divide  b1 b2 = Intg (the_Intg(b1) div the_Intg(b2))"


text{* Apply  ifcmp Generic for integers *}

consts
 "applyIf" :: "[PrimOp,val,val] => bool"


primrec
   "applyIf Equal b1 b2 =(the_Intg(b1) = the_Intg(b2))"
   "applyIf NotEqual b1 b2 = (the_Intg(b1) ≠ the_Intg(b2))"
   "applyIf GreaterEqual b1 b2 = (the_Intg(b1) ≥ the_Intg(b2))"
   "applyIf GreaterThan b1 b2 = (the_Intg(b1) > the_Intg(b2))"
   "applyIf LessThan b1 b2 = (the_Intg(b1) < the_Intg(b2))"
   "applyIf LessEqual b1 b2 = (the_Intg(b1) ≤ the_Intg(b2))"
   


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"
        | Invoke_special cname mname "ty list" 
                                    -- "no dynamic type lookup, for constructors"
        | Return                    -- "return from method"
        | Return_Void               -- "return from void method"
        | Pop                       -- "pop top element from opstack"
        | Dup                       -- "duplicate top element of opstack"
        | Dup2                      -- "duplicate two element of opstack"   
        | Dup_x1                    -- "duplicate next to top element"
        | Dup_x2                    -- "duplicate 3rd element"
        | 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"
        | Jsr int                   -- "jump to subroutine"
        | Ret nat                   -- "return from subroutine"
        | ArrLoad                   -- "load indexed entry from array"
        | ArrStore                  -- "store value into indexed array entry"
        | ArrLength                 -- "get array length"
        | ArrNew ty                 -- "create new 1-dimensional array"
        | Invoke_static cname mname "(ty list)" -- "invoke a class (static) method"
        | Getstatic vname cname     --  "get value of static field"
        | Putstatic vname cname     -- "set value of static field"
        | Tableswitch int int "(int list)" -- "jump according to a table"
        | BinOp PrimOp                  -- "Binary Operation"
        | Ifcmp PrimOp int     -- " Generic Branch "  


types
  bytecode = "instr list"
  exception_entry = "p_count × p_count × p_count × cname" 
                  -- "start-pc, end-pc, handler-pc, exception type"
  exception_table = "exception_entry list"
  jvm_method = "nat × nat × bytecode × exception_table"
  jvm_prog = "jvm_method prog" 

end