Theory BVSpec

theory BVSpec
imports Effect
(*  Title:      HOL/MicroJava/BV/BVSpec.thy
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹The Bytecode Verifier \label{sec:BVSpec}›

theory BVSpec
imports Effect
begin

text ‹
  This theory contains a specification of the BV. The specification
  describes correct typings of method bodies; it corresponds 
  to type \emph{checking}.
›

definition
   "The program counter will always be inside the method:"
  check_bounded :: "instr list ⇒ exception_table ⇒ bool" where
  "check_bounded ins et ⟷
  (∀pc < length ins. ∀pc' ∈ set (succs (ins!pc) pc). pc' < length ins) ∧
                     (∀e ∈ set et. fst (snd (snd e)) < length ins)"

definition
   "The method type only contains declared classes:"
  check_types :: "jvm_prog ⇒ nat ⇒ nat ⇒ JVMType.state list ⇒ bool" where
  "check_types G mxs mxr phi ⟷ set phi ⊆ states G mxs mxr"

definition
   "An instruction is welltyped if it is applicable and its effect"
   "is compatible with the type at all successor instructions:"
  wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
                exception_table,p_count] ⇒ bool" where
  "wt_instr i G rT phi mxs max_pc et pc ⟷
  app i G mxs rT pc et (phi!pc) ∧
  (∀(pc',s') ∈ set (eff i G pc et (phi!pc)). pc' < max_pc ∧ G ⊢ s' <=' phi!pc')"

definition
   ‹The type at ‹pc=0› conforms to the method calling convention:›
  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] ⇒ bool" where
  "wt_start G C pTs mxl phi ⟷
  G ⊢ Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"

definition
   "A method is welltyped if the body is not empty, if execution does not"
   "leave the body, if the method type covers all instructions and mentions"
   "declared classes only, if the method calling convention is respected, and"
   "if all instructions are welltyped."
  wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
                 exception_table,method_type] ⇒ bool" where
  "wt_method G C pTs rT mxs mxl ins et phi ⟷
  (let max_pc = length ins in
  0 < max_pc ∧ 
  length phi = length ins ∧
  check_bounded ins et ∧ 
  check_types G mxs (1+length pTs+mxl) (map OK phi) ∧
  wt_start G C pTs mxl phi ∧
  (∀pc. pc<max_pc ⟶ wt_instr (ins!pc) G rT phi mxs max_pc et pc))"

definition
   "A program is welltyped if it is wellformed and all methods are welltyped"
  wt_jvm_prog :: "[jvm_prog,prog_type] ⇒ bool" where
  "wt_jvm_prog G phi ⟷
  wf_prog (λG C (sig,rT,(maxs,maxl,b,et)).
           wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"


lemma check_boundedD:
  "⟦ check_bounded ins et; pc < length ins; 
    (pc',s') ∈ set (eff (ins!pc) G pc et s)  ⟧ ⟹ 
  pc' < length ins"
  apply (unfold eff_def)
  apply simp
  apply (unfold check_bounded_def)
  apply clarify
  apply (erule disjE)
   apply blast
  apply (erule allE, erule impE, assumption)
  apply (unfold xcpt_eff_def)
  apply clarsimp    
  apply (drule xcpt_names_in_et)
  apply clarify
  apply (drule bspec, assumption)
  apply simp
  done

lemma wt_jvm_progD:
  "wt_jvm_prog G phi ⟹ (∃wt. wf_prog wt G)"
  by (unfold wt_jvm_prog_def, blast)

lemma wt_jvm_prog_impl_wt_instr:
  "⟦ wt_jvm_prog G phi; is_class G C;
      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins ⟧ 
  ⟹ wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
  by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
      simp, simp, simp add: wf_mdecl_def wt_method_def)

text ‹
  We could leave out the check @{term "pc' < max_pc"} in the 
  definition of @{term wt_instr} in the context of @{term wt_method}.
›
lemma wt_instr_def2:
  "⟦ wt_jvm_prog G Phi; is_class G C;
      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins; 
      i = ins!pc; phi = Phi C sig; max_pc = length ins ⟧ 
  ⟹ wt_instr i G rT phi maxs max_pc et pc =
     (app i G maxs rT pc et (phi!pc) ∧
     (∀(pc',s') ∈ set (eff i G pc et (phi!pc)). G ⊢ s' <=' phi!pc'))"
apply (simp add: wt_instr_def)
apply (unfold wt_jvm_prog_def)
apply (drule method_wf_mdecl)
apply (simp, simp, simp add: wf_mdecl_def wt_method_def)
apply (auto dest: check_boundedD)
done

lemma wt_jvm_prog_impl_wt_start:
  "⟦ wt_jvm_prog G phi; is_class G C;
      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) ⟧ ⟹ 
  0 < (length ins) ∧ wt_start G C (snd sig) maxl (phi C sig)"
  by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
      simp, simp, simp add: wf_mdecl_def wt_method_def)

end