Commit 749fa737 authored by David Monniaux's avatar David Monniaux
Browse files

-fcse3-trivial-ops

parent e21a56ac
......@@ -58,7 +58,8 @@ Definition transf_instr (fmap : PMap.t RB.t)
match instr with
| Iop op args dst s =>
let args' := subst_args fmap pc args in
match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with
match (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)
then None else find_op_in_fmap fmap pc op args') with
| None => Iop op args' dst s
| Some src => Iop Omove (src::nil) dst s
end
......
......@@ -463,12 +463,12 @@ Proof.
destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
(subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
* destruct (if is_trivial_op op
* destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)
then None
else
rhs_find pc (SOp op)
(subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND.
** destruct (is_trivial_op op). discriminate.
** destruct ((negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)). discriminate.
apply exec_Iop with (op := Omove) (args := r :: nil).
TR_AT.
subst instr'.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment