Theory Exception_Tables

(*  Title:      JinjaThreads/Compiler/Exception_Tables.thy
    Author:     Andreas Lochbihler
*)

section ‹Various Operations for Exception Tables›

theory Exception_Tables imports
  Compiler2
  "../Common/ExternalCallWF"
  "../JVM/JVMExceptions"
begin

definition pcs :: "ex_table  nat set"
where "pcs xt    (f,t,C,h,d)  set xt. {f ..< t}"

lemma pcs_subset:
  fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows "pcs(compxE2 e pc d)  {pc..<pc+size(compE2 e)}"
  and "pcs(compxEs2 es pc d)  {pc..<pc+size(compEs2 es)}" 
apply(induct e pc d and es pc d rule: compxE2_compxEs2_induct)
apply (simp_all add:pcs_def)
apply (fastforce)+
done

lemma pcs_Nil [simp]: "pcs [] = {}"
by(simp add:pcs_def)

lemma pcs_Cons [simp]: "pcs (x#xt) = {fst x ..< fst(snd x)}  pcs xt"
by(auto simp add: pcs_def)

lemma pcs_append [simp]: "pcs(xt1 @ xt2) = pcs xt1  pcs xt2"
by(simp add:pcs_def)

lemma [simp]: "pc < pc0  pc0+size(compE2 e)  pc  pc  pcs(compxE2 e pc0 d)"
using pcs_subset by fastforce

lemma [simp]: "pc < pc0  pc0+size(compEs2 es)  pc  pc  pcs(compxEs2 es pc0 d)"
using pcs_subset by fastforce

lemma [simp]: "pc1 + size(compE2 e1)  pc2  pcs(compxE2 e1 pc1 d1)  pcs(compxE2 e2 pc2 d2) = {}"
using pcs_subset by fastforce

lemma [simp]: "pc1 + size(compE2 e)  pc2  pcs(compxE2 e pc1 d1)  pcs(compxEs2 es pc2 d2) = {}"
using pcs_subset by fastforce

lemma match_ex_table_append_not_pcs [simp]:
 "pc  pcs xt0  match_ex_table P C pc (xt0 @ xt1) = match_ex_table P C pc xt1"
by (induct xt0) (auto simp: matches_ex_entry_def)

lemma outside_pcs_not_matches_entry [simp]:
  " x  set xt; pc  pcs xt   ¬ matches_ex_entry P D pc x"
by(auto simp:matches_ex_entry_def pcs_def)

lemma outside_pcs_compxE2_not_matches_entry [simp]:
  assumes xe: "xe  set(compxE2 e pc d)"
  and outside: "pc' < pc  pc+size(compE2 e)  pc'"
  shows "¬ matches_ex_entry P C pc' xe"
proof
  assume "matches_ex_entry P C pc' xe"
  with xe have "pc'  pcs(compxE2 e pc d)"
    by(force simp add:matches_ex_entry_def pcs_def)
  with outside show False by simp
qed

lemma outside_pcs_compxEs2_not_matches_entry [simp]:
  assumes xe: "xe  set(compxEs2 es pc d)" 
  and outside: "pc' < pc  pc+size(compEs2 es)  pc'"
  shows "¬ matches_ex_entry P C pc' xe"
proof
  assume "matches_ex_entry P C pc' xe"
  with xe have "pc'  pcs(compxEs2 es pc d)"
    by(force simp add:matches_ex_entry_def pcs_def)
  with outside show False by simp
qed

lemma match_ex_table_app[simp]:
  "xte  set xt1. ¬ matches_ex_entry P D pc xte 
  match_ex_table P D pc (xt1 @ xt) = match_ex_table P D pc xt"
by(induct xt1) simp_all

lemma match_ex_table_eq_NoneI [simp]:
  "x  set xtab. ¬ matches_ex_entry P C pc x 
  match_ex_table P C pc xtab = None"
using match_ex_table_app[where ?xt = "[]"] by fastforce

lemma match_ex_table_not_pcs_None:
  "pc  pcs xt  match_ex_table P C pc xt = None"
by(auto intro: match_ex_table_eq_NoneI)

lemma match_ex_entry:
  fixes start shows
  "matches_ex_entry P C pc (start, end, catch_type, handler) =
  (start  pc  pc < end  (case catch_type of None  True | C'  P  C * C'))"
by(simp add:matches_ex_entry_def)

lemma pcs_compxE2D [dest]:
  "pc  pcs (compxE2 e pc' d)  pc'  pc  pc < pc' + length (compE2 e)"
using pcs_subset by(fastforce)

lemma pcs_compxEs2D [dest]:
  "pc  pcs (compxEs2 es pc' d)  pc'  pc  pc < pc' + length (compEs2 es)"
using pcs_subset by(fastforce)

