From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/ConstpropOp.vp | 22 +++++++++++++++-- powerpc/ConstpropOpproof.v | 24 ++++++++++++++++++ powerpc/Unusedglob1.ml | 61 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 105 insertions(+), 2 deletions(-) create mode 100644 powerpc/Unusedglob1.ml (limited to 'powerpc') diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 32986713..60b5c63c 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -70,11 +70,13 @@ Definition eval_static_condition_val (cond: condition) (vl: list approx) := Definition eval_static_intoffloat (f: float) := match Float.intoffloat f with Some x => I x | None => Unknown end. +Parameter propagate_float_constants: unit -> bool. + Nondetfunction eval_static_operation (op: operation) (vl: list approx) := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => F n + | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown | Oaddrsymbol s n, nil => G s n | Oaddrstack n, nil => S n | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1) @@ -119,11 +121,27 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2) | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1) | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1 - | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2) + | Ofloatofwords, I n1 :: I n2 :: nil => if propagate_float_constants tt then F(Float.from_words n1 n2) else Unknown | Ocmp c, vl => eval_static_condition_val c vl | _, _ => Unknown end. +Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) := + match addr, vl with + | Aindexed n, I n1::nil => I (Int.add n1 n) + | Aindexed n, G id ofs::nil => G id (Int.add ofs n) + | Aindexed n, S ofs::nil => S (Int.add ofs n) + | Aindexed2, I n1::I n2::nil => I (Int.add n1 n2) + | Aindexed2, G id ofs::I n2::nil => G id (Int.add ofs n2) + | Aindexed2, I n1::G id ofs::nil => G id (Int.add ofs n1) + | Aindexed2, S ofs::I n2::nil => S (Int.add ofs n2) + | Aindexed2, I n1::S ofs::nil => S (Int.add ofs n1) + | Aglobal id ofs, nil => G id ofs + | Abased id ofs, I n1::nil => G id (Int.add ofs n1) + | Ainstack ofs, nil => S ofs + | _, _ => Unknown + end. + (** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 3b5021e2..1c050bdb 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -118,6 +118,8 @@ Proof. case (eval_static_operation_match op al); intros; InvVLMA; simpl in *; FuncInv; try subst v; auto. + destruct (propagate_float_constants tt); simpl; auto. + rewrite shift_symbol_address; auto. rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. auto. @@ -149,6 +151,8 @@ Proof. unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0. simpl; auto. + destruct (propagate_float_constants tt); simpl; auto. + unfold eval_static_condition_val, Val.of_optbool. destruct (eval_static_condition c vl0) as []_eqn. rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). @@ -156,6 +160,26 @@ Proof. simpl; auto. Qed. +Lemma eval_static_addressing_correct: + forall addr al vl v, + val_list_match_approx al vl -> + eval_addressing ge sp addr vl = Some v -> + val_match_approx (eval_static_addressing addr al) v. +Proof. + intros until v. unfold eval_static_addressing. + case (eval_static_addressing_match addr al); intros; + InvVLMA; simpl in *; FuncInv; try subst v; auto. + rewrite shift_symbol_address; auto. + rewrite Val.add_assoc. auto. + repeat rewrite shift_symbol_address. auto. + fold (Val.add (Vint n1) (symbol_address ge id ofs)). + repeat rewrite shift_symbol_address. apply Val.add_commut. + repeat rewrite Val.add_assoc. auto. + fold (Val.add (Vint n1) (Val.add sp (Vint ofs))). + rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto. + rewrite shift_symbol_address. auto. +Qed. + (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml new file mode 100644 index 00000000..c16cd2f1 --- /dev/null +++ b/powerpc/Unusedglob1.ml @@ -0,0 +1,61 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Identifiers referenced from a PowerPC Asm instruction *) + +open Datatypes +open AST +open Asm + +let referenced_constant = function + | Cint n -> [] + | Csymbol_low(s, ofs) -> [s] + | Csymbol_high(s, ofs) -> [s] + | Csymbol_sda(s, ofs) -> [s] + +let referenced_builtin ef = + match ef with + | EF_vload_global(chunk, id, ofs) -> [id] + | EF_vstore_global(chunk, id, ofs) -> [id] + | _ -> [] + +let referenced_instr = function + | Pbl s -> [s] + | Pbs s -> [s] + | Paddi(_, _, c) + | Paddic(_, _, c) + | Paddis(_, _, c) + | Pandi_(_, _, c) + | Pandis_(_, _, c) + | Pcmplwi(_, c) + | Pcmpwi(_, c) + | Plbz(_, c, _) + | Plfd(_, c, _) + | Plfs(_, c, _) + | Plha(_, c, _) + | Plhz(_, c, _) + | Plwz(_, c, _) + | Pmulli(_, _, c) + | Pori(_, _, c) + | Poris(_, _, c) + | Pstb(_, c, _) + | Pstfd(_, c, _) + | Pstfs(_, c, _) + | Psth(_, c, _) + | Pstw(_, c, _) + | Psubfic(_, _, c) + | Pxori(_, _, c) + | Pxoris(_, _, c) -> referenced_constant c + | Pbuiltin(ef, _, _) -> referenced_builtin ef + | _ -> [] + +let code_of_function f = f -- cgit