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