Module SliceScopeExits

Lemmas related to SliceScopeExits.

Require Import Coqlib.
Require Import Errors.
Require Import Registers.
Require Import RTL.
Require Import Maps.

Require Import UtilTacs.
Require Import UtilLemmas.
Require Import RTLPaths.
Require Import SliceScopeExits.
Require Import Scope.
Require Import SliceObs.
Require Import SliceGen.
Require Import SliceObs_proof.

This validator relates scopes and slice nodes, ensuring a necessary property for the semantic preservation of the slicing: exiting a scope not in the slice does not reset the counters of the slicing criterion.

Section SCOPE_EXITS_CHECKER.

  Variable f : function.
  Variable fsc : Scope.family f.
  Variable nc : t_criterion.
  Variable of : obs_function.
  Variable exit_n : node.
  Variable reg_vint : reg.
  Hypothesis FOK : compute_slice ext_slicer f nc fsc exit_n reg_vint = OK of.

  Notation entry := f.(fn_entrypoint).
  Notation succ_node' := (succ_node f).
  Notation exited_scopes' := (exited_scopes fsc).

  Hypothesis SCOPEOK: scope_exits_checker f fsc nc (_slice_nodes of) = true.

  Hypothesis exit_no_succ:
    forall s, ~ succ_node f (_exit of) s.

  Lemma scopes_wf_nc:
    forall pc pc'
      (PC_OUT : ~ In pc (_slice_nodes of))
      (SUCC: succ_node' pc pc'),
      ~ In nc (exited_scopes' pc pc').

Proof.

    intros.
    unfolds in SCOPEOK.
    unfolds in SUCC. destruct SUCC as [i [INST SUCC]].
    eapply Utils.ptree_forall with (i := pc) (x := successors_instr i) in SCOPEOK.
    rewrite orb_true_iff in SCOPEOK.
    destruct SCOPEOK.
    projInv H.
    eapply forallb_forall in H; eauto.
    rewrite forallb_forall in H.
    gen (H nc) as IMP; clear H.
    intro. apply IMP in H.
    apply negb_true_iff in H.
    projInv H.
    case_eq (slice_function f nc fsc exit_n reg_vint); intros.
    destruct p.
    assert (o = of).
      unfolds in H0.
      rewrite FOK in H0.
      monadInv H0. inv EQ; auto.
    subst o.
    exploit crit_in_slice; eauto.
    unfolds in H0.
    rewrite FOK in H0; trim.
    unfold successors.
    rewrite PTree.gmap1.
    unfolds.
    rewrite INST; auto.
  Qed.

End SCOPE_EXITS_CHECKER.

Module SliceScopeExits_proof