From 3ec022950ec233a2af418aacd1755fce4d701724 Mon Sep 17 00:00:00 2001 From: xleroy 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 --- backend/Constprop.v | 4 ++-- backend/Constpropproof.v | 5 +++-- backend/SelectDiv.vp | 45 +++++++++++++++++++++++++++++---------------- backend/SelectDivproof.v | 42 +++++++++++++++++++++++++----------------- backend/Tailcall.v | 3 +-- backend/Tailcallproof.v | 1 + backend/ValueAnalysis.v | 7 ++++--- backend/ValueDomain.v | 29 +++++++++++++---------------- 8 files changed, 78 insertions(+), 58 deletions(-) (limited to 'backend') 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 -- cgit v1.2.3