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

8 files changed, 78 insertions, 58 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index 76d8e6c..d2c4d44 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -74,7 +74,7 @@ Definition transf_ros (ae: AE.t) (ros: reg + ident) : reg + ident :=
 Definition const_for_result (a: aval) : option operation :=
   match a with
   | I n => Some(Ointconst n)
-  | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
+  | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | Ptr(Gl symb ofs) => Some(Oaddrsymbol symb ofs)
   | Ptr(Stk ofs) => Some(Oaddrstack ofs)
   | _ => None
@@ -108,7 +108,7 @@ Fixpoint annot_strength_reduction
       let (targs'', args'') := annot_strength_reduction ae targs' args' in
       match ty, areg ae arg with
       | Tint, I n => (AA_int n :: targs'', args'')
-      | Tfloat, F n => if generate_float_constants tt
+      | Tfloat, F n => if Compopts.generate_float_constants tt
                        then (AA_float n :: targs'', args'')
                        else (AA_arg ty :: targs'', arg :: args'')
       | _, _ => (AA_arg ty :: targs'', arg :: args'')
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 41afe8c..d88d6e4 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
@@ -157,7 +158,7 @@ Proof.
 - (* integer *)
   inv H. inv H0. exists (Vint n); auto.
 - (* float *)
-  destruct (generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto.
+  destruct (Compopts.generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto.
 - (* pointer *)
   destruct p; try discriminate.
   + (* global *)
@@ -235,7 +236,7 @@ Proof.
     * exists eargs''; split; auto; simpl; f_equal; auto. 
       generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM.
       inv VM. rewrite <- H0 in *. inv H5; auto.
-    * destruct (generate_float_constants tt); inv H1; auto. 
+    * destruct (Compopts.generate_float_constants tt); inv H1; auto. 
       exists eargs''; split; auto; simpl; f_equal; auto. 
       generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM.
       inv VM. rewrite <- H0 in *. inv H5; auto.
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 1d9168c..938ce5d 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -13,6 +13,7 @@
 (** Instruction selection for division and modulus *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -77,10 +78,13 @@ Definition divuimm (e1: expr) (n2: int) :=
   match Int.is_power2 n2 with
   | Some l => shruimm e1 l
   | None =>
-      match divu_mul_params (Int.unsigned n2) with
-      | None => divu_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (divu_mul p m)
-      end
+      if optim_for_size tt then
+        divu_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divu_mul_params (Int.unsigned n2) with
+        | None => divu_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (divu_mul p m)
+        end
   end.
 
 Nondetfunction divu (e1: expr) (e2: expr) := 
@@ -96,10 +100,13 @@ Definition moduimm (e1: expr) (n2: int) :=
   match Int.is_power2 n2 with
   | Some l => andimm (Int.sub n2 Int.one) e1
   | None =>
-      match divu_mul_params (Int.unsigned n2) with
-      | None => modu_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
-      end
+      if optim_for_size tt then
+        modu_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divu_mul_params (Int.unsigned n2) with
+        | None => modu_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
+        end
   end.
 
 Nondetfunction modu (e1: expr) (e2: expr) := 
@@ -123,10 +130,13 @@ Definition divsimm (e1: expr) (n2: int) :=
       then shrximm e1 l
       else divs_base e1 (Eop (Ointconst n2) Enil)
   | None =>
-      match divs_mul_params (Int.signed n2) with
-      | None => divs_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (divs_mul p m)
-      end
+      if optim_for_size tt then
+        divs_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divs_mul_params (Int.signed n2) with
+        | None => divs_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (divs_mul p m)
+        end
   end.
 
 Nondetfunction divs (e1: expr) (e2: expr) := 
@@ -142,10 +152,13 @@ Definition modsimm (e1: expr) (n2: int) :=
       then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2)
       else mods_base e1 (Eop (Ointconst n2) Enil)
   | None =>
-      match divs_mul_params (Int.signed n2) with
-      | None => mods_base e1 (Eop (Ointconst n2) Enil)
-      | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2)
-      end
+      if optim_for_size tt then
+        mods_base e1 (Eop (Ointconst n2) Enil)
+      else
+        match divs_mul_params (Int.signed n2) with
+        | None => mods_base e1 (Eop (Ointconst n2) Enil)
+        | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2)
+        end
   end.
 
 Nondetfunction mods (e1: expr) (e2: expr) := 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 0719a5e..9228cde 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -369,10 +369,12 @@ Proof.
   replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). 
   apply eval_shruimm; auto.
   simpl. erewrite Int.is_power2_range; eauto. 
-- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
-  + exists (Vint (Int.divu i n2)); split; auto.
-    econstructor; eauto. eapply eval_divu_mul; eauto. 
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_divu_base; eauto. EvalOp.
+  + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+    * exists (Vint (Int.divu i n2)); split; auto.
+      econstructor; eauto. eapply eval_divu_mul; eauto. 
+    * eapply eval_divu_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_divu:
@@ -412,13 +414,15 @@ Proof.
   change (Vint (Int.and i (Int.sub n2 Int.one)))
     with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))).
   apply eval_andimm. auto.
-- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
-  + econstructor; split. 
-    econstructor; eauto. eapply eval_mod_from_div. 
-    eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. 
-    rewrite Int.modu_divu. auto. 
-    red; intros; subst n2; discriminate.
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_modu_base; eauto. EvalOp.
+  + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS.
+    * econstructor; split. 
+      econstructor; eauto. eapply eval_mod_from_div. 
+      eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. 
+      rewrite Int.modu_divu. auto. 
+      red; intros; subst n2; discriminate.
+    * eapply eval_modu_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_modu:
@@ -485,10 +489,12 @@ Proof.
 - destruct (Int.ltu l (Int.repr 31)) eqn:LT31.
   + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto.
   + eapply eval_divs_base; eauto. EvalOp.
-- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
-  + exists (Vint (Int.divs i n2)); split; auto.
-    econstructor; eauto. eapply eval_divs_mul; eauto. 
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_divs_base; eauto. EvalOp.
+  + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
+    * exists (Vint (Int.divs i n2)); split; auto.
+      econstructor; eauto. eapply eval_divs_mul; eauto. 
+    * eapply eval_divs_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_divs:
@@ -524,12 +530,14 @@ Proof.
     apply eval_mod_from_div. eexact X. simpl; eauto. 
     simpl. auto.
   + eapply eval_mods_base; eauto. EvalOp.
-- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
-  + econstructor; split. 
-    econstructor. eauto. apply eval_mod_from_div with (x := i); auto.
-    eapply eval_divs_mul with (x := i); eauto.
-    simpl. auto.
+- destruct (Compopts.optim_for_size tt).
   + eapply eval_mods_base; eauto. EvalOp.
+  + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS.
+    * econstructor; split. 
+      econstructor. eauto. apply eval_mod_from_div with (x := i); auto.
+      eapply eval_divs_mul with (x := i); eauto.
+      simpl. auto.
+    * eapply eval_mods_base; eauto. EvalOp.
 Qed.
 
 Theorem eval_mods:
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 26beb34..25da531 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -14,6 +14,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Registers.
 Require Import Op.
@@ -98,8 +99,6 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
   as explained above.  Moreover, we can turn tail calls off
   using a compilation option. *)
 
