1 files changed, 32 insertions, 44 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v
index daea1f9e..746ba399 100644
--- a/backend/CSE3.v
+++ b/backend/CSE3.v
@@ -76,49 +76,38 @@ Definition find_cond_in_fmap fmap pc cond args :=
 
 Definition transf_instr (fmap : PMap.t RB.t)
            (pc: node) (instr: instruction) :=
-  if Compopts.optim_CSE3_only_conditions tt then
-    match instr with
-    | Icond cond 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
-    | _ => instr
+  match instr with
+  | Iop op args dst s =>
+    let args' := subst_args fmap pc args in
+    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
-  else
-    match instr with
-    | Iop op args dst s =>
-      let args' := subst_args fmap pc args in
-      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
-    | Iload trap chunk addr args dst s =>
-      let args' := subst_args fmap pc args in
-      match find_load_in_fmap fmap pc chunk addr args' with
-      | None => Iload trap chunk addr args' dst s
-      | Some src => Iop Omove (src::nil) dst s
-      end
-    | Istore chunk addr args src s =>
-      Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s
-    | Icall sig ros args dst s =>
-      Icall sig ros (subst_args fmap pc args) dst s
-    | Itailcall sig ros args =>
-      Itailcall sig ros (subst_args fmap pc args)
-    | Icond cond 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) =>
-      Ireturn (Some (subst_arg fmap pc arg))
-    | _ => instr
-    end.
+  | Iload trap chunk addr args dst s =>
+    let args' := subst_args fmap pc args in
+    match find_load_in_fmap fmap pc chunk addr args' with
+    | None => Iload trap chunk addr args' dst s
+    | Some src => Iop Omove (src::nil) dst s
+    end
+  | Istore chunk addr args src s =>
+    Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s
+  | Icall sig ros args dst s =>
+    Icall sig ros (subst_args fmap pc args) dst s
+  | Itailcall sig ros args =>
+    Itailcall sig ros (subst_args fmap pc args)
+  | Icond cond 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) =>
+    Ireturn (Some (subst_arg fmap pc arg))
+  | _ => instr
+  end.
 End REWRITE.
 
 Definition transf_function (f: function) : res function :=
@@ -132,8 +121,7 @@ Definition transf_function (f: function) : res function :=
           fn_stacksize := f.(fn_stacksize);
           fn_code := PTree.map (transf_instr (ctx := ctx) invariants)
                                f.(fn_code);
-          fn_entrypoint := f.(fn_entrypoint);
-          fn_untrusted_analysis := mkuntrustedanalysis None None |}
+          fn_entrypoint := f.(fn_entrypoint) |}
   else Error (msg "cse3: not inductive").
 
 Definition transf_fundef (fd: fundef) : res fundef :=