(*  Title:      Jinja/JVM/JVMState.thy

    Author:     Cornelia Pusch, Gerwin Klein, Susannah Mansky
    Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory JVM/JVMState.thy by Cornelia Pusch and Gerwin Klein
*)

chapter ‹ Jinja Virtual Machine \label{cha:jvm} ›

section ‹ State of the JVM ›

theory JVMState imports "../Common/Objects" begin


type_synonym 
  pc = nat

abbreviation start_sheap :: "sheap"
where "start_sheap ≡ (λx. None)(Start ↦ (Map.empty,Done))"

definition start_sheap_preloaded :: "'m prog → sheap"
where
  "start_sheap_preloaded P ≡ fold (λ(C,cl) f. f(C := Some (sblank P C, Prepared))) P (λx. None)"

subsection ‹ Frame Stack ›

datatype init_call_status = No_ics | Calling cname "cname list"
                          | Called "cname list" | Throwing "cname list" addr
 ― ‹@{text "No_ics"} = not currently calling or waiting for the result of an initialization procedure call›
  ― ‹@{text "Calling C Cs"} = current instruction is calling for initialization of classes @{text "C#Cs"} (last class
 is the original) -- still collecting classes to be initialized, @{text "C"} most recently collected›
  ― ‹@{text "Called Cs"} = current instruction called initialization and is waiting for the result
 -- now initializing classes in the list›
  ― ‹@{text "Throwing Cs a"} = frame threw or was thrown an error causing erroneous end of initialization
 procedure for classes @{text "Cs"}›

type_synonym
  frame = "val list × val list × cname × mname × pc × init_call_status"
  ― ‹operand stack›
  ― ‹registers (including this pointer, method parameters, and local variables)›
  ― ‹name of class where current method is defined›
  ― ‹current method›
  ― ‹program counter within frame›
  ― ‹indicates frame's initialization call status›

translations
  (type) "frame" <= (type) "val list × val list × char list × char list × nat × init_call_status"

fun curr_stk :: "frame → val list" where
"curr_stk (stk, loc, C, M, pc, ics) = stk"

fun curr_class :: "frame → cname" where
"curr_class (stk, loc, C, M, pc, ics) = C"

fun curr_method :: "frame → mname" where
"curr_method (stk, loc, C, M, pc, ics) = M"

fun curr_pc :: "frame → nat" where
"curr_pc (stk, loc, C, M, pc, ics) = pc"

fun init_status :: "frame → init_call_status" where
 "init_status (stk, loc, C, M, pc, ics) = ics"

fun ics_of :: "frame → init_call_status" where
 "ics_of fr = snd(snd(snd(snd(snd fr))))"


subsection ‹ Runtime State ›

type_synonym
  jvm_state = "addr option × heap × frame list × sheap"  
  ― ‹exception flag, heap, frames, static heap›

translations
  (type) "jvm_state" <= (type) "nat option × heap × frame list × sheap"

fun frames_of :: "jvm_state → frame list" where
"frames_of (xp, h, frs, sh) = frs"

abbreviation sheap :: "jvm_state → sheap" where
"sheap js ≡ snd (snd (snd js))"

end