Theory Dom_Kildall

section ‹A kildall's algorithm for computing dominators›

theory Dom_Kildall
imports Dom_Semi_List  "HOL-Library.While_Combinator" "Jinja.SemilatAlg" 
begin

text ‹A kildall's algorithm for computing dominators. 
      It uses the ideas and the framework of kildall's algorithm implemented in Jinja \<^cite>‹"Kildall-AFP"›,
      and modifications are needed to make it work for a fast algorithm for computing dominators›

type_synonym state_dom = "nat list "

primrec  propa :: 
  "'s binop ⇒ (nat × 's) list ⇒ 's list ⇒ nat list ⇒ 's list * nat list"
where
  "propa f []      τs wl = (τs,wl)"
| "propa f (q'# qs) τs wl = (let (q,τ) = q';
                             u =  (τ ⊔⇘f⇙ τs!q);
                             wl' = (if u = τs!q then wl 
                                    else (insort q (remove1 q wl)))
                         in propa f qs (τs[q := u]) wl')"

definition  iter :: 
  "'s binop ⇒ 's step_type ⇒ 's list ⇒ nat list ⇒ 's list × nat list"
where
  "iter f step τs w =
   while (λ(τs,w). w ≠ [])
         (λ(τs,w). let p = hd w
                   in propa f (step p (τs!p)) τs (tl w))
         (τs,w)"

definition unstables :: "state_dom ord ⇒  state_dom step_type ⇒ state_dom list ⇒ nat list"
where
  "unstables r step τs = sorted_list_of_set  {p. p < size τs ∧ ¬ stable r step τs p}"

definition  kildall :: "state_dom ord ⇒state_dom binop  ⇒ state_dom step_type ⇒ state_dom list ⇒ state_dom list" where
  "kildall r f step τs = fst(iter f step τs (unstables r step τs))"

lemma init_worklist_is_sorted: "sorted (unstables r step τs)"
  by (simp add:sorted_less_sorted_list_of_set unstables_def)


context cfg_doms

begin

definition transf :: "node ⇒ state_dom ⇒ state_dom " where 
"transf n input ≡  (n # input)"

definition exec :: "node ⇒ state_dom ⇒ (node × state_dom) list"
  where "exec n xs = map (λpc. (pc, (transf n xs))) (rev (sorted_list_of_set(succs n)))"

lemma transf_res_is_rev: "sorted (rev ns) ⟹ n > hd ns  ⟹ sorted (rev ((transf n ( ns))))"
  by (induct ns) (auto simp add:transf_def sorted_wrt_append) 

abbreviation "start ≡  [] # (replicate (length (g_V G) - 1) ( (rev[0..<length(g_V G)])))"

definition dom_kildall :: "state_dom list ⇒ state_dom list"
  where "dom_kildall = kildall (fst (snd nodes_semi)) (snd (snd nodes_semi)) exec"

definition dom:: "nat ⇒ nat ⇒ bool" where
"dom i j ≡(let res = (dom_kildall start) !j in i ∈ (set res) ∨ i = j )"

lemma dom_refl: "dom i i" 
  by (unfold dom_def) simp

definition strict_dom :: "nat ⇒ nat ⇒ bool" where
"strict_dom i j ≡ (let res = (dom_kildall start) !j in  i ∈ set res)"


lemma strict_domI1: "(dom_kildall ([] # (replicate (length (g_V G) - 1) ( (rev[0..<length(g_V G)])))))!j =  res ⟹ i ∈ set res ⟹ strict_dom i j" 
  by (auto simp add:strict_dom_def )

lemma strict_domD: 
  "strict_dom i j ⟹ 
  dom_kildall (( [] # (replicate (length (g_V G) - 1) ( (rev[0..<length(g_V G)])))))!j  =  a ⟹ 
  i ∈ set a"  
  by (auto simp add:strict_dom_def )

lemma sdom_dom: "strict_dom i j ⟹ dom i j"  
  by (unfold strict_dom_def) (auto simp add:dom_def)

lemma not_sdom_not_dom: "¬strict_dom i j ⟹ i ≠ j ⟹ ¬dom i j"  
  by (unfold strict_dom_def) (auto simp add:dom_def)

lemma dom_sdom: "dom i j ⟹ i ≠ j ⟹ strict_dom i j" 
  by (unfold dom_def)  (auto simp add:dom_def strict_dom_def)

end


end