Module InliningCFG

RTL function inlining

Require Import Coqlib.
Require Import Wfsimpl.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Op.
Require Import Cminor.
Require Import CFG.

Ltac xomega := unfold Plt, Ple in *; zify; omega.

Environment of inlinable functions

We maintain a mapping from function names to their definitions. In this mapping, we only include 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 should_inline: ident -> function -> bool.

Definition add_fundef (fenv: funenv) (idf: ident * fundef) : funenv :=
  match idf with
  | (id, External ef) =>
      PTree.remove id fenv
  | (id, Internal f) =>
      if should_inline id f
      then PTree.set id f fenv
      else PTree.remove id fenv
  end.

Definition remove_vardef (fenv: funenv) (idv: ident * globvar unit) : funenv :=
  PTree.remove (fst idv) fenv.

Definition funenv_program (p: program) : funenv :=
  List.fold_left remove_vardef p.(prog_vars)
    (List.fold_left add_fundef p.(prog_funct) (PTree.empty function)).

Resources used by a function.

Maximum PC (node number) in the CFG of a function. All nodes of the CFG of f are between 1 and max_pc_function f (inclusive).

Definition max_pc_function (f: function) :=
  PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive.

Fixpoint max_id_expr e : positive :=
  match e with
    | Evar id => id
    | Econst _ => 1%positive
    | Eunop unop e => max_id_expr e
    | Ebinop binop e1 e2 => Pmax (max_id_expr e1) (max_id_expr e2)
    | Eload chunk addr => max_id_expr addr
    | Econdition cond e1 e2 => Pmax (max_id_expr cond) (Pmax (max_id_expr e1) (max_id_expr e2))
  end.

Definition max_id_exprs es : positive :=
  List.fold_left (fun m0 e => Pmax m0 (max_id_expr e)) es 1%positive.

Definition max_id_instr (i: instruction) :=
  match i with
  | Iskip s => 1%positive
  | Iassign id a s => Pmax id (max_id_expr a)
  | Istore chunk addr res s =>
    Pmax (max_id_expr addr) (max_id_expr res)
  | Icall optres sig fn args s =>
    let m := Pmax (max_id_expr fn) (max_id_exprs args) in
    match optres with
      | None => m
      | Some res => Pmax m res
    end
  | Itailcall sig fn args =>
    Pmax (max_id_expr fn) (max_id_exprs args)
  | Ibuiltin optres ef args s =>
    let m := max_id_exprs args in
    match optres with
      | None => m
      | Some res => Pmax m res
    end
  | Iifthenelse cond ifso ifnot =>
    max_id_expr cond
  | Iswitch a cases default =>
    max_id_expr a
  | Ireturn optres =>
    match optres with
      | None => 1%positive
      | Some res => max_id_expr res
    end
  end.

Definition max_def_instr (i: instruction) :=
  match i with
  | Iassign id a s => id
  | Istore chunk addr res s => match res with
                                   | Evar id => id
                                   | _ => 1%positive
                               end
  | Icall optres sig fn args s =>
    match optres with
      | None => 1%positive
      | Some res => res
    end
  | Ibuiltin optres ef args s =>
    match optres with
      | None => 1%positive
      | Some res => res
    end
  | _ => 1%positive
  end.

Maximum ident used in a function. All results of an instruction of f, as well as all parameters of f, are between 1 and max_def_function (inclusive).

Definition max_id_function (f : function) :=
  let max_params := List.fold_left (fun m r => Pmax m r) f.(fn_params) 1%positive in
  let max_vars := List.fold_left (fun m r => Pmax m r) f.(fn_vars) 1%positive in
  Pmax
    (PTree.fold (fun m pc i => Pmax m (max_id_instr i)) f.(fn_code) 1%positive)
    (Pmax max_params max_vars).

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_nextid: positive; (* last used ident *)
  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 (NEXTID: Ple s1.(st_nextid) s2.(st_nextid))
        (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; xomega.
Qed.

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

Proof.

intros. inv H; inv H0. constructor; xomega.
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_nextid) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize))
      _.

Next Obligation.