From a8fc4625c2c172484341b9105c1aa8ea1c6a49f3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 17 Aug 2009 15:28:52 +0000 Subject: Refactoring of Constprop and Constpropproof into a machine-dependent part and a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constprop.v | 235 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 235 insertions(+) create mode 100644 backend/Constprop.v (limited to 'backend/Constprop.v') diff --git a/backend/Constprop.v b/backend/Constprop.v new file mode 100644 index 00000000..cccce9a3 --- /dev/null +++ b/backend/Constprop.v @@ -0,0 +1,235 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Constant propagation over RTL. This is one of the optimizations + performed at RTL level. It proceeds by a standard dataflow analysis + and the corresponding code rewriting. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Globalenvs. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Lattice. +Require Import Kildall. +Require Import ConstpropOp. + +(** * Static analysis *) + +(** The type [approx] of compile-time approximations of values is + defined in the machine-dependent part [ConstpropOp]. *) + +(** We equip this type of approximations with a semi-lattice structure. + The ordering is inclusion between the sets of values denoted by + the approximations. *) + +Module Approx <: SEMILATTICE_WITH_TOP. + Definition t := approx. + Definition eq (x y: t) := (x = y). + Definition eq_refl: forall x, eq x x := (@refl_equal t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}. + Proof. + decide equality. + apply Int.eq_dec. + apply Float.eq_dec. + apply Int.eq_dec. + apply ident_eq. + Qed. + Definition beq (x y: t) := if eq_dec x y then true else false. + Lemma beq_correct: forall x y, beq x y = true -> x = y. + Proof. + unfold beq; intros. destruct (eq_dec x y). auto. congruence. + Qed. + Definition ge (x y: t) : Prop := + x = Unknown \/ y = Novalue \/ x = y. + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge; tauto. + Qed. + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge; intuition congruence. + Qed. + Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. + Proof. + unfold eq, ge; intros; congruence. + Qed. + Definition bot := Novalue. + Definition top := Unknown. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot; tauto. + Qed. + Lemma ge_top: forall x, ge top x. + Proof. + unfold ge, bot; tauto. + Qed. + Definition lub (x y: t) : t := + if eq_dec x y then x else + match x, y with + | Novalue, _ => y + | _, Novalue => x + | _, _ => Unknown + end. + Lemma lub_commut: forall x y, eq (lub x y) (lub y x). + Proof. + unfold lub, eq; intros. + case (eq_dec x y); case (eq_dec y x); intros; try congruence. + destruct x; destruct y; auto. + Qed. + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold lub; intros. + case (eq_dec x y); intro. + apply ge_refl. apply eq_refl. + destruct x; destruct y; unfold ge; tauto. + Qed. +End Approx. + +Module D := LPMap Approx. + +(** The transfer function for the dataflow analysis is straightforward: + for [Iop] instructions, we set the approximation of the destination + register to the result of executing abstractly the operation; + for [Iload] and [Icall], we set the approximation of the destination + to [Unknown]. *) + +Definition approx_reg (app: D.t) (r: reg) := + D.get r app. + +Definition approx_regs (app: D.t) (rl: list reg):= + List.map (approx_reg app) rl. + +Definition transfer (f: function) (pc: node) (before: D.t) := + match f.(fn_code)!pc with + | None => before + | Some i => + match i with + | Inop s => + before + | Iop op args res s => + let a := eval_static_operation op (approx_regs before args) in + D.set res a before + | Iload chunk addr args dst s => + D.set dst Unknown before + | Istore chunk addr args src s => + before + | Icall sig ros args res s => + D.set res Unknown before + | Itailcall sig ros args => + before +(* + | Ialloc arg res s => + D.set res Unknown before +*) + | Icond cond args ifso ifnot => + before + | Ireturn optarg => + before + end + end. + +(** The static analysis itself is then an instantiation of Kildall's + generic solver for forward dataflow inequations. [analyze f] + returns a mapping from program points to mappings of pseudo-registers + to approximations. It can fail to reach a fixpoint in a reasonable + number of iterations, in which case [None] is returned. *) + +Module DS := Dataflow_Solver(D)(NodeSetForward). + +Definition analyze (f: RTL.function): PMap.t D.t := + match DS.fixpoint (successors f) (transfer f) + ((f.(fn_entrypoint), D.top) :: nil) with + | None => PMap.init D.top + | Some res => res + end. + +(** * Code transformation *) + +(** The code transformation proceeds instruction by instruction. + Operators whose arguments are all statically known are turned + into ``load integer constant'', ``load float constant'' or + ``load symbol address'' operations. Operators for which some + but not all arguments are known are subject to strength reduction, + and similarly for the addressing modes of load and store instructions. + Other instructions are unchanged. *) + +Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident := + match ros with + | inl r => + match D.get r app with + | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros + | _ => ros + end + | inr s => ros + end. + +Definition transf_instr (app: D.t) (instr: instruction) := + match instr with + | Iop op args res s => + match eval_static_operation op (approx_regs app args) with + | I n => + Iop (Ointconst n) nil res s + | F n => + Iop (Ofloatconst n) nil res s + | S symb ofs => + Iop (Oaddrsymbol symb ofs) nil res s + | _ => + let (op', args') := op_strength_reduction (approx_reg app) op args in + Iop op' args' res s + end + | Iload chunk addr args dst s => + let (addr', args') := addr_strength_reduction (approx_reg app) addr args in + Iload chunk addr' args' dst s + | Istore chunk addr args src s => + let (addr', args') := addr_strength_reduction (approx_reg app) addr args in + Istore chunk addr' args' src s + | Icall sig ros args res s => + Icall sig (transf_ros app ros) args res s + | Itailcall sig ros args => + Itailcall sig (transf_ros app ros) args + | Icond cond args s1 s2 => + match eval_static_condition cond (approx_regs app args) with + | Some b => + if b then Inop s1 else Inop s2 + | None => + let (cond', args') := cond_strength_reduction (approx_reg app) cond args in + Icond cond' args' s1 s2 + end + | _ => + instr + end. + +Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code := + PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs. + +Definition transf_function (f: function) : function := + let approxs := analyze f in + mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + (transf_code approxs f.(fn_code)) + f.(fn_entrypoint). + +Definition transf_fundef (fd: fundef) : fundef := + AST.transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. -- cgit