Module Inlining

RTL function inlining

Require Import Coqlib Wfsimpl Maps Errors Integers.
Require Import AST Linking.
Require Import Op Registers RTL.

Environment of inlinable functions

We maintain a mapping from function names to their definitions. In this mapping, we only include internal functions that are eligible for inlining, as determined by the external heuristic should_inline.

Definition funenv : Type := PTree.t function.

Definition size_fenv (fenv: funenv) := PTree_Properties.cardinal fenv.

Parameter inlining_info: Type.

Parameter inlining_analysis: program -> inlining_info.

Parameter should_inline: inlining_info -> ident -> function -> bool.

Definition add_globdef (io: inlining_info) (fenv: funenv) (idg: ident * globdef fundef unit) : funenv :=
  match idg with
  | (id, Gfun (Internal f)) =>
      if should_inline io id f
      then PTree.set id f fenv
      else PTree.remove id fenv
  | (id, _) =>
      PTree.remove id fenv
  end.

Definition funenv_program (p: program) : funenv :=
  let io := inlining_analysis p in
  List.fold_left (add_globdef io) p.(prog_defs) (PTree.empty function).

State monad

To construct incrementally the CFG of a function after inlining, we use a state monad similar to that used in module RTLgen. It records the current state of the CFG, plus counters to generate fresh pseudo-registers and fresh CFG nodes. It also records the stack size needed for the inlined function.

Record state : Type := mkstate {
  st_nextreg: positive; (* last used pseudo-register *)
  st_nextnode: positive; (* last used CFG node *)
  st_code: code; (* current CFG *)
  st_stksize: Z (* current stack size *)
}.

Monotone evolution of the state.

Inductive sincr (s1 s2: state) : Prop :=
  Sincr (NEXTREG: Ple s1.(st_nextreg) s2.(st_nextreg))
        (NEXTNODE: Ple s1.(st_nextnode) s2.(st_nextnode))
        (STKSIZE: s1.(st_stksize) <= s2.(st_stksize)).

Remark sincr_refl: forall s, sincr s s.

Proof.

intros; constructor; extlia.
Qed.

Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3.

Proof.

intros. inv H; inv H0. constructor; extlia.
Qed.

Dependently-typed state monad, ensuring that the final state is greater or equal (in the sense of predicate sincr above) than the initial state.

Inductive res {A: Type} {s: state}: Type := R (x: A) (s': state) (I: sincr s s').

Definition mon (A: Type) : Type := forall (s: state), @res A s.

Operations on this monad.

Definition ret {A: Type} (x: A): mon A :=
  fun s => R x s (sincr_refl s).

Definition bind {A B: Type} (x: mon A) (f: A -> mon B): mon B :=
  fun s1 => match x s1 with R vx s2 I1 =>
              match f vx s2 with R vy s3 I2 =>
                R vy s3 (sincr_trans s1 s2 s3 I1 I2)
              end
            end.

Notation "'do' X <- A ; B" := (bind A (fun X => B))
   (at level 200, X ident, A at level 100, B at level 200).

Definition initstate :=
  mkstate 1%positive 1%positive (PTree.empty instruction) 0.

Program Definition set_instr (pc: node) (i: instruction): mon unit :=
  fun s =>
    R tt
      (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize))
      _.

Next Obligation.