Theory JVMState

Up to index of Isabelle/HOL/arrays

(*  Title:      HOL/MicroJava/JVM/JVMState.thy
    ID:         $Id: JVMState.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

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

theory JVMState = Conform:

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)"

 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 \<Rightarrow> xcpt \<Rightarrow> val option"
  "raise_system_xcpt b x \<equiv> if b then Some (Addr (XcptRef x)) else None"

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

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

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


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

  blank_arr :: "ty \<Rightarrow> nat \<Rightarrow> heap_entry"
  "blank_arr T len \<equiv> Arr T len (\<lambda>x. if x < len then Some (default_val T) else None)"

  start_heap :: "'c prog \<Rightarrow> aheap"
  "start_heap G \<equiv> 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))"

  start_iheap :: init_heap
  "start_iheap \<equiv> ((((((\<lambda>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)))"


section {* Lemmas *}

lemma new_AddrD:
  assumes new: "new_Addr hp = (ref, xcp)" 
  shows "hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
proof -
  from new obtain xcpT where old: "State.new_Addr hp = (ref,xcpT)"
    by (cases "State.new_Addr hp") (simp add: new_Addr_def)
  from this [symmetric] 
  have "hp ref = None \<and> xcpT = None \<or> xcpT = Some OutOfMemory" 
    by (rule State.new_AddrD)
  with new old show ?thesis
    by (auto simp add: new_Addr_def raise_system_xcpt_def)
qed


lemma new_Addr_OutOfMemory:
  "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
proof - 
  obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
  moreover assume "snd (new_Addr hp) = Some xcp" 
  ultimately show ?thesis by (auto dest: new_AddrD)
qed  

end

Frame Stack

Exceptions

Lemmas

lemma

  JVMState.new_Addr hp = (ref, xcp)
  ==> hp ref = None & xcp = None | xcp = Some (Addr (XcptRef OutOfMemory))

lemma new_Addr_OutOfMemory:

  snd (JVMState.new_Addr hp) = Some xcp ==> xcp = Addr (XcptRef OutOfMemory)