Common subexpression elimination over RTL. This optimization
proceeds by value numbering over extended basic blocks.
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking Builtins.
Require Import Values Memory Events.
Require Import Op Registers RTL.
Require Import ValueDomain ValueAnalysis CSEdomain CombineOp.
The idea behind value numbering algorithms is to associate
abstract identifiers (``value numbers'') to the contents of registers
at various program points, and record equations between these
identifiers. For instance, consider the instruction
r1 = add(r2, r3) and assume that r2 and r3 are mapped
to abstract identifiers x and y respectively at the program
point just before this instruction. At the program point just after,
we can add the equation z = add(x, y) and associate r1 with z,
where z is a fresh abstract identifier. However, if we already
knew an equation u = add(x, y), we can preferably add no equation
and just associate r1 with u. If there exists a register r4
mapped with u at this point, we can then replace the instruction
r1 = add(r2, r3) by a move instruction r1 = r4, therefore eliminating
a common subexpression and reusing the result of an earlier addition.
The representation of value numbers and equations is described in
module CSEdomain.
Operations on value numberings
valnum_reg n r returns the value number for the contents of
register r. If none exists, a fresh value number is returned
and associated with register r. The possibly updated numbering
is also returned. valnum_regs is similar, but for a list of
registers.
Definition valnum_reg (
n:
numbering) (
r:
reg) :
numbering *
valnum :=
match PTree.get r n.(
num_reg)
with
|
Some v => (
n,
v)
|
None =>
let v :=
n.(
num_next)
in
( {|
num_next :=
Pos.succ v;
num_eqs :=
n.(
num_eqs);
num_reg :=
PTree.set r v n.(
num_reg);
num_val :=
PMap.set v (
r ::
nil)
n.(
num_val) |},
v)
end.
Fixpoint valnum_regs (
n:
numbering) (
rl:
list reg)
{
struct rl} :
numbering *
list valnum :=
match rl with
|
nil =>
(
n,
nil)
|
r1 ::
rs =>
let (
n1,
v1) :=
valnum_reg n r1 in
let (
ns,
vs) :=
valnum_regs n1 rs in
(
ns,
v1 ::
vs)
end.
Fixpoint valnum_builtin_arg (
n:
numbering) (
a:
builtin_arg reg)
{
struct a} :
numbering *
builtin_arg valnum :=
match a with
|
BA r =>
let (
n,
v) :=
valnum_reg n r in (
n,
BA v)
|
BA_int i => (
n,
BA_int i)
|
BA_long i => (
n,
BA_long i)
|
BA_float f => (
n,
BA_float f)
|
BA_single f => (
n,
BA_single f)
|
BA_loadstack chunk ofs => (
n,
BA_loadstack chunk ofs)
|
BA_addrstack ofs => (
n,
BA_addrstack ofs)
|
BA_loadglobal chunk id ofs => (
n,
BA_loadglobal chunk id ofs)
|
BA_addrglobal id ofs => (
n,
BA_addrglobal id ofs)
|
BA_splitlong a1 a2 =>
let (
n,
v1) :=
valnum_builtin_arg n a1 in
let (
n,
v2) :=
valnum_builtin_arg n a2 in
(
n,
BA_splitlong v1 v2)
|
BA_addptr a1 a2 =>
let (
n,
v1) :=
valnum_builtin_arg n a1 in
let (
n,
v2) :=
valnum_builtin_arg n a2 in
(
n,
BA_addptr v1 v2)
end.
Fixpoint valnum_builtin_args (
n:
numbering) (
args:
list (
builtin_arg reg))
{
struct args} :
numbering *
list (
builtin_arg valnum) :=
match args with
|
nil =>
(
n,
nil)
|
arg1 ::
args =>
let (
n1,
v1) :=
valnum_builtin_arg n arg1 in
let (
ns,
vs) :=
valnum_builtin_args n1 args in
(
ns,
v1 ::
vs)
end.
find_valnum_rhs rhs eqs searches the list of equations eqs
for an equation of the form vn = rhs for some value number vn.
If found, Some vn is returned, otherwise None is returned.
Fixpoint find_valnum_rhs (
r:
rhs) (
eqs:
list equation)
{
struct eqs} :
option valnum :=
match eqs with
|
nil =>
None
|
Eq v str r' ::
eqs1 =>
if str &&
compat_rhs r r' then Some v else find_valnum_rhs r eqs1
end.
find_valnum_rhs' rhs eqs is similar, but also accepts equations
of the form vn >= rhs.
Fixpoint find_valnum_rhs' (
r:
rhs) (
eqs:
list equation)
{
struct eqs} :
option valnum :=
match eqs with
|
nil =>
None
|
Eq v str r' ::
eqs1 =>
if compat_rhs r r' then Some v else find_valnum_rhs' r eqs1
end.
find_valnum_num vn eqs searches the list of equations eqs
for an equation of the form vn = rhs for some equation rhs.
If found, Some rhs is returned, otherwise None is returned.
Fixpoint find_valnum_num (
v:
valnum) (
eqs:
list equation)
{
struct eqs} :
option rhs :=
match eqs with
|
nil =>
None
|
Eq v' str r' ::
eqs1 =>
if str &&
peq v v' then Some r' else find_valnum_num v eqs1
end.
reg_valnum n vn returns a register that is mapped to value number
vn, or None if no such register exists.
Definition reg_valnum (
n:
numbering) (
vn:
valnum) :
option reg :=
match PMap.get vn n.(
num_val)
with
|
nil =>
None
|
r ::
rs =>
Some r
end.
regs_valnums is similar, for a list of value numbers.
Fixpoint regs_valnums (
n:
numbering) (
vl:
list valnum) :
option (
list reg) :=
match vl with
|
nil =>
Some nil
|
v1 ::
vs =>
match reg_valnum n v1,
regs_valnums n vs with
|
Some r1,
Some rs =>
Some (
r1 ::
rs)
| _, _ =>
None
end
end.
find_rhs return a register that already holds the result of the
given arithmetic operation or memory load, or a value more defined
than this result, according to the given
numbering. None is returned if no such register exists.
Definition find_rhs (
n:
numbering) (
rh:
rhs) :
option reg :=
match find_valnum_rhs' rh n.(
num_eqs)
with
|
None =>
None
|
Some vres =>
reg_valnum n vres
end.
Update the num_val mapping prior to a redefinition of register r.
Definition forget_reg (
n:
numbering) (
rd:
reg) :
PMap.t (
list reg) :=
match PTree.get rd n.(
num_reg)
with
|
None =>
n.(
num_val)
|
Some v =>
PMap.set v (
List.remove peq rd (
PMap.get v n.(
num_val)))
n.(
num_val)
end.
Definition update_reg (
n:
numbering) (
rd:
reg) (
vn:
valnum) :
PMap.t (
list reg) :=
let nv :=
forget_reg n rd in PMap.set vn (
rd ::
PMap.get vn nv)
nv.
add_rhs n rd rhs updates the value numbering n to reflect
the computation of the operation or load represented by rhs
and the storing of the result in register rd. If an equation
vn = rhs is known, register rd is set to vn. Otherwise,
a fresh value number vn is generated and associated with rd,
and the equation vn = rhs is added.
Definition add_rhs (
n:
numbering) (
rd:
reg) (
rh:
rhs) :
numbering :=
match find_valnum_rhs rh n.(
num_eqs)
with
|
Some vres =>
{|
num_next :=
n.(
num_next);
num_eqs :=
n.(
num_eqs);
num_reg :=
PTree.set rd vres n.(
num_reg);
num_val :=
update_reg n rd vres |}
|
None =>
{|
num_next :=
Pos.succ n.(
num_next);
num_eqs :=
Eq n.(
num_next)
true rh ::
n.(
num_eqs);
num_reg :=
PTree.set rd n.(
num_next)
n.(
num_reg);
num_val :=
update_reg n rd n.(
num_next) |}
end.
add_op n rd op rs specializes
add_rhs for the case of an
arithmetic operation. The right-hand side corresponding to
op
and the value numbers for the argument registers
rs is built
and added to
n as described in
add_rhs.
If
op is a move instruction, we simply assign the value number of
the source register to the destination register, since we know that
the source and destination registers have exactly the same value.
This enables more common subexpressions to be recognized. For instance:
z = add(x, y); u = x; v = add(u, y);
Since
u and
x have the same value number, the second
add
is recognized as computing the same result as the first
add,
and therefore
u and
z have the same value number.
Definition add_op (
n:
numbering) (
rd:
reg) (
op:
operation) (
rs:
list reg) :=
match is_move_operation op rs with
|
Some r =>
let (
n1,
v) :=
valnum_reg n r in
{|
num_next :=
n1.(
num_next);
num_eqs :=
n1.(
num_eqs);
num_reg :=
PTree.set rd v n1.(
num_reg);
num_val :=
update_reg n1 rd v |}
|
None =>
let (
n1,
vs) :=
valnum_regs n rs in
add_rhs n1 rd (
Op op vs)
end.
add_load n rd chunk addr rs specializes add_rhs for the case of a
memory load. The right-hand side corresponding to chunk, addr
and the value numbers for the argument registers rs is built
and added to n as described in add_rhs.
Definition add_load (
n:
numbering) (
rd:
reg)
(
chunk:
memory_chunk) (
addr:
addressing)
(
rs:
list reg) (
p:
aptr) :=
let (
n1,
vs) :=
valnum_regs n rs in
add_rhs n1 rd (
Load chunk addr vs p).
add_builtin n res bf args specializes add_rhs for the case of a
built-in function. The right-hand side corresponding to bf
and the value numbers for the argument args rs is built
and added to n as described in add_rhs.
Definition add_builtin (
n:
numbering) (
dst:
builtin_res reg)
(
bf:
builtin_function) (
args:
list (
builtin_arg reg)) :=
match dst with
|
BR rd =>
let (
n1,
args1) :=
valnum_builtin_args n args in
add_rhs n1 rd (
Builtin bf args1)
| _ =>
n
end.
Definition set_unknown (
n:
numbering) (
rd:
reg) :=
{|
num_next :=
n.(
num_next);
num_eqs :=
n.(
num_eqs);
num_reg :=
PTree.remove rd n.(
num_reg);
num_val :=
forget_reg n rd |}.
Definition set_res_unknown (
n:
numbering) (
res:
builtin_res reg) :=
match res with
|
BR r =>
set_unknown n r
| _ =>
n
end.
kill_equations pred n remove all equations satisfying predicate pred.
Fixpoint kill_eqs (
pred:
rhs ->
bool) (
eqs:
list equation) :
list equation :=
match eqs with
|
nil =>
nil
| (
Eq l strict r)
as eq ::
rem =>
if pred r then kill_eqs pred rem else eq ::
kill_eqs pred rem
end.
Definition kill_equations (
pred:
rhs ->
bool) (
n:
numbering) :
numbering :=
{|
num_next :=
n.(
num_next);
num_eqs :=
kill_eqs pred n.(
num_eqs);
num_reg :=
n.(
num_reg);
num_val :=
n.(
num_val) |}.
kill_all_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
|
Builtin bf args =>
builtin_args_depends_on_memory args
end.
Definition kill_all_loads (
n:
numbering) :
numbering :=
kill_equations filter_loads n.
kill_loads_after_store app n chunk addr args removes all equations
involving loads that could be invalidated by a store of quantity chunk
at address determined by addr and args. Loads that are disjoint
from this store are preserved. Equations involving memory-dependent
operators are also removed.
Definition filter_after_store (
n:
numbering) (
p:
aptr) (
sz:
Z) (
r:
rhs) :=
match r with
|
Op op vl =>
op_depends_on_memory op
|
Load chunk addr vl q =>
negb (
pdisjoint q (
size_chunk chunk)
p sz)
|
Builtin bf args =>
builtin_args_depends_on_memory args
end.
Definition kill_loads_after_store
(
app:
VA.t) (
n:
numbering)
(
chunk:
memory_chunk) (
addr:
addressing) (
args:
list reg) :=
let p :=
aaddressing app addr args in
kill_equations (
filter_after_store n p (
size_chunk chunk))
n.
kill_cheap_computations n removes all equations corresponding to
``cheap'' computations, i.e. computations that are not worth
factoring across a call to a runtime library function.
(Such a factoring has its own costs, since the result must be kept
in a callee-save register or a stack location.)
As a rough approximation of costs, we say that all Op and Load
computations are cheap, and all Builtin computations are
expensive. More precise criteria are possible.
Definition filter_cheap (
r:
rhs) :
bool :=
match r with
|
Op _ _ =>
true
|
Load _ _ _ _ =>
true
|
Builtin _ _ =>
false
end.
Definition kill_cheap_computations (
n:
numbering) :
numbering :=
kill_equations filter_cheap n.
add_store_result n chunk addr rargs rsrc updates the numbering n
to reflect the knowledge gained after executing an instruction
Istore chunk addr rargs rsrc. An equation vsrc >= Load chunk addr vargs
is added, but only if the value of rsrc is known to be normalized
with respect to chunk.
Definition store_normalized_range (
chunk:
memory_chunk) :
aval :=
match chunk with
|
Mbool =>
Uns Ptop 1
|
Mint8signed =>
Sgn Ptop 8
|
Mint8unsigned =>
Uns Ptop 8
|
Mint16signed =>
Sgn Ptop 16
|
Mint16unsigned =>
Uns Ptop 16
| _ =>
Vtop
end.
Definition add_store_result (
app:
VA.t) (
n:
numbering) (
chunk:
memory_chunk) (
addr:
addressing)
(
rargs:
list reg) (
rsrc:
reg) :=
if vincl (
avalue app rsrc) (
store_normalized_range chunk)
then
let (
n1,
vsrc) :=
valnum_reg n rsrc in
let (
n2,
vargs) :=
valnum_regs n1 rargs in
{|
num_next :=
n2.(
num_next);
num_eqs :=
Eq vsrc false (
Load chunk addr vargs (
aaddressing app addr rargs)) ::
n2.(
num_eqs);
num_reg :=
n2.(
num_reg);
num_val :=
n2.(
num_val) |}
else n.
kill_loads_after_storebyte n dst sz removes all equations
involving loads that could be invalidated by a store of sz bytes
starting at address dst. Loads that are disjoint from this
store-bytes are preserved. Equations involving memory-dependent
operators are also removed.
Definition kill_loads_after_storebytes
(
n:
numbering) (
dst:
aptr) (
sz:
Z) :=
kill_equations (
filter_after_store n dst sz)
n.
add_memcpy app n1 n2 rsrc rdst sz adds equations to n2 that
represent the effect of a memcpy block copy operation of sz bytes
from the address denoted by rsrc to the address denoted by rdst.
n2 is the numbering returned by kill_loads_after_storebytes
and n1 is the original numbering before the memcpy operation.
Valid equations (found in n1) involving loads within the source
area of the memcpy are translated as equations involving loads
within the destination area, and added to numbering n2.
Currently, we only track memcpy operations between stack
locations, as often occur when compiling assignments between local C
variables of struct type.
Definition shift_memcpy_eq (
src sz delta:
Z) (
e:
equation) :=
match e with
|
Eq l strict (
Load chunk (
Ainstack i) _ _) =>
let i :=
Ptrofs.unsigned i in
let j :=
i +
delta in
if zle src i
&&
zle (
i +
size_chunk chunk) (
src +
sz)
&&
zeq (
Z.modulo delta (
align_chunk chunk)) 0
&&
zle 0
j
&&
zle j Ptrofs.max_unsigned
then Some(
Eq l strict (
Load chunk (
Ainstack (
Ptrofs.repr j))
nil (
Stk (
Ptrofs.repr j))))
else None
| _ =>
None
end.
Fixpoint add_memcpy_eqs (
src sz delta:
Z) (
eqs1 eqs2:
list equation) :=
match eqs1 with
|
nil =>
eqs2
|
e ::
eqs =>
match shift_memcpy_eq src sz delta e with
|
None =>
add_memcpy_eqs src sz delta eqs eqs2
|
Some e' =>
e' ::
add_memcpy_eqs src sz delta eqs eqs2
end
end.
Definition add_memcpy (
n1 n2:
numbering) (
asrc adst:
aptr) (
sz:
Z) :=
match asrc,
adst with
|
Stk src,
Stk dst =>
{|
num_next :=
n2.(
num_next);
num_eqs :=
add_memcpy_eqs (
Ptrofs.unsigned src)
sz
(
Ptrofs.unsigned dst -
Ptrofs.unsigned src)
n1.(
num_eqs)
n2.(
num_eqs);
num_reg :=
n2.(
num_reg);
num_val :=
n2.(
num_val) |}
| _, _ =>
n2
end.
Take advantage of known equations to select more efficient
forms of operations, addressing modes, and conditions.
Section REDUCE.
Variable A:
Type.
Variable f: (
valnum ->
option rhs) ->
A ->
list valnum ->
option (
A *
list valnum).
Variable n:
numbering.
Fixpoint reduce_rec (
niter:
nat) (
op:
A) (
args:
list valnum) :
option(
A *
list reg) :=
match niter with
|
O =>
None
|
Datatypes.S niter' =>
match f (
fun v =>
find_valnum_num v n.(
num_eqs))
op args with
|
None =>
None
|
Some(
op',
args') =>
match reduce_rec niter' op' args' with
|
None =>
match regs_valnums n args' with Some rl =>
Some(
op',
rl) |
None =>
None end
|
Some _
as res =>
res
end
end
end.
Definition reduce (
op:
A) (
rl:
list reg) (
vl:
list valnum) :
A *
list reg :=
match reduce_rec 4%
nat op vl with
|
None => (
op,
rl)
|
Some res =>
res
end.
End REDUCE.
The static analysis
We now equip the type numbering with a partial order and a greatest
element. The partial order is based on entailment: n1 is greater
than n2 if n1 is satisfiable whenever n2 is. The greatest element
is, of course, the empty numbering (no equations).
Module Numbering.
Definition t :=
numbering.
Definition ge (
n1 n2:
numbering) :
Prop :=
forall valu ge sp rs m,
numbering_holds valu ge sp rs m n2 ->
numbering_holds valu ge sp rs m n1.
Definition top :=
empty_numbering.
Lemma top_ge:
forall x,
ge top x.
Proof.
Lemma refl_ge:
forall x,
ge x x.
Proof.
intros; red; auto.
Qed.
End Numbering.
We reuse the solver for forward dataflow inequations based on
propagation over extended basic blocks defined in library Kildall.
Module Solver :=
BBlock_solver(
Numbering).
The transfer function for the dataflow analysis returns the numbering
``after'' execution of the instruction at
pc, as a function of the
numbering ``before''.
-
For Iop and Iload instructions, we add equations or reuse
existing value numbers as described for add_op and add_load.
-
For Istore instructions, we forget equations involving memory
loads at possibly overlapping locations, then add an equation for
loads from the same location stored to.
-
For Icall instructions, we could simply associate a fresh,
unconstrained by equations value number to the result register.
However, it is often undesirable to eliminate common subexpressions
across a function call (there is a risk of increasing too much the
register pressure across the call), so we just forget all equations
and start afresh with an empty numbering.
-
Finally, for instructions that modify neither registers nor
the memory, we keep the numbering unchanged.
For builtin invocations
Ibuiltin, we have four strategies:
-
Forget all equations. This is appropriate for builtins that can be
turned into function calls
(EF_external, EF_runtime, EF_malloc, EF_free).
-
Forget equations involving loads but keep equations over registers.
This is appropriate for builtins that can modify memory,
e.g. volatile stores, or EF_builtin for unknown builtin functions.
-
Keep all equations, taking advantage of the fact that neither memory
nor registers are modified. This is appropriate for annotations and
volatile loads.
-
Keep all equations and add a new equation. This is appropriate for
builtin functions with known semantics.
Icall instructions that call runtime library functions with known
semantics can be analyzed like a builtin invocation,
by adding a new
Builtin equation.
(
f:
function) (
dm:
defmap) (
approx:
PMap.t VA.t) (
pc:
node) (
before:
numbering) :=
match f.(
fn_code)!
pc with
|
None =>
before
|
Some i =>
match i with
|
Inop s =>
before
|
Iop op args res s =>
add_op before res op args
|
Iload chunk addr args dst s =>
add_load before dst chunk addr args (
aaddressing approx!!
pc addr args)
|
Istore chunk addr args src s =>
let app :=
approx!!
pc in
let n :=
kill_loads_after_store app before chunk addr args in
add_store_result app n chunk addr args src
|
Icall sig ros args res s =>
match is_known_runtime_function dm ros with
|
None =>
empty_numbering
|
Some bf =>
let n :=
kill_cheap_computations before in
add_builtin n (
BR res)
bf (
map (@
BA _)
args)
end
|
Itailcall sig ros args =>
empty_numbering
|
Ibuiltin ef args res s =>
match ef with
|
EF_external _ _ |
EF_runtime _ _ |
EF_malloc |
EF_free |
EF_inline_asm _ _ _ =>
empty_numbering
|
EF_vstore _ =>
set_res_unknown (
kill_all_loads before)
res
|
EF_builtin name sg =>
match lookup_builtin_function name sg with
|
Some bf =>
add_builtin before res bf args
|
None =>
set_res_unknown (
kill_all_loads before)
res
end
|
EF_memcpy sz al =>
match args with
|
dst ::
src ::
nil =>
let app :=
approx!!
pc in
let adst :=
aaddr_arg app dst in
let asrc :=
aaddr_arg app src in
let n :=
kill_loads_after_storebytes before adst sz in
set_res_unknown (
add_memcpy before n asrc adst sz)
res
| _ =>
empty_numbering
end
|
EF_vload _ |
EF_annot _ _ _ |
EF_annot_val _ _ _ |
EF_debug _ _ _ =>
set_res_unknown before res
end
|
Icond cond args ifso ifnot =>
before
|
Ijumptable arg tbl =>
before
|
Ireturn optarg =>
before
end
end.
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.
Definition analyze (
f:
RTL.function) (
dm:
defmap) (
approx:
PMap.t VA.t):
option (
PMap.t numbering) :=
Solver.fixpoint (
fn_code f)
successors_instr (
transfer f dm approx)
f.(
fn_entrypoint).
Code transformation
The code transformation is performed instruction by instruction.
Iload instructions, non-trivial Iop instructions, and Ibuiltin
with known built-in functions are turned into move instructions if
their result is already available in a register, as indicated by the
numbering inferred at that program point.
Some operations are so cheap to compute that it is generally not
worth reusing their results. These operations are detected by the
function is_trivial_op in module Op.
Definition transf_instr (
dm:
defmap) (
n:
numbering) (
instr:
instruction) :=
match instr with
|
Iop op args res s =>
if is_trivial_op op then instr else
let (
n1,
vl) :=
valnum_regs n args in
match find_rhs n1 (
Op op vl)
with
|
Some r =>
Iop Omove (
r ::
nil)
res s
|
None =>
let (
op',
args') :=
reduce _
combine_op n1 op args vl in
Iop op' args' res s
end
|
Iload chunk addr args dst s =>
let (
n1,
vl) :=
valnum_regs n args in
match find_rhs n1 (
Load chunk addr vl Ptop)
with
|
Some r =>
Iop Omove (
r ::
nil)
dst s
|
None =>
let (
addr',
args') :=
reduce _
combine_addr n1 addr args vl in
Iload chunk addr' args' dst s
end
|
Istore chunk addr args src s =>
let (
n1,
vl) :=
valnum_regs n args in
let (
addr',
args') :=
reduce _
combine_addr n1 addr args vl in
Istore chunk addr' args' src s
|
Icall sg ros args res s =>
match is_known_runtime_function dm ros with
|
None =>
instr
|
Some bf =>
let (
n1,
args') :=
valnum_builtin_args n (
map (@
BA _)
args)
in
match find_rhs n1 (
Builtin bf args')
with
|
Some r =>
Iop Omove (
r ::
nil)
res s
|
None =>
instr
end
end
|
Ibuiltin (
EF_builtin name sg)
args (
BR res)
s =>
match lookup_builtin_function name sg with
|
Some bf =>
let (
n1,
args') :=
valnum_builtin_args n args in
match find_rhs n1 (
Builtin bf args')
with
|
Some r =>
Iop Omove (
r ::
nil)
res s
|
None =>
instr
end
|
None =>
instr
end
|
Icond cond args s1 s2 =>
let (
n1,
vl) :=
valnum_regs n args in
match combine_cond' cond vl with
|
Some b =>
Inop (
if b then s1 else s2)
|
None =>
let (
cond',
args') :=
reduce _
combine_cond n1 cond args vl in
Icond cond' args' s1 s2
end
| _ =>
instr
end.
Definition transf_code (
dm:
defmap) (
approxs:
PMap.t numbering) (
instrs:
code) :
code :=
PTree.map (
fun pc instr =>
transf_instr dm approxs!!
pc instr)
instrs.
Definition vanalyze :=
ValueAnalysis.analyze.
Definition globdefs :=
PTree.t (
globdef fundef unit).
Definition transf_function (
dm:
defmap) (
rm:
romem) (
f:
function) :
res function :=
let approx :=
vanalyze rm f in
match analyze f dm approx with
|
None =>
Error (
msg "CSE failure")
|
Some approxs =>
OK(
mkfunction
f.(
fn_sig)
f.(
fn_params)
f.(
fn_stacksize)
(
transf_code dm approxs f.(
fn_code))
f.(
fn_entrypoint))
end.
Definition transf_fundef (
dm:
defmap) (
rm:
romem) (
f:
fundef) :
res fundef :=
AST.transf_partial_fundef (
transf_function dm rm)
f.
Definition transf_program (
p:
program) :
res program :=
transform_partial_program (
transf_fundef (
prog_defmap p) (
romem_for p))
p.