src/HOL/MicroJava/BV/BVSpec.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 26453 758c6fef7b94
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/BV/BVSpec.thy
     2     ID:         $Id$
     3     Author:     Cornelia Pusch, Gerwin Klein
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 *)
     7 
     8 header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
     9 
    10 theory BVSpec imports Effect begin
    11 
    12 text {*
    13   This theory contains a specification of the BV. The specification
    14   describes correct typings of method bodies; it corresponds 
    15   to type \emph{checking}.
    16 *}
    17 
    18 constdefs
    19   -- "The program counter will always be inside the method:"
    20   check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
    21   "check_bounded ins et \<equiv> 
    22   (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
    23                      (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
    24 
    25   -- "The method type only contains declared classes:"
    26   check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
    27   "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
    28 
    29   -- "An instruction is welltyped if it is applicable and its effect"
    30   -- "is compatible with the type at all successor instructions:"
    31   wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
    32                 exception_table,p_count] \<Rightarrow> bool"
    33   "wt_instr i G rT phi mxs max_pc et pc \<equiv>
    34   app i G mxs rT pc et (phi!pc) \<and>
    35   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
    36 
    37   -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
    38   wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
    39   "wt_start G C pTs mxl phi == 
    40   G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
    41 
    42   -- "A method is welltyped if the body is not empty, if execution does not"
    43   -- "leave the body, if the method type covers all instructions and mentions"
    44   -- "declared classes only, if the method calling convention is respected, and"
    45   -- "if all instructions are welltyped."
    46   wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
    47                  exception_table,method_type] \<Rightarrow> bool"
    48   "wt_method G C pTs rT mxs mxl ins et phi \<equiv>
    49   let max_pc = length ins in
    50   0 < max_pc \<and> 
    51   length phi = length ins \<and>
    52   check_bounded ins et \<and> 
    53   check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
    54   wt_start G C pTs mxl phi \<and>
    55   (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc)"
    56 
    57   -- "A program is welltyped if it is wellformed and all methods are welltyped"
    58   wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
    59   "wt_jvm_prog G phi ==
    60   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
    61            wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
    62 
    63 
    64 lemma check_boundedD:
    65   "\<lbrakk> check_bounded ins et; pc < length ins; 
    66     (pc',s') \<in> set (eff (ins!pc) G pc et s)  \<rbrakk> \<Longrightarrow> 
    67   pc' < length ins"
    68   apply (unfold eff_def)
    69   apply simp
    70   apply (unfold check_bounded_def)
    71   apply clarify
    72   apply (erule disjE)
    73    apply blast
    74   apply (erule allE, erule impE, assumption)
    75   apply (unfold xcpt_eff_def)
    76   apply clarsimp    
    77   apply (drule xcpt_names_in_et)
    78   apply clarify
    79   apply (drule bspec, assumption)
    80   apply simp
    81   done
    82 
    83 lemma wt_jvm_progD:
    84   "wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
    85   by (unfold wt_jvm_prog_def, blast)
    86 
    87 lemma wt_jvm_prog_impl_wt_instr:
    88   "\<lbrakk> wt_jvm_prog G phi; is_class G C;
    89       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk> 
    90   \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    91   by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    92       simp, simp, simp add: wf_mdecl_def wt_method_def)
    93 
    94 text {*
    95   We could leave out the check @{term "pc' < max_pc"} in the 
    96   definition of @{term wt_instr} in the context of @{term wt_method}.
    97 *}
    98 lemma wt_instr_def2:
    99   "\<lbrakk> wt_jvm_prog G Phi; is_class G C;
   100       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins; 
   101       i = ins!pc; phi = Phi C sig; max_pc = length ins \<rbrakk> 
   102   \<Longrightarrow> wt_instr i G rT phi maxs max_pc et pc =
   103      (app i G maxs rT pc et (phi!pc) \<and>
   104      (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). G \<turnstile> s' <=' phi!pc'))"
   105 apply (simp add: wt_instr_def)
   106 apply (unfold wt_jvm_prog_def)
   107 apply (drule method_wf_mdecl)
   108 apply (simp, simp, simp add: wf_mdecl_def wt_method_def)
   109 apply (auto dest: check_boundedD)
   110 done
   111 
   112 lemma wt_jvm_prog_impl_wt_start:
   113   "\<lbrakk> wt_jvm_prog G phi; is_class G C;
   114       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow> 
   115   0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
   116   by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
   117       simp, simp, simp add: wf_mdecl_def wt_method_def)
   118 
   119 end