From 3ec022950ec233a2af418aacd1755fce4d701724 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 19 Feb 2014 09:55:45 +0000
Subject: Add option -Os to optimize for code size rather than for execution
 speed. Refactored compilation flags that affect the Coq part (module
 Compopts). Added support for C99 for loops with declarations.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/ConstpropOp.vp     |  1 +
 powerpc/ConstpropOpproof.v |  1 +
 powerpc/SelectOp.vp        | 10 +++++++---
 powerpc/SelectOpproof.v    |  4 +++-
 powerpc/ValueAOp.v         |  1 +
 5 files changed, 13 insertions(+), 4 deletions(-)

(limited to 'powerpc')

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.
-- 
cgit v1.2.3