Quelle  JVMDefensive.thy

(*  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₀ pc frs =
    (n < length loc)"

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

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

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

| check_instr_Getfield:
    "check_instr (Getfield F C) P h stk loc C₀ M₀ 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₀ M₀ 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₀ M₀ 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₀ M₀ 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₀ M₀ pc frs =
    (0 < length stk ∧ ((0 < length frs) ⟶
      (P ⊨ C₀ has M₀) ∧
      (let v = hd stk;
           T = fst (snd (snd (method P C₀ M₀)))
       in P,h ⊨ v :≤ T)))"
 
| check_instr_Pop:
    "check_instr Pop P h stk loc C₀ M₀ pc frs =
    (0 < length stk)"

| check_instr_IAdd:
    "check_instr IAdd P h stk loc C₀ M₀ 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₀ M₀ pc frs =
    (0 < length stk ∧ is_Bool (hd stk) ∧ 0 ≤ int pc+b)"

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

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

| check_instr_Throw:
    "check_instr Throw P h stk loc C₀ M₀ 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₀,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→₁ _› [61,61,61]60)
  for P :: jvm_prog
where
  "P ⊨ σ -jvmd→₁ σ' ≡ (σ,σ') ∈ exec_1_d P"
| exec_1_d_ErrorI: "exec_d P σ = TypeError ==> P ⊨ Normal σ -jvmd→₁ TypeError"
| exec_1_d_NormalI: "exec_d P σ = Normal (Some σ') ==> P ⊨ Normal σ -jvmd→₁ 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