Theory JVMDefensive

(*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
    ID:         $Id: JVMDefensive.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Gerwin Klein
    Copyright   GPL
*)

header {* \isaheader{A Defensive JVM} *}

theory JVMDefensive = JVMExec + Conform:

text {*
  Extend the state space by one element indicating a type error (or
  other abnormal termination) *}
datatype 'a type_error = TypeError | Normal 'a

consts is_Addr :: "val => bool"
recdef is_Addr "{}"
  "is_Addr (Addr a) = True"
  "is_Addr v        = False"

consts is_Intg :: "val => bool"
recdef is_Intg "{}"
  "is_Intg (Intg i) = True"
  "is_Intg v        = False"

consts is_Bool :: "val => bool"
recdef is_Bool "{}"
  "is_Bool (Bool b) = True"
  "is_Bool v        = False"

constdefs
  is_Ref :: "val => bool"
  "is_Ref v ≡ v = Null ∨ is_Addr v"

(* FIXME: move *)
constdefs
  has_ :: "'c prog => cname => mname => bool" ("_ \<turnstile> _ has _")
  "P \<turnstile> C has M ≡ ∃Ts T m D. P \<turnstile> C sees M:Ts->T = m in D"

consts
  check_instr :: "[instr, jvm_prog, heap, val list, val list, 
                  cname, mname, pc, frame list] => bool"
primrec 
check_instr_Load:
  "check_instr (Load n) P hp stk loc C M0 pc frs = 
  (n < length loc)"

check_instr_Store:
  "check_instr (Store n) P hp stk loc C0 M0 pc frs = 
  (0 < length stk ∧ n < length loc)"

check_instr_Push:
  "check_instr (Push v) P hp stk loc C0 M0 pc frs = 
  (¬is_Addr v)"

check_instr_New:
  "check_instr (New C) P hp stk loc C0 M0 pc frs = 
  is_class P C"

check_instr_Getfield:
  "check_instr (Getfield F C) P hp stk loc C0 M0 pc frs = 
  (0 < length stk ∧ (∃C' T. P \<turnstile> C sees F:T in C') ∧ 
  (let (C', T) = field P C F; ref = hd stk in 
    C' = C ∧ is_Ref ref ∧ (ref ≠ Null --> 
      hp (the_Addr ref) ≠ None ∧ 
      (let (D,vs) = the (hp (the_Addr ref)) in 
        P \<turnstile> D \<preceq>* C ∧ vs (F,C) ≠ None ∧ P,hp \<turnstile> the (vs (F,C)) :≤ T))))" 

check_instr_Putfield:
  "check_instr (Putfield F C) P hp stk loc C0 M0 pc frs = 
  (1 < length stk ∧ (∃C' T. P \<turnstile> C sees F:T in C') ∧
  (let (C', T) = field P C F; v = hd stk; ref = hd (tl stk) in 
    C' = C ∧ is_Ref ref ∧ (ref ≠ Null --> 
      hp (the_Addr ref) ≠ None ∧ 
      (let D = fst (the (hp (the_Addr ref))) in 
        P \<turnstile> D \<preceq>* C ∧ P,hp \<turnstile> v :≤ T))))" 

check_instr_Checkcast:
  "check_instr (Checkcast C) P hp stk loc C0 M0 pc frs =
  (0 < length stk ∧ is_class P C ∧ is_Ref (hd stk))"

check_instr_Invoke:
  "check_instr (Invoke M n) P hp stk loc C0 M0 pc frs =
  (n < length stk ∧ is_Ref (stk!n) ∧  
  (stk!n ≠ Null --> 
    (let a = the_Addr (stk!n); 
         C = cname_of hp a;
         Ts = fst (snd (method P C M))
    in hp a ≠ None ∧ P \<turnstile> C has M ∧ 
       P,hp \<turnstile> rev (take n stk) [:≤] Ts)))"
 
check_instr_Return:
  "check_instr Return P hp stk loc C0 M0 pc frs =
  (0 < length stk ∧ ((0 < length frs) --> 
    (P \<turnstile> C0 has M0) ∧    
    (let v = hd stk; 
         T = fst (snd (snd (method P C0 M0)))
     in P,hp \<turnstile> v :≤ T)))"
 
check_instr_Pop:
  "check_instr Pop P hp stk loc C0 M0 pc frs = 
  (0 < length stk)"

check_instr_IAdd:
  "check_instr IAdd P hp stk loc C0 M0 pc frs =
  (1 < length stk ∧ is_Intg (hd stk) ∧ is_Intg (hd (tl stk)))"

