Theory JinjaDCI.Exceptions

(*  Title:      JinjaDCI/Common/Exceptions.thy

    Author:     Gerwin Klein, Martin Strecker, Susannah Mansky
    Copyright   2002 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory Common/Exceptions.thy by Gerwin Klein and Martin Strecker
*)

section ‹ Exceptions ›

theory Exceptions imports Objects begin

definition ErrorCl :: "string" where "ErrorCl = ''Error''"
definition ThrowCl :: "string" where "ThrowCl = ''Throwable''"

definition NullPointer :: cname
where
  "NullPointer  ''NullPointer''"

definition ClassCast :: cname
where
  "ClassCast  ''ClassCast''"

definition OutOfMemory :: cname
where
  "OutOfMemory  ''OutOfMemory''"

definition NoClassDefFoundError :: cname
where
  "NoClassDefFoundError  ''NoClassDefFoundError''"

definition IncompatibleClassChangeError :: cname
where
  "IncompatibleClassChangeError  ''IncompatibleClassChangeError''"

definition NoSuchFieldError :: cname
where
  "NoSuchFieldError  ''NoSuchFieldError''"

definition NoSuchMethodError :: cname
where
  "NoSuchMethodError  ''NoSuchMethodError''"

definition sys_xcpts :: "cname set"
where
  "sys_xcpts    {NullPointer, ClassCast, OutOfMemory, NoClassDefFoundError,
                    IncompatibleClassChangeError, 
                    NoSuchFieldError, NoSuchMethodError}"

definition addr_of_sys_xcpt :: "cname  addr"
where
  "addr_of_sys_xcpt s  if s = NullPointer then 0 else
                        if s = ClassCast then 1 else
                        if s = OutOfMemory then 2 else
                        if s = NoClassDefFoundError then 3 else
                        if s = IncompatibleClassChangeError then 4 else
                        if s = NoSuchFieldError then 5 else
                        if s = NoSuchMethodError then 6 else undefined"


lemmas sys_xcpts_defs = NullPointer_def ClassCast_def OutOfMemory_def NoClassDefFoundError_def
                       IncompatibleClassChangeError_def NoSuchFieldError_def NoSuchMethodError_def

lemma Start_nsys_xcpts: "Start  sys_xcpts"
 by(simp add: Start_def sys_xcpts_def sys_xcpts_defs)

lemma Start_nsys_xcpts1 [simp]: "Start  NullPointer" "Start  ClassCast"
 "Start  OutOfMemory" "Start  NoClassDefFoundError"
 "Start  IncompatibleClassChangeError" "Start  NoSuchFieldError"
 "Start  NoSuchMethodError"
using Start_nsys_xcpts by(auto simp: sys_xcpts_def)

lemma Start_nsys_xcpts2 [simp]: "NullPointer  Start" "ClassCast  Start"
 "OutOfMemory  Start" "NoClassDefFoundError  Start"
 "IncompatibleClassChangeError  Start" "NoSuchFieldError  Start"
 "NoSuchMethodError  Start"
using Start_nsys_xcpts by(auto simp: sys_xcpts_def dest: sym)

definition start_heap :: "'c prog  heap"
where
  "start_heap G  Map.empty (addr_of_sys_xcpt NullPointer  blank G NullPointer,
                        addr_of_sys_xcpt ClassCast  blank G ClassCast,
                        addr_of_sys_xcpt OutOfMemory  blank G OutOfMemory,
                        addr_of_sys_xcpt NoClassDefFoundError  blank G NoClassDefFoundError,
                        addr_of_sys_xcpt IncompatibleClassChangeError  blank G IncompatibleClassChangeError,
                        addr_of_sys_xcpt NoSuchFieldError  blank G NoSuchFieldError,
                        addr_of_sys_xcpt NoSuchMethodError  blank G NoSuchMethodError)"

definition preallocated :: "heap  bool"
where
  "preallocated h  C  sys_xcpts. fs. h(addr_of_sys_xcpt C) = Some (C,fs)"

subsection "System exceptions"

lemma sys_xcpts_incl [simp]: "NullPointer  sys_xcpts  OutOfMemory  sys_xcpts
    ClassCast  sys_xcpts  NoClassDefFoundError  sys_xcpts
    IncompatibleClassChangeError  sys_xcpts  NoSuchFieldError  sys_xcpts
    NoSuchMethodError  sys_xcpts"
(*<*)by(simp add: sys_xcpts_def)(*>*)

lemma sys_xcpts_cases [consumes 1, cases set]:
  " C  sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast; P NoClassDefFoundError;
  P IncompatibleClassChangeError; P NoSuchFieldError;
  P NoSuchMethodError   P C"
(*<*)by (auto simp: sys_xcpts_def)(*>*)

subsection "Starting heap"

lemma start_heap_sys_xcpts:
assumes "C  sys_xcpts"
shows "start_heap P (addr_of_sys_xcpt C) = Some(blank P C)"
by(rule sys_xcpts_cases[OF assms])
  (auto simp add: start_heap_def sys_xcpts_def addr_of_sys_xcpt_def sys_xcpts_defs)

lemma start_heap_classes:
 "start_heap P a = Some(C,fs)  C  sys_xcpts"
 by(simp add: start_heap_def blank_def split: if_split_asm)

lemma start_heap_nStart: "start_heap P a = Some obj  fst(obj)  Start"
 by(cases obj, auto dest!: start_heap_classes simp: Start_nsys_xcpts)

subsection "@{term preallocated}"

lemma preallocated_dom [simp]: 
  " preallocated h; C  sys_xcpts   addr_of_sys_xcpt C  dom h"
(*<*)by (fastforce simp:preallocated_def dom_def)(*>*)


lemma preallocatedD:
  " preallocated h; C  sys_xcpts   fs. h(addr_of_sys_xcpt C) = Some (C, fs)"
(*<*)by(auto simp: preallocated_def sys_xcpts_def)(*>*)


lemma preallocatedE [elim?]:
  " preallocated h;  C  sys_xcpts; fs. h(addr_of_sys_xcpt C) = Some(C,fs)  P h C
   P h C"
(*<*)by (fast dest: preallocatedD)(*>*)


lemma cname_of_xcp [simp]:
  " preallocated h; C  sys_xcpts   cname_of h (addr_of_sys_xcpt C) = C"
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_ClassCast [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_OutOfMemory [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt OutOfMemory)) = Some(Class OutOfMemory)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_NullPointer [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt NullPointer)) = Some(Class NullPointer)" 
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_NoClassDefFoundError [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt NoClassDefFoundError)) = Some(Class NoClassDefFoundError)" 
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_IncompatibleClassChangeError [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt IncompatibleClassChangeError)) = Some(Class IncompatibleClassChangeError)" 
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_NoSuchFieldError [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt NoSuchFieldError)) = Some(Class NoSuchFieldError)" 
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_NoSuchMethodError [simp]:
  "preallocated h  typeof⇘h(Addr(addr_of_sys_xcpt NoSuchMethodError)) = Some(Class NoSuchMethodError)" 
(*<*)by (auto elim: preallocatedE)(*>*)

lemma preallocated_hext:
  " preallocated h; h  h'   preallocated h'"
(*<*)by (simp add: preallocated_def hext_def)(*>*)

(*<*)
lemmas preallocated_upd_obj = preallocated_hext [OF _ hext_upd_obj]
lemmas preallocated_new  = preallocated_hext [OF _ hext_new]
(*>*)

lemma preallocated_start:
  "preallocated (start_heap P)"
 by(auto simp: start_heap_sys_xcpts blank_def preallocated_def)

end