Theory JinjaDCI.JVMInstructions

(*  Title:      JinjaDCI/JVM/JVMInstructions.thy

    Author:     Gerwin Klein, Susannah Mansky
    Copyright   2000 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory JVM/JVMInstructions.thy by Gerwin Klein
*)

section ‹ Instructions of the JVM ›


theory JVMInstructions imports JVMState 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›
        | Getfield vname cname      ― ‹Fetch field from object›
        | Getstatic cname vname cname     ― ‹Fetch static field from class›
        | Putfield vname cname      ― ‹Set field in object    ›
        | Putstatic cname vname cname     ― ‹Set static field in class›
        | Checkcast cname           ― ‹Check whether object is of given type›
        | Invoke mname nat          ― ‹inv. instance meth of an object›
        | Invokestatic cname mname nat    ― ‹inv. static method of a class›
        | Return                    ― ‹return from method›
        | Pop                       ― ‹pop top element from opstack›
        | IAdd                      ― ‹integer addition›
        | Goto int                  ― ‹goto relative address›
        | CmpEq                     ― ‹equality comparison›
        | IfFalse int               ― ‹branch if top of stack false›
        | Throw                     ― ‹throw top of stack as exception›

type_synonym
  bytecode = "instr list"

type_synonym
  ex_entry = "pc × pc × cname × pc × nat" 
  ― ‹start-pc, end-pc, exception type, handler-pc, remaining stack depth›

type_synonym
  ex_table = "ex_entry list"

type_synonym
  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›

type_synonym
  jvm_prog = "jvm_method prog"

(*<*)
translations
  (type) "bytecode" <= (type) "instr list"
  (type) "ex_entry" <= (type) "nat × nat × char list × nat × nat"
  (type) "ex_table" <= (type) "ex_entry list"
  (type) "jvm_method"   <= (type) "nat × nat × bytecode × ex_table"
  (type) "jvm_prog" <= (type) "jvm_method prog"
(*>*)

end