src/HOL/MicroJava/BV/Altern.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 26450 158b924b5153
child 35416 d8d7d1b785af
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
streckem@14045
     1
(*  Title:      HOL/MicroJava/BV/Altern.thy
streckem@14045
     2
    Author:     Martin Strecker
streckem@14045
     3
*)
streckem@14045
     4
haftmann@33954
     5
header {* Alternative definition of well-typing of bytecode,  used in compiler type correctness proof *}
streckem@14045
     6
haftmann@33954
     7
theory Altern
haftmann@33954
     8
imports BVSpec
haftmann@33954
     9
begin
streckem@13672
    10
streckem@13672
    11
constdefs
wenzelm@26450
    12
  check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool"
streckem@13672
    13
  "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
streckem@13672
    14
streckem@13672
    15
  wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
streckem@13672
    16
                exception_table,p_count] \<Rightarrow> bool"
streckem@13672
    17
  "wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
streckem@13672
    18
  app i G mxs rT pc et (phi!pc) \<and>
streckem@13672
    19
  check_type G mxs mxr (OK (phi!pc)) \<and>
streckem@13672
    20
  (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
streckem@13672
    21
streckem@13672
    22
  wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
streckem@13672
    23
                 exception_table,method_type] \<Rightarrow> bool"
streckem@13672
    24
  "wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
streckem@13672
    25
  let max_pc = length ins in
streckem@13672
    26
  0 < max_pc \<and> 
streckem@13672
    27
  length phi = length ins \<and>
streckem@13672
    28
  check_bounded ins et \<and> 
streckem@13672
    29
  wt_start G C pTs mxl phi \<and>
streckem@13672
    30
  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"
streckem@13672
    31
streckem@13672
    32
streckem@13672
    33
lemma wt_method_wt_method_altern : 
streckem@13672
    34
  "wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi"
streckem@13672
    35
apply (simp add: wt_method_def wt_method_altern_def)
streckem@13672
    36
apply (intro strip)
streckem@13672
    37
apply clarify
streckem@13672
    38
apply (drule spec, drule mp, assumption)
streckem@13672
    39
apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
streckem@13672
    40
apply (auto  intro: imageI)
streckem@13672
    41
done
streckem@13672
    42
streckem@13672
    43
streckem@13672
    44
lemma check_type_check_types [rule_format]: 
streckem@13672
    45
  "(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc)))
streckem@13672
    46
  \<longrightarrow> check_types G mxs mxr (map OK phi)"
streckem@13672
    47
apply (induct phi)
streckem@13672
    48
apply (simp add: check_types_def)
streckem@13672
    49
apply (simp add: check_types_def)
streckem@13672
    50
apply clarify
streckem@13672
    51
apply (frule_tac x=0 in spec)
streckem@13672
    52
apply (simp add: check_type_def)
streckem@13672
    53
apply auto
streckem@13672
    54
done
streckem@13672
    55
streckem@13672
    56
lemma wt_method_altern_wt_method [rule_format]: 
streckem@13672
    57
  "wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi"
streckem@13672
    58
apply (simp add: wt_method_def wt_method_altern_def)
streckem@13672
    59
apply (intro strip)
streckem@13672
    60
apply clarify
streckem@13672
    61
apply (rule conjI)
streckem@13672
    62
  (* show check_types *)
streckem@13672
    63
apply (rule check_type_check_types)
streckem@13672
    64
apply (simp add: wt_instr_altern_def)
streckem@13672
    65
streckem@13672
    66
  (* show wt_instr *)
streckem@13672
    67
apply (intro strip)
streckem@13672
    68
apply (drule spec, drule mp, assumption)
streckem@13672
    69
apply (simp add: wt_instr_def wt_instr_altern_def)
streckem@13672
    70
done
streckem@13672
    71
streckem@13672
    72
streckem@13672
    73
end