Theory JVMState

Up to index of Isabelle/HOL/verificard

(*  Title:      HOL/MicroJava/JVM/JVMState.thy
    ID:         $Id: JVMState.thy,v 1.5.2.10 2002/03/09 22:12:50 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 == if b then Some (Addr (XcptRef x)) else None"


section {* Runtime State *}

constdefs
  new_Addr :: "aheap => loc × val option"
  "new_Addr h == SOME (a,x). (h a = None \<and>  x = None) |
                             x = raise_system_xcpt True OutOfMemory"
    -- {* redefines @{text "State.new_Addr"} *}

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> obj"
  "blank G C \<equiv> (C,init_vars (fields(G,C)))" 

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

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


section {* Lemmas *}

lemma new_AddrD:
  "new_Addr hp = (ref, xcp) \<Longrightarrow> hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
  apply (drule sym)
  apply (unfold new_Addr_def)
  apply (simp add: raise_system_xcpt_def)
  apply (simp add: Pair_fst_snd_eq Eps_split)
  apply (rule someI)
  apply (rule disjI2)
  apply (rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
  apply auto
  done

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

Runtime State

Lemmas

lemma new_AddrD:

  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)