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(xt⇩1 @ xt⇩2) = pcs xt⇩1 ∪ pcs xt⇩2"
by(simp add:pcs_def)

lemma [simp]: "pc < pc⇩0 ∨ pc⇩0+size(compE2 e) ≤ pc ⟹ pc ∉ pcs(compxE2 e pc⇩0 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]: "pc⇩1 + size(compE2 e) ≤ pc⇩2 ⟹ pcs(compxE2 e pc⇩1 d⇩1) ∩ pcs(compxEs2 es pc⇩2 d⇩2) = {}"
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 xt⇩1. ¬ matches_ex_entry P D pc xte ⟹
  match_ex_table P D pc (xt⇩1 @ xt) = match_ex_table P D pc xt"
by(induct xt⇩1) 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 (xt⇩1 @ xt⇩2) = shift n xt⇩1 @ shift n xt⇩2"
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