summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/ConstpropOp.vp1
-rw-r--r--powerpc/ConstpropOpproof.v1
-rw-r--r--powerpc/SelectOp.vp10
-rw-r--r--powerpc/SelectOpproof.v4
-rw-r--r--powerpc/ValueAOp.v1
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.