Module CfgIterator

Fixpoint checker for the value analysis.

Require Import Coqlib DLib.
Require Import AST.
Require Import Op.
Require Import Registers Maps.
Require Import BinPos.
Require Import LatticeSignatures.

Local Notation node := positive.

external iterator written in OCaml, linked with ExternCfgIterator.iterator during extraction
Parameter extern_iterator : forall {A:Type} {instruction:Type},
  (A -> A -> bool) ->
  (A -> A -> A) ->
  (A -> A -> A) ->
  A ->
  A ->
  (node -> instruction -> list (node* (A -> A))) ->
  node ->
  PTree.t instruction ->
  A ->
  PMap.t A.

Module BourdoncleIterator.

Section lat.
Context {t0 B instruction: Type}.
Definition t := t0+⊥.
Variable ab : adom t B.

Definition get_extern_fixpoint
  (entrypoint:node) (code:PTree.t instruction)
  (transfer:node -> instruction -> list (node* (t -> t)))
  (init:t) : PMap.t t :=
  extern_iterator leb join widen top (bot ab) transfer entrypoint code init.

Definition check_fxp
  (entrypoint:node) (code:PTree.t instruction)
  (transfer:node -> instruction -> list (node* (t -> t)))
  (fxp:PMap.t t) : bool :=
  init ⊑ (PMap.get entrypoint fxp)
    && ptree_forall code
    (fun n ins =>
      let ab := PMap.get n fxp in
      (fun x:(node*(t->t)) =>
        let (n',tf) := x in
          (tf ab) ⊑ (PMap.get n' fxp))
      (transfer n ins)).

Definition get_fxp (fxp:PMap.t t) (n:node) : t := fxp!!n.

Definition top_solve_pfp (n:node) := ⊤.

Definition solve_pfp
  (entrypoint:node) (code:PTree.t instruction)
  (transfer:node -> instruction -> list (node* (t -> t)))
  (init:t) : node -> t :=
  let fxp := get_extern_fixpoint entrypoint code transfer init in
    if check_fxp entrypoint code transfer init fxp
      then get_fxp fxp
      else top_solve_pfp.

Lemma solve_pfp_entrypoint: forall entrypoint code transfer init,
  γ init ⊆ γ (solve_pfp entrypoint code transfer init entrypoint).
  unfold solve_pfp, check_fxp, get_fxp; intros entrypoint code transfer init x.
  case_eq (leb init (get_extern_fixpoint entrypoint code transfer init) # entrypoint);
    simpl; intros; eauto.
  destruct_bool_in_goal; simpl; eauto.
  eapply (gamma_top); eauto.
  eapply (gamma_top); eauto.

Lemma solve_pfp_postfixpoint: forall entrypoint code transfer init pc1 ins,
  code!pc1 = Some ins -> forall pc2 tf,
  In (pc2,tf) (transfer pc1 ins) ->
  γ (tf (solve_pfp entrypoint code transfer init pc1)) ⊆ γ (solve_pfp entrypoint code transfer init pc2).
  unfold solve_pfp, check_fxp; intros.
  destruct (leb init (get_extern_fixpoint entrypoint code transfer init) # entrypoint);
    simpl in *; intros; auto.
  case_eq_bool_in_goal; simpl; intros; auto.
  rewrite H2 in H1.
  rewrite ptree_forall_correct in H2.
  exploit H2; eauto; clear H2; simpl; intros.
  rewrite forallb_forall in H2.
  unfold get_fxp.
  exploit H2; eauto; simpl; intros.
  eapply gamma_monotone; eauto.
  eapply (gamma_top); eauto.
  eapply (gamma_top); eauto.

End lat.
End BourdoncleIterator.