From 0e76ac320601a81a67c700759526d0f8b7a8ed7b Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 23 Feb 2012 14:00:06 +0000 Subject: More aggressive common subexpression elimination (CSE) of memory loads. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CSE.v | 104 ++++++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 69 insertions(+), 35 deletions(-) (limited to 'backend/CSE.v') diff --git a/backend/CSE.v b/backend/CSE.v index 44ed5908..ba8dec8b 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -15,6 +15,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. @@ -24,6 +25,7 @@ Require Import Globalenvs. Require Import Op. Require Import Registers. Require Import RTL. +Require Import RTLtyping. Require Import Kildall. (** * Value numbering *) @@ -188,26 +190,57 @@ Definition add_unknown (n: numbering) (rd: reg) := n.(num_eqs) (PTree.set rd n.(num_next) n.(num_reg)). -(** [kill_load n] removes all equations involving memory loads, - as well as those involving memory-dependent operators. - It is used to reflect the effect of a memory store, which can - potentially invalidate all such equations. *) +(** [kill_equations pred n] remove all equations satisfying predicate [pred]. *) -Fixpoint kill_load_eqs (eqs: list (valnum * rhs)) : list (valnum * rhs) := +Fixpoint kill_eqs (pred: rhs -> bool) (eqs: list (valnum * rhs)) : list (valnum * rhs) := match eqs with | nil => nil - | eq :: rem => - match eq with - | (_, Op op _) => if op_depends_on_memory op then kill_load_eqs rem else eq :: kill_load_eqs rem - | (_, Load _ _ _) => kill_load_eqs rem - end + | eq :: rem => if pred (snd eq) then kill_eqs pred rem else eq :: kill_eqs pred rem end. -Definition kill_loads (n: numbering) : numbering := +Definition kill_equations (pred: rhs -> bool) (n: numbering) : numbering := mknumbering n.(num_next) - (kill_load_eqs n.(num_eqs)) + (kill_eqs pred n.(num_eqs)) n.(num_reg). +(** [kill_loads n] removes all equations involving memory loads, + as well as those involving memory-dependent operators. + It is used to reflect the effect of a builtin operation, which can + change memory in unpredictable ways and potentially invalidate all such equations. *) + +Definition filter_loads (r: rhs) : bool := + match r with + | Op op _ => op_depends_on_memory op + | Load _ _ _ => true + end. + +Definition kill_loads (n: numbering) : numbering := + kill_equations filter_loads n. + +(** [add_store n chunk addr rargs rsrc] updates the numbering [n] to reflect + the effect of a store instruction [Istore chunk addr rargs rsrc]. + Equations involving the memory state are removed from [n], unless we + can prove that the store does not invalidate them. + Then, an equations [rsrc = Load chunk addr rargs] is added to reflect + the known content of the stored memory area, but only if [chunk] is + a "full-size" quantity ([Mint32] or [Mfloat64]). *) + +Definition filter_after_store (chunk: memory_chunk) (addr: addressing) (vl: list valnum) (r: rhs) : bool := + match r with + | Op op vl' => op_depends_on_memory op + | Load chunk' addr' vl' => + negb(eq_list_valnum vl vl' && addressing_separated chunk addr chunk' addr') + end. + +Definition add_store (n: numbering) (chunk: memory_chunk) (addr: addressing) + (rargs: list reg) (rsrc: reg) : numbering := + let (n1, vargs) := valnum_regs n rargs in + let n2 := kill_equations (filter_after_store chunk addr vargs) n1 in + match chunk with + | Mint32 | Mfloat64 => add_rhs n2 rsrc (Load chunk addr vargs) + | _ => n2 + end. + (* [reg_valnum n vn] returns a register that is mapped to value number [vn], or [None] if no such register exists. *) @@ -339,7 +372,7 @@ Definition transfer (f: function) (pc: node) (before: numbering) := | Iload chunk addr args dst s => add_load before dst chunk addr args | Istore chunk addr args src s => - kill_loads before + add_store before chunk addr args src | Icall sig ros args res s => empty_numbering | Itailcall sig ros args => @@ -358,16 +391,10 @@ Definition transfer (f: function) (pc: node) (before: numbering) := (** The static analysis solves the dataflow inequations implied by the [transfer] function using the ``extended basic block'' solver, which produces sub-optimal solutions quickly. The result is - a mapping from program points to numberings. In the unlikely - case where the solver fails to find a solution, we simply associate - empty numberings to all program points, which is semantically correct - and effectively deactivates the CSE optimization. *) - -Definition analyze (f: RTL.function): PMap.t numbering := - match Solver.fixpoint (successors f) (transfer f) f.(fn_entrypoint) with - | None => PMap.init empty_numbering - | Some res => res - end. + a mapping from program points to numberings. *) + +Definition analyze (f: RTL.function): option (PMap.t numbering) := + Solver.fixpoint (successors f) (transfer f) f.(fn_entrypoint). (** * Code transformation *) @@ -400,18 +427,25 @@ Definition transf_instr (n: numbering) (instr: instruction) := Definition transf_code (approxs: PMap.t numbering) (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_function (f: function) : res function := + match type_function f with + | Error msg => Error msg + | OK tyenv => + match analyze f with + | None => Error (msg "CSE failure") + | Some approxs => + OK(mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + (transf_code approxs f.(fn_code)) + f.(fn_entrypoint)) + end + end. -Definition transf_fundef (f: fundef) : fundef := - AST.transf_fundef transf_function f. +Definition transf_fundef (f: fundef) : res fundef := + AST.transf_partial_fundef transf_function f. -Definition transf_program (p: program) : program := - transform_program transf_fundef p. +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. -- cgit