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

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

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

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

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

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

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

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

| check_instr_Throw:
    "check_instr Throw P h stk loc C0 M0 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,mxl0,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