Module Kildall

Require Import Coqlib.
Require Import Iteration.
Require Import Maps.
Require Import Lattice.
Require Import Kildall.
Require Import KildallComp.

Module Backward_Dataflow_Solver (LAT: SEMILATTICE) (NS: NODE_SET)<:
BACKWARD_DATAFLOW_SOLVER with Module L := LAT.

Module L := LAT.

Module DS := Dataflow_Solver L NS.

Section Kildall.

Context {A: Type}.
Variable code: PTree.t A.
Variable successors: A -> list positive.
Variable transf: positive -> L.t -> L.t.

Finding entry points for the reverse control-flow graph.

Section Exit_points.

Assuming that the nodes of the CFG code are numbered in reverse postorder (cf. pass Renumber), an edge from n to s is a normal edge if s < n and a back-edge otherwise. sequential_node returns true if the given node has at least one normal outgoing edge. It returns false if the given node is an exit node (no outgoing edges) or the final node of a loop body (all outgoing edges are back-edges). As we prove later, the set of all non-sequential node is an appropriate set of entry points for exploring the reverse CFG.

Definition sequential_node (pc: positive) (instr: A): bool :=
  existsb (fun s => match code!s with None => false | Some _ => plt s pc end)
          (successors instr).

Definition exit_points : NS.t :=
  PTree.fold
    (fun ep pc instr =>
       if sequential_node pc instr
       then ep
       else NS.add pc ep)
    code NS.empty.

Lemma exit_points_charact:
  forall n,
  NS.In n exit_points <-> exists i, code!n = Some i /\ sequential_node n i = false.

Proof.

  intros n. unfold exit_points. eapply PTree_Properties.fold_rec.
- (* extensionality *)
  intros. rewrite <- H. auto.
- (* base case *)
  simpl. split; intros.
  eelim NS.empty_spec; eauto.
  destruct H as [i [P Q]]. rewrite PTree.gempty in P. congruence.
- (* inductive case *)
  intros. destruct (sequential_node k v) eqn:SN.
  + rewrite H1. rewrite PTree.gsspec. destruct (peq n k).
    subst. split; intros [i [P Q]]. congruence. inv P. congruence.
    tauto.
  + rewrite NS.add_spec. rewrite H1. rewrite PTree.gsspec. destruct (peq n k).
    subst. split. intros. exists v; auto. auto.
    split. intros [P | [i [P Q]]]. congruence. exists i; auto.
    intros [i [P Q]]. right; exists i; auto.
Qed.

Lemma reachable_exit_points:
forall pc i,
code!pc = Some i -> exists x, NS.In x exit_points /\ reachable code successors pc x.

Proof.

  intros pc0. pattern pc0. apply (well_founded_ind Plt_wf).
  intros pc HR i CODE.
  destruct (sequential_node pc i) eqn:SN.
- (* at least one successor that decreases the pc *)
  unfold sequential_node in SN. rewrite existsb_exists in SN.
  destruct SN as [s [P Q]]. destruct (code!s) as [i'|] eqn:CS; try discriminate. InvBooleans.
  exploit (HR s); eauto. intros [x [U V]].
  exists x; split; auto. eapply reachable_left; eauto.
- (* otherwise we are an exit point *)
  exists pc; split.
  rewrite exit_points_charact. exists i; auto. constructor.
Qed.

The crucial property of exit points is that any nonempty node in the CFG is reverse-reachable from an exit point.

Lemma reachable_exit_points_predecessor:
  forall pc i,
  code!pc = Some i ->
  exists x, NS.In x exit_points /\ reachable (make_predecessors code successors) (fun l => l) x pc.

Proof.

intros. exploit reachable_exit_points; eauto. intros [x [P Q]].
exists x; split; auto. apply reachable_predecessors. auto.
Qed.

End Exit_points.

The efficient backward solver.

Definition fixpoint :=
  DS.fixpoint_nodeset
    (make_predecessors code successors) (fun l => l)
    transf exit_points.

Theorem fixpoint_solution:
  forall res n instr s,
  fixpoint = Some res ->
  code!n = Some instr -> In s (successors instr) ->
  (forall n a, code!n = None -> L.eq (transf n a) L.bot) ->
  L.ge res!!n (transf s res!!s).

Proof.

  intros.
  exploit (make_predecessors_correct_2 code); eauto. intros [l [P Q]].
  destruct code!s as [instr'|] eqn:CS.
- exploit reachable_exit_points_predecessor. eexact CS. intros (ep & U & V).
  unfold fixpoint in H. eapply DS.fixpoint_nodeset_solution; eauto.
- apply L.ge_trans with L.bot. apply L.ge_bot.
  apply L.ge_refl. apply L.eq_sym. auto.
Qed.

The alternate solver that starts with all nodes of the CFG instead of just the exit points.

Definition fixpoint_allnodes :=
  DS.fixpoint_allnodes
    (make_predecessors code successors) (fun l => l)
    transf.

Theorem fixpoint_allnodes_solution:
  forall res n instr s,
  fixpoint_allnodes = Some res ->
  code!n = Some instr -> In s (successors instr) ->
  L.ge res!!n (transf s res!!s).

Proof.

  intros.
  exploit (make_predecessors_correct_2 code); eauto. intros [l [P Q]].
  unfold fixpoint_allnodes in H.
  eapply DS.fixpoint_allnodes_solution; eauto.
Qed.

Lemma propagate_succ_no_succ : forall s out n pc,
pc <> n ->
(DS.propagate_succ s out n).(DS.aval) ! pc = s.(DS.aval) ! pc.

Proof.

  intros. unfold DS.propagate_succ. destruct (s.(DS.aval) ! n) eqn:HH.
  - destruct (DS.L.beq t (DS.L.lub t out)).
    + reflexivity.
    + simpl. rewrite PTree.gso; congruence.
  - simpl. rewrite PTree.gso; congruence.
Qed.

Lemma propagate_succ_list_no_succ : forall s out l pc,
~ In pc l ->
(DS.propagate_succ_list s out l).(DS.aval) ! pc = s.(DS.aval) ! pc.

Proof.

  intros s out l. revert s. induction l; intros.
  - simpl. reflexivity.
  - simpl. rewrite IHl. apply propagate_succ_no_succ.
    intros contra. apply H. left. congruence.
    intros contra. apply H. right. assumption.
Qed.

Theorem fixpoint_no_succ : forall res pc i,
  fixpoint = Some res ->
  code ! pc = Some i ->
  successors i = nil ->
  L.eq res!!pc L.bot.

Proof.

  intros. unfold fixpoint in H. unfold DS.fixpoint_nodeset in H.
  unfold DS.fixpoint_from in H.
  pose proof (PrimIter.iterate_prop _ _ (DS.step (make_predecessors code successors) (fun l : list positive => l) transf)
    (fun s => forall pc i, code ! pc = Some i -> successors i = nil -> s.(DS.aval) ! pc = None)
     (fun res => forall pc i, code ! pc = Some i -> successors i = nil -> L.eq res !! pc L.bot)) as Hp.

     eapply Hp; clear Hp.
     2:eassumption.
     3-4:eassumption.
     intros.
     { unfold DS.step.
     destruct (NS.pick (DS.worklist a)) as [(n0, rem)|] eqn:HH.
     - destruct ((make_predecessors code successors) ! n0) eqn:HH0.
       + intros. assert (~ List.In pc0 l).
         { intros contra.
           exploit @make_predecessors_correct2; eauto.
           unfold successors_list. unfold make_preds. rewrite HH0.
           assumption. rewrite H4. contradiction.
         }
         rewrite propagate_succ_list_no_succ by assumption.
         eauto.
       + simpl. eauto.
     - intros. unfold "!!". simpl. erewrite H2; try eassumption. apply L.eq_refl.
     }
     intros. simpl. apply PTree.gempty.
Qed.

Theorem fixpoint_some : forall res pc,
  fixpoint = Some res ->
  code ! pc = None ->
  L.eq res!!pc L.bot.

Proof.

  intros. unfold fixpoint, DS.fixpoint_nodeset, DS.fixpoint_from in H.
  pose proof (PrimIter.iterate_prop _ _ (DS.step (make_predecessors code successors) (fun l => l) transf)
    (fun s => forall pc, code ! pc = None -> s.(DS.aval) ! pc = None)
    (fun res => forall pc, code ! pc = None -> L.eq res!!pc L.bot)) as Hp.

  eapply Hp; clear Hp.
  2:eassumption.
  3-4:eassumption.
  intros.
  { unfold DS.step.
   destruct (NS.pick (DS.worklist a)) as [(n0, rem)|] eqn:HH.
   - destruct ((make_predecessors code successors) ! n0) eqn:HH0.
     + intros. assert (~ List.In pc0 l).
       { intros contra.
         eapply make_predecessors_some in contra; eauto.
         destruct contra as (i & contra). congruence.
       }
       rewrite propagate_succ_list_no_succ by assumption.
       eauto.
     + simpl. eauto.
   - intros. unfold "!!". simpl. erewrite H1; try eassumption. apply L.eq_refl.
   }
   intros. simpl. apply PTree.gempty.
Qed.

End Kildall.

End Backward_Dataflow_Solver.

Module Kildall_v2