Theory BVSpec

(*  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