Theory JVMDefensive

(*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
    Author:     Gerwin Klein
    Copyright   GPL
*)

section ‹A Defensive JVM›

theory JVMDefensive
imports JVMExec "../Common/Conform"
begin

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

fun is_Addr :: "val ⇒ bool" where
  "is_Addr (Addr a) ⟷ True"
| "is_Addr v ⟷ False"

fun is_Intg :: "val ⇒ bool" where
  "is_Intg (Intg i) ⟷ True"
| "is_Intg v ⟷ False"

fun is_Bool :: "val ⇒ bool" where
  "is_Bool (Bool b) ⟷ True"
| "is_Bool v ⟷ False"

definition is_Ref :: "val ⇒ bool" where
  "is_Ref v ⟷ v = Null ∨ is_Addr v"

primrec check_instr :: "[instr, jvm_prog, heap, val list, val list, 
                  cname, mname, pc, frame list] ⇒ bool" where
  check_instr_Load:
    "check_instr (Load n) P h stk loc C M⇩0 pc frs = 
    (n < length loc)"

| check_instr_Store:
    "check_instr (Store n) P h stk loc C⇩0 M⇩0 pc frs = 
    (0 < length stk ∧ n < length loc)"

| check_instr_Push:
    "check_instr (Push v) P h stk loc C⇩0 M⇩0 pc frs = 
    (¬is_Addr v)"

| check_instr_New:
    "check_instr (New C) P h stk loc C⇩0 M⇩0 pc frs = 
    is_class P C"

| check_instr_Getfield:
    "check_instr (Getfield F C) P h stk loc C⇩0 M⇩0 pc frs = 
    (0 < length stk ∧ (∃C' T. P ⊢ C sees F:T in C') ∧ 
    (let (C', T) = field P C F; ref = hd stk in 
      C' = C ∧ is_Ref ref ∧ (ref ≠ Null ⟶ 
        h (the_Addr ref) ≠ None ∧ 
        (let (D,vs) = the (h (the_Addr ref)) in 
          P ⊢ D ≼⇧* C ∧ vs (F,C) ≠ None ∧ P,h ⊢ the (vs (F,C)) :≤ T))))" 

| check_instr_Putfield:
    "check_instr (Putfield F C) P h stk loc C⇩0 M⇩0 pc frs = 
    (1 < length stk ∧ (∃C' T. P ⊢ 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 ⟶ 
        h (the_Addr ref) ≠ None ∧ 
        (let D = fst (the (h (the_Addr ref))) in 
          P ⊢ D ≼⇧* C ∧ P,h ⊢ v :≤ T))))" 

| check_instr_Checkcast:
    "check_instr (Checkcast C) P h stk loc C⇩0 M⇩0 pc frs =
    (0 < length stk ∧ is_class P C ∧ is_Ref (hd stk))"

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

| check_instr_IAdd:
    "check_instr IAdd P h stk loc C⇩0 M⇩0 pc frs =
    (1 < length stk ∧ is_Intg (hd stk) ∧ is_Intg (hd (tl stk)))"

| check_instr_IfFalse:
    "check_instr (IfFalse b) P h stk loc C⇩0 M⇩0 pc frs =
    (0 < length stk ∧ is_Bool (hd stk) ∧ 0 ≤ int pc+b)"

| check_instr_CmpEq:
    "check_instr CmpEq P h stk loc C⇩0 M⇩0 pc frs =
    (1 < length stk)"

| check_instr_Goto:
    "check_instr (Goto b) P h stk loc C⇩0 M⇩0 pc frs =
    (0 ≤ int pc+b)"

| check_instr_Throw:
    "check_instr Throw P h stk loc C⇩0 M⇩0 pc frs =
    (0 < length stk ∧ is_Ref (hd stk))"

definition check :: "jvm_prog ⇒ jvm_state ⇒ bool" where
  "check P σ = (let (xcpt, h, frs) = σ in
               (case frs of [] ⇒ True | (stk,loc,C,M,pc)#frs' ⇒ 
                P ⊢ C has M ∧
                (let (C',Ts,T,mxs,mxl⇩0,ins,xt) = method P C M; i = ins!pc in
                 pc < size ins ∧ size stk ≤ mxs ∧
                 check_instr i P h stk loc C M pc frs')))"


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


inductive_set
  exec_1_d :: "jvm_prog ⇒ (jvm_state type_error × jvm_state type_error) set" 
  and exec_1_d' :: "jvm_prog ⇒ jvm_state type_error ⇒ jvm_state type_error ⇒ bool" 
                   (‹_ ⊢ _ -jvmd→⇩1 _› [61,61,61]60)
  for P :: jvm_prog
where
  "P ⊢ σ -jvmd→⇩1 σ' ≡ (σ,σ') ∈ exec_1_d P"
| exec_1_d_ErrorI: "exec_d P σ = TypeError ⟹ P ⊢ Normal σ -jvmd→⇩1 TypeError"
| exec_1_d_NormalI: "exec_d P σ = Normal (Some σ') ⟹ P ⊢ Normal σ -jvmd→⇩1 Normal σ'"

― ‹reflexive transitive closure:›
definition exec_all_d :: "jvm_prog ⇒ jvm_state type_error ⇒ jvm_state type_error ⇒ bool" 
    (‹_ ⊢ _ -jvmd→ _› [61,61,61]60) where
  exec_all_d_def1: "P ⊢ σ -jvmd→ σ' ⟷ (σ,σ') ∈ (exec_1_d P)⇧*"

notation (ASCII)
  "exec_all_d"  (‹_ |- _ -jvmd-> _› [61,61,61]60)

lemma exec_1_d_eq:
  "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.cases 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 ⊢ (Normal σ) -jvmd→ (Normal σ') ⟹ P ⊢ σ -jvm→ σ'"
(*<*)
proof -
  have "⋀x y. P ⊢ x -jvmd→ y ⟹ ∀σ σ'. x = Normal σ ⟶ y = Normal σ' ⟶  P ⊢ σ -jvm→ σ'"
  proof -
    fix x y assume xy: "P ⊢ x -jvmd→ y"
    then have "(x, y) ∈ (exec_1_d P)⇧*" by (unfold exec_all_d_def1)
    then show "∀σ σ'. x = Normal σ ⟶ y = Normal σ' ⟶  P ⊢ σ -jvm→ σ'"
    proof(induct rule: rtrancl_induct)
      case base
      then show ?case by (simp add: exec_all_def)
    next
      case (step y' z')
      show ?case proof(induct rule: exec_1_d.cases[OF step.hyps(2)])
        case (2 σ σ')
        then have "(σ, σ') ∈ {(σ, σ'). exec (P, σ) = ⌊σ'⌋}⇧*" using step
          by(fastforce simp: exec_d_def split: type_error.splits if_split_asm)
        then show ?case using step 2 by (auto simp: exec_all_def)
      qed simp
    qed
  qed
  moreover
  assume "P ⊢ (Normal σ) -jvmd→ (Normal σ')" 
  ultimately
  show "P ⊢ σ -jvm→ σ'" by blast
qed
(*>*)

end