src/HOL/MicroJava/JVM/JVMExceptions.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 35102 cc7a0b9f938c
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein, Martin Strecker
     4     Copyright   2001 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Exception handling in the JVM} *}
     8 
     9 theory JVMExceptions imports JVMInstructions begin
    10 
    11 constdefs
    12   match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool"
    13   "match_exception_entry G cn pc ee == 
    14                  let (start_pc, end_pc, handler_pc, catch_type) = ee in
    15                  start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
    16 
    17 
    18 consts
    19   match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
    20                           \<Rightarrow> p_count option"
    21 primrec
    22   "match_exception_table G cn pc []     = None"
    23   "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
    24                                            then Some (fst (snd (snd e))) 
    25                                            else match_exception_table G cn pc es)"
    26 
    27 consts
    28   ex_table_of :: "jvm_method \<Rightarrow> exception_table"
    29 translations
    30   "ex_table_of m" == "snd (snd (snd m))"
    31 
    32 
    33 consts
    34   find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
    35 primrec
    36   "find_handler G xcpt hp [] = (xcpt, hp, [])"
    37   "find_handler G xcpt hp (fr#frs) = 
    38       (case xcpt of
    39          None \<Rightarrow> (None, hp, fr#frs)
    40        | Some xc \<Rightarrow> 
    41        let (stk,loc,C,sig,pc) = fr in
    42        (case match_exception_table G (cname_of hp xc) pc 
    43               (ex_table_of (snd(snd(the(method (G,C) sig))))) of
    44           None \<Rightarrow> find_handler G (Some xc) hp frs
    45         | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"
    46 
    47 
    48 text {*
    49   System exceptions are allocated in all heaps:
    50 *}
    51 
    52 
    53 text {*
    54   Only program counters that are mentioned in the exception table
    55   can be returned by @{term match_exception_table}:
    56 *}
    57 lemma match_exception_table_in_et:
    58   "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"
    59   by (induct et) (auto split: split_if_asm)
    60 
    61 
    62 end