Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: BVSpec.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>The Bytecode Verifier \label{sec:BVSpec}\<close>

theory BVSpec
imports Effect
begin

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

definition
  \<comment> \<open>The program counter will always be inside the method:\<close>
  check_bounded :: "instr list \ exception_table \ bool" where
  "check_bounded ins et \
  (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
                     (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"

definition
  \<comment> \<open>The method type only contains declared classes:\<close>
  check_types :: "jvm_prog \ nat \ nat \ JVMType.state list \ bool" where
  "check_types G mxs mxr phi \ set phi \ states G mxs mxr"

definition
  \<comment> \<open>An instruction is welltyped if it is applicable and its effect\<close>
  \<comment> \<open>is compatible with the type at all successor instructions:\<close>
  wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
                exception_table,p_count] \<Rightarrow> bool" where
  "wt_instr i G rT phi mxs max_pc et pc \
  app i G mxs rT pc et (phi!pc) \<and>
  (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"

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

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

definition
  \<comment> \<open>A program is welltyped if it is wellformed and all methods are welltyped\<close>
  wt_jvm_prog :: "[jvm_prog,prog_type] \ bool" where
  "wt_jvm_prog G phi \
  wf_prog (\<lambda>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') \<in> set (eff (ins!pc) G pc et s)  \<rbrakk> \<Longrightarrow>
  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 \<rbrakk>
  \<Longrightarrow> 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 \<open>
  We could leave out the check \<^term>\<open>pc' < max_pc\<close> in the
  definition of \<^term>\<open>wt_instr\<close> in the context of \<^term>\<open>wt_method\<close>.
\<close>
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 \<rbrakk>
  \<Longrightarrow> wt_instr i G rT phi maxs max_pc et pc =
     (app i G maxs rT pc et (phi!pc) \<and>
     (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). G \<turnstile> 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) \<rbrakk> \<Longrightarrow>
  0 < (length ins) \<and> 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

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.