Module RTLpathWFcheck

Require Import Coqlib.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import Globalenvs Smallstep RTL RTLpath.
Require Import Bool Errors.
Require Import Program.
Require RTLpathLivegen.

Local Open Scope lazy_bool_scope.

Local Open Scope option_monad_scope.

Definition exit_checker {A} (pm: path_map) (pc: node) (v:A): option A :=
   SOME path <- pm!pc IN
   Some v.

Lemma exit_checker_path_entry A (pm: path_map) (pc: node) (v:A) res:
  exit_checker pm pc v = Some res -> path_entry pm pc.
Proof.
  unfold exit_checker, path_entry.
  inversion_SOME path; simpl; congruence.
Qed.

Lemma exit_checker_res A (pm: path_map) (pc: node) (v:A) res:
  exit_checker pm pc v = Some res -> v=res.
Proof.
  unfold exit_checker, path_entry.
  inversion_SOME path; try_simplify_someHyps.
Qed.

Definition iinst_checker (pm: path_map) (i: instruction): option (node) :=
  match i with
  | Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc'
  | Istore _ _ _ _ pc' => Some (pc')
  | Icond cond args ifso ifnot _ =>
      exit_checker pm ifso ifnot
  | _ => None
  end.

Local Hint Resolve exit_checker_path_entry: core.

Lemma iinst_checker_path_entry (pm: path_map) (i: instruction) res pc:
  iinst_checker pm i = Some res ->
  early_exit i = Some pc -> path_entry pm pc.
Proof.
  destruct i; simpl; try_simplify_someHyps; subst.
Qed.

Lemma iinst_checker_default_succ (pm: path_map) (i: instruction) res pc:
  iinst_checker pm i = Some res ->
  pc = res ->
  default_succ i = Some pc.
Proof.
  destruct i; simpl; try_simplify_someHyps; subst;
  repeat (inversion_ASSERT); try_simplify_someHyps.
  intros; exploit exit_checker_res; eauto.
  intros; subst. simpl; auto.
Qed.

Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (pc:node): option (node) :=
  match ps with
  | O => Some (pc)
  | S p =>
    SOME i <- f.(fn_code)!pc IN
    SOME res <- iinst_checker pm i IN
    ipath_checker p f pm res
  end.

Lemma ipath_checker_wellformed f pm ps: forall pc res,
   ipath_checker ps f pm pc = Some res ->
   wellformed_path f.(fn_code) pm 0 res ->
   wellformed_path f.(fn_code) pm ps pc.
Proof.
  induction ps; simpl; try_simplify_someHyps.
  inversion_SOME i; inversion_SOME res'.
  intros. eapply wf_internal_node; eauto.
  * eapply iinst_checker_default_succ; eauto.
  * intros; eapply iinst_checker_path_entry; eauto.
Qed.

Fixpoint exit_list_checker (pm: path_map) (l: list node): bool :=
   match l with
   | nil => true
   | pc::l' => exit_checker pm pc tt &&& exit_list_checker pm l'
   end.

Lemma exit_list_checker_correct pm l pc:
  exit_list_checker pm l = true -> List.In pc l -> exit_checker pm pc tt = Some tt.
Proof.
  intros EXIT PC; induction l; intuition.
  simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT.
  firstorder (subst; eauto).
Qed.

Local Hint Resolve exit_list_checker_correct: core.

Definition inst_checker (pm: path_map) (i: instruction): option unit :=
   match i with
   | Icall sig ros args res pc' =>
      exit_checker pm pc' tt
   | Itailcall sig ros args =>
      Some tt
   | Ibuiltin ef args res pc' =>
      exit_checker pm pc' tt
   | Ijumptable arg tbl =>
      ASSERT exit_list_checker pm tbl IN
      Some tt
   | Ireturn optarg =>
      Some tt
   | _ =>
      SOME res <- iinst_checker pm i IN
      exit_checker pm res tt
   end.

Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (i: instruction):
  inst_checker pm i = Some tt ->
  c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
  intros CHECK PC. eapply wf_last_node; eauto.
  clear c pc PC. intros pc PC.
  destruct i; simpl in * |- *; intuition (subst; eauto);
  try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
  intros X; exploit exit_checker_res; eauto.
  clear X. intros; subst; eauto.
Qed.

Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
   SOME res <- ipath_checker (path.(psize)) f pm pc IN
   SOME i <- f.(fn_code)!res IN
   inst_checker pm i.

Lemma path_checker_wellformed f pm pc path:
   path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
Proof.
  unfold path_checker.
  inversion_SOME res.
  inversion_SOME i.
  intros; eapply ipath_checker_wellformed; eauto.
  eapply inst_checker_wellformed; eauto.
Qed.

Fixpoint list_path_checker f pm (l:list (node*path_info)): bool :=
  match l with
  | nil => true
  | (pc, path)::l' =>
      path_checker f pm pc path &&& list_path_checker f pm l'
  end.

Lemma list_path_checker_correct f pm l:
  list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.
Proof.
  intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
  simpl in * |- *. rewrite RTLpathLivegen.lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.

Definition function_checker (f: RTL.function) (pm: path_map): bool :=
  pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm).

Lemma function_checker_correct f pm pc path:
  function_checker f pm = true ->
  pm!pc = Some path ->
  path_checker f pm pc path = Some tt.
Proof.
  unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true.
  intros (ENTRY & PATH) PC.
  exploit list_path_checker_correct; eauto.
  - eapply PTree.elements_correct; eauto.
  - simpl; auto.
Qed.

Lemma function_checker_wellformed_path_map f pm:
  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
Proof.
  unfold wellformed_path_map.
  intros; eapply path_checker_wellformed; eauto.
  intros; eapply function_checker_correct; eauto.
Qed.

Lemma function_checker_path_entry f pm:
  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
Proof.
  unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true;
  unfold path_entry. firstorder congruence.
Qed.