-Parameter eliminate_tailcalls: unit -> bool.
-
 Definition transf_function (f: function) : function :=
   if zeq f.(fn_stacksize) 0 && eliminate_tailcalls tt
   then RTL.transf_function (transf_instr f) f
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 77725cf..1965b18 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -13,6 +13,7 @@
 (** Recognition of tail calls: correctness proof *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index f580438..e293028 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -12,6 +12,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -74,7 +75,7 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func
   match classify_builtin ef args ae with
   | Builtin_vload chunk aaddr => 
       let a :=
-        if strict
+        if va_strict tt
         then vlub (loadv chunk rm am aaddr) (vnormalize chunk (Ifptr Glob))
         else vnormalize chunk Vtop in
       VA.State (AE.set res a ae) am
@@ -1255,11 +1256,11 @@ Proof.
   * (* true volatile access *)
     assert (V: vmatch bc v0 (Ifptr Glob)).
     { inv H4; constructor. econstructor. eapply GE; eauto. }
-    destruct strict. apply vmatch_lub_r. apply vnormalize_sound. auto. 
+    destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. 
     apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor.
   * (* normal memory access *)
     exploit loadv_sound; eauto. simpl; eauto. intros V.
-    destruct strict. 
+    destruct (va_strict tt). 
     apply vmatch_lub_l. auto.
     eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. 
 + (* volatile store *)
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index eee4762..239dd47 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -13,6 +13,7 @@
 Require Import Coqlib.
 Require Import Zwf.
 Require Import Maps.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -25,10 +26,6 @@ Require Import Kildall.
 Require Import Registers.
 Require Import RTL.
 
-Parameter strict: bool.
-Parameter propagate_float_constants: unit -> bool.
-Parameter generate_float_constants : unit -> bool.
-
 Inductive block_class : Type :=
   | BCinvalid
   | BCglob (id: ident)
@@ -819,7 +816,7 @@ Definition vlub (v w: aval) : aval :=
   | I i, Sgn n | Sgn n, I i =>
       sgn (Z.max (ssize i) n)
   | I i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i =>
-      if strict || Int.eq i Int.zero then Ifptr p else Vtop
+      if va_strict tt || Int.eq i Int.zero then Ifptr p else Vtop
   | Uns n1, Uns n2 => Uns (Z.max n1 n2)
   | Uns n1, Sgn n2 => sgn (Z.max (n1 + 1) n2)
   | Sgn n1, Uns n2 => sgn (Z.max n1 (n2 + 1))
@@ -837,7 +834,7 @@ Definition vlub (v w: aval) : aval :=
   | Ptr p1, Ifptr p2 => Ifptr(plub p1 p2)
   | Ifptr p1, Ptr p2 => Ifptr(plub p1 p2)
   | Ifptr p1, Ifptr p2 => Ifptr(plub p1 p2)
-  | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if strict then Ifptr p else Vtop
+  | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if va_strict tt then Ifptr p else Vtop
   | _, _ => Vtop
   end.
 
@@ -989,8 +986,8 @@ Lemma pmatch_vplub:
   forall b ofs x p, pmatch b ofs p -> pmatch b ofs (vplub x p).
 Proof.
   intros. 
-  assert (DFL: pmatch b ofs (if strict then p else Ptop)).
-  { destruct strict; auto. eapply pmatch_top'; eauto. }
+  assert (DFL: pmatch b ofs (if va_strict tt then p else Ptop)).
+  { destruct (va_strict tt); auto. eapply pmatch_top'; eauto. }
   unfold vplub; destruct x; auto; apply pmatch_lub_r; auto.
 Qed.
 
@@ -1495,7 +1492,7 @@ Definition divs (v w: aval) :=
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
       || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
-      then if strict then Vbot else itop
+      then if va_strict tt then Vbot else itop
       else I (Int.divs i1 i2)
   | _, _ => itop
   end.
@@ -1513,7 +1510,7 @@ Definition divu (v w: aval) :=
   match w, v with
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
-       then if strict then Vbot else itop
+       then if va_strict tt then Vbot else itop
       else I (Int.divu i1 i2)
   | _, _ => itop
   end.
@@ -1531,7 +1528,7 @@ Definition mods (v w: aval) :=
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
       || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
-      then if strict then Vbot else itop
+      then if va_strict tt then Vbot else itop
       else I (Int.mods i1 i2)
   | _, _ => itop
   end.
@@ -1549,7 +1546,7 @@ Definition modu (v w: aval) :=
   match w, v with
   | I i2, I i1 =>
       if Int.eq i2 Int.zero
-      then if strict then Vbot else itop
+      then if va_strict tt then Vbot else itop
       else I (Int.modu i1 i2)
   | I i2, _ => uns (usize i2)
   | _, _ => itop
@@ -1693,7 +1690,7 @@ Definition intoffloat (x: aval) :=
   | F f =>
       match Float.intoffloat f with
       | Some i => I i
-      | None => if strict then Vbot else itop
+      | None => if va_strict tt then Vbot else itop
       end
   | _ => itop
   end.
@@ -1711,7 +1708,7 @@ Definition intuoffloat (x: aval) :=
   | F f =>
       match Float.intuoffloat f with
       | Some i => I i
-      | None => if strict then Vbot else itop
+      | None => if va_strict tt then Vbot else itop
       end
   | _ => itop
   end.
@@ -2823,7 +2820,7 @@ Definition mtop := minit Ptop.
 
 Definition load (chunk: memory_chunk) (rm: romem) (m: amem) (p: aptr) : aval :=
   match p with
-  | Pbot => if strict then Vbot else Vtop
+  | Pbot => if va_strict tt then Vbot else Vtop
   | Gl id ofs =>
       match rm!id with
       | Some ab => ablock_load chunk ab (Int.unsigned ofs)
@@ -2882,7 +2879,7 @@ Definition storev (chunk: memory_chunk) (m: amem) (addr: aval) (v: aval): amem :
 
 Definition loadbytes (m: amem) (rm: romem) (p: aptr) : aptr :=
   match p with
-  | Pbot => if strict then Pbot else Ptop
+  | Pbot => if va_strict tt then Pbot else Ptop
   | Gl id _ | Glo id =>
       match rm!id with
       | Some ab => ablock_loadbytes ab