check_instr_IfFalse:
  "check_instr (IfFalse b) P hp stk loc C0 M0 pc frs =
  (0 < length stk ∧ is_Bool (hd stk) ∧ 0 ≤ int pc+b)"

check_instr_CmpEq:
  "check_instr CmpEq P hp stk loc C0 M0 pc frs =
  (1 < length stk)"

check_instr_Goto:
  "check_instr (Goto b) P hp stk loc C0 M0 pc frs =
  (0 ≤ int pc+b)"

check_instr_Throw:
  "check_instr Throw P hp stk loc C0 M0 pc frs =
  (0 < length stk ∧ is_Ref (hd stk))"

constdefs
  check :: "jvm_prog => jvm_state => bool"
  "check P σ ≡ let (xcpt, hp, frs) = σ in
               (case frs of [] => True | (stk,loc,C,M,pc)#frs' => 
                (let (C',Ts,T,mxs,mxl0,ins,xt) = method P C M; i = ins!pc in
                 pc < size ins ∧ size stk ≤ mxs ∧
                 check_instr i P hp stk loc C M pc frs'))"


  exec_d :: "jvm_prog => jvm_state => jvm_state option type_error"
  "exec_d P σ ≡ if check P σ then Normal (exec (P, σ)) else TypeError"


consts
  "exec_1_d" :: "jvm_prog => (jvm_state type_error × jvm_state type_error) set" 
syntax (xsymbols)
  "@exec_1_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool" 
                   ("_ \<turnstile> _ -jvmd->1 _" [61,61,61]60)  
translations
  "P \<turnstile> σ -jvmd->1 σ'" == "(σ,σ') ∈ exec_1_d P"
inductive "exec_1_d P" intros
  exec_1_d_ErrorI: "exec_d P σ = TypeError ==> P \<turnstile> Normal σ -jvmd->1 TypeError"
  exec_1_d_NormalI: "exec_d P σ = Normal (Some σ') ==> P \<turnstile> Normal σ -jvmd->1 Normal σ'"

-- "reflexive transitive closure:"
consts
  "exec_all_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool" 
                   ("_ |- _ -jvmd-> _" [61,61,61]60)
syntax (xsymbols)
  "exec_all_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool" 
                   ("_ \<turnstile> _ -jvmd-> _" [61,61,61]60)  
defs
  exec_all_d_def1: "P \<turnstile> σ -jvmd-> σ' ≡ (σ,σ') ∈ (exec_1_d P)*"

lemma exec_1_d_def:
  "exec_1_d P = {(s,t). ∃σ. s = Normal σ ∧ t = TypeError ∧ exec_d P σ = TypeError} ∪ 
                {(s,t). ∃σ σ'. s = Normal σ ∧ t = Normal σ' ∧ exec_d P σ = Normal (Some σ')}"
by (auto elim!: exec_1_d.elims intro!: exec_1_d.intros)


declare split_paired_All [simp del]
declare split_paired_Ex [simp del]

lemma if_neq [dest!]:
  "(if P then A else B) ≠ B ==> P"
  by (cases P, auto)

lemma exec_d_no_errorI [intro]:
  "check P σ ==> exec_d P σ ≠ TypeError"
  by (unfold exec_d_def) simp

theorem no_type_error_commutes:
  "exec_d P σ ≠ TypeError ==> exec_d P σ = Normal (exec (P, σ))"
  by (unfold exec_d_def, auto)


lemma defensive_imp_aggressive:
  "P \<turnstile> (Normal σ) -jvmd-> (Normal σ') ==> P \<turnstile> σ -jvm-> σ'"
(*<*)
proof -
  have "!!x y. P \<turnstile> x -jvmd-> y ==> ∀σ σ'. x = Normal σ --> y = Normal σ' -->  P \<turnstile> σ -jvm-> σ'"
    apply (unfold exec_all_d_def1)
    apply (erule rtrancl_induct)
     apply (simp add: exec_all_def)
    apply (fold exec_all_d_def1)
    apply simp
    apply (intro allI impI)
    apply (erule exec_1_d.elims, simp)
    apply (simp add: exec_all_def exec_d_def split: type_error.splits split_if_asm)
    apply (rule rtrancl_trans, assumption)
    apply blast
    done
  moreover
  assume "P \<turnstile> (Normal σ) -jvmd-> (Normal σ')" 
  ultimately
  show "P \<turnstile> σ -jvm-> σ'" by blast
qed
(*>*)

end