diff options
Diffstat (limited to 'backend/CSE3.v')
| -rw-r--r-- | backend/CSE3.v | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index 482069d7..3a680cf7 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -54,22 +54,25 @@ Definition subst_args fmap pc xl := forward_move_l_b (PMap.get pc fmap) xl. Definition find_cond_in_fmap fmap pc cond args := - match PMap.get pc fmap with - | Some rel => - if is_condition_present (ctx:=ctx) pc rel cond args - then Some true - else - let ncond := negate_condition cond in - if is_condition_present (ctx:=ctx) pc rel ncond args - then Some false - else let args' := subst_args fmap pc args in - if is_condition_present (ctx:=ctx) pc rel cond args' - then Some true - else if is_condition_present (ctx:=ctx) pc rel ncond args' - then Some false - else None - | None => None - end. + if Compopts.optim_CSE3_conditions tt + then + match PMap.get pc fmap with + | Some rel => + if is_condition_present (ctx:=ctx) pc rel cond args + then Some true + else + let ncond := negate_condition cond in + if is_condition_present (ctx:=ctx) pc rel ncond args + then Some false + else let args' := subst_args fmap pc args in + if is_condition_present (ctx:=ctx) pc rel cond args' + then Some true + else if is_condition_present (ctx:=ctx) pc rel ncond args' + then Some false + else None + | None => None + end + else None. Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := |