src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
author wenzelm
Fri, 23 Sep 2011 21:51:49 +0200
changeset 45068 3cc2ac688fd9
parent 45054 73accf69135d
child 53024 e0968e1f6fe9
permissions -rw-r--r--
tuned proof;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
     2
    Author:     Cornelia Pusch, Gerwin Klein
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     3
    Copyright   1999 Technische Universitaet Muenchen
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
*)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     5
12911
704713ca07ea new document
kleing
parents: 12545
diff changeset
     6
header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
     7
27680
5a557a5afc48 added explicit root theory; some tuning
haftmann
parents: 23467
diff changeset
     8
theory BVSpecTypeSafe
5a557a5afc48 added explicit root theory; some tuning
haftmann
parents: 23467
diff changeset
     9
imports Correct
5a557a5afc48 added explicit root theory; some tuning
haftmann
parents: 23467
diff changeset
    10
begin
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    11
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    12
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    13
  This theory contains proof that the specification of the bytecode
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    14
  verifier only admits type safe programs.  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    15
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    16
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    17
section {* Preliminaries *}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    18
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    19
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    20
  Simp and intro setup for the type safety proof:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    21
*}
10812
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10763
diff changeset
    22
lemmas defs1 = sup_state_conv correct_state_def correct_frame_def 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    23
               wt_instr_def eff_def norm_eff_def 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
    24
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
    25
lemmas widen_rules[intro] = approx_val_widen approx_loc_widen approx_stk_widen
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
    26
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    27
lemmas [simp del] = split_paired_All
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    28
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    29
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    30
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    31
  If we have a welltyped program and a conforming state, we
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    32
  can directly infer that the current instruction is well typed:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    33
*}
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    34
lemma wt_jvm_prog_impl_wt_instr_cor:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
    35
  "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
    36
      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
    37
  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    38
apply (unfold correct_state_def Let_def correct_frame_def)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    39
apply simp
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    40
apply (blast intro: wt_jvm_prog_impl_wt_instr)
9819
wenzelm
parents: 9757
diff changeset
    41
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
    42
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    43
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    44
section {* Exception Handling *}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    45
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    46
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    47
  Exceptions don't touch anything except the stack:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    48
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    49
lemma exec_instr_xcpt:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    50
  "(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    51
  = (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs = 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    52
            (Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    53
  by (cases i, auto simp add: split_beta split: split_if_asm)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    54
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    55
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    56
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    57
  Relates @{text match_any} from the Bytecode Verifier with 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    58
  @{text match_exception_table} from the operational semantics:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    59
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    60
lemma in_match_any:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
    61
  "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow> 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    62
  \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    63
      match_exception_table G C pc et = Some pc'"
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
    64
  (is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    65
proof (induct et)  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    66
  show "PROP ?P []" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    67
    by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    68
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    69
  fix e es
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    70
  assume IH: "PROP ?P es"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    71
  assume match: "?match (e#es)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    72
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    73
  obtain start_pc end_pc handler_pc catch_type where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    74
    e [simp]: "e = (start_pc, end_pc, handler_pc, catch_type)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    75
    by (cases e) 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    76
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    77
  from IH match
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    78
  show "?match_any (e#es)" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    79
  proof (cases "match_exception_entry G xcpt pc e")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    80
    case False
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    81
    with match
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    82
    have "match_exception_table G xcpt pc es = Some pc'" by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    83
    with IH
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    84
    obtain C where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    85
      set: "C \<in> set (match_any G pc es)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    86
      C:   "G \<turnstile> xcpt \<preceq>C C" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    87
      m:   "match_exception_table G C pc es = Some pc'" by blast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    88
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    89
    from set
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    90
    have "C \<in> set (match_any G pc (e#es))" by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    91
    moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    92
    from False C
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    93
    have "\<not> match_exception_entry G C pc e"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    94
      by - (erule contrapos_nn, 
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18551
diff changeset
    95
            auto simp add: match_exception_entry_def)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    96
    with m
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    97
    have "match_exception_table G C pc (e#es) = Some pc'" by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    98
    moreover note C
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
    99
    ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   100
    show ?thesis by blast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   101
  next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   102
    case True with match
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   103
    have "match_exception_entry G catch_type pc e"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   104
      by (simp add: match_exception_entry_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   105
    moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   106
    from True match
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   107
    obtain 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   108
      "start_pc \<le> pc" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   109
      "pc < end_pc" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   110
      "G \<turnstile> xcpt \<preceq>C catch_type" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   111
      "handler_pc = pc'" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   112
      by (simp add: match_exception_entry_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   113
    ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   114
    show ?thesis by auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   115
  qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   116
qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   117
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   118
lemma match_et_imp_match:
13717
78f91fcdf560 beautified "match"
kleing
parents: 13678
diff changeset
   119
  "match_exception_table G (Xcpt X) pc et = Some handler
78f91fcdf560 beautified "match"
kleing
parents: 13678
diff changeset
   120
  \<Longrightarrow> match G X pc et = [Xcpt X]"
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   121
  apply (simp add: match_some_entry)
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   122
  apply (induct et)
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   123
  apply (auto split: split_if_asm)
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   124
  done
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   125
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   126
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   127
  We can prove separately that the recursive search for exception
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   128
  handlers (@{text find_handler}) in the frame stack results in 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   129
  a conforming state (if there was no matching exception handler 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   130
  in the current frame). We require that the exception is a valid
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   131
  heap address, and that the state before the exception occured
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   132
  conforms. 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   133
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   134
lemma uncaught_xcpt_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   135
  "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   136
      G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   137
  \<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   138
  (is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   139
proof (induct frs) 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   140
  -- "the base case is trivial, as it should be"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   141
  show "?correct (?find [])" by (simp add: correct_state_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   142
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   143
  -- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   144
  assume wt: ?wt 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   145
  then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   146
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   147
  -- "these two don't change in the induction:"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   148
  assume adr: ?adr
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   149
  assume hp: ?hp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   150
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   151
  -- "the assumption for the cons case:"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   152
  fix f f' frs' 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   153
  assume cr: "?correct (None, hp, f#f'#frs')" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   154
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   155
  -- "the induction hypothesis as produced by Isabelle, immediatly simplified
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   156
    with the fixed assumptions above"
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   157
  assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"  
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   158
  with wt adr hp 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   159
  have IH: "\<And>f. ?correct (None, hp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   160
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   161
  from cr
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   162
  have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   163
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   164
  obtain stk loc C sig pc where f' [simp]: "f' = (stk,loc,C,sig,pc)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   165
    by (cases f') 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   166
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   167
  from cr 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   168
  obtain rT maxs maxl ins et where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   169
    meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   170
    by (simp add: correct_state_def, blast)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   171
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   172
  hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   173
    by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   174
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   175
  show "?correct (?find (f'#frs'))" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   176
  proof (cases "match_exception_table G (cname_of hp xcp) pc et")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   177
    case None
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   178
    with cr' IH 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   179
    show ?thesis by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   180
  next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   181
    fix handler_pc 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   182
    assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   183
    (is "?match (cname_of hp xcp) = _")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   184
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   185
    from wt meth cr' [simplified]
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   186
    have wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   187
      by (rule wt_jvm_prog_impl_wt_instr_cor)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   188
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   189
    from cr meth
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   190
    obtain C' mn pts ST LT where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   191
      ins: "ins!pc = Invoke C' mn pts" (is "_ = ?i") and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   192
      phi: "phi C sig ! pc = Some (ST, LT)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   193
      by (simp add: correct_state_def) blast    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   194
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   195
    from match
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   196
    obtain D where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   197
      in_any: "D \<in> set (match_any G pc et)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   198
      D:      "G \<turnstile> cname_of hp xcp \<preceq>C D" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   199
      match': "?match D = Some handler_pc"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   200
      by (blast dest: in_match_any)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   201
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   202
    from ins wti phi have 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   203
      "\<forall>D\<in>set (match_any G pc et). the (?match D) < length ins \<and> 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   204
      G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?match D)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   205
      by (simp add: wt_instr_def eff_def xcpt_eff_def)      
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   206
    with in_any match' obtain
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   207
      pc: "handler_pc < length ins" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   208
      "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler_pc"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   209
      by auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   210
    then obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   211
      phi': "phi C sig ! handler_pc = Some (ST',LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   212
      less: "G \<turnstile> ([Class D], LT) <=s (ST',LT')"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   213
      by auto    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   214
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   215
    from cr' phi meth f'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   216
    have "correct_frame G hp (ST, LT) maxl ins f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   217
      by (unfold correct_state_def) auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   218
    then obtain
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   219
     len: "length loc = 1+length (snd sig)+maxl" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   220
     loc: "approx_loc G hp loc LT"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   221
      by (unfold correct_frame_def) auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   222
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   223
    let ?f = "([xcp], loc, C, sig, handler_pc)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   224
    have "correct_frame G hp (ST', LT') maxl ins ?f" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   225
    proof -
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   226
      from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   227
      have "approx_loc G hp loc LT'" by (simp add: sup_state_conv) blast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   228
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   229
      from D adr hp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   230
      have "G,hp \<turnstile> xcp ::\<preceq> Class D" by (simp add: conf_def obj_ty_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   231
      with wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   232
      have "approx_stk G hp [xcp] ST'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   233
        by (auto simp add: sup_state_conv approx_stk_def approx_val_def 
40928
ace26e2cee91 eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
krauss
parents: 32960
diff changeset
   234
                 elim: conf_widen split: err.split)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   235
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   236
      note len pc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   237
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   238
      show ?thesis by (simp add: correct_frame_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   239
    qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   240
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   241
    with cr' match phi' meth  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   242
    show ?thesis by (unfold correct_state_def) auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   243
  qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   244
qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   245
13672
b95d12325b51 Added compiler
streckem
parents: 13524
diff changeset
   246
declare raise_if_def [simp]
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   247
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   248
  The requirement of lemma @{text uncaught_xcpt_correct} (that
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   249
  the exception is a valid reference on the heap) is always met
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   250
  for welltyped instructions and conformant states:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   251
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   252
lemma exec_instr_xcpt_hp:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   253
  "\<lbrakk>  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   254
       wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   255
       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   256
  \<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   257
  (is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   258
proof -
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   259
  note [simp] = split_beta raise_system_xcpt_def
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   260
  note [split] = split_if_asm option.split_asm 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   261
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   262
  assume wt: ?wt ?correct
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   263
  hence pre: "preallocated hp" by (simp add: correct_state_def)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   264
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   265
  assume xcpt: ?xcpt with pre show ?thesis 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   266
  proof (cases "ins!pc")
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   267
    case New with xcpt pre
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   268
    show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD) 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   269
  next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   270
    case Throw with xcpt wt
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   271
    show ?thesis
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   272
      by (auto simp add: wt_instr_def correct_state_def correct_frame_def 
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   273
               dest: non_npD dest!: preallocatedD)
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   274
  qed (auto dest!: preallocatedD)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   275
qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   276
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   277
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   278
lemma cname_of_xcp [intro]:
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   279
  "\<lbrakk>preallocated hp; xcp = Addr (XcptRef x)\<rbrakk> \<Longrightarrow> cname_of hp xcp = Xcpt x"
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   280
  by (auto elim: preallocatedE [of hp x])
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   281
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   282
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   283
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   284
  Finally we can state that, whenever an exception occurs, the
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   285
  resulting next state always conforms:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   286
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   287
lemma xcpt_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   288
  "\<lbrakk> wt_jvm_prog G phi;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   289
      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   290
      wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   291
      fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp; 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   292
      Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   293
      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   294
  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   295
proof -
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   296
  assume wtp: "wt_jvm_prog G phi"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   297
  assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   298
  assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   299
  assume xp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   300
  assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   301
  assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   302
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   303
  from wtp obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   304
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   305
  note xp' = meth s' xp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   306
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   307
  note wtp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   308
  moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   309
  from xp wt correct
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   310
  obtain adr T where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   311
    adr: "xcp = Addr adr" "hp adr = Some T"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   312
    by (blast dest: exec_instr_xcpt_hp)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   313
  moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   314
  note correct
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   315
  ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   316
  have "G,phi \<turnstile>JVM find_handler G (Some xcp) hp frs \<surd>" by (rule uncaught_xcpt_correct)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   317
  with xp'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   318
  have "match_exception_table G (cname_of hp xcp) pc et = None \<Longrightarrow> ?thesis" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   319
    (is "?m (cname_of hp xcp) = _ \<Longrightarrow> _" is "?match = _ \<Longrightarrow> _")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   320
    by (clarsimp simp add: exec_instr_xcpt split_beta)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   321
  moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   322
  { fix handler
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   323
    assume some_handler: "?match = Some handler"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   324
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   325
    from correct meth
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   326
    obtain ST LT where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   327
      hp_ok:  "G \<turnstile>h hp \<surd>" and
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   328
      prehp:  "preallocated hp" and
18551
be0705186ff5 class now an keyword, quoted where necessary
haftmann
parents: 16417
diff changeset
   329
      "class":  "is_class G C" and
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   330
      phi_pc: "phi C sig ! pc = Some (ST, LT)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   331
      frame:  "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   332
      frames: "correct_frames G hp phi rT sig frs"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   333
      by (unfold correct_state_def) auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   334
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   335
    from frame obtain 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   336
      stk: "approx_stk G hp stk ST" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   337
      loc: "approx_loc G hp loc LT" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   338
      pc:  "pc < length ins" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   339
      len: "length loc = 1+length (snd sig)+maxl"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   340
      by (unfold correct_frame_def) auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   341
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   342
    from wt obtain
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   343
      eff: "\<forall>(pc', s')\<in>set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et).
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   344
             pc' < length ins \<and> G \<turnstile> s' <=' phi C sig!pc'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   345
      by (simp add: wt_instr_def eff_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   346
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   347
    from some_handler xp'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   348
    have state': 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   349
      "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)"
45068
3cc2ac688fd9 tuned proof;
wenzelm
parents: 45054
diff changeset
   350
      by (cases "ins!pc") (auto simp add: raise_system_xcpt_def split_beta 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   351
                               split: split_if_asm) (* takes long! *)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   352
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   353
    let ?f' = "([xcp], loc, C, sig, handler)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   354
    from eff
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   355
    obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   356
      phi_pc': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   357
      frame': "correct_frame G hp (ST',LT') maxl ins ?f'" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   358
    proof (cases "ins!pc")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   359
      case Return -- "can't generate exceptions:"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   360
      with xp' have False by (simp add: split_beta split: split_if_asm)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   361
      thus ?thesis ..
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   362
    next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   363
      case New
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   364
      with some_handler xp'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   365
      have xcp: "xcp = Addr (XcptRef OutOfMemory)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   366
        by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   367
      with prehp have "cname_of hp xcp = Xcpt OutOfMemory" ..
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   368
      with New some_handler phi_pc eff 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   369
      obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   370
        phi': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   371
        less: "G \<turnstile> ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   372
        pc':  "handler < length ins"
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   373
        by (simp add: xcpt_eff_def match_et_imp_match) blast
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   374
      note phi'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   375
      moreover
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   376
      { from xcp prehp
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   377
        have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)"
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   378
          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   379
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   380
        from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   381
        have "approx_loc G hp loc LT'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   382
          by (simp add: sup_state_conv) blast        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   383
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   384
        note wf less pc' len 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   385
        ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   386
        have "correct_frame G hp (ST',LT') maxl ins ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   387
          by (unfold correct_frame_def) (auto simp add: sup_state_conv 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   388
              approx_stk_def approx_val_def split: err.split elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   389
      }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   390
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   391
      show ?thesis by (rule that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   392
    next 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   393
      case Getfield
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   394
      with some_handler xp'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   395
      have xcp: "xcp = Addr (XcptRef NullPointer)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   396
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   397
      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   398
      with Getfield some_handler phi_pc eff 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   399
      obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   400
        phi': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   401
        less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   402
        pc':  "handler < length ins"
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   403
        by (simp add: xcpt_eff_def match_et_imp_match) blast
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   404
      note phi'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   405
      moreover
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   406
      { from xcp prehp
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   407
        have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   408
          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   409
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   410
        from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   411
        have "approx_loc G hp loc LT'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   412
          by (simp add: sup_state_conv) blast        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   413
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   414
        note wf less pc' len 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   415
        ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   416
        have "correct_frame G hp (ST',LT') maxl ins ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   417
          by (unfold correct_frame_def) (auto simp add: sup_state_conv 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   418
              approx_stk_def approx_val_def split: err.split elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   419
      }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   420
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   421
      show ?thesis by (rule that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   422
    next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   423
      case Putfield
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   424
      with some_handler xp'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   425
      have xcp: "xcp = Addr (XcptRef NullPointer)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   426
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   427
      with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   428
      with Putfield some_handler phi_pc eff 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   429
      obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   430
        phi': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   431
        less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   432
        pc':  "handler < length ins"
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   433
        by (simp add: xcpt_eff_def match_et_imp_match) blast
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   434
      note phi'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   435
      moreover
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   436
      { from xcp prehp
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   437
        have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)"
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   438
          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   439
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   440
        from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   441
        have "approx_loc G hp loc LT'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   442
          by (simp add: sup_state_conv) blast        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   443
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   444
        note wf less pc' len 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   445
        ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   446
        have "correct_frame G hp (ST',LT') maxl ins ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   447
          by (unfold correct_frame_def) (auto simp add: sup_state_conv 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   448
              approx_stk_def approx_val_def split: err.split elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   449
      }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   450
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   451
      show ?thesis by (rule that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   452
    next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   453
      case Checkcast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   454
      with some_handler xp'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   455
      have xcp: "xcp = Addr (XcptRef ClassCast)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   456
        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   457
      with prehp have "cname_of hp xcp = Xcpt ClassCast" ..
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   458
      with Checkcast some_handler phi_pc eff 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   459
      obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   460
        phi': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   461
        less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   462
        pc':  "handler < length ins"
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
   463
        by (simp add: xcpt_eff_def match_et_imp_match) blast
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   464
      note phi'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   465
      moreover
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   466
      { from xcp prehp
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   467
        have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ClassCast)"
13052
3bf41c474a88 canonical start state
kleing
parents: 13006
diff changeset
   468
          by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   469
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   470
        from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   471
        have "approx_loc G hp loc LT'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   472
          by (simp add: sup_state_conv) blast        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   473
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   474
        note wf less pc' len 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   475
        ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   476
        have "correct_frame G hp (ST',LT') maxl ins ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   477
          by (unfold correct_frame_def) (auto simp add: sup_state_conv 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   478
              approx_stk_def approx_val_def split: err.split elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   479
      }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   480
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   481
      show ?thesis by (rule that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   482
    next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   483
      case Invoke
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   484
      with phi_pc eff 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   485
      have 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   486
        "\<forall>D\<in>set (match_any G pc et). 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   487
        the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   488
        by (simp add: xcpt_eff_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   489
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   490
      from some_handler
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   491
      obtain D where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   492
        "D \<in> set (match_any G pc et)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   493
        D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   494
        "?m D = Some handler"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   495
        by (blast dest: in_match_any)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   496
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   497
      obtain 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   498
        pc': "handler < length ins" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   499
        "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   500
        by auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   501
      then
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   502
      obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   503
        phi': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   504
        less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   505
        by auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   506
      from xp wt correct
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   507
      obtain addr T where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   508
        xcp: "xcp = Addr addr" "hp addr = Some T"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   509
        by (blast dest: exec_instr_xcpt_hp)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   510
      note phi'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   511
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   512
      { from xcp D
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   513
        have "G,hp \<turnstile> xcp ::\<preceq> Class D"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   514
          by (simp add: conf_def obj_ty_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   515
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   516
        from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   517
        have "approx_loc G hp loc LT'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   518
          by (simp add: sup_state_conv) blast        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   519
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   520
        note wf less pc' len 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   521
        ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   522
        have "correct_frame G hp (ST',LT') maxl ins ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   523
          by (unfold correct_frame_def) (auto simp add: sup_state_conv 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   524
              approx_stk_def approx_val_def split: err.split elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   525
      }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   526
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   527
      show ?thesis by (rule that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   528
    next
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   529
      case Throw
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   530
      with phi_pc eff 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   531
      have 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   532
        "\<forall>D\<in>set (match_any G pc et). 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   533
        the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   534
        by (simp add: xcpt_eff_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   535
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   536
      from some_handler
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   537
      obtain D where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   538
        "D \<in> set (match_any G pc et)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   539
        D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   540
        "?m D = Some handler"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   541
        by (blast dest: in_match_any)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   542
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   543
      obtain 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   544
        pc': "handler < length ins" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   545
        "G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   546
        by auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   547
      then
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   548
      obtain ST' LT' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   549
        phi': "phi C sig ! handler = Some (ST', LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   550
        less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   551
        by auto
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   552
      from xp wt correct
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   553
      obtain addr T where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   554
        xcp: "xcp = Addr addr" "hp addr = Some T"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   555
        by (blast dest: exec_instr_xcpt_hp)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   556
      note phi'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   557
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   558
      { from xcp D
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   559
        have "G,hp \<turnstile> xcp ::\<preceq> Class D"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   560
          by (simp add: conf_def obj_ty_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   561
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   562
        from wf less loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   563
        have "approx_loc G hp loc LT'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   564
          by (simp add: sup_state_conv) blast        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   565
        moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   566
        note wf less pc' len 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   567
        ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   568
        have "correct_frame G hp (ST',LT') maxl ins ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   569
          by (unfold correct_frame_def) (auto simp add: sup_state_conv 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   570
              approx_stk_def approx_val_def split: err.split elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   571
      }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   572
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   573
      show ?thesis by (rule that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   574
    qed (insert xp', auto) -- "the other instructions don't generate exceptions"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   575
23467
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   576
    from state' meth hp_ok "class" frames phi_pc' frame' prehp
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   577
    have ?thesis by (unfold correct_state_def) simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   578
  }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   579
  ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   580
  show ?thesis by (cases "?match") blast+ 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   581
qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   582
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   583
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   584
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10920
diff changeset
   585
section {* Single Instructions *}
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10920
diff changeset
   586
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   587
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   588
  In this section we look at each single (welltyped) instruction, and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   589
  prove that the state after execution of the instruction still conforms.
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   590
  Since we have already handled exceptions above, we can now assume, that
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   591
  on exception occurs for this (single step) execution.
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   592
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   593
10812
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10763
diff changeset
   594
lemmas [iff] = not_Err_eq
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10763
diff changeset
   595
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   596
lemma Load_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   597
"\<lbrakk> wf_prog wt G;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   598
    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   599
    ins!pc = Load idx; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   600
    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   601
    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   602
    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   603
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
   604
apply (clarsimp simp add: defs1)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   605
apply (blast intro: approx_loc_imp_approx_val_sup)
9819
wenzelm
parents: 9757
diff changeset
   606
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   607
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   608
lemma Store_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   609
"\<lbrakk> wf_prog wt G;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   610
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   611
  ins!pc = Store idx;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   612
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   613
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   614
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   615
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
   616
apply (clarsimp simp add: defs1)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   617
apply (blast intro: approx_loc_subst)
9819
wenzelm
parents: 9757
diff changeset
   618
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   619
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   620
10897
697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents: 10812
diff changeset
   621
lemma LitPush_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   622
"\<lbrakk> wf_prog wt G;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   623
    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
10897
697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents: 10812
diff changeset
   624
    ins!pc = LitPush v;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   625
    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   626
    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   627
    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   628
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
   629
apply (clarsimp simp add: defs1 sup_PTS_eq)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   630
apply (blast dest: conf_litval intro: conf_widen)
9819
wenzelm
parents: 9757
diff changeset
   631
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   632
10897
697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents: 10812
diff changeset
   633
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   634
lemma Cast_conf2:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   635
  "\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   636
      G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   637
  \<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   638
apply (unfold cast_ok_def)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   639
apply (frule widen_Class)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   640
apply (elim exE disjE) 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   641
 apply (simp add: null)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   642
apply (clarsimp simp add: conf_def obj_ty_def)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   643
apply (cases v)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18551
diff changeset
   644
apply auto
9819
wenzelm
parents: 9757
diff changeset
   645
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   646
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13052
diff changeset
   647
lemmas defs2 = defs1 raise_system_xcpt_def
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   648
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   649
lemma Checkcast_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   650
"\<lbrakk> wt_jvm_prog G phi;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   651
    method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   652
    ins!pc = Checkcast D; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   653
    wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   654
    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   655
    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   656
    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   657
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
   658
apply (clarsimp simp add: defs2 wt_jvm_prog_def split: split_if_asm)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   659
apply (blast intro: Cast_conf2)
9819
wenzelm
parents: 9757
diff changeset
   660
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   661
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   662
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   663
lemma Getfield_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   664
"\<lbrakk> wt_jvm_prog G phi;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   665
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   666
  ins!pc = Getfield F D; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   667
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   668
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   669
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   670
  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   671
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
   672
apply (clarsimp simp add: defs2 wt_jvm_prog_def split_beta
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   673
                split: option.split split_if_asm)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   674
apply (frule conf_widen)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   675
apply assumption+
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   676
apply (drule conf_RefTD)
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13052
diff changeset
   677
apply (clarsimp simp add: defs2)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   678
apply (rule conjI)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   679
 apply (drule widen_cfs_fields)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   680
 apply assumption+
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   681
 apply (erule wf_prog_ws_prog)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   682
 apply (erule conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   683
 prefer 2
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   684
  apply assumption
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   685
 apply (simp add: hconf_def oconf_def lconf_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   686
 apply (elim allE)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   687
 apply (erule impE, assumption)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   688
 apply simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   689
 apply (elim allE)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   690
 apply (erule impE, assumption)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   691
 apply clarsimp
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   692
apply blast
9819
wenzelm
parents: 9757
diff changeset
   693
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   694
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   695
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   696
lemma Putfield_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   697
"\<lbrakk> wf_prog wt G;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   698
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   699
  ins!pc = Putfield F D; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   700
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   701
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   702
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   703
  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   704
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
40928
ace26e2cee91 eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
krauss
parents: 32960
diff changeset
   705
apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   706
apply (frule conf_widen)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   707
prefer 2
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   708
  apply assumption
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   709
 apply assumption
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   710
apply (drule conf_RefTD)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   711
apply clarsimp
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   712
apply (blast 
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   713
       intro: 
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   714
         hext_upd_obj approx_stk_sup_heap
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   715
         approx_loc_sup_heap 
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   716
         hconf_field_update
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   717
         preallocated_field_update
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   718
         correct_frames_field_update conf_widen 
10056
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   719
       dest: 
9f84ffa4a8d0 tuned spacing for document generation
kleing
parents: 10042
diff changeset
   720
         widen_cfs_fields)
9819
wenzelm
parents: 9757
diff changeset
   721
done
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   722
    
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   723
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   724
lemma New_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   725
"\<lbrakk> wf_prog wt G;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   726
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   727
  ins!pc = New X; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   728
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   729
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   730
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   731
  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   732
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   733
proof -
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   734
  assume wf:   "wf_prog wt G"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   735
  assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   736
  assume ins:  "ins!pc = New X"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   737
  assume wt:   "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   738
  assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   739
  assume conf: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   740
  assume no_x: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None"
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   741
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   742
  from ins conf meth
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   743
  obtain ST LT where
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   744
    heap_ok:    "G\<turnstile>h hp\<surd>" and
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   745
    prealloc:   "preallocated hp" and
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   746
    phi_pc:     "phi C sig!pc = Some (ST,LT)" and
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   747
    is_class_C: "is_class G C" and
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   748
    frame:      "correct_frame G hp (ST,LT) maxl ins (stk, loc, C, sig, pc)" and
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   749
    frames:     "correct_frames G hp phi rT sig frs"
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   750
    by (auto simp add: correct_state_def iff del: not_None_eq)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   751
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   752
  from phi_pc ins wt
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   753
  obtain ST' LT' where
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   754
    is_class_X: "is_class G X" and
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   755
    maxs:       "length ST < maxs" and
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   756
    suc_pc:     "Suc pc < length ins" and
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   757
    phi_suc:    "phi C sig ! Suc pc = Some (ST', LT')" and
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   758
    less:       "G \<turnstile> (Class X # ST, LT) <=s (ST', LT')"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   759
    by (unfold wt_instr_def eff_def norm_eff_def) auto
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   760
 
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   761
  obtain oref xp' where
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   762
    new_Addr: "new_Addr hp = (oref,xp')"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   763
    by (cases "new_Addr hp") 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   764
  with ins no_x
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   765
  obtain hp: "hp oref = None" and "xp' = None"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   766
    by (auto dest: new_AddrD simp add: raise_system_xcpt_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   767
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   768
  with exec ins meth new_Addr 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   769
  have state':
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   770
    "state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))), 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   771
              (Addr oref # stk, loc, C, sig, Suc pc) # frs)" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   772
    (is "state' = Norm (?hp', ?f # frs)")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   773
    by simp    
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   774
  moreover
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   775
  from wf hp heap_ok is_class_X
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   776
  have hp': "G \<turnstile>h ?hp' \<surd>"
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   777
    by - (rule hconf_newref, 
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   778
          auto simp add: oconf_def dest: fields_is_type)
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   779
  moreover
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   780
  from hp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   781
  have sup: "hp \<le>| ?hp'" by (rule hext_new)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   782
  from hp frame less suc_pc wf
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   783
  have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   784
    apply (unfold correct_frame_def sup_state_conv)
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
   785
    apply (clarsimp simp add: conf_def fun_upd_apply approx_val_def)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   786
    apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   787
    done      
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   788
  moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   789
  from hp frames wf heap_ok is_class_X
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   790
  have "correct_frames G ?hp' phi rT sig frs"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   791
    by - (rule correct_frames_newref, 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   792
          auto simp add: oconf_def dest: fields_is_type)
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   793
  moreover
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   794
  from hp prealloc have "preallocated ?hp'" by (rule preallocated_newref)
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   795
  ultimately
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   796
  show ?thesis
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   797
    by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq)
10920
9b74eceea2d2 newref -> new_Addr
kleing
parents: 10897
diff changeset
   798
qed
11085
b830bf10bf71 tuned for 99-2 release
kleing
parents: 10920
diff changeset
   799
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   800
lemmas [simp del] = split_paired_Ex
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   801
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   802
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
   803
lemma Invoke_correct: 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   804
"\<lbrakk> wt_jvm_prog G phi; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   805
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   806
  ins ! pc = Invoke C' mn pTs; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   807
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   808
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   809
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   810
  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   811
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   812
proof -
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   813
  assume wtprog: "wt_jvm_prog G phi"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   814
  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   815
  assume ins:    "ins ! pc = Invoke C' mn pTs"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   816
  assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   817
  assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
10812
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10763
diff changeset
   818
  assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   819
  assume no_xcp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None"
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   820
  
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   821
  from wtprog 
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   822
  obtain wfmb where
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   823
    wfprog: "wf_prog wfmb G" 
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   824
    by (simp add: wt_jvm_prog_def)
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
   825
      
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   826
  from ins method approx
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   827
  obtain s where
10812
ead84e90bfeb merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents: 10763
diff changeset
   828
    heap_ok: "G\<turnstile>h hp\<surd>" and
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
   829
    prealloc:"preallocated hp" and
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   830
    phi_pc:  "phi C sig!pc = Some s" and
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
   831
    is_class_C: "is_class G C" and
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   832
    frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   833
    frames:  "correct_frames G hp phi rT sig frs"
23467
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   834
    by (auto iff del: not_None_eq simp add: correct_state_def)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   835
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   836
  from ins wti phi_pc
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   837
  obtain apTs X ST LT D' rT body where 
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
   838
    is_class: "is_class G C'" and
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   839
    s:  "s = (rev apTs @ X # ST, LT)" and
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   840
    l:  "length apTs = length pTs" and
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   841
    X:  "G\<turnstile> X \<preceq> Class C'" and
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 18551
diff changeset
   842
    w:  "\<forall>(x, y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq> y" and
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   843
    mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   844
    pc: "Suc pc < length ins" and
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   845
    eff: "G \<turnstile> norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   846
    by (simp add: wt_instr_def eff_def del: not_None_eq) 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   847
       (elim exE conjE, rule that)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   848
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   849
  from eff
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   850
  obtain ST' LT' where
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   851
    s': "phi C sig ! Suc pc = Some (ST', LT')"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   852
    by (simp add: norm_eff_def split_paired_Ex) blast
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   853
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   854
  from X 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   855
  obtain T where
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   856
    X_Ref: "X = RefT T"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   857
    by - (drule widen_RefT2, erule exE, rule that)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   858
  
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   859
  from s ins frame 
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   860
  obtain 
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   861
    a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   862
    a_loc: "approx_loc G hp loc LT" and
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   863
    suc_l: "length loc = Suc (length (snd sig) + maxl)"
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   864
    by (simp add: correct_frame_def)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   865
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   866
  from a_stk
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   867
  obtain opTs stk' oX where
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   868
    opTs:   "approx_stk G hp opTs (rev apTs)" and
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents: 10387
diff changeset
   869
    oX:     "approx_val G hp oX (OK X)" and
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   870
    a_stk': "approx_stk G hp stk' ST" and
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   871
    stk':   "stk = opTs @ oX # stk'" and
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   872
    l_o:    "length opTs = length apTs" 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   873
            "length stk' = length ST"  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   874
    by - (drule approx_stk_append, auto)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   875
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   876
  from oX X_Ref
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   877
  have oX_conf: "G,hp \<turnstile> oX ::\<preceq> RefT T"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   878
    by (simp add: approx_val_def)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   879
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   880
  from stk' l_o l
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
   881
  have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   882
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   883
  with state' method ins no_xcp oX_conf
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   884
  obtain ref where oX_Addr: "oX = Addr ref"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   885
    by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   886
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   887
  with oX_conf X_Ref
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   888
  obtain obj D where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   889
    loc:    "hp ref = Some obj" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   890
    obj_ty: "obj_ty obj = Class D" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   891
    D:      "G \<turnstile> Class D \<preceq> X"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   892
    by (auto simp add: conf_def) blast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   893
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   894
  with X_Ref obtain X' where X': "X = Class X'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   895
    by (blast dest: widen_Class)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   896
      
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   897
  with X have X'_subcls: "G \<turnstile> X' \<preceq>C C'"  by simp
10612
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10592
diff changeset
   898
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   899
  with mC' wfprog
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   900
  obtain D0 rT0 maxs0 maxl0 ins0 et0 where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   901
    mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0, et0)" "G\<turnstile>rT0\<preceq>rT"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   902
    by (auto dest: subtype_widen_methd intro: that)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   903
    
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   904
  from X' D have D_subcls: "G \<turnstile> D \<preceq>C X'" by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   905
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   906
  with wfprog mX
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   907
  obtain D'' rT' mxs' mxl' ins' et' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   908
    mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   909
        "G \<turnstile> rT' \<preceq> rT0"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   910
    by (auto dest: subtype_widen_methd intro: that)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   911
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   912
  from mX mD have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   913
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   914
  from is_class X'_subcls D_subcls
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   915
  have is_class_D: "is_class G D" by (auto dest: subcls_is_class2)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   916
  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   917
  with mD wfprog
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   918
  obtain mD'': 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   919
    "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   920
    "is_class G D''"
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   921
    by (auto dest: wf_prog_ws_prog [THEN method_in_md])
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   922
      
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   923
  from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   924
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   925
  with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   926
  have state'_val:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   927
    "state' =
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27680
diff changeset
   928
     Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   929
                D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   930
    (is "state' = Norm (hp, ?f # ?f' # frs)")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   931
    by (simp add: raise_system_xcpt_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   932
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   933
  from wtprog mD''
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   934
  have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   935
    by (auto dest: wt_jvm_prog_impl_wt_start)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   936
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   937
  then obtain LT0 where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   938
    LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   939
    by (clarsimp simp add: wt_start_def sup_state_conv)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   940
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   941
  have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   942
  proof -
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   943
    from start LT0
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   944
    have sup_loc: 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   945
      "G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   946
      (is "G \<turnstile> ?LT <=l LT0")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   947
      by (simp add: wt_start_def sup_state_conv)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   948
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27680
diff changeset
   949
    have r: "approx_loc G hp (replicate mxl' undefined) (replicate mxl' Err)"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   950
      by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   951
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   952
    from wfprog mD is_class_D
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   953
    have "G \<turnstile> Class D \<preceq> Class D''"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   954
      by (auto dest: method_wf_mdecl)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   955
    with obj_ty loc
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   956
    have a: "approx_val G hp (Addr ref) (OK (Class D''))"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   957
      by (simp add: approx_val_def conf_def)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   958
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   959
    from opTs w l l_o wfprog 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   960
    have "approx_stk G hp opTs (rev pTs)" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   961
      by (auto elim!: approx_stk_all_widen simp add: zip_rev)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   962
    hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   963
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   964
    with r a l_o l
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27680
diff changeset
   965
    have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' undefined) ?LT"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   966
      (is "approx_loc G hp ?lt ?LT")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   967
      by (auto simp add: approx_loc_append approx_stk_def)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   968
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   969
    from this sup_loc wfprog
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   970
    have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   971
    with start l_o l
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   972
    show ?thesis by (simp add: correct_frame_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   973
  qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   974
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   975
  from state'_val heap_ok mD'' ins method phi_pc s X' l mX
23467
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   976
       frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   977
  show ?thesis
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   978
    apply (simp add: correct_state_def)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   979
    apply (intro exI conjI)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   980
       apply blast
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   981
      apply (rule l)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   982
     apply (rule mX)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   983
    apply (rule mD)
d1b97708d5eb tuned proofs -- avoid implicit prems;
wenzelm
parents: 22271
diff changeset
   984
    done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   985
qed
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   986
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   987
lemmas [simp del] = map_append
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   988
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   989
lemma Return_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   990
"\<lbrakk> wt_jvm_prog G phi; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   991
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   992
  ins ! pc = Return; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   993
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
   994
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   995
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
   996
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   997
proof -
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   998
  assume wt_prog: "wt_jvm_prog G phi"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
   999
  assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1000
  assume ins: "ins ! pc = Return"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1001
  assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1002
  assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1003
  assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1004
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1005
  from wt_prog 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1006
  obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1007
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1008
  from meth ins s'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1009
  have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1010
  moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1011
  { fix f frs' 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1012
    assume frs': "frs = f#frs'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1013
    moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1014
    obtain stk' loc' C' sig' pc' where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1015
      f: "f = (stk',loc',C',sig',pc')" by (cases f)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1016
    moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1017
    obtain mn pt where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1018
      sig: "sig = (mn,pt)" by (cases sig)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1019
    moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1020
    note meth ins s'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1021
    ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1022
    have state':
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1023
      "state' = (None,hp,(hd stk#(drop (1+length pt) stk'),loc',C',sig',pc'+1)#frs')"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1024
      (is "state' = (None,hp,?f'#frs')")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1025
      by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1026
    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1027
    from correct meth
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1028
    obtain ST LT where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1029
      hp_ok:  "G \<turnstile>h hp \<surd>" and
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
  1030
      alloc:  "preallocated hp" and
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1031
      phi_pc: "phi C sig ! pc = Some (ST, LT)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1032
      frame:  "correct_frame G hp (ST, LT) maxl ins (stk,loc,C,sig,pc)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1033
      frames: "correct_frames G hp phi rT sig frs"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1034
      by (simp add: correct_state_def, clarify, blast)    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1035
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1036
    from phi_pc ins wt
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1037
    obtain T ST' where "ST = T # ST'" "G \<turnstile> T \<preceq> rT"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1038
      by (simp add: wt_instr_def) blast    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1039
    with wf frame 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1040
    have hd_stk: "G,hp \<turnstile> (hd stk) ::\<preceq> rT"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1041
      by (auto simp add: correct_frame_def elim: conf_widen)
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1042
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1043
    from f frs' frames sig
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1044
    obtain apTs ST0' ST' LT' D D' D'' rT' rT'' maxs' maxl' ins' et' body where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1045
      phi':   "phi C' sig' ! pc' = Some (ST',LT')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1046
      class': "is_class G C'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1047
      meth':  "method (G,C') sig' = Some (C',rT',maxs',maxl',ins',et')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1048
      ins':   "ins' ! pc' = Invoke D' mn pt" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1049
      frame': "correct_frame G hp (ST', LT') maxl' ins' f" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1050
      frames':"correct_frames G hp phi rT' sig' frs'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1051
      rT'':   "G \<turnstile> rT \<preceq> rT''" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1052
      meth'': "method (G, D) sig = Some (D'', rT'', body)" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1053
      ST0':   "ST' = rev apTs @ Class D # ST0'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1054
      len':   "length apTs = length pt" 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1055
      by clarsimp blast    
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1056
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1057
    from f frame'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1058
    obtain
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1059
      stk': "approx_stk G hp stk' ST'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1060
      loc': "approx_loc G hp loc' LT'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1061
      pc':  "pc' < length ins'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1062
      lloc':"length loc' = Suc (length (snd sig') + maxl')"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1063
      by (simp add: correct_frame_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1064
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1065
    from wt_prog class' meth' pc'  
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1066
    have "wt_instr (ins'!pc') G rT' (phi C' sig') maxs' (length ins') et' pc'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1067
      by (rule wt_jvm_prog_impl_wt_instr)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1068
    with ins' phi' sig
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1069
    obtain apTs ST0 X ST'' LT'' body' rT0 mD where
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1070
      phi_suc: "phi C' sig' ! Suc pc' = Some (ST'', LT'')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1071
      ST0:     "ST' = rev apTs @ X # ST0" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1072
      len:     "length apTs = length pt" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1073
      less:    "G \<turnstile> (rT0 # ST0, LT') <=s (ST'', LT'')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1074
      methD':  "method (G, D') sig = Some (mD, rT0, body')" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1075
      lessD':  "G \<turnstile> X \<preceq> Class D'" and
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1076
      suc_pc': "Suc pc' < length ins'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1077
      by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1078
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1079
    from len len' ST0 ST0'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1080
    have "X = Class D" by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1081
    with lessD'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1082
    have "G \<turnstile> D \<preceq>C D'" by simp
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1083
    moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1084
    note wf meth'' methD'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1085
    ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1086
    have "G \<turnstile> rT'' \<preceq> rT0" by (auto dest: subcls_widen_methd)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1087
    with wf hd_stk rT''
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1088
    have hd_stk': "G,hp \<turnstile> (hd stk) ::\<preceq> rT0" by (auto elim: conf_widen widen_trans)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1089
        
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1090
    have frame'':
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1091
      "correct_frame G hp (ST'',LT'') maxl' ins' ?f'"
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1092
    proof -
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1093
      from wf hd_stk' len stk' less ST0
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1094
      have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''" 
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
  1095
        by (auto simp add: sup_state_conv
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1096
                 dest!: approx_stk_append elim: conf_widen)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1097
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1098
      from wf loc' less
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1099
      have "approx_loc G hp loc' LT''" by (simp add: sup_state_conv) blast
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1100
      moreover
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1101
      note suc_pc' lloc'
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1102
      ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1103
      show ?thesis by (simp add: correct_frame_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1104
    qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1105
12545
7319d384d0d3 removed preallocated heaps axiom (now in type safety invariant)
kleing
parents: 12516
diff changeset
  1106
    with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' alloc
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1107
    have ?thesis by (simp add: correct_state_def)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1108
  }
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1109
  ultimately
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1110
  show ?thesis by (cases frs) blast+
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1111
qed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1112
  
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1113
lemmas [simp] = map_append
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1114
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1115
lemma Goto_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1116
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1117
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1118
  ins ! pc = Goto branch; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1119
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1120
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1121
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1122
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13052
diff changeset
  1123
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1124
apply fast
9819
wenzelm
parents: 9757
diff changeset
  1125
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1126
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1127
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1128
lemma Ifcmpeq_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1129
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1130
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1131
  ins ! pc = Ifcmpeq branch; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1132
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1133
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1134
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1135
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13052
diff changeset
  1136
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1137
apply fast
9819
wenzelm
parents: 9757
diff changeset
  1138
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1139
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1140
lemma Pop_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1141
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1142
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1143
  ins ! pc = Pop;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1144
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1145
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1146
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1147
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13052
diff changeset
  1148
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1149
apply fast
9819
wenzelm
parents: 9757
diff changeset
  1150
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1151
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1152
lemma Dup_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1153
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1154
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1155
  ins ! pc = Dup;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1156
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1157
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1158
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1159
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
  1160
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1161
apply (blast intro: conf_widen)
9819
wenzelm
parents: 9757
diff changeset
  1162
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1163
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1164
lemma Dup_x1_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1165
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1166
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1167
  ins ! pc = Dup_x1;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1168
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1169
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1170
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1171
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
  1172
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1173
apply (blast intro: conf_widen)
9819
wenzelm
parents: 9757
diff changeset
  1174
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1175
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1176
lemma Dup_x2_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1177
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1178
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1179
  ins ! pc = Dup_x2;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1180
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1181
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1182
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1183
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
  1184
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1185
apply (blast intro: conf_widen)
9819
wenzelm
parents: 9757
diff changeset
  1186
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1187
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1188
lemma Swap_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1189
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1190
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1191
  ins ! pc = Swap;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1192
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1193
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1194
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1195
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
  1196
apply (clarsimp simp add: defs2)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1197
apply (blast intro: conf_widen)
9819
wenzelm
parents: 9757
diff changeset
  1198
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1199
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1200
lemma IAdd_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1201
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1202
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1203
  ins ! pc = IAdd; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1204
  wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1205
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1206
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1207
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13717
diff changeset
  1208
apply (clarsimp simp add: defs2 approx_val_def conf_def)
11252
71c00cb091d2 cleanup, tuned
kleing
parents: 11085
diff changeset
  1209
apply blast
9819
wenzelm
parents: 9757
diff changeset
  1210
done
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1211
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1212
lemma Throw_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1213
"\<lbrakk> wf_prog wt G; 
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1214
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1215
  ins ! pc = Throw; 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1216
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1217
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1218
  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1219
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1220
  by simp
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1221
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1222
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1223
text {*
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1224
  The next theorem collects the results of the sections above,
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1225
  i.e.~exception handling and the execution step for each 
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1226
  instruction. It states type safety for single step execution:
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1227
  in welltyped programs, a conforming state is transformed
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1228
  into another conforming state when one instruction is executed.
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1229
*}
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1230
theorem instr_correct:
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1231
"\<lbrakk> wt_jvm_prog G phi;
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1232
  method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1233
  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
13006
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1234
  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
51c5f3f11d16 symbolized
kleing
parents: 12951
diff changeset
  1235
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1236
apply (frule wt_jvm_prog_impl_wt_instr_cor)
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1237
apply assumption+
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1238
apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)")
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1239
defer
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1240
apply (erule xcpt_correct, assumption+) 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1241
apply (cases "ins!pc")
10897
697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents: 10812
diff changeset
  1242
prefer 8
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
  1243
apply (rule Invoke_correct, assumption+)
10897
697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents: 10812
diff changeset
  1244
prefer 8
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
  1245
apply (rule Return_correct, assumption+)
12516
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1246
prefer 5
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1247
apply (rule Getfield_correct, assumption+)
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1248
prefer 6
d09d0f160888 exceptions
kleing
parents: 12389
diff changeset
  1249
apply (rule Checkcast_correct, assumption+)
10612
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10592
diff changeset
  1250
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 8011
diff changeset
  1251
apply (unfold wt_jvm_prog_def)
10626
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
  1252
apply (rule Load_correct, assumption+)
46bcddfe9e7b update for changes in Correct.thy and class/is_class defs
kleing
parents: 10612
diff changeset
  1253
apply (rule Store_correct, assumption+)
10897
697fab84709e removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents: 10812
diff changeset
  1254
apply (rule LitPush_correct, assumption+)
10626
46bcddfe9e7b update for changes in Correct.thy and