5 files changed, 13 insertions, 4 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 9dbaa78..6aa0925 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -14,6 +14,7 @@
     This is the machine-dependent part of [Constprop]. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index e7dd3a4..0c88246 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -13,6 +13,7 @@
 (** Correctness proof for operator strength reduction. *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index bdb94bd..ad4f3b9 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -37,6 +37,7 @@
 *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -190,9 +191,12 @@ Definition mulimm_base (n1: int) (e2: expr) :=
   | i :: nil =>
       shlimm e2 i
   | i :: j :: nil =>
-      Elet e2
-        (Eop Oadd (shlimm (Eletvar 0) i :::
-                   shlimm (Eletvar 0) j ::: Enil))
+      if optim_for_size tt then
+        Eop (Omulimm n1) (e2:::Enil)
+      else
+        Elet e2
+          (Eop Oadd (shlimm (Eletvar 0) i :::
+                     shlimm (Eletvar 0) j ::: Enil))
   | _ =>
       Eop (Omulimm n1) (e2:::Enil)
   end.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 0cfa707..4d26cf6 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -304,7 +305,8 @@ Proof.
   replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul.
   apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib.
   destruct l.
-  intros. rewrite H1. simpl.
+  intros. destruct (optim_for_size tt). TrivialExists.
+  rewrite H1. simpl.
   exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
   exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
   exists (Val.add v1 v2); split.
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 3789953..7f16bb3 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.