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.

Lemma exit_checker_res A (pm: path_map) (pc: node) (v:A) res:
  exit_checker pm pc v = Some res -> v=res.

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.

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.

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.

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.

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.

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.

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.

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.

Lemma function_checker_wellformed_path_map f pm:
  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.

Lemma function_checker_path_entry f pm:
  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).