header {* 
  \isaheader{Jinja VCG} 
*}

theory JBC_VCG = JBC_SafetyLogic + VCG_Upgrades:


section {* Control Flow Graph *}


consts xcpt_cond::"jbc_prog \<Rightarrow> cname \<Rightarrow> pos \<Rightarrow> expr"
defs xcpt_cond_def:
"xcpt_cond \<Pi> X p \<equiv> (case (cmd \<Pi> p) of None \<Rightarrow> TT | Some c \<Rightarrow> (case c
of New C \<Rightarrow> Eq (NewA 0) (Cn Null)
| Getfield F C \<Rightarrow> Eq (St 0) (Cn Null)
| Putfield F C \<Rightarrow> Eq (St 1) (Cn Null)
| Checkcast C \<Rightarrow> And ((Neg (Eq (St 0) (Cn Null)))#(map (\<lambda> Cl. Neg (Ty (St 0) (Class Cl))) [Cl \<in> (classnames (fst \<Pi>)). (fst \<Pi>) \<turnstile> Cl  \<preceq>\<^sup>* C]))
| Invoke M n \<Rightarrow> Eq (St n) (Cn Null)
| Throw \<Rightarrow> (if X = NullPointer then Neg (And [Neg (Eq (St 0) (Cn Null)), Neg (Ty (St 0) (Class X))]) else Ty (St 0) (Class X))
| _ \<Rightarrow> TT ))"


consts
succsInvoke::"(jbc_prog \<times> mname \<times> nat \<times> pos) \<Rightarrow> (pos \<times> expr) list"
recdef succsInvoke "{}"
"succsInvoke (\<Pi>,M,n,p) = (case anF \<Pi> p of None \<Rightarrow> [] 
 | Some A \<Rightarrow> concat (map (\<lambda> tp.  (case tp of Void \<Rightarrow> [] 
                            | Boolean \<Rightarrow> [] 
                            | Integer \<Rightarrow> [] 
                            | NT \<Rightarrow> [] 
                            | Class X \<Rightarrow> [((fst (method (fst \<Pi>) X M),M,0),And [Neg (xcpt_cond \<Pi> NullPointer p), Ty (St n) (Class X)])])) (extractTy (A,St n))))" 


constdefs
succsNormal::"jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list"
"succsNormal \<Pi> p \<equiv> (case cmd \<Pi> p of None \<Rightarrow> []
| Some c \<Rightarrow> (case c 
of Load n \<Rightarrow> [(incA p,TT)]
| Store n \<Rightarrow> [(incA p,TT)]
| Push v \<Rightarrow> [(incA p,TT)]
| New C \<Rightarrow> [(incA p,Neg (xcpt_cond \<Pi> OutOfMemory p))]
| Getfield F C \<Rightarrow> [(incA p,Neg (xcpt_cond \<Pi> NullPointer p))]
| Putfield F C \<Rightarrow> [(incA p,Neg (xcpt_cond \<Pi> NullPointer p))]
| Checkcast C \<Rightarrow> [(incA p,Neg (xcpt_cond \<Pi> ClassCast p))]
| Invoke M n \<Rightarrow> succsInvoke (\<Pi>,M,n,p) 
| Return \<Rightarrow> map (\<lambda> p'. (incA p',Call (And [aF \<Pi> p',Pos p']))) (callers \<Pi> p)
| Pop \<Rightarrow> [(incA p,TT)]
| IBin no \<Rightarrow> [(incA p,TT)]
| Goto t \<Rightarrow> let (C,M,n)=p in [((C,M,nat ((int n)+t)),TT)]
| CmpEq \<Rightarrow> [(incA p,TT)]
| IfIntCmp ro t \<Rightarrow> let (C,M,n)=p 
               in [((C,M,nat ((int n)+t)),Rel (St 1) ro (St 0)),
                   (incA p, Neg (Rel (St 1) ro (St 0)))]
| IfFalse t \<Rightarrow> let (C,M,n)=p 
               in [((C,M,nat ((int n)+t)),Eq (St 0) (Cn (Bool False))),
                   (incA p, Neg (Eq (St 0) (Cn (Bool False))))]
| Throw \<Rightarrow> []
))"

consts
  match_ex_table_e :: "'m prog \<Rightarrow> cname \<Rightarrow> pc \<Rightarrow> ex_table \<Rightarrow> ex_entry option"
primrec
  "match_ex_table_e P C pc []     = None"
  "match_ex_table_e P C pc (e#es) = (if matches_ex_entry P C pc e
                                    then Some e
                                    else match_ex_table_e P C pc es)"

lemma match_ex_table_e_sim:
"(match_ex_table_e P C pc et = Some e) \<Longrightarrow> (match_ex_table P C pc et = Some (snd (snd (snd e))))"
proof (induct et)
assume A: "(match_ex_table_e P C pc [] = Some e)"
from A
show   "(match_ex_table P C pc [] = Some (snd (snd (snd e))))"
  by simp
next  
fix a et
assume hyp: "(match_ex_table_e P C pc et = Some e) \<Longrightarrow> (match_ex_table P C pc et = Some (snd (snd (snd e))))"
assume A: "match_ex_table_e P C pc (a # et) = Some e"
show "match_ex_table P C pc (a#et) = Some (snd (snd (snd e)))"
proof (cases "matches_ex_entry P C pc a")
  case True
  from True A show ?thesis
    by simp
next
  case False
  from False A hyp show ?thesis
    by simp
qed
qed

lemma match_ex_table_e_sim2:
"match_ex_table P C pc et = Some pc_h \<Longrightarrow> (\<exists> e.(match_ex_table_e P C pc et = Some e) \<and> snd (snd (snd e)) = pc_h) "
proof (induct et)
assume A: "(match_ex_table P C pc [] = Some pc_h)"
from A
show   "\<exists> e. match_ex_table_e P C pc [] = Some e \<and> snd (snd (snd e)) = pc_h "
  by simp
next  
fix a et
assume hyp: "(match_ex_table P C pc et = Some pc_h) \<Longrightarrow> (\<exists> e. match_ex_table_e P C pc et = Some e \<and> snd (snd (snd e)) = pc_h)"
assume A: "match_ex_table P C pc (a # et) = Some pc_h"
show "(\<exists> e. match_ex_table_e P C pc (a#et) = Some e \<and> snd (snd (snd e)) = pc_h)"
proof (cases "matches_ex_entry P C pc a")
  case True
  from True A show ?thesis
    by simp
next
  case False
  from False A hyp show ?thesis
    by simp
qed
qed

consts match_ex_table::"'m prog \<Rightarrow> cname \<Rightarrow> pc \<Rightarrow> ex_table \<Rightarrow> pc option"
defs match_ex_table_def [simp]:
"match_ex_table P C pc et == (case (JVMExceptions.match_ex_table P C pc et) of None \<Rightarrow> None | Some h \<Rightarrow> Some (fst h))"

                 
consts
succsXpt::"(jbc_prog \<times> cname \<times> pos list) \<Rightarrow> (pos \<times> expr) list" 
recdef succsXpt "measure (\<lambda>(\<Pi>,X,ps). length (domC \<Pi>) - (length ps))"
"succsXpt ((P,An),X,ps) = (case length (domC (P,An)) \<le> length ps 
of True \<Rightarrow> map (\<lambda>p. (p,TT)) (domC (P,An))
| False \<Rightarrow> (case ps of [] \<Rightarrow> map (\<lambda>p. (p,TT)) (domC (P,An))
            | p#pss \<Rightarrow> let (C,M,pc)=p; et = ex_table_of P C M; A=aF (P,An) p
                       in (case match_ex_table_e P X pc et 
                           of None \<Rightarrow> concat (map (\<lambda>p'. succsXpt ((P,An),X,p'#ps)) (callers (P,An) p))
                           | Some e \<Rightarrow> (let (f,t,X',pc',d) = e 
                                        in [((C,M,pc'),And ((if pss=[] then [] else [Catch X' A,Catch X (Pos p)])@ 
                                                            [xcpt_cond (P,An) X (last ps)]))]))))"


constdefs
succsExcept::"jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list"
"succsExcept \<Pi> p \<equiv> (case cmd \<Pi> p of None \<Rightarrow> []
| Some c \<Rightarrow> (case c 
of Load n \<Rightarrow> []
| Store n \<Rightarrow> []
| Push v \<Rightarrow> []
| New C \<Rightarrow> succsXpt (\<Pi>,OutOfMemory,[p])
| Getfield F C \<Rightarrow> succsXpt (\<Pi>,NullPointer,[p])
| Putfield F C \<Rightarrow> succsXpt (\<Pi>,NullPointer,[p])
| Checkcast C \<Rightarrow> succsXpt (\<Pi>,ClassCast,[p])
| Invoke M n \<Rightarrow> succsXpt (\<Pi>,NullPointer,[p])
| Return \<Rightarrow> []
| Pop \<Rightarrow> []
| IBin no \<Rightarrow> []
| Goto t \<Rightarrow> []
| CmpEq \<Rightarrow> []
| IfIntCmp ro t \<Rightarrow> []
| IfFalse t \<Rightarrow> []
| Throw \<Rightarrow> succsXpt (\<Pi>,NullPointer,[p]) @ (case anF \<Pi> p of None \<Rightarrow> [] 
            | Some a \<Rightarrow> concat (map (\<lambda> tp. (case tp of Void \<Rightarrow> [] | Boolean \<Rightarrow> [] | Integer \<Rightarrow> [] | NT \<Rightarrow> [] 
         | Class X \<Rightarrow> succsXpt (\<Pi>,X,[p]))) (extractTy (a,St 0)))) 
))"


constdefs addPos::"pos \<Rightarrow> ((pos \<times> expr) list) \<Rightarrow> (pos \<times> expr) list"
"addPos p es \<equiv> (map (\<lambda> (p',B). (p',And [Pos p,B])) es)"


constdefs succsF::"jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list"
"succsF \<Pi> p \<equiv> addPos p (succsNormal \<Pi> p @ succsExcept \<Pi> p)"


section {* Static Semantics *}


constdefs
handlesEx'::"jvm_prog \<Rightarrow> pos \<Rightarrow> cname list"
"handlesEx' P p \<equiv> remdups' (concat (map (\<lambda>(C,(S,Fs,Ms)). 
                             concat (map (\<lambda>(M,Ts,T,(mxs,mxl,is,et)). 
                                            concat (map (\<lambda>(b,e,cn,h,d). 
                                                           if p=(C,M,h) 
                                                           then [cn] else []) 
                                                         et)) 
                                          Ms)) 
                            P))"

constdefs 
handlesEx::"jvm_prog \<Rightarrow> pos \<Rightarrow> cname option"
"handlesEx P p \<equiv> (case handlesEx' P p of [] \<Rightarrow> None
                                      | cn#cns \<Rightarrow> Some cn)" 

constdefs
catchesEx::"jvm_prog \<Rightarrow> cname \<Rightarrow> pos \<Rightarrow> bool"
"catchesEx P X p \<equiv> (let (C,M,pc) = p; m = match_ex_table P X pc (ex_table_of P C M) 
                    in (case m of None \<Rightarrow> False | Some pc' \<Rightarrow> True))"

constdefs sys_xcpt_of :: "instr \<Rightarrow> cname"
"sys_xcpt_of i \<equiv> (case i of New C \<Rightarrow> OutOfMemory 
                       | Getfield F C \<Rightarrow> NullPointer
                       | Putfield F C \<Rightarrow> NullPointer
                       | Checkcast C \<Rightarrow> ClassCast
                       | Invoke M n \<Rightarrow> NullPointer
                       | Throw \<Rightarrow> NullPointer
                       | _ \<Rightarrow> Exception)"

text {* \clearpage *}
constdefs
wpF::"jbc_prog \<Rightarrow> pos \<Rightarrow> pos \<Rightarrow> expr \<Rightarrow> expr"
"wpF \<Pi> p p' Q \<equiv> 
(let pm=map (\<lambda>q. (Pos q,if q=p' then Pos p else FF)) (getPosEx Q) in 
(case cmd \<Pi> p of None \<Rightarrow> FF | Some ins \<Rightarrow> 
(case handlesEx (fst \<Pi>) p' of None \<Rightarrow> (case ins
 of Load n \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,if k=0 then Rg n 
                                    else St (k - 1))) (stkIds Q))) Q

 | Store n \<Rightarrow> substE (pm@((Rg n,St 0)#
                      map (\<lambda>k. (St k, St (k+1))) (stkIds Q))) Q

 | Push v \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,if k=0 then Cn v 
                                    else St (k - 1))) (stkIds Q))) Q

 | New Cl \<Rightarrow> (let em=(pm@(map (\<lambda>k. (St k,if k=0 then NewA 0
                     else St (k - 1))) (stkIds Q))@
                     (map (\<lambda>n. (NewA n, NewA (n+1))) (getNewEx Q))); 
                 gfe'=foldl (\<lambda>mp hex. (case hex 
of GF F C ex \<Rightarrow> (let ex'=substE mp ex 
                 in (Gf F C ex,IF ex' \<doteq> NewA 0 
                              THEN Cn (the ((snd (blank (fst \<Pi>) Cl))(F,C))) 
                              ELSE Gf F C ex'))
| TY ex ty   \<Rightarrow> (let ex'=substE mp ex
                 in (Ty ex ty,IF ex' \<doteq> NewA 0 
                             THEN Cn (Bool ((Class Cl) = ty)) 
                             ELSE Ty ex' ty)))#mp)
                      em (remdups' (getHeapEx Q))
                  in substE gfe' Q)

 | Getfield F C \<Rightarrow> substE (pm@[(St 0,Gf F C (St 0))]) Q

 | Putfield F C \<Rightarrow> (let em=pm@(map (\<lambda>k. (St k,St (k+2))) (stkIds Q));
                      gfe'=foldl (\<lambda>mp ex. let ex'=substE mp ex 
                                          in (Gf F C ex,IF (ex' \<doteq> St 1) 
                                             THEN St 0 ELSE Gf F C ex')#mp)
                                 em (remdups' (getGfEx F C Q))
                  in substE gfe' Q)

 | Checkcast C \<Rightarrow> substE pm Q 

 | Invoke M n \<Rightarrow> substE (pm@(FrNr,FrNr \<oplus> (Cn (Intg 1)))#
                        (map (\<lambda>k. (Rg k,if k \<le> n then St (n-k) 
                                        else (if k \<le> n + fst (snd (snd (snd (snd (method (fst \<Pi>) (fst p') M)))))
                                              then Cn arb
                                              else none))) (rgIds Q))@
                        (map (\<lambda>k. (St k,none)) (stkIds Q))@
                        (map (\<lambda>ex. (Call ex,ex)) (getCallEx Q))@
                        (concat (map (\<lambda>(cn',ex'). 
                        (if catchesEx (fst \<Pi>) cn' p 
                         then [(Catch cn' ex',ex')] 
                         else [(Catch cn' ex',
                               IF (FrNr \<doteq> Cn (Intg 1)) THEN ex' 
                               ELSE Catch cn' ex')])) (getCatchEx Q)))) Q

 | Return \<Rightarrow> let (C,M,pc)=p; (P,An)=\<Pi>; n = length (fst (snd (method P C M))) 
             in substE (pm@(FrNr,FrNr \<ominus> (Cn (Intg 1)))#
                    (map (\<lambda>k. (St k,if 1 \<le> k then Call (St (n+k)) 
                                     else St 0)) (stkIds Q))@
                   (map (\<lambda>k. (Rg k,Call (Rg k))) (rgIds Q))@
                   (map (\<lambda>ex. (Call ex,Call (Call ex))) (getCallEx Q))@
                   (map (\<lambda>(cn',ex'). (Catch cn' ex',Call (Catch cn' ex'))) 
                        (getCatchEx Q))) Q

 | Pop \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,St (k+1))) (stkIds Q))) Q

 | IBin no \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,if k=0 then Num (St 1) no (St 0) else (St (k+1)))) (stkIds Q))) Q

 | Goto t \<Rightarrow> substE pm Q
 | CmpEq \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,if k=0 then (St 0)\<doteq>(St 1) 
                                         else (St (k+1)))) (stkIds Q))) Q  
 | IfIntCmp ro t \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,St (k+2))) (stkIds Q))) Q
 | IfFalse t \<Rightarrow> substE (pm@(map (\<lambda>k. (St k,St (k+1))) (stkIds Q))) Q
 | Throw \<Rightarrow> FF ) 

| Some cn \<Rightarrow> (let mp=pm@(map (\<lambda>k. (St k,if 1\<le>k then none 
                  else (if (ins = Throw) 
                       then (IF St 0 \<doteq> Cn (Null) 
                             THEN (Cn (Addr (addr_of_sys_xcpt NullPointer))) 
                             ELSE St 0) 
                        else Cn (Addr (addr_of_sys_xcpt (sys_xcpt_of ins)))))) (stkIds Q))@
                (let (C,M,pc)=p; (C',M',pc')=p'; (P,An)=\<Pi> in
                 (if match_ex_table P cn pc (ex_table_of P C M) = Some pc' then [] 
                  else 
                  let rgm=map (\<lambda>k. (Rg k,Catch cn (Rg k))) (rgIds Q);
                      om =map (\<lambda>ex. (Call ex,Catch cn (Call ex))) (getCallEx Q);
                      cm= map (\<lambda>(cn',ex'). (Catch cn' ex', Catch cn (Catch cn' ex'))) 
                              (getCatchEx Q)
                  in (FrNr,Catch cn FrNr)#rgm@om@cm))
              in substE mp Q))))"


section {* Welformedness  *}

constdefs pTy::"jvm_prog \<Rightarrow> ty\<^isub>P"
"pTy P \<equiv> (map_of2 (convert_pt (prog_kil P)))"

consts
throwChk::"jbc_prog \<times> instr option \<times> expr option \<times> pos \<Rightarrow> bool"

--{* Throw instructions require a type annotation (disjunction of Ty (St 0) (Class X)). 
     The successor function uses these to find proper handlers. The initial intruction must
     not be Throw. In typesafe programs (no exception on top of initial stack) this cannot
     happen anyway. *}
defs throwChk_def:
"throwChk \<equiv> \<lambda> (\<Pi>,ins,an,p). (case ins of None \<Rightarrow> True
                                   | Some c \<Rightarrow> 
(case c of Throw \<Rightarrow> (case an of None \<Rightarrow> False 
                          | Some A  \<Rightarrow> (if p=ipc \<Pi> then False else
                            (case extractTy (A,St 0) of [] \<Rightarrow> False 
                                  | ty#tys \<Rightarrow> (list_all (\<lambda> tp. 
                                              (case tp of Void \<Rightarrow> False | Boolean \<Rightarrow> False 
                                                       | Integer \<Rightarrow> False | NT \<Rightarrow> False 
                                                       | Class X \<Rightarrow> True)) (ty#tys)))))
        | _ \<Rightarrow> True))"


lemma throwChk_Throw_A [simp]:
"throwChk (\<Pi>, Some Throw, Some A, p) = 
(if p=ipc \<Pi> then False else
(case extractTy (A,St 0) of [] \<Rightarrow> False 
 | ty#tys \<Rightarrow> (list_all (\<lambda> tp. (case tp of Void \<Rightarrow> False | Boolean \<Rightarrow> False 
                       | Integer \<Rightarrow> False | NT \<Rightarrow> False 
                       | Class X \<Rightarrow> True)) (ty#tys))))"
(*<*)
by (simp add: throwChk_def)
(*>*)

lemma throwChk_Throw_None [simp]:
"throwChk (\<Pi>,Some Throw,None,p) = False"
(*<*)
by (simp add: throwChk_def)
(*>*)


lemma throwChk_oth_None [simp]:
"ins \<noteq> Some Throw \<Longrightarrow> throwChk (\<Pi>,ins,None,p) = True"
 (*<*)
apply (simp add: throwChk_def)
apply (rule allI)
apply (case_tac "a")
apply simp+
done
(*>*)


lemma throwChk_oth_Some [simp]:
"ins \<noteq> Some Throw \<Longrightarrow> throwChk (\<Pi>,ins,Some A,p) = True"
 (*<*)
apply (simp add: throwChk_def)
apply (rule allI)
apply (case_tac "a")
apply simp+
done
(*>*)


consts
invokeChk::"jbc_prog \<times> (instr option) \<times> (expr option) \<times> pos \<Rightarrow> bool"

--{* Invoke instructions require a type annotation (disjunction of Ty (St n) (Class X)). The successor
     function uses these to determine the potential method entry points. In addition the first instruction
     must not be Invoke. In typesafe programs this cannot happen anyway (no object reference on top of initial stack). We also
     forbid recursive calls of the main method (M ~= fst (snd (ipc Pi))). This ensures that the frame stack never becomes
     empty (A Return in method main stops execution). *}
defs invokeChk_def:
"invokeChk \<equiv> \<lambda> (\<Pi>,ins,an,p). (case ins of None \<Rightarrow> True | Some c \<Rightarrow> case c
of Invoke M n \<Rightarrow> (case an of None \<Rightarrow> False
                  | Some A \<Rightarrow> (if p=ipc \<Pi> then False else 
                              (case extractTy (A,St n) of [] \<Rightarrow> False 
                                    | ty#tys \<Rightarrow> (list_all (\<lambda> tp. (case tp of Void \<Rightarrow> False | Boolean \<Rightarrow> False 
                                                          | Integer \<Rightarrow> False | NT \<Rightarrow> True 
                                                          | Class X \<Rightarrow> has_method (fst \<Pi>) X M)) (ty#tys)) \<and> M \<noteq> fst (snd (ipc \<Pi>)))))
| _ \<Rightarrow> True)"


lemma invokeChk_Invoke_A [simp]:
"invokeChk (\<Pi>,Some (Invoke M n),Some A,p) = (if p=ipc \<Pi> then False else 
(case extractTy (A,St n) of [] \<Rightarrow> False | ty#tys \<Rightarrow> (list_all (\<lambda> tp. (case tp of Void \<Rightarrow> False | Boolean \<Rightarrow> False 
                                     | Integer \<Rightarrow> False | NT \<Rightarrow> True 
                                     | Class X \<Rightarrow> has_method (fst \<Pi>) X M)) (ty#tys)) \<and> M \<noteq> fst (snd (ipc \<Pi>))))"
(*<*)
by (simp add: invokeChk_def)
(*>*)


lemma invokeChk_Invoke_None [simp]:
"invokeChk (\<Pi>,Some (Invoke M n),None,p) = False"
(*<*)
by (simp add: invokeChk_def)
(*>*)


lemma invokeChk_oth_None [simp]:
"(\<forall> M n. ins \<noteq> Some (Invoke M n)) \<Longrightarrow> invokeChk (\<Pi>,ins,None,p) = True"
(*<*)
apply (simp add: invokeChk_def)
apply (rule allI)
apply (case_tac "a")
apply simp+
done
(*>*)


lemma invokeChk_oth_Some [simp]:
"(\<forall> M n. ins \<noteq> Some (Invoke M n)) \<Longrightarrow> invokeChk (\<Pi>,ins,Some A,p) = True"
(*<*)
apply (simp add: invokeChk_def)
apply (rule allI)
apply (case_tac "a")
apply simp+
done
(*>*)

consts
  checkPos :: "jbc_prog \<Rightarrow> (pos list) \<Rightarrow> bool"

--{* checkPos ensures that targets of backward jumps (idx (domC Pi) p' <= idx (domC Pi) p) are annotated. This ensures
     termination of the generic VCG. In addition all successors must be in the code range (p' mem (domC Pi)) and successors
     from the normal successor function must not be entry points of handlers. Throw and Invoke instructions are checked
     for the extra requirements described above. *}
primrec
 "checkPos \<Pi> [] = True"
 "checkPos \<Pi> (p#ps) = (if (let scsn = map fst (succsNormal \<Pi> p);
                            scse = map fst (succsExcept \<Pi> p)
                       in list_all (\<lambda>p'. ((idx (domC \<Pi>) p' \<le> idx (domC \<Pi>) p) 
                                          \<longrightarrow> anF \<Pi> p' \<noteq> None) \<and> p' mem (domC \<Pi>) \<and> 
                                          (p' mem scsn \<longrightarrow> handlesEx (fst \<Pi>) p' = None) \<and> p'\<noteq> ipc \<Pi>) 
                          (scsn @ scse) \<and>  (set scse \<subset> set (domC \<Pi>)) ) \<and> throwChk (\<Pi>,cmd \<Pi> p,anF \<Pi> p,p) \<and> 
                                            invokeChk (\<Pi>,cmd \<Pi> p,anF \<Pi> p,p) 
                       then (checkPos \<Pi> ps) else False)"


lemma checkPos_split:
"checkPos \<Pi> (l1@l2) = ((checkPos \<Pi> l1) \<and> (checkPos \<Pi> l2))"
(*<*) by (induct_tac l1,simp+) (*>*)


constdefs checkExTables ::"jbc_prog \<Rightarrow> bool"
(* "checkExTables \<Pi> \<equiv> list_all (\<lambda>x. x) (concat (map (\<lambda>(C,(S,Fs,Ms)). 
                             concat (map (\<lambda>(M,Ts,T,(mxs,mxl,is,et)). 
                                               (map (\<lambda>(b,e,cn,h,d). d = 0 \<and> 
                                                           cn \<noteq> Object \<and> 
                                                           (C,M,h) \<in> set (domC \<Pi>) \<and> 
 remdups' (concat (map (\<lambda>(b, e, cn, h',d). if h' = h then [cn] else []) et)) = [cn]) et)) 
                                     Ms)) 
                            (fst \<Pi>)))" *)
"checkExTables \<Pi> \<equiv> list_all (\<lambda>x. x) (concat (map (\<lambda>(C,(S,Fs,Ms)). 
                             concat (map (\<lambda>(M,Ts,T,(mxs,mxl,is,et)). 
                                               (map (\<lambda>(b,e,cn,h,d). d = 0 \<and> 
                                                           
                                                           (C,M,h) \<in> set (domC \<Pi>) \<and> 
 remdups' (concat (map (\<lambda>(b, e, cn, h',d). if h' = h then [cn] else []) et)) = [cn]) et)) 
                                     Ms)) 
                            (fst \<Pi>)))"


--{* Programs are wellformed iff
     (1) all positions are wellformed (checkPos). That is
         - targets of backward jumps are annotated (enforces VCG termination).
         - Throw and Invoke instructions have type annotations (possibly inserted by the
           bytecode verifier).
         - the main method is not invoked (only automatically at start up).
     (2) all exception tables are wellformed. That is
         - remaining stack height d is 0 (no catch inside expressions).
         - the catching class is not Object.
         - handler entry points are within the code range.
         - handler entry points are distinct for each handler.
     (3) all classes and methods have distinct names.
     (4) the programs containts all system classes (object, exceptions).
     (5) the intial position is in the code range.
     (6) the main method has no arguments (type safety theorems from BV require this). *}

constdefs
wf :: "jbc_prog \<Rightarrow> bool" 
"wf \<Pi> \<equiv> checkPos \<Pi> (domC \<Pi>) \<and> 
         checkExTables \<Pi> \<and> 
         distinct (classnames (fst \<Pi>)) \<and> 
         distinct (methodnames (fst \<Pi>)) \<and> 
        (\<exists>cdl. fst \<Pi> = (SystemClasses @ cdl)) \<and> (ipc \<Pi> \<in> set (domC \<Pi>))
        \<and> wf_jvm_prog_phi (pTy (fst \<Pi>)) (fst \<Pi>)
        \<and> fst (snd (method (fst \<Pi>) (fst (ipc \<Pi>)) (fst (snd (ipc \<Pi>))))) = []"

section {* System Invariants *}

text {* The following functions yield formulas that hold for 
        all states reachable in wellformed programs *}

subsection {* Position information *}


constdefs inv_Pos::"jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"inv_Pos \<Pi> p \<equiv> Pos p"


subsection {* Frame Stack Size *}

constdefs inv_FrNr:: "jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"inv_FrNr \<Pi> \<equiv> (\<lambda>(C,M,pc). if (let (C0,M0,pc0) = ipc \<Pi> in C=C0 \<and> M=M0) then Eq FrNr (Cn (Intg 1)) else (Rel (Cn (Intg 1)) Less FrNr))" 


subsection {* System Exception Types *}


constdefs inv_ExTys::"jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"inv_ExTys \<Pi> p \<equiv> And [Ty (Cn (Addr (addr_of_sys_xcpt NullPointer))) (Class NullPointer),
                       Ty (Cn (Addr (addr_of_sys_xcpt ClassCast))) (Class ClassCast),
                       Ty (Cn (Addr (addr_of_sys_xcpt OutOfMemory))) (Class OutOfMemory)]"


subsection {* Bytecode Verifier Types *}


constdefs conv_st::"jvm_prog \<Rightarrow> ty\<^isub>i \<Rightarrow> expr"
"conv_st P \<equiv> (\<lambda> (st,rt). (let ex_st = map (\<lambda> n. STy P (St n) (st!n)) (upt 0 (length st));
                              ex_rt = map (\<lambda> n. (case rt!n of Err \<Rightarrow> not_none (Rg n)
                                                           | OK tp \<Rightarrow> STy P (Rg n) tp)) (upt 0 (length rt))
                          in (And (ex_st @ ex_rt))))"



constdefs annotate_types::"jvm_prog \<Rightarrow> ((cname \<times> mname) \<times> (ty\<^isub>i'  list)) list \<Rightarrow> (pos \<Rightarrow> expr)"
"annotate_types P pt \<equiv> (\<lambda> (C,M,pc). 
(if (C,M) mem (methodnames P) then (case pt ? (C,M) of None \<Rightarrow> FF 
 | Some mt \<Rightarrow> (if pc < length mt then (case mt ! pc of None \<Rightarrow> FF | Some tyi \<Rightarrow> conv_st P tyi)
                                 else TT))
else TT))"


constdefs inv_Ty::"jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"inv_Ty \<Pi> p \<equiv> annotate_types (fst \<Pi>) (convert_pt (prog_kil (fst \<Pi>))) p"


section {* Instantiating the VCG *}


constdefs
vcg_jbc :: "jbc_prog \<Rightarrow> expr"
"vcg_jbc prg \<equiv> vcG And Imp FF ipc initF safeF succsF wpF domC domA anF prg"


section {* Upgrade the VCG *}

text {* Here we upgrade the VCG by instantiating it with successor functions that add invariants to branch conditions. *}

constdefs upg::"(jbc_prog \<Rightarrow> pos \<Rightarrow> expr) \<Rightarrow> (jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list) \<Rightarrow> (jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list)"
"upg iF sucF \<equiv> (\<lambda> \<Pi> p. map (\<lambda> (p',B). (p', And [B, iF \<Pi> p])) (sucF \<Pi> p))"


subsection {* Upgrade Frame Stack Size *}


constdefs succsFrNrF:: "jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list"
"succsFrNrF \<equiv> upg inv_FrNr succsF"


constdefs
vcgFrNr :: "jbc_prog \<Rightarrow> expr"
"vcgFrNr prg \<equiv> vcG And Imp FF ipc initF safeF succsFrNrF wpF domC domA anF prg"


subsection {* Upgrade System Exception Types. *}


constdefs succsExTysF:: "jbc_prog \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list"
"succsExTysF \<equiv> upg inv_ExTys succsFrNrF"


constdefs
vcgExTys :: "jbc_prog \<Rightarrow> expr"
"vcgExTys prg \<equiv> vcG And Imp FF ipc initF safeF succsExTysF wpF domC domA anF prg"


subsection {* Upgrade Types *}


constdefs succsTyF:: "jbc_prog  \<Rightarrow> pos \<Rightarrow> (pos \<times> expr) list"
"succsTyF \<equiv> upg inv_Ty succsExTysF"


constdefs
vcgTy :: "jbc_prog \<Rightarrow> expr"
"vcgTy \<Pi> \<equiv> (vcG And Imp FF ipc initF safeF succsTyF wpF domC domA anF \<Pi>)"

end