From 3570ba2827908b280315c922ba7e43289f6d802a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 26 Nov 2020 22:12:38 +0100 Subject: not yet the transfer functions that record predicates --- backend/CSE3.v | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) (limited to 'backend/CSE3.v') diff --git a/backend/CSE3.v b/backend/CSE3.v index df1c2bfc..482069d7 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -53,6 +53,24 @@ Definition forward_move_l_b (rb : RB.t) (xl : list reg) := 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. + Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with @@ -75,7 +93,11 @@ Definition transf_instr (fmap : PMap.t RB.t) | Itailcall sig ros args => Itailcall sig ros (subst_args fmap pc args) | Icond cond args s1 s2 expected => - Icond cond (subst_args fmap pc args) s1 s2 expected + let args' := subst_args fmap pc args in + match find_cond_in_fmap fmap pc cond args with + | None => Icond cond args' s1 s2 expected + | Some b => Inop (if b then s1 else s2) + end | Ijumptable arg tbl => Ijumptable (subst_arg fmap pc arg) tbl | Ireturn (Some arg) => -- cgit From eb1121d703835e76babc15b057276d2852ade4ab Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 16:25:46 +0100 Subject: totally switch off conditions in cse3 --- backend/CSE3.v | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) (limited to 'backend/CSE3.v') 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) := -- cgit