Conditions now propagated by CSE3

Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work

1 files changed, 26 insertions, 1 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
index 13d07e65..746ba399 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -53,6 +53,27 @@ 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 :=
+  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) :=
   match instr with
@@ -76,7 +97,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) =>