Theory StaticControlDependences

section ‹Interpretations of the various static control dependences›

theory StaticControlDependences imports 
  AdditionalLemmas 
  SemanticsWellFormed
begin

lemma WhilePostdomination_aux:
  "Postdomination sourcenode targetnode kind (valid_edge prog) Entry Exit"
proof(unfold_locales)
  fix n assume "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
  hence "valid_node prog n" by(simp add:valid_node_def While_CFG.valid_node_def)
  thus "∃as. prog ⊢ (_Entry_) -as→* n" by(rule valid_node_Entry_path)
next
  fix n assume "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
  hence "valid_node prog n" by(simp add:valid_node_def While_CFG.valid_node_def)
  thus "∃as. prog ⊢ n -as→* (_Exit_)" by(rule valid_node_Exit_path)
qed

interpretation WhilePostdomination: 
  Postdomination sourcenode targetnode kind "valid_edge prog" Entry Exit
by(rule WhilePostdomination_aux)


lemma WhileStrongPostdomination_aux:
  "StrongPostdomination sourcenode targetnode kind (valid_edge prog) Entry Exit"
proof(unfold_locales)
  fix n assume "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
  hence "valid_node prog n" by(simp add:valid_node_def While_CFG.valid_node_def)
  show "finite {n'. ∃a'. valid_edge prog a' ∧ sourcenode a' = n ∧
                         targetnode a' = n'}"
    by(rule finite_successors)
qed

interpretation WhileStrongPostdomination: 
  StrongPostdomination sourcenode targetnode kind "valid_edge prog" Entry Exit
by(rule WhileStrongPostdomination_aux)


subsection ‹Standard Control Dependence›

lemma WStandardControlDependence_aux:
  "StandardControlDependencePDG sourcenode targetnode kind (valid_edge prog)
  Entry (Defs prog) (Uses prog) id Exit"
by(unfold_locales)

interpretation WStandardControlDependence:
  StandardControlDependencePDG sourcenode targetnode kind "valid_edge prog"
                    Entry "Defs prog" "Uses prog" id Exit
  by(rule WStandardControlDependence_aux)


lemma Fundamental_property_scd_aux: "BackwardSlice_wf sourcenode targetnode kind 
  (valid_edge prog) Entry (Defs prog) (Uses prog) id 
  (WStandardControlDependence.PDG_BS_s prog) reds (labels_nodes prog)"
proof -
  interpret BackwardSlice sourcenode targetnode kind "valid_edge prog" Entry
    "Defs prog" "Uses prog" id
    "StandardControlDependencePDG.PDG_BS_s sourcenode targetnode
    (valid_edge prog) (Defs prog) (Uses prog) Exit"
    by(rule WStandardControlDependence.PDGBackwardSliceCorrect)
  show ?thesis by(unfold_locales)
qed

interpretation Fundamental_property_scd: BackwardSlice_wf sourcenode targetnode kind 
  "valid_edge prog" Entry "Defs prog" "Uses prog" id 
  "WStandardControlDependence.PDG_BS_s prog" reds "labels_nodes prog"
  by(rule Fundamental_property_scd_aux)


subsection ‹Weak Control Dependence›

lemma WWeakControlDependence_aux:
  "WeakControlDependencePDG sourcenode targetnode kind (valid_edge prog)
  Entry (Defs prog) (Uses prog) id Exit"
by(unfold_locales)

interpretation WWeakControlDependence:
  WeakControlDependencePDG sourcenode targetnode kind "valid_edge prog"
                    Entry "Defs prog" "Uses prog" id Exit
  by(rule WWeakControlDependence_aux)


lemma Fundamental_property_wcd_aux: "BackwardSlice_wf sourcenode targetnode kind 
  (valid_edge prog) Entry (Defs prog) (Uses prog) id 
  (WWeakControlDependence.PDG_BS_w prog) reds (labels_nodes prog)"
proof -
  interpret BackwardSlice sourcenode targetnode kind "valid_edge prog" Entry
    "Defs prog" "Uses prog" id
    "WeakControlDependencePDG.PDG_BS_w sourcenode targetnode
    (valid_edge prog) (Defs prog) (Uses prog) Exit"
    by(rule WWeakControlDependence.WeakPDGBackwardSliceCorrect)
  show ?thesis by(unfold_locales)
qed

interpretation Fundamental_property_wcd: BackwardSlice_wf sourcenode targetnode kind 
  "valid_edge prog" Entry "Defs prog" "Uses prog" id 
  "WWeakControlDependence.PDG_BS_w prog" reds "labels_nodes prog"
  by(rule Fundamental_property_wcd_aux)


subsection ‹Weak Order Dependence›

lemma Fundamental_property_wod_aux: "BackwardSlice_wf sourcenode targetnode kind 
  (valid_edge prog) Entry (Defs prog) (Uses prog) id 
  (While_CFG_wf.wod_backward_slice prog) reds (labels_nodes prog)"
proof -
  interpret BackwardSlice sourcenode targetnode kind "valid_edge prog" Entry
    "Defs prog" "Uses prog" id
    "CFG_wf.wod_backward_slice sourcenode targetnode (valid_edge prog)
    (Defs prog) (Uses prog)"
    by(rule While_CFG_wf.WODBackwardSliceCorrect)
  show ?thesis by(unfold_locales)
qed

interpretation Fundamental_property_wod: BackwardSlice_wf sourcenode targetnode kind 
  "valid_edge prog" Entry "Defs prog" "Uses prog" id 
  "While_CFG_wf.wod_backward_slice prog" reds "labels_nodes prog"
  by(rule Fundamental_property_wod_aux)

end