Theory JVMState

(*  Title:      HOL/MicroJava/JVM/JVMState.thy
    ID:         $Id: JVMState.thy,v 1.5.2.13 2002/08/09 14:02:05 kleing Exp $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* 
  {Java Virtual Machine}\label{cha:jvm}
  \isaheader{State of the JVM} 
*}

theory JVMState
imports State
begin
text {*  
For object initialization, we tag each location with the current init 
status. The tags use an extended type system for object initialization
(that gets reused in the BV).
 
We have either  
\begin{itemize}
\item usual initialized types, or
\item a class that is not yet initialized and has been created
      by a @{text New} instruction at a certain line number, or 
\item a partly initialized class (on which the next super class 
      constructor has to be called). We store the name of the class
      the super class constructor has to be called of.
\end{itemize}
*}  
datatype init_ty = Init ty | UnInit cname nat | PartInit cname

section {* Frame Stack *}
types
 opstack   = "val list"
 locvars   = "val list" 
 p_count   = nat
 ref_upd    = "(val × val)"
 sheap = "cname × vname \<rightharpoonup> val"


 frame = "opstack ×     
          locvars ×   
          cname ×     
          sig ×     
          p_count × 
          ref_upd"

  -- "operand stack" 
  -- "local variables (including this pointer and method parameters)"
  -- "name of class where current method is defined"
  -- "method name + parameter types"
  -- "program counter within frame"
  -- "ref update for obj init proof"


section {* Exceptions *}
constdefs
  raise_system_xcpt :: "bool => xcpt => val option"
  "raise_system_xcpt b x ≡ if b then Some (Addr (XcptRef x)) else None"

  -- "redefines State.new\\_Addr:"
  new_Addr :: "aheap => loc × val option"
  "new_Addr h ≡ let (a, x) = State.new_Addr h 
                in  (a, raise_system_xcpt (x ~= None) OutOfMemory)"

types
  init_heap = "loc => init_ty" 
    -- "type tags to track init status of objects"

  jvm_state = "val option × sheap × aheap × init_heap × frame list"  
    -- "exception flag,static heap, heap, tag heap, frames"


text {* a new, blank object with default values in all fields: *}
constdefs
  blank :: "'c prog => cname => heap_entry"
  "blank G C ≡ Obj C (init_vars (fields(G,C)))" 

  blank_arr :: "ty => nat => heap_entry"
  "blank_arr T len ≡ Arr T len (λx. if x < len then Some (default_val T) else None)"

  start_heap :: "'c prog => aheap"
  "start_heap G ≡ empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
                      (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
                      (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))
                      (XcptRef ArrayIndexOutOfBounds \<mapsto> blank G (Xcpt ArrayIndexOutOfBounds))
                      (XcptRef NegativeArraySize \<mapsto> blank G (Xcpt NegativeArraySize))
                      (XcptRef ArrayStore \<mapsto> blank G (Xcpt ArrayStore))"

(* Initialize static heap *)
 start_sheap :: "'c prog => sheap"
  "start_sheap G ≡ empty"  

  start_iheap :: init_heap
  "start_iheap ≡ ((((((λx. arbitrary) 
                  (XcptRef NullPointer := Init (Class (Xcpt NullPointer))))
                  (XcptRef ClassCast := Init (Class (Xcpt ClassCast))))
                  (XcptRef OutOfMemory := Init (Class ((Xcpt OutOfMemory)))))
                  (XcptRef ArrayIndexOutOfBounds := Init (Class (Xcpt ArrayIndexOutOfBounds))))
                  (XcptRef NegativeArraySize := Init (Class (Xcpt NegativeArraySize))))
                  (XcptRef ArrayStore := Init (Class (Xcpt ArrayStore)))"




end