definition shift :: "nat  ex_table  ex_table"
where
  "shift n xt  map (λ(from,to,C,handler,depth). (n+from,n+to,C,n+handler,depth)) xt"

lemma shift_0 [simp]: "shift 0 xt = xt"
by(induct xt)(auto simp:shift_def)

lemma shift_Nil [simp]: "shift n [] = []"
by(simp add:shift_def)

lemma shift_Cons_tuple [simp]:
  "shift n ((from, to, C, handler, depth) # xt) = (from + n, to + n, C, handler + n, depth) # shift n xt"
by(simp add: shift_def)

lemma shift_append [simp]: "shift n (xt1 @ xt2) = shift n xt1 @ shift n xt2"
by(simp add:shift_def)

lemma shift_shift [simp]: "shift m (shift n xt) = shift (m+n) xt"
by(simp add: shift_def split_def)

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows shift_compxE2: "shift pc (compxE2 e pc' d) = compxE2 e (pc' + pc) d"
  and  shift_compxEs2: "shift pc (compxEs2 es pc' d) = compxEs2 es (pc' + pc) d"
by(induct e and es arbitrary: pc pc' d and pc pc' d rule: compE2.induct compEs2.induct)
  (auto simp:shift_def ac_simps)

lemma compxE2_size_convs [simp]: "n  0  compxE2 e n d = shift n (compxE2 e 0 d)"
 and compxEs2_size_convs: "n  0  compxEs2 es n d = shift n (compxEs2 es 0 d)" 
by(simp_all add:shift_compxE2 shift_compxEs2)

lemma pcs_shift_conv [simp]: "pcs (shift n xt) = (+) n ` pcs xt"
apply(auto simp add: shift_def pcs_def)
apply(rule_tac x="x-n" in image_eqI)
apply(auto)
apply(rule bexI)
 prefer 2
 apply(assumption)
apply(auto)
done

lemma image_plus_const_conv [simp]:
  fixes m :: nat
  shows "m  (+) n ` A  m  n  m - n  A"
by(force)

lemma match_ex_table_shift_eq_None_conv [simp]:
  "match_ex_table P C pc (shift n xt) = None  pc < n  match_ex_table P C (pc - n) xt = None"
by(induct xt)(auto simp add: match_ex_entry split: if_split_asm)

lemma match_ex_table_shift_pc_None:
  "pc  n  match_ex_table P C pc (shift n xt) = None  match_ex_table P C (pc - n) xt = None"
by(simp add: match_ex_table_shift_eq_None_conv)

lemma match_ex_table_shift_eq_Some_conv [simp]:
  "match_ex_table P C pc (shift n xt) = (pc', d) 
   pc  n  pc'  n  match_ex_table P C (pc - n) xt = (pc' - n, d)"
by(induct xt)(auto simp add: match_ex_entry split: if_split_asm)

lemma match_ex_table_shift:
 "match_ex_table P C pc xt = (pc', d)  match_ex_table P C (n + pc) (shift n xt) = (n + pc', d)"
by(simp add: match_ex_table_shift_eq_Some_conv)

lemma match_ex_table_shift_pcD:
  "match_ex_table P C pc (shift n xt) = (pc', d)  pc  n  pc'  n  match_ex_table P C (pc - n) xt = (pc' - n, d)"
by(simp add: match_ex_table_shift_eq_Some_conv)

lemma match_ex_table_pcsD: "match_ex_table P C pc xt = (pc', D)  pc  pcs xt"
by(induct xt)(auto split: if_split_asm simp add: match_ex_entry)


definition stack_xlift :: "nat  ex_table  ex_table"
where "stack_xlift n xt  map (λ(from,to,C,handler,depth). (from, to, C, handler, n + depth)) xt"

lemma stack_xlift_0 [simp]: "stack_xlift 0 xt = xt"
by(induct xt, auto simp add: stack_xlift_def)

lemma stack_xlift_Nil [simp]: "stack_xlift n [] = []"
by(simp add: stack_xlift_def)

lemma stack_xlift_Cons_tuple [simp]:
  "stack_xlift n ((from, to, C, handler, depth) # xt) = (from, to, C, handler, depth + n) # stack_xlift n xt"
by(simp add: stack_xlift_def)

lemma stack_xlift_append [simp]: "stack_xlift n (xt @ xt') = stack_xlift n xt @ stack_xlift n xt'"
by(simp add: stack_xlift_def)

lemma stack_xlift_stack_xlift [simp]: "stack_xlift n (stack_xlift m xt) = stack_xlift (n + m) xt"
by(simp add: stack_xlift_def split_def)

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows stack_xlift_compxE2: "stack_xlift n (compxE2 e pc d) = compxE2 e pc (n + d)"
  and stack_xlift_compxEs2: "stack_xlift n (compxEs2 es pc d) = compxEs2 es pc (n + d)"
by(induct e and es arbitrary: d pc and d pc rule: compE2.induct compEs2.induct)
  (auto simp add: shift_compxE2 simp del: compxE2_size_convs)

lemma compxE2_stack_xlift_convs [simp]: "d > 0  compxE2 e pc d = stack_xlift d (compxE2 e pc 0)"
  and compxEs2_stack_xlift_convs [simp]: "d > 0  compxEs2 es pc d = stack_xlift d (compxEs2 es pc 0)"
by(simp_all add: stack_xlift_compxE2 stack_xlift_compxEs2)

lemma stack_xlift_shift [simp]: "stack_xlift d (shift n xt) = shift n (stack_xlift d xt)"
by(induct xt)(auto)

lemma pcs_stack_xlift_conv [simp]: "pcs (stack_xlift n xt) = pcs xt"
by(auto simp add: pcs_def stack_xlift_def)

lemma match_ex_table_stack_xlift_eq_None_conv [simp]:
  "match_ex_table P C pc (stack_xlift d xt) = None  match_ex_table P C pc xt = None"
by(induct xt)(auto simp add: match_ex_entry)

lemma match_ex_table_stack_xlift_eq_Some_conv [simp]:
  "match_ex_table P C pc (stack_xlift n xt) = (pc', d)  d  n  match_ex_table P C pc xt = (pc', d - n)"
by(induct xt)(auto simp add: match_ex_entry)

lemma match_ex_table_stack_xliftD:
  "match_ex_table P C pc (stack_xlift n xt) = (pc', d)  d  n  match_ex_table P C pc xt = (pc', d - n)"
by(simp)

lemma match_ex_table_stack_xlift:
  "match_ex_table P C pc xt = (pc', d)  match_ex_table P C pc (stack_xlift n xt) = (pc', n + d)"
by simp

lemma pcs_stack_xlift: "pcs (stack_xlift n xt) = pcs xt"
by(auto simp add: stack_xlift_def pcs_def)

lemma match_ex_table_None_append [simp]:
  "match_ex_table P C pc xt = None
   match_ex_table P C pc (xt @ xt') = match_ex_table P C pc xt'"
by(induct xt, auto)

lemma match_ex_table_Some_append [simp]: 
  "match_ex_table P C pc xt = (pc', d)  match_ex_table P C pc (xt @ xt') = (pc', d)"
by(induct xt)(auto)

lemma match_ex_table_append:
  "match_ex_table P C pc (xt @ xt') = (case match_ex_table P C pc xt of None  match_ex_table P C pc xt' 
                                                                  | Some pcd  Some pcd)"
by(auto)

lemma match_ex_table_pc_length_compE2:
  "match_ex_table P a pc (compxE2 e pc' d) = pcd  pc'  pc  pc < length (compE2 e) + pc'"
  
  and match_ex_table_pc_length_compEs2:
  "match_ex_table P a pc (compxEs2 es pc' d) = pcd  pc'  pc  pc < length (compEs2 es) + pc'"
using pcs_subset by(cases pcd, fastforce dest!: match_ex_table_pcsD)+

lemma match_ex_table_compxE2_shift_conv:
  "f > 0  match_ex_table P C pc (compxE2 e f d) = (pc', d')  pc  f  pc'  f  match_ex_table P C (pc - f) (compxE2 e 0 d) = (pc' - f, d')"
by simp

lemma match_ex_table_compxEs2_shift_conv:
  "f > 0  match_ex_table P C pc (compxEs2 es f d) = (pc', d')  pc  f  pc'  f  match_ex_table P C (pc - f) (compxEs2 es 0 d) = (pc' - f, d')"
by(simp add: compxEs2_size_convs)

lemma match_ex_table_compxE2_stack_conv:
  "d > 0  match_ex_table P C pc (compxE2 e 0 d) = (pc', d')  d'  d  match_ex_table P C pc (compxE2 e 0 0) = (pc', d' - d)"
by simp

lemma match_ex_table_compxEs2_stack_conv:
  "d > 0  match_ex_table P C pc (compxEs2 es 0 d) = (pc', d')  d'  d  match_ex_table P C pc (compxEs2 es 0 0) = (pc', d' - d)"
by(simp add: compxEs2_stack_xlift_convs)

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows match_ex_table_compxE2_not_same: "match_ex_table P C pc (compxE2 e n d) = (pc', d')  pc  pc'"
  and match_ex_table_compxEs2_not_same:"match_ex_table P C pc (compxEs2 es n d) = (pc', d')  pc  pc'"
apply(induct e n d and es n d rule: compxE2_compxEs2_induct)
apply(auto simp add: match_ex_table_append match_ex_entry simp del: compxE2_size_convs compxEs2_size_convs compxE2_stack_xlift_convs compxEs2_stack_xlift_convs split: if_split_asm)
done

end