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