Theory JinjaDCI.Effect

(*  Title:      JinjaDCI/BV/Effect.thy
    Author:     Gerwin Klein, Susannah Mansky
    Copyright   2000 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory BV/Effect.thy by Gerwin Klein
*)

section ‹Effect of Instructions on the State Type›

theory Effect
imports JVM_SemiType "../JVM/JVMExceptions"
begin

― ‹FIXME›
locale prog =
  fixes P :: "'a prog"

locale jvm_method = prog +
  fixes mxs :: nat  
  fixes mxl0 :: nat   
  fixes Ts :: "ty list" 
  fixes Tr :: ty
  fixes "is" :: "instr list" 
  fixes xt :: ex_table

  fixes mxl :: nat
  defines mxl_def: "mxl  1+size Ts+mxl0"

text ‹ Program counter of successor instructions: ›
primrec succs :: "instr  tyi  pc  pc list" where
  "succs (Load idx) τ pc     = [pc+1]"
| "succs (Store idx) τ pc    = [pc+1]"
| "succs (Push v) τ pc       = [pc+1]"
| "succs (Getfield F C) τ pc = [pc+1]"
| "succs (Getstatic C F D) τ pc = [pc+1]"
| "succs (Putfield F C) τ pc = [pc+1]"
| "succs (Putstatic C F D) τ pc = [pc+1]"
| "succs (New C) τ pc        = [pc+1]"
| "succs (Checkcast C) τ pc  = [pc+1]"
| "succs Pop τ pc            = [pc+1]"
| "succs IAdd τ pc           = [pc+1]"
| "succs CmpEq τ pc          = [pc+1]"
| succs_IfFalse:
    "succs (IfFalse b) τ pc    = [pc+1, nat (int pc + b)]"
| succs_Goto:
    "succs (Goto b) τ pc       = [nat (int pc + b)]"
| succs_Return:
    "succs Return τ pc         = []"  
| succs_Invoke:
    "succs (Invoke M n) τ pc   = (if (fst τ)!n = NT then [] else [pc+1])"
| succs_Invokestatic:
    "succs (Invokestatic C M n) τ pc   = [pc+1]"
| succs_Throw:
    "succs Throw τ pc          = []"

text "Effect of instruction on the state type:"

fun the_class:: "ty  cname" where
  "the_class (Class C) = C"

fun effi :: "instr × 'm prog × tyi  tyi" where
  effi_Load:
    "effi (Load n,  P, (ST, LT))          = (ok_val (LT ! n) # ST, LT)"
| effi_Store:
    "effi (Store n, P, (T#ST, LT))        = (ST, LT[n:= OK T])"
| effi_Push:
    "effi (Push v, P, (ST, LT))             = (the (typeof v) # ST, LT)"
| effi_Getfield:
    "effi (Getfield F C, P, (T#ST, LT))    = (snd (snd (field P C F)) # ST, LT)"
| effi_Getstatic:
    "effi (Getstatic C F D, P, (ST, LT))    = (snd (snd (field P C F)) # ST, LT)"
| effi_Putfield:
   "effi (Putfield F C, P, (T1#T2#ST, LT)) = (ST,LT)"
| effi_Putstatic:
   "effi (Putstatic C F D, P, (T#ST, LT)) = (ST,LT)"
| effi_New:
   "effi (New C, P, (ST,LT))               = (Class C # ST, LT)"
| effi_Checkcast:
   "effi (Checkcast C, P, (T#ST,LT))       = (Class C # ST,LT)"
| effi_Pop:
   "effi (Pop, P, (T#ST,LT))               = (ST,LT)"
| effi_IAdd:
   "effi (IAdd, P,(T1#T2#ST,LT))           = (Integer#ST,LT)"
| effi_CmpEq:
   "effi (CmpEq, P, (T1#T2#ST,LT))         = (Boolean#ST,LT)"
| effi_IfFalse:
   "effi (IfFalse b, P, (T1#ST,LT))        = (ST,LT)"
| effi_Invoke:
   "effi (Invoke M n, P, (ST,LT))          =
    (let C = the_class (ST!n); (D,b,Ts,Tr,m) = method P C M
     in (Tr # drop (n+1) ST, LT))"
| effi_Invokestatic:
   "effi (Invokestatic C M n, P, (ST,LT))  =
    (let (D,b,Ts,Tr,m) = method P C M
     in (Tr # drop n ST, LT))"
| effi_Goto:
   "effi (Goto n, P, s)                    = s"

fun is_relevant_class :: "instr  'm prog  cname  bool" where
  rel_Getfield:
    "is_relevant_class (Getfield F D)
     = (λP C. P  NullPointer * C  P  NoSuchFieldError * C
             P  IncompatibleClassChangeError * C)" 
| rel_Getstatic:
    "is_relevant_class (Getstatic C F D)
     = (λP C. True)"
| rel_Putfield:
    "is_relevant_class (Putfield F D)
     = (λP C. P  NullPointer * C  P  NoSuchFieldError * C
             P  IncompatibleClassChangeError * C)" 
| rel_Putstatic:
    "is_relevant_class (Putstatic C F D)
     = (λP C. True)" 
| rel_Checkcast:
    "is_relevant_class (Checkcast D)  = (λP C. P  ClassCast * C)" 
| rel_New:
    "is_relevant_class (New D)        = (λP C. True)"
| rel_Throw:
    "is_relevant_class Throw          = (λP C. True)"
| rel_Invoke:
    "is_relevant_class (Invoke M n)   = (λP C. True)"
| rel_Invokestatic:
    "is_relevant_class (Invokestatic C M n)   = (λP C. True)"
| rel_default:
    "is_relevant_class i              = (λP C. False)"

definition is_relevant_entry :: "'m prog  instr  pc  ex_entry  bool" where
  "is_relevant_entry P i pc e  (let (f,t,C,h,d) = e in is_relevant_class i P C  pc  {f..<t})"

definition relevant_entries :: "'m prog  instr  pc  ex_table  ex_table" where
  "relevant_entries P i pc = filter (is_relevant_entry P i pc)"

definition xcpt_eff :: "instr  'm prog  pc  tyi 
                ex_table  (pc × tyi') list" where    
  "xcpt_eff i P pc τ et = (let (ST,LT) = τ in 
  map (λ(f,t,C,h,d). (h, Some (Class C#drop (size ST - d) ST, LT))) (relevant_entries P i pc et))"

definition norm_eff :: "instr  'm prog  nat  tyi  (pc × tyi') list" where
  "norm_eff i P pc τ = map (λpc'. (pc',Some (effi (i,P,τ)))) (succs i τ pc)"

definition eff :: "instr  'm prog  pc  ex_table  tyi'  (pc × tyi') list" where
  "eff i P pc et t = (case t of           
    None  []          
  | Some τ  (norm_eff i P pc τ) @ (xcpt_eff i P pc τ et))"


lemma eff_None:
  "eff i P pc xt None = []"
by (simp add: eff_def)

lemma eff_Some:
  "eff i P pc xt (Some τ) = norm_eff i P pc τ @ xcpt_eff i P pc τ xt"
by (simp add: eff_def)

(* FIXME: getfield, ∃T D. P ⊢ C sees F:T in D ∧ .. *)

text "Conditions under which eff is applicable:"

fun appi :: "instr × 'm prog × pc × nat × ty × tyi  bool" where
  appi_Load:
    "appi (Load n, P, pc, mxs, Tr, (ST,LT)) = 
    (n < length LT  LT ! n  Err  length ST < mxs)"
| appi_Store:
    "appi (Store n, P, pc, mxs, Tr, (T#ST, LT)) = 
    (n < length LT)"
| appi_Push:
    "appi (Push v, P, pc, mxs, Tr, (ST,LT)) = 
     (length ST < mxs  typeof v  None)"
| appi_Getfield:
    "appi (Getfield F C, P, pc, mxs, Tr, (T#ST, LT)) = 
    (Tf. P  C sees F,NonStatic:Tf in C  P  T  Class C)"
| appi_Getstatic:
    "appi (Getstatic C F D, P, pc, mxs, Tr, (ST, LT)) = 
     (length ST < mxs  (Tf. P  C sees F,Static:Tf in D))"
| appi_Putfield:
    "appi (Putfield F C, P, pc, mxs, Tr, (T1#T2#ST, LT)) = 
    (Tf. P  C sees F,NonStatic:Tf in C  P  T2  (Class C)  P  T1  Tf)" 
| appi_Putstatic:
    "appi (Putstatic C F D, P, pc, mxs, Tr, (T#ST, LT)) = 
    (Tf. P  C sees F,Static:Tf in D  P  T  Tf)" 
| appi_New:
    "appi (New C, P, pc, mxs, Tr, (ST,LT)) = 
    (is_class P C  length ST < mxs)"
| appi_Checkcast:
    "appi (Checkcast C, P, pc, mxs, Tr, (T#ST,LT)) = 
    (is_class P C  is_refT T)"
| appi_Pop:
    "appi (Pop, P, pc, mxs, Tr, (T#ST,LT)) = 
    True"
| appi_IAdd:
    "appi (IAdd, P, pc, mxs, Tr, (T1#T2#ST,LT)) = (T1 = T2  T1 = Integer)"
| appi_CmpEq:
    "appi (CmpEq, P, pc, mxs, Tr, (T1#T2#ST,LT)) =
    (T1 = T2  is_refT T1  is_refT T2)"
| appi_IfFalse:
    "appi (IfFalse b, P, pc, mxs, Tr, (Boolean#ST,LT)) = 
    (0  int pc + b)"
| appi_Goto:
    "appi (Goto b, P, pc, mxs, Tr, s) = 
    (0  int pc + b)"
| appi_Return:
    "appi (Return, P, pc, mxs, Tr, (T#ST,LT)) = 
    (P  T  Tr)"
| appi_Throw:
    "appi (Throw, P, pc, mxs, Tr, (T#ST,LT)) = 
    is_refT T"
| appi_Invoke:
    "appi (Invoke M n, P, pc, mxs, Tr, (ST,LT)) =
    (n < length ST  
    (ST!n  NT 
      (C D Ts T m. ST!n = Class C  P  C sees M,NonStatic:Ts  T = m in D 
                    P  rev (take n ST) [≤] Ts)))"
| appi_Invokestatic:
    "appi (Invokestatic C M n, P, pc, mxs, Tr, (ST,LT)) =
    (length ST - n < mxs  n  length ST  M  clinit 
      (D Ts T m. P  C sees M,Static:Ts  T = m in D 
                    P  rev (take n ST) [≤] Ts))"
    
| appi_default:
    "appi (i,P, pc,mxs,Tr,s) = False"


definition xcpt_app :: "instr  'm prog  pc  nat  ex_table  tyi  bool" where
  "xcpt_app i P pc mxs xt τ  ((f,t,C,h,d)  set (relevant_entries P i pc xt). is_class P C  d  size (fst τ)  d < mxs)"

definition app :: "instr  'm prog  nat  ty  nat  nat  ex_table  tyi'  bool" where
  "app i P mxs Tr pc mpc xt t = (case t of None  True | Some τ  
  appi (i,P,pc,mxs,Tr,τ)  xcpt_app i P pc mxs xt τ  
  ((pc',τ')  set (eff i P pc xt t). pc' < mpc))"


lemma app_Some:
  "app i P mxs Tr pc mpc xt (Some τ) = 
  (appi (i,P,pc,mxs,Tr,τ)  xcpt_app i P pc mxs xt τ  
  ((pc',s')  set (eff i P pc xt (Some τ)). pc' < mpc))"
by (simp add: app_def)

locale eff = jvm_method +
  fixes effi and appi and eff and app 
  fixes norm_eff and xcpt_app and xcpt_eff

  fixes mpc
  defines "mpc  size is"

  defines "effi i τ  Effect.effi (i,P,τ)"
  notes effi_simps [simp] = Effect.effi.simps [where P = P, folded effi_def]

  defines "appi i pc τ  Effect.appi (i, P, pc, mxs, Tr, τ)"
  notes appi_simps [simp] = Effect.appi.simps [where P=P and mxs=mxs and Tr=Tr, folded appi_def]

  defines "xcpt_eff i pc τ  Effect.xcpt_eff i P pc τ xt"
  notes xcpt_eff = Effect.xcpt_eff_def [of _ P _ _ xt, folded xcpt_eff_def]

  defines "norm_eff i pc τ  Effect.norm_eff i P pc τ"
  notes norm_eff = Effect.norm_eff_def [of _ P, folded norm_eff_def effi_def]

  defines "eff i pc  Effect.eff i P pc xt"
  notes eff = Effect.eff_def [of _ P  _ xt, folded eff_def norm_eff_def xcpt_eff_def]

  defines "xcpt_app i pc τ  Effect.xcpt_app i P pc mxs xt τ"
  notes xcpt_app = Effect.xcpt_app_def [of _ P _ mxs xt, folded xcpt_app_def]

  defines "app i pc  Effect.app i P mxs Tr pc mpc xt"
  notes app = Effect.app_def [of _ P mxs Tr _ mpc xt, folded app_def xcpt_app_def appi_def eff_def]


lemma length_cases2:
  assumes "LT. P ([],LT)"
  assumes "l ST LT. P (l#ST,LT)"
  shows "P s"
  by (cases s, cases "fst s") (auto intro!: assms)


lemma length_cases3:
  assumes "LT. P ([],LT)"
  assumes "l LT. P ([l],LT)"
  assumes "l ST LT. P (l#ST,LT)"
  shows "P s"
(*<*)
proof -
  obtain xs LT where s: "s = (xs,LT)" by (cases s)
  show ?thesis
  proof (cases xs)
    case Nil with assms s show ?thesis by simp
  next
    fix l xs' assume "xs = l#xs'"
    with assms s show ?thesis by simp
  qed
qed
(*>*)

lemma length_cases4:
  assumes "LT. P ([],LT)"
  assumes "l LT. P ([l],LT)"
  assumes "l l' LT. P ([l,l'],LT)"
  assumes "l l' ST LT. P (l#l'#ST,LT)"
  shows "P s"
(*<*)
proof -
  obtain xs LT where s: "s = (xs,LT)" by (cases s)
  show ?thesis
  proof (cases xs)
    case Nil with assms s show ?thesis by simp
  next
    fix l xs' assume xs: "xs = l#xs'"
    thus ?thesis
    proof (cases xs')
      case Nil with assms s xs show ?thesis by simp
    next
      fix l' ST assume "xs' = l'#ST"
     with assms s xs show ?thesis by simp
    qed
  qed
qed
(*>*)

text ‹ 
\medskip
simp rules for @{term app}
lemma appNone[simp]: "app i P mxs Tr pc mpc et None = True" 
  by (simp add: app_def)


lemma appLoad[simp]:
"appi (Load idx, P, Tr, mxs, pc, s) = (ST LT. s = (ST,LT)  idx < length LT  LT!idx  Err  length ST < mxs)"
  by (cases s, simp)

lemma appStore[simp]:
"appi (Store idx,P,pc,mxs,Tr,s) = (ts ST LT. s = (ts#ST,LT)  idx < length LT)"
  by (rule length_cases2, auto)

lemma appPush[simp]:
"appi (Push v,P,pc,mxs,Tr,s) =
 (ST LT. s = (ST,LT)  length ST < mxs  typeof v  None)"
  by (cases s, simp)

lemma appGetField[simp]:
"appi (Getfield F C,P,pc,mxs,Tr,s) = 
 ( oT vT ST LT. s = (oT#ST, LT)  
  P  C sees F,NonStatic:vT in C  P  oT  (Class C))"
  by (rule length_cases2 [of _ s]) auto

lemma appGetStatic[simp]:
"appi (Getstatic C F D,P,pc,mxs,Tr,s) = 
 ( vT ST LT. s = (ST, LT)  length ST < mxs  P  C sees F,Static:vT in D)"
  by (rule length_cases2 [of _ s]) auto

lemma appPutField[simp]:
"appi (Putfield F C,P,pc,mxs,Tr,s) = 
 ( vT vT' oT ST LT. s = (vT#oT#ST, LT) 
  P  C sees F,NonStatic:vT' in C  P  oT  (Class C)  P  vT  vT')"
  by (rule length_cases4 [of _ s], auto)

lemma appPutstatic[simp]:
"appi (Putstatic C F D,P,pc,mxs,Tr,s) = 
 ( vT vT' ST LT. s = (vT#ST, LT) 
  P  C sees F,Static:vT' in D  P  vT  vT')"
  by (rule length_cases4 [of _ s], auto)

lemma appNew[simp]:
  "appi (New C,P,pc,mxs,Tr,s) = 
  (ST LT. s=(ST,LT)  is_class P C  length ST < mxs)"
  by (cases s, simp)

lemma appCheckcast[simp]: 
  "appi (Checkcast C,P,pc,mxs,Tr,s) =  
  (T ST LT. s = (T#ST,LT)  is_class P C  is_refT T)"
  by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)

lemma appiPop[simp]: 
"appi (Pop,P,pc,mxs,Tr,s) = (ts ST LT. s = (ts#ST,LT))"
  by (rule length_cases2, auto)

lemma appIAdd[simp]:
"appi (IAdd,P,pc,mxs,Tr,s) = (ST LT. s = (Integer#Integer#ST,LT))"
(*<*)
proof -
  obtain ST LT where [simp]: "s = (ST,LT)" by (cases s)
  have "ST = []  (T. ST = [T])  (T1 T2 ST'. ST = T1#T2#ST')"
    by (cases ST, auto, case_tac list, auto)
  moreover
  { assume "ST = []" hence ?thesis by simp }
  moreover
  { fix T assume "ST = [T]" hence ?thesis by (cases T, auto) }
  moreover
  { fix T1 T2 ST' assume "ST = T1#T2#ST'"
    hence ?thesis by (cases T1, auto)
  }
  ultimately show ?thesis by blast
qed
(*>*)


lemma appIfFalse [simp]:
"appi (IfFalse b,P,pc,mxs,Tr,s) = 
  (ST LT. s = (Boolean#ST,LT)  0  int pc + b)"
(*<*)
 (is "?P s")
proof(rule length_cases2)
  fix LT show "?P ([],LT)" by simp
next
  fix l ST LT show "?P (l#ST,LT)"
    by (case_tac l) auto
qed
(*>*)

lemma appCmpEq[simp]:
"appi (CmpEq,P,pc,mxs,Tr,s) = 
  (T1 T2 ST LT. s = (T1#T2#ST,LT)  (¬is_refT T1  T2 = T1  is_refT T1  is_refT T2))"
  by (rule length_cases4, auto)

lemma appReturn[simp]:
"appi (Return,P,pc,mxs,Tr,s) = (T ST LT. s = (T#ST,LT)  P  T  Tr)" 
  by (rule length_cases2, auto)

lemma appThrow[simp]:
  "appi (Throw,P,pc,mxs,Tr,s) = (T ST LT. s=(T#ST,LT)  is_refT T)"
  by (rule length_cases2, auto)  

lemma effNone: 
  "(pc', s')  set (eff i P pc et None)  s' = None"
  by (auto simp add: eff_def xcpt_eff_def norm_eff_def)


text ‹ some helpers to make the specification directly executable: ›
lemma relevant_entries_append [simp]:
  "relevant_entries P i pc (xt @ xt') = relevant_entries P i pc xt @ relevant_entries P i pc xt'"
  by (unfold relevant_entries_def) simp

lemma xcpt_app_append [iff]:
  "xcpt_app i P pc mxs (xt@xt') τ = (xcpt_app i P pc mxs xt τ  xcpt_app i P pc mxs xt' τ)"
  by (unfold xcpt_app_def) fastforce

lemma xcpt_eff_append [simp]:
  "xcpt_eff i P pc τ (xt@xt') = xcpt_eff i P pc τ xt @ xcpt_eff i P pc τ xt'"
 by (unfold xcpt_eff_def, cases τ) simp

lemma app_append [simp]:
  "app i P pc T mxs mpc (xt@xt') τ = (app i P pc T mxs mpc xt τ  app i P pc T mxs mpc xt' τ)"
  by (unfold app_def eff_def) auto

end