src/HOL/MicroJava/BV/LBVComplete.thy
author kleing
Thu Mar 09 13:54:03 2000 +0100 (2000-03-09)
changeset 8388 b66d3c49cb8d
child 9012 d1bd2144ab5d
permissions -rw-r--r--
completeness of the lightweight bytecode verifier
kleing@8388
     1
(*  Title:      HOL/MicroJava/BV/LBVComplete.thy
kleing@8388
     2
    ID:         $Id$
kleing@8388
     3
    Author:     Gerwin Klein
kleing@8388
     4
    Copyright   2000 Technische Universitaet Muenchen
kleing@8388
     5
kleing@8388
     6
Proof of completeness for the lightweight bytecode verifier
kleing@8388
     7
*)
kleing@8388
     8
kleing@8388
     9
LBVComplete= LBVSpec +
kleing@8388
    10
kleing@8388
    11
constdefs
kleing@8388
    12
  is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
kleing@8388
    13
  "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
kleing@8388
    14
                   (a!n = None \\<or> a!n = Some (b!n)))"
kleing@8388
    15
  
kleing@8388
    16
  fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
kleing@8388
    17
  "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
kleing@8388
    18
                            (\\<forall> pc. pc < length ins \\<longrightarrow>
kleing@8388
    19
                                   contains_dead ins cert phi pc \\<and> 
kleing@8388
    20
                                   contains_targets ins cert phi pc)"
kleing@8388
    21
kleing@8388
    22
  contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
kleing@8388
    23
  "contains_dead ins cert phi pc \\<equiv>
kleing@8388
    24
    (((\\<exists> branch. ins!pc = BR (Goto branch)) \\<or> ins!pc = MR Return) \\<or>
kleing@8388
    25
     (\\<exists>mi. ins!pc = MI mi)) \\<longrightarrow> Suc pc < length phi \\<longrightarrow>
kleing@8388
    26
      cert ! (Suc pc) = Some (phi ! Suc pc)"
kleing@8388
    27
kleing@8388
    28
  contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
kleing@8388
    29
  "contains_targets ins cert phi pc \\<equiv> 
kleing@8388
    30
    \\<forall> branch. (ins!pc = BR (Goto branch) \\<or> ins!pc = BR (Ifcmpeq branch)) \\<longrightarrow>
kleing@8388
    31
        (let pc' = nat (int pc+branch) in pc' < length phi \\<longrightarrow> cert!pc' = Some (phi!pc'))" 
kleing@8388
    32
kleing@8388
    33
  is_target :: "[instr list, p_count] \\<Rightarrow> bool" 
kleing@8388
    34
  "is_target ins pc \\<equiv> 
kleing@8388
    35
     \\<exists> pc' branch. pc' < length ins \\<and> 
kleing@8388
    36
                   (ins ! pc' = (BR (Ifcmpeq branch)) \\<or> ins ! pc' = (BR (Goto branch))) \\<and> 
kleing@8388
    37
                   pc = (nat(int pc'+branch))"
kleing@8388
    38
  
kleing@8388
    39
  maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
kleing@8388
    40
  "maybe_dead ins pc \\<equiv>
kleing@8388
    41
     \\<exists> pc'. pc = pc'+1 \\<and> ((\\<exists> branch. ins!pc' = BR (Goto branch)) \\<or>
kleing@8388
    42
                          ins!pc' = MR Return \\<or>
kleing@8388
    43
                          (\\<exists>mi. ins!pc' = MI mi))"
kleing@8388
    44
kleing@8388
    45
kleing@8388
    46
  mdot :: "[instr list, p_count] \\<Rightarrow> bool"
kleing@8388
    47
  "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"
kleing@8388
    48
kleing@8388
    49
kleing@8388
    50
consts
kleing@8388
    51
  option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list" 
kleing@8388
    52
primrec 
kleing@8388
    53
  "option_filter_n []    P n = []"  
kleing@8388
    54
  "option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) 
kleing@8388
    55
                                         else None   # option_filter_n t P (n+1))"  
kleing@8388
    56
  
kleing@8388
    57
constdefs 
kleing@8388
    58
  option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list" 
kleing@8388
    59
  "option_filter l P \\<equiv> option_filter_n l P 0" 
kleing@8388
    60
  
kleing@8388
    61
  make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
kleing@8388
    62
  "make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
kleing@8388
    63
  
kleing@8388
    64
  make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
kleing@8388
    65
  "make_Cert G Phi \\<equiv>  \\<lambda> C sig.
kleing@8388
    66
    let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
kleing@8388
    67
      let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
kleing@8388
    68
        make_cert b (Phi C sig)"
kleing@8388
    69
  
kleing@8388
    70
constdefs
kleing@8388
    71
  wfprg :: "jvm_prog \\<Rightarrow> bool"
kleing@8388
    72
  "wfprg G \\<equiv> \\<exists>wf_mb. wf_prog wf_mb G"
kleing@8388
    73
kleing@8388
    74
end