From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Op.v | 1265 ++++++++++++++++++++++++++++------------------------------ 1 file changed, 605 insertions(+), 660 deletions(-) (limited to 'powerpc/Op.v') diff --git a/powerpc/Op.v b/powerpc/Op.v index 7bd42478..68b349ec 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -59,9 +59,7 @@ Inductive operation : Type := | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) - | Ocast8unsigned: operation (**r [rd] is 8-bit zero extension of [r1] *) | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) - | Ocast16unsigned: operation (**r [rd] is 16-bit zero extension of [r1] *) | Oadd: operation (**r [rd = r1 + r2] *) | Oaddimm: int -> operation (**r [rd = r1 + n] *) | Osub: operation (**r [rd = r1 - r2] *) @@ -131,138 +129,80 @@ Proof. decide equality. Qed. -(** Evaluation of conditions, operators and addressing modes applied - to lists of values. Return [None] when the computation is undefined: - wrong number of arguments, arguments of the wrong types, undefined - operations such as division by zero. [eval_condition] returns a boolean, - [eval_operation] and [eval_addressing] return a value. *) +(** * Evaluation functions *) -Definition eval_compare_mismatch (c: comparison) : option bool := - match c with Ceq => Some false | Cne => Some true | _ => None end. +Definition symbol_address (F V: Type) (genv: Genv.t F V) (id: ident) (ofs: int) : val := + match Genv.find_symbol genv id with + | Some b => Vptr b ofs + | None => Vundef + end. -Definition eval_compare_null (c: comparison) (n: int) : option bool := - if Int.eq n Int.zero then eval_compare_mismatch c else None. +(** Evaluation of conditions, operators and addressing modes applied + to lists of values. Return [None] when the computation can trigger an + error, e.g. integer division by zero. [eval_condition] returns a boolean, + [eval_operation] and [eval_addressing] return a value. *) -Definition eval_condition (cond: condition) (vl: list val) (m: mem): - option bool := +Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with - | Ccomp c, Vint n1 :: Vint n2 :: nil => - Some (Int.cmp c n1 n2) - | Ccompu c, Vint n1 :: Vint n2 :: nil => - Some (Int.cmpu c n1 n2) - | Ccompu c, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if Mem.valid_pointer m b1 (Int.unsigned n1) - && Mem.valid_pointer m b2 (Int.unsigned n2) then - if eq_block b1 b2 - then Some (Int.cmpu c n1 n2) - else eval_compare_mismatch c - else None - | Ccompu c, Vptr b1 n1 :: Vint n2 :: nil => - eval_compare_null c n2 - | Ccompu c, Vint n1 :: Vptr b2 n2 :: nil => - eval_compare_null c n1 - | Ccompimm c n, Vint n1 :: nil => - Some (Int.cmp c n1 n) - | Ccompuimm c n, Vint n1 :: nil => - Some (Int.cmpu c n1 n) - | Ccompuimm c n, Vptr b1 n1 :: nil => - eval_compare_null c n - | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil => - Some (Float.cmp c f1 f2) - | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil => - Some (negb (Float.cmp c f1 f2)) - | Cmaskzero n, Vint n1 :: nil => - Some (Int.eq (Int.and n1 n) Int.zero) - | Cmasknotzero n, Vint n1 :: nil => - Some (negb (Int.eq (Int.and n1 n) Int.zero)) - | _, _ => - None - end. - -Definition offset_sp (sp: val) (delta: int) : option val := - match sp with - | Vptr b n => Some (Vptr b (Int.add n delta)) - | _ => None + | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 + | Ccompu c, v1 :: v2 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 + | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n) + | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n) + | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 + | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) + | Cmaskzero n, Vint n1 :: nil => Some (Int.eq (Int.and n1 n) Int.zero) + | Cmasknotzero n, Vint n1 :: nil => Some (negb (Int.eq (Int.and n1 n) Int.zero)) + | _, _ => None end. Definition eval_operation - (F V: Type) (genv: Genv.t F V) (sp: val) - (op: operation) (vl: list val) (m: mem): option val := + (F V: Type) (genv: Genv.t F V) (sp: val) + (op: operation) (vl: list val) (m: mem): option val := match op, vl with | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) - | Oaddrsymbol s ofs, nil => - match Genv.find_symbol genv s with - | None => None - | Some b => Some (Vptr b ofs) - end - | Oaddrstack ofs, nil => offset_sp sp ofs - | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) - | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) - | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) - | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1) - | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) - | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) - | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) - | Oaddimm n, Vint n1 :: nil => Some (Vint (Int.add n1 n)) - | Oaddimm n, Vptr b1 n1 :: nil => Some (Vptr b1 (Int.add n1 n)) - | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2)) - | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2)) - | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None - | Osubimm n, Vint n1 :: nil => Some (Vint (Int.sub n n1)) - | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2)) - | Omulimm n, Vint n1 :: nil => Some (Vint (Int.mul n1 n)) - | Odiv, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) - | Odivu, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) - | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2)) - | Oandimm n, Vint n1 :: nil => Some (Vint (Int.and n1 n)) - | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2)) - | Oorimm n, Vint n1 :: nil => Some (Vint (Int.or n1 n)) - | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2)) - | Oxorimm n, Vint n1 :: nil => Some (Vint (Int.xor n1 n)) - | Onand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.and n1 n2))) - | Onor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.or n1 n2))) - | Onxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.xor n1 n2))) - | Oshl, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None - | Oshr, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None - | Oshrimm n, Vint n1 :: nil => - if Int.ltu n Int.iwordsize then Some (Vint (Int.shr n1 n)) else None - | Oshrximm n, Vint n1 :: nil => - if Int.ltu n Int.iwordsize then Some (Vint (Int.shrx n1 n)) else None - | Oshru, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None - | Orolm amount mask, Vint n1 :: nil => - Some (Vint (Int.rolm n1 amount mask)) - | Oroli amount mask, Vint n1 :: Vint n2 :: nil => - Some (Vint (Int.or (Int.and n1 (Int.not mask)) (Int.rolm n2 amount mask))) - | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) - | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) - | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) - | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) - | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) - | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) - | Omuladdf, Vfloat f1 :: Vfloat f2 :: Vfloat f3 :: nil => - Some (Vfloat (Float.add (Float.mul f1 f2) f3)) - | Omulsubf, Vfloat f1 :: Vfloat f2 :: Vfloat f3 :: nil => - Some (Vfloat (Float.sub (Float.mul f1 f2) f3)) - | Osingleoffloat, v1 :: nil => - Some (Val.singleoffloat v1) - | Ointoffloat, Vfloat f1 :: nil => - option_map Vint (Float.intoffloat f1) - | Ofloatofwords, Vint i1 :: Vint i2 :: nil => - Some (Vfloat (Float.from_words i1 i2)) - | Ocmp c, _ => - match eval_condition c vl m with - | None => None - | Some false => Some Vfalse - | Some true => Some Vtrue - end + | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs) + | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) + | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) + | Oadd, v1::v2::nil => Some (Val.add v1 v2) + | Oaddimm n, v1::nil => Some (Val.add v1 (Vint n)) + | Osub, v1::v2::nil => Some (Val.sub v1 v2) + | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1) + | Omul, v1::v2::nil => Some (Val.mul v1 v2) + | Omulimm n, v1::nil => Some (Val.mul v1 (Vint n)) + | Odiv, v1::v2::nil => Val.divs v1 v2 + | Odivu, v1::v2::nil => Val.divu v1 v2 + | Oand, v1::v2::nil => Some(Val.and v1 v2) + | Oandimm n, v1::nil => Some (Val.and v1 (Vint n)) + | Oor, v1::v2::nil => Some(Val.or v1 v2) + | Oorimm n, v1::nil => Some (Val.or v1 (Vint n)) + | Oxor, v1::v2::nil => Some(Val.xor v1 v2) + | Oxorimm n, v1::nil => Some (Val.xor v1 (Vint n)) + | Onand, v1::v2::nil => Some (Val.notint (Val.and v1 v2)) + | Onor, v1::v2::nil => Some (Val.notint (Val.or v1 v2)) + | Onxor, v1::v2::nil => Some (Val.notint (Val.xor v1 v2)) + | Oshl, v1::v2::nil => Some (Val.shl v1 v2) + | Oshr, v1::v2::nil => Some (Val.shr v1 v2) + | Oshrimm n, v1::nil => Some (Val.shr v1 (Vint n)) + | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) + | Oshru, v1::v2::nil => Some (Val.shru v1 v2) + | Orolm amount mask, v1::nil => Some (Val.rolm v1 amount mask) + | Oroli amount mask, v1::v2::nil => + Some(Val.or (Val.and v1 (Vint (Int.not mask))) (Val.rolm v2 amount mask)) + | Onegf, v1::nil => Some(Val.negf v1) + | Oabsf, v1::nil => Some(Val.absf v1) + | Oaddf, v1::v2::nil => Some(Val.addf v1 v2) + | Osubf, v1::v2::nil => Some(Val.subf v1 v2) + | Omulf, v1::v2::nil => Some(Val.mulf v1 v2) + | Odivf, v1::v2::nil => Some(Val.divf v1 v2) + | Omuladdf, v1::v2::v3::nil => Some(Val.addf (Val.mulf v1 v2) v3) + | Omulsubf, v1::v2::v3::nil => Some(Val.subf (Val.mulf v1 v2) v3) + | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) + | Ointoffloat, v1::nil => Val.intoffloat v1 + | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) + | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m)) | _, _ => None end. @@ -270,39 +210,14 @@ Definition eval_addressing (F V: Type) (genv: Genv.t F V) (sp: val) (addr: addressing) (vl: list val) : option val := match addr, vl with - | Aindexed n, Vptr b1 n1 :: nil => - Some (Vptr b1 (Int.add n1 n)) - | Aindexed2, Vptr b1 n1 :: Vint n2 :: nil => - Some (Vptr b1 (Int.add n1 n2)) - | Aindexed2, Vint n1 :: Vptr b2 n2 :: nil => - Some (Vptr b2 (Int.add n2 n1)) - | Aglobal s ofs, nil => - match Genv.find_symbol genv s with - | None => None - | Some b => Some (Vptr b ofs) - end - | Abased s ofs, Vint n1 :: nil => - match Genv.find_symbol genv s with - | None => None - | Some b => Some (Vptr b (Int.add ofs n1)) - end - | Ainstack ofs, nil => - offset_sp sp ofs + | Aindexed n, v1::nil => Some (Val.add v1 (Vint n)) + | Aindexed2, v1::v2::nil => Some (Val.add v1 v2) + | Aglobal s ofs, nil => Some (symbol_address genv s ofs) + | Abased s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1) + | Ainstack ofs, nil => Some(Val.add sp (Vint ofs)) | _, _ => None end. -Definition negate_condition (cond: condition): condition := - match cond with - | Ccomp c => Ccomp(negate_comparison c) - | Ccompu c => Ccompu(negate_comparison c) - | Ccompimm c n => Ccompimm (negate_comparison c) n - | Ccompuimm c n => Ccompuimm (negate_comparison c) n - | Ccompf c => Cnotcompf c - | Cnotcompf c => Ccompf c - | Cmaskzero n => Cmasknotzero n - | Cmasknotzero n => Cmaskzero n - end. - Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => @@ -315,103 +230,7 @@ Ltac FuncInv := idtac end. -Remark eval_negate_compare_mismatch: - forall c b, - eval_compare_mismatch c = Some b -> - eval_compare_mismatch (negate_comparison c) = Some (negb b). -Proof. - intros until b. unfold eval_compare_mismatch. - destruct c; intro EQ; inv EQ; auto. -Qed. - -Remark eval_negate_compare_null: - forall c i b, - eval_compare_null c i = Some b -> - eval_compare_null (negate_comparison c) i = Some (negb b). -Proof. - unfold eval_compare_null; intros. - destruct (Int.eq i Int.zero). apply eval_negate_compare_mismatch; auto. congruence. -Qed. - -Lemma eval_negate_condition: - forall cond vl m b, - eval_condition cond vl m = Some b -> - eval_condition (negate_condition cond) vl m = Some (negb b). -Proof. - intros. - destruct cond; simpl in H; FuncInv; try subst b; simpl. - rewrite Int.negate_cmp. auto. - rewrite Int.negate_cmpu. auto. - apply eval_negate_compare_null; auto. - apply eval_negate_compare_null; auto. - destruct (Mem.valid_pointer m b0 (Int.unsigned i) && - Mem.valid_pointer m b1 (Int.unsigned i0)); try congruence. - destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence. - apply eval_negate_compare_mismatch; auto. - rewrite Int.negate_cmp. auto. - rewrite Int.negate_cmpu. auto. - apply eval_negate_compare_null; auto. - auto. - rewrite negb_elim. auto. - auto. - rewrite negb_elim. auto. -Qed. - -(** [eval_operation] and [eval_addressing] depend on a global environment - for resolving references to global symbols. We show that they give - the same results if a global environment is replaced by another that - assigns the same addresses to the same symbols. *) - -Section GENV_TRANSF. - -Variable F1 F2 V1 V2: Type. -Variable ge1: Genv.t F1 V1. -Variable ge2: Genv.t F2 V2. -Hypothesis agree_on_symbols: - forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. - -Lemma eval_operation_preserved: - forall sp op vl m, - eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. -Proof. - intros. - unfold eval_operation; destruct op; try rewrite agree_on_symbols; - reflexivity. -Qed. - -Lemma eval_addressing_preserved: - forall sp addr vl, - eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl. -Proof. - intros. - unfold eval_addressing; destruct addr; try rewrite agree_on_symbols; - reflexivity. -Qed. - -End GENV_TRANSF. - -(** Recognition of move operations. *) - -Definition is_move_operation - (A: Type) (op: operation) (args: list A) : option A := - match op, args with - | Omove, arg :: nil => Some arg - | _, _ => None - end. - -Lemma is_move_operation_correct: - forall (A: Type) (op: operation) (args: list A) (a: A), - is_move_operation op args = Some a -> - op = Omove /\ args = a :: nil. -Proof. - intros until a. unfold is_move_operation; destruct op; - try (intros; discriminate). - destruct args. intros; discriminate. - destruct args. intros. intuition congruence. - intros; discriminate. -Qed. - -(** Static typing of conditions, operators and addressing modes. *) +(** * Static typing of conditions, operators and addressing modes. *) Definition type_of_condition (c: condition) : list typ := match c with @@ -433,9 +252,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oaddrsymbol _ _ => (nil, Tint) | Oaddrstack _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) - | Ocast8unsigned => (Tint :: nil, Tint) | Ocast16signed => (Tint :: nil, Tint) - | Ocast16unsigned => (Tint :: nil, Tint) | Oadd => (Tint :: Tint :: nil, Tint) | Oaddimm _ => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) @@ -497,38 +314,52 @@ Lemma type_of_operation_sound: op <> Omove -> eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). -Proof. +Proof with (try exact I). intros. - destruct op; simpl in H0; FuncInv; try subst v; try exact I. + destruct op; simpl in H0; FuncInv; subst; simpl. congruence. - destruct (Genv.find_symbol genv i); simplify_eq H0; intro; subst v; exact I. - simpl. unfold offset_sp in H0. destruct sp; try discriminate. - inversion H0. exact I. - destruct v0; exact I. - destruct v0; exact I. - destruct v0; exact I. - destruct v0; exact I. - destruct (eq_block b b0). injection H0; intro; subst v; exact I. - discriminate. - destruct (Int.eq i0 Int.zero). discriminate. - injection H0; intro; subst v; exact I. - destruct (Int.eq i0 Int.zero). discriminate. - injection H0; intro; subst v; exact I. - destruct (Int.ltu i0 Int.iwordsize). - injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 Int.iwordsize). - injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i Int.iwordsize). - injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i Int.iwordsize). - injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 Int.iwordsize). - injection H0; intro; subst v; exact I. discriminate. - destruct v0; exact I. - destruct (Float.intoffloat f); simpl in H0; inv H0. exact I. - destruct (eval_condition c vl). - destruct b; injection H0; intro; subst v; exact I. - discriminate. + exact I. + exact I. + unfold symbol_address. destruct (Genv.find_symbol genv i)... + destruct sp... + destruct v0... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... simpl. destruct (zeq b b0)... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... + destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... + destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... + destruct v0; simpl in *; inv H0. destruct (Int.ltu i (Int.repr 31)); inv H2... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1; destruct v2... + destruct v0; destruct v1; destruct v2... + destruct v0... + destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2... + destruct v0; destruct v1... + destruct (eval_condition c vl m); simpl... destruct b... Qed. Lemma type_of_chunk_correct: @@ -546,243 +377,436 @@ Qed. End SOUNDNESS. -(** Alternate definition of [eval_condition], [eval_op], [eval_addressing] - as total functions that return [Vundef] when not applicable - (instead of [None]). Used in the proof of [PPCgen]. *) - -Section EVAL_OP_TOTAL. +(** * Manipulating and transforming operations *) -Variable F V: Type. -Variable genv: Genv.t F V. +(** Recognition of move operations. *) -Definition find_symbol_offset (id: ident) (ofs: int) : val := - match Genv.find_symbol genv id with - | Some b => Vptr b ofs - | None => Vundef +Definition is_move_operation + (A: Type) (op: operation) (args: list A) : option A := + match op, args with + | Omove, arg :: nil => Some arg + | _, _ => None end. -Definition eval_condition_total (cond: condition) (vl: list val) : val := - match cond, vl with - | Ccomp c, v1::v2::nil => Val.cmp c v1 v2 - | Ccompu c, v1::v2::nil => Val.cmpu c v1 v2 - | Ccompimm c n, v1::nil => Val.cmp c v1 (Vint n) - | Ccompuimm c n, v1::nil => Val.cmpu c v1 (Vint n) - | Ccompf c, v1::v2::nil => Val.cmpf c v1 v2 - | Cnotcompf c, v1::v2::nil => Val.notbool(Val.cmpf c v1 v2) - | Cmaskzero n, v1::nil => Val.notbool (Val.and v1 (Vint n)) - | Cmasknotzero n, v1::nil => Val.notbool(Val.notbool (Val.and v1 (Vint n))) - | _, _ => Vundef +Lemma is_move_operation_correct: + forall (A: Type) (op: operation) (args: list A) (a: A), + is_move_operation op args = Some a -> + op = Omove /\ args = a :: nil. +Proof. + intros until a. unfold is_move_operation; destruct op; + try (intros; discriminate). + destruct args. intros; discriminate. + destruct args. intros. intuition congruence. + intros; discriminate. +Qed. + +(** [negate_condition cond] returns a condition that is logically + equivalent to the negation of [cond]. *) + +Definition negate_condition (cond: condition): condition := + match cond with + | Ccomp c => Ccomp(negate_comparison c) + | Ccompu c => Ccompu(negate_comparison c) + | Ccompimm c n => Ccompimm (negate_comparison c) n + | Ccompuimm c n => Ccompuimm (negate_comparison c) n + | Ccompf c => Cnotcompf c + | Cnotcompf c => Ccompf c + | Cmaskzero n => Cmasknotzero n + | Cmasknotzero n => Cmaskzero n end. -Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val := - match op, vl with - | Omove, v1::nil => v1 - | Ointconst n, nil => Vint n - | Ofloatconst n, nil => Vfloat n - | Oaddrsymbol s ofs, nil => find_symbol_offset s ofs - | Oaddrstack ofs, nil => Val.add sp (Vint ofs) - | Ocast8signed, v1::nil => Val.sign_ext 8 v1 - | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1 - | Ocast16signed, v1::nil => Val.sign_ext 16 v1 - | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1 - | Oadd, v1::v2::nil => Val.add v1 v2 - | Oaddimm n, v1::nil => Val.add v1 (Vint n) - | Osub, v1::v2::nil => Val.sub v1 v2 - | Osubimm n, v1::nil => Val.sub (Vint n) v1 - | Omul, v1::v2::nil => Val.mul v1 v2 - | Omulimm n, v1::nil => Val.mul v1 (Vint n) - | Odiv, v1::v2::nil => Val.divs v1 v2 - | Odivu, v1::v2::nil => Val.divu v1 v2 - | Oand, v1::v2::nil => Val.and v1 v2 - | Oandimm n, v1::nil => Val.and v1 (Vint n) - | Oor, v1::v2::nil => Val.or v1 v2 - | Oorimm n, v1::nil => Val.or v1 (Vint n) - | Oxor, v1::v2::nil => Val.xor v1 v2 - | Oxorimm n, v1::nil => Val.xor v1 (Vint n) - | Onand, v1::v2::nil => Val.notint(Val.and v1 v2) - | Onor, v1::v2::nil => Val.notint(Val.or v1 v2) - | Onxor, v1::v2::nil => Val.notint(Val.xor v1 v2) - | Oshl, v1::v2::nil => Val.shl v1 v2 - | Oshr, v1::v2::nil => Val.shr v1 v2 - | Oshrimm n, v1::nil => Val.shr v1 (Vint n) - | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) - | Oshru, v1::v2::nil => Val.shru v1 v2 - | Orolm amount mask, v1::nil => Val.rolm v1 amount mask - | Oroli amount mask, v1::v2::nil => - Val.or (Val.and v1 (Vint (Int.not mask))) (Val.rolm v2 amount mask) - | Onegf, v1::nil => Val.negf v1 - | Oabsf, v1::nil => Val.absf v1 - | Oaddf, v1::v2::nil => Val.addf v1 v2 - | Osubf, v1::v2::nil => Val.subf v1 v2 - | Omulf, v1::v2::nil => Val.mulf v1 v2 - | Odivf, v1::v2::nil => Val.divf v1 v2 - | Omuladdf, v1::v2::v3::nil => Val.addf (Val.mulf v1 v2) v3 - | Omulsubf, v1::v2::v3::nil => Val.subf (Val.mulf v1 v2) v3 - | Osingleoffloat, v1::nil => Val.singleoffloat v1 - | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ofloatofwords, v1::v2::nil => Val.floatofwords v1 v2 - | Ocmp c, _ => eval_condition_total c vl - | _, _ => Vundef +Lemma eval_negate_condition: + forall cond vl m b, + eval_condition cond vl m = Some b -> + eval_condition (negate_condition cond) vl m = Some (negb b). +Proof. + intros. + destruct cond; simpl in H; FuncInv; simpl. + rewrite Val.negate_cmp_bool; rewrite H; auto. + rewrite Val.negate_cmpu_bool; rewrite H; auto. + rewrite Val.negate_cmp_bool; rewrite H; auto. + rewrite Val.negate_cmpu_bool; rewrite H; auto. + rewrite H; auto. + destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. + rewrite H0; auto. + rewrite <- H0. rewrite negb_elim; auto. +Qed. + +(** Shifting stack-relative references. This is used in [Stacking]. *) + +Definition shift_stack_addressing (delta: int) (addr: addressing) := + match addr with + | Ainstack ofs => Ainstack (Int.add delta ofs) + | _ => addr end. -Definition eval_addressing_total - (sp: val) (addr: addressing) (vl: list val) : val := - match addr, vl with - | Aindexed n, v1::nil => Val.add v1 (Vint n) - | Aindexed2, v1::v2::nil => Val.add v1 v2 - | Aglobal s ofs, nil => find_symbol_offset s ofs - | Abased s ofs, v1::nil => Val.add (find_symbol_offset s ofs) v1 - | Ainstack ofs, nil => Val.add sp (Vint ofs) - | _, _ => Vundef +Definition shift_stack_operation (delta: int) (op: operation) := + match op with + | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | _ => op end. -Lemma eval_compare_mismatch_weaken: - forall c b, - eval_compare_mismatch c = Some b -> - Val.cmp_mismatch c = Val.of_bool b. +Lemma type_shift_stack_addressing: + forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. Proof. - unfold eval_compare_mismatch. intros. destruct c; inv H; auto. + intros. destruct addr; auto. Qed. -Lemma eval_compare_null_weaken: - forall n c b, - eval_compare_null c n = Some b -> - (if Int.eq n Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b. +Lemma type_shift_stack_operation: + forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. Proof. - unfold eval_compare_null. - intros. destruct (Int.eq n Int.zero). apply eval_compare_mismatch_weaken. auto. - discriminate. + intros. destruct op; auto. Qed. -Lemma eval_condition_weaken: - forall c vl b m, - eval_condition c vl m = Some b -> - eval_condition_total c vl = Val.of_bool b. +Lemma eval_shift_stack_addressing: + forall F V (ge: Genv.t F V) sp addr vl delta, + eval_addressing ge sp (shift_stack_addressing delta addr) vl = + eval_addressing ge (Val.add sp (Vint delta)) addr vl. Proof. - intros. - unfold eval_condition in H; destruct c; FuncInv; - try subst b; try reflexivity; simpl; - try (apply eval_compare_null_weaken; auto). - destruct (Mem.valid_pointer m b0 (Int.unsigned i) && - Mem.valid_pointer m b1 (Int.unsigned i0)); try congruence. - unfold eq_block in H. destruct (zeq b0 b1). - congruence. - apply eval_compare_mismatch_weaken; auto. - symmetry. apply Val.notbool_negb_1. - symmetry. apply Val.notbool_negb_1. + intros. destruct addr; simpl; auto. + rewrite Val.add_assoc. simpl. auto. Qed. -Lemma eval_operation_weaken: - forall sp op vl v m, - eval_operation genv sp op vl m = Some v -> - eval_operation_total sp op vl = v. +Lemma eval_shift_stack_operation: + forall F V (ge: Genv.t F V) sp op vl m delta, + eval_operation ge sp (shift_stack_operation delta op) vl m = + eval_operation ge (Val.add sp (Vint delta)) op vl m. Proof. - intros. - unfold eval_operation in H; destruct op; FuncInv; - try subst v; try reflexivity; simpl. - unfold find_symbol_offset. - destruct (Genv.find_symbol genv i); try discriminate. - congruence. - unfold offset_sp in H. - destruct sp; try discriminate. simpl. congruence. - unfold eq_block in H. destruct (zeq b b0); congruence. - destruct (Int.eq i0 Int.zero); congruence. - destruct (Int.eq i0 Int.zero); congruence. - destruct (Int.ltu i0 Int.iwordsize); congruence. - destruct (Int.ltu i0 Int.iwordsize); congruence. - destruct (Int.ltu i Int.iwordsize); congruence. - destruct (Int.ltu i Int.iwordsize); congruence. - destruct (Int.ltu i0 Int.iwordsize); congruence. - destruct (Float.intoffloat f); inv H. auto. - caseEq (eval_condition c vl m); intros; rewrite H0 in H. - replace v with (Val.of_bool b). - eapply eval_condition_weaken; eauto. - destruct b; simpl; congruence. - discriminate. + intros. destruct op; simpl; auto. + rewrite Val.add_assoc. simpl. auto. Qed. -Lemma eval_addressing_weaken: - forall sp addr vl v, - eval_addressing genv sp addr vl = Some v -> - eval_addressing_total sp addr vl = v. +(** Transformation of addressing modes with two operands or more + into an equivalent arithmetic operation. This is used in the [Reload] + pass when a store instruction cannot be reloaded directly because + it runs out of temporary registers. *) + +(** For the PowerPC, there is only one binary addressing mode: [Aindexed2]. + The corresponding operation is [Oadd]. *) + +Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. + +Lemma eval_op_for_binary_addressing: + forall (F V: Type) (ge: Genv.t F V) sp addr args v m, + (length args >= 2)%nat -> + eval_addressing ge sp addr args = Some v -> + eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. Proof. intros. - unfold eval_addressing in H; destruct addr; FuncInv; - try subst v; simpl; try reflexivity. - unfold find_symbol_offset. - destruct (Genv.find_symbol genv i); congruence. - unfold find_symbol_offset. - destruct (Genv.find_symbol genv i); try congruence. - inversion H. reflexivity. - unfold offset_sp in H. destruct sp; simpl; congruence. + destruct addr; simpl in H0; FuncInv; simpl in H; try omegaContradiction. + simpl; congruence. Qed. -Lemma eval_condition_total_is_bool: - forall cond vl, Val.is_bool (eval_condition_total cond vl). +Lemma type_op_for_binary_addressing: + forall addr, + (length (type_of_addressing addr) >= 2)%nat -> + type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). Proof. - intros; destruct cond; - destruct vl; try apply Val.undef_is_bool; - destruct vl; try apply Val.undef_is_bool; - try (destruct vl; try apply Val.undef_is_bool); simpl. - apply Val.cmp_is_bool. - apply Val.cmpu_is_bool. - apply Val.cmp_is_bool. - apply Val.cmpu_is_bool. - apply Val.cmpf_is_bool. - apply Val.notbool_is_bool. - apply Val.notbool_is_bool. - apply Val.notbool_is_bool. + intros. destruct addr; simpl in H; reflexivity || omegaContradiction. Qed. -End EVAL_OP_TOTAL. +(** Two-address operations. There is only one: rotate-mask-insert. *) -(** Compatibility of the evaluation functions with the - ``is less defined'' relation over values. *) +Definition two_address_op (op: operation) : bool := + match op with + | Oroli _ _ => true + | _ => false + end. -Section EVAL_LESSDEF. +(** Operations that are so cheap to recompute that CSE should not factor them out. *) + +Definition is_trivial_op (op: operation) : bool := + match op with + | Omove => true + | Ointconst _ => true + | Oaddrsymbol _ _ => true + | Oaddrstack _ => true + | _ => false + end. + +(** Operations that depend on the memory state. *) + +Definition op_depends_on_memory (op: operation) : bool := + match op with + | Ocmp (Ccompu _) => true + | _ => false + end. + +Lemma op_depends_on_memory_correct: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + op_depends_on_memory op = false -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op; simpl; try congruence. + destruct c; simpl; auto; discriminate. +Qed. + +(** * Invariance and compatibility properties. *) + +(** [eval_operation] and [eval_addressing] depend on a global environment + for resolving references to global symbols. We show that they give + the same results if a global environment is replaced by another that + assigns the same addresses to the same symbols. *) + +Section GENV_TRANSF. + +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. +Hypothesis agree_on_symbols: + forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. + +Lemma eval_operation_preserved: + forall sp op vl m, + eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. +Proof. + intros. destruct op; simpl; auto. + destruct vl; auto. decEq. unfold symbol_address. rewrite agree_on_symbols. auto. +Qed. + +Lemma eval_addressing_preserved: + forall sp addr vl, + eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl. +Proof. + intros. destruct addr; simpl; auto; unfold symbol_address; rewrite agree_on_symbols; auto. +Qed. + +End GENV_TRANSF. + +(** Compatibility of the evaluation functions with value injections. *) + +Section EVAL_COMPAT. Variable F V: Type. Variable genv: Genv.t F V. +Variable f: meminj. -Ltac InvLessdef := +Hypothesis symbol_address_inj: + forall id ofs, + val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs). + +Variable m1: mem. +Variable m2: mem. + +Hypothesis valid_pointer_inj: + forall b1 ofs b2 delta, + f b1 = Some(b2, delta) -> + Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + +Hypothesis valid_pointer_no_overflow: + forall b1 ofs b2 delta, + f b1 = Some(b2, delta) -> + Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> + 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + +Hypothesis valid_different_pointers_inj: + forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + b1 <> b2 -> + Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + f b1 = Some (b1', delta1) -> + f b2 = Some (b2', delta2) -> + b1' <> b2' \/ + Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + +Ltac InvInject := match goal with - | [ H: Val.lessdef (Vint _) _ |- _ ] => - inv H; InvLessdef - | [ H: Val.lessdef (Vfloat _) _ |- _ ] => - inv H; InvLessdef - | [ H: Val.lessdef (Vptr _ _) _ |- _ ] => - inv H; InvLessdef - | [ H: Val.lessdef_list nil _ |- _ ] => - inv H; InvLessdef - | [ H: Val.lessdef_list (_ :: _) _ |- _ ] => - inv H; InvLessdef + | [ H: val_inject _ (Vint _) _ |- _ ] => + inv H; InvInject + | [ H: val_inject _ (Vfloat _) _ |- _ ] => + inv H; InvInject + | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + inv H; InvInject + | [ H: val_list_inject _ nil _ |- _ ] => + inv H; InvInject + | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + inv H; InvInject | _ => idtac end. -Lemma eval_condition_lessdef: - forall cond vl1 vl2 b m1 m2, - Val.lessdef_list vl1 vl2 -> - Mem.extends m1 m2 -> +Remark val_add_inj: + forall v1 v1' v2 v2', + val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2'). +Proof. + intros. inv H; inv H0; simpl; econstructor; eauto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. +Qed. + +Lemma eval_condition_inj: + forall cond vl1 vl2 b, + val_list_inject f vl1 vl2 -> eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. - intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto. - destruct (Mem.valid_pointer m1 b0 (Int.unsigned i) && - Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate. - destruct (andb_prop _ _ Heqb2) as [A B]. - assert (forall b ofs, Mem.valid_pointer m1 b ofs = true -> Mem.valid_pointer m2 b ofs = true). - intros until ofs. repeat rewrite Mem.valid_pointer_nonempty_perm. - apply Mem.perm_extends; auto. - rewrite (H _ _ A). rewrite (H _ _ B). auto. +Opaque Int.add. + assert (CMPU: + forall c v1 v2 v1' v2' b, + val_inject f v1 v1' -> + val_inject f v2 v2' -> + Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b -> + Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b). + intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. + destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) as []_eqn; try discriminate. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) as []_eqn; try discriminate. + rewrite (valid_pointer_inj _ H2 Heqb4). + rewrite (valid_pointer_inj _ H Heqb0). simpl. + destruct (zeq b1 b0); simpl in H1. + inv H1. rewrite H in H2; inv H2. rewrite zeq_true. + decEq. apply Int.translate_cmpu. + eapply valid_pointer_no_overflow; eauto. + eapply valid_pointer_no_overflow; eauto. + exploit valid_different_pointers_inj; eauto. intros P. + destruct (zeq b2 b3); auto. + destruct P. congruence. + destruct c; simpl in H1; inv H1. + simpl; decEq. rewrite Int.eq_false; auto. congruence. + simpl; decEq. rewrite Int.eq_false; auto. congruence. + + intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. + inv H3; inv H2; simpl in H0; inv H0; auto. + eauto. + inv H3; simpl in H0; inv H0; auto. + eauto. + inv H3; inv H2; simpl in H0; inv H0; auto. + inv H3; inv H2; simpl in H0; inv H0; auto. Qed. Ltac TrivialExists := match goal with - | [ |- exists v2, Some ?v1 = Some v2 /\ Val.lessdef ?v1 v2 ] => - exists v1; split; [auto | constructor] + | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + exists v1; split; auto | _ => idtac end. +Lemma eval_operation_inj: + forall op sp1 vl1 sp2 vl2 v1, + val_inject f sp1 sp2 -> + val_list_inject f vl1 vl2 -> + eval_operation genv sp1 op vl1 m1 = Some v1 -> + exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. +Proof. + intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + inv H; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + inv H4; simpl; auto. + inv H4; simpl; auto. + apply val_add_inj; auto. + apply val_add_inj; auto. + inv H4; inv H2; simpl; auto. econstructor; eauto. + rewrite Int.sub_add_l. auto. + destruct (zeq b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite zeq_true. + rewrite Int.sub_shifted. auto. + inv H4; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. + inv H4; simpl in *; inv H1. destruct (Int.ltu i (Int.repr 31)); inv H2. econstructor; eauto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto; inv H2; simpl; auto; inv H3; simpl; auto. + inv H4; simpl; auto; inv H2; simpl; auto; inv H3; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2. + exists (Vint i); auto. + inv H4; inv H2; simpl; auto. + subst v1. destruct (eval_condition c vl1 m1) as []_eqn. + exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. + destruct b; simpl; constructor. + simpl; constructor. +Qed. + +Lemma eval_addressing_inj: + forall addr sp1 vl1 sp2 vl2 v1, + val_inject f sp1 sp2 -> + val_list_inject f vl1 vl2 -> + eval_addressing genv sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. +Proof. + intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply val_add_inj; auto. + apply val_add_inj; auto. + apply val_add_inj; auto. + apply val_add_inj; auto. +Qed. + +End EVAL_COMPAT. + +(** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) + +Section EVAL_LESSDEF. + +Variable F V: Type. +Variable genv: Genv.t F V. + +Remark valid_pointer_extends: + forall m1 m2, Mem.extends m1 m2 -> + forall b1 ofs b2 delta, + Some(b1, 0) = Some(b2, delta) -> + Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. +Proof. + intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. +Qed. + +Remark valid_pointer_no_overflow_extends: + forall m1 b1 ofs b2 delta, + Some(b1, 0) = Some(b2, delta) -> + Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> + 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. +Proof. + intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2. +Qed. + +Remark valid_different_pointers_extends: + forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + b1 <> b2 -> + Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Some(b1, 0) = Some (b1', delta1) -> + Some(b2, 0) = Some (b2', delta2) -> + b1' <> b2' \/ + Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)). +Proof. + intros. inv H2; inv H3. auto. +Qed. + +Lemma eval_condition_lessdef: + forall cond vl1 vl2 b m1 m2, + Val.lessdef_list vl1 vl2 -> + Mem.extends m1 m2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. +Proof. + intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1). + apply valid_pointer_extends; auto. + apply valid_pointer_no_overflow_extends; auto. + apply valid_different_pointers_extends; auto. + rewrite <- val_list_inject_lessdef. eauto. auto. +Qed. + Lemma eval_operation_lessdef: forall sp op vl1 vl2 v1 m1 m2, Val.lessdef_list vl1 vl2 -> @@ -790,28 +814,18 @@ Lemma eval_operation_lessdef: eval_operation genv sp op vl1 m1 = Some v1 -> exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists. - exists v2; auto. - destruct (Genv.find_symbol genv i); inv H1. TrivialExists. - exists v1; auto. - exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto. - exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto. - exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto. - exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto. - destruct (eq_block b b0); inv H1. TrivialExists. - destruct (Int.eq i0 Int.zero); inv H1; TrivialExists. - destruct (Int.eq i0 Int.zero); inv H1; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. - exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. - destruct (Float.intoffloat f); simpl in *; inv H1. TrivialExists. - caseEq (eval_condition c vl1 m1); intros. rewrite H2 in H1. - rewrite (eval_condition_lessdef c H H0 H2). - destruct b; inv H1; TrivialExists. - rewrite H2 in H1. discriminate. + intros. rewrite val_list_inject_lessdef in H. + assert (exists v2 : val, + eval_operation genv sp op vl2 m2 = Some v2 + /\ val_inject (fun b => Some(b, 0)) v1 v2). + eapply eval_operation_inj with (m1 := m1) (sp1 := sp). + intros. rewrite <- val_inject_lessdef; auto. + apply valid_pointer_extends; auto. + apply valid_pointer_no_overflow_extends; auto. + apply valid_different_pointers_extends; auto. + rewrite <- val_inject_lessdef; auto. + eauto. auto. + destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. Lemma eval_addressing_lessdef: @@ -820,40 +834,19 @@ Lemma eval_addressing_lessdef: eval_addressing genv sp addr vl1 = Some v1 -> exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2. Proof. - intros. destruct addr; simpl in *; FuncInv; InvLessdef; TrivialExists. - destruct (Genv.find_symbol genv i); inv H0. TrivialExists. - destruct (Genv.find_symbol genv i); inv H0. TrivialExists. - exists v1; auto. + intros. rewrite val_list_inject_lessdef in H. + assert (exists v2 : val, + eval_addressing genv sp addr vl2 = Some v2 + /\ val_inject (fun b => Some(b, 0)) v1 v2). + eapply eval_addressing_inj with (sp1 := sp). + intros. rewrite <- val_inject_lessdef; auto. + rewrite <- val_inject_lessdef; auto. + eauto. auto. + destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. End EVAL_LESSDEF. -(** Shifting stack-relative references. This is used in [Stacking]. *) - -Definition shift_stack_addressing (delta: int) (addr: addressing) := - match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) - | _ => addr - end. - -Definition shift_stack_operation (delta: int) (op: operation) := - match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) - | _ => op - end. - -Lemma type_shift_stack_addressing: - forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. -Proof. - intros. destruct addr; auto. -Qed. - -Lemma type_shift_stack_operation: - forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. -Proof. - intros. destruct op; auto. -Qed. - (** Compatibility of the evaluation functions with memory injections. *) Section EVAL_INJECT. @@ -867,20 +860,13 @@ Variable sp2: block. Variable delta: Z. Hypothesis sp_inj: f sp1 = Some(sp2, delta). -Ltac InvInject := - match goal with - | [ H: val_inject _ (Vint _) _ |- _ ] => - inv H; InvInject - | [ H: val_inject _ (Vfloat _) _ |- _ ] => - inv H; InvInject - | [ H: val_inject _ (Vptr _ _) _ |- _ ] => - inv H; InvInject - | [ H: val_list_inject _ nil _ |- _ ] => - inv H; InvInject - | [ H: val_list_inject _ (_ :: _) _ |- _ ] => - inv H; InvInject - | _ => idtac - end. +Remark symbol_address_inject: + forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs). +Proof. + intros. unfold symbol_address. destruct (Genv.find_symbol genv id) as []_eqn; auto. + exploit (proj1 globals); eauto. intros. + econstructor; eauto. rewrite Int.add_zero; auto. +Qed. Lemma eval_condition_inject: forall cond vl1 vl2 b m1 m2, @@ -889,35 +875,12 @@ Lemma eval_condition_inject: eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. - intros. destruct cond; simpl in *; FuncInv; InvInject; auto. - destruct (Mem.valid_pointer m1 b0 (Int.unsigned i)) as [] _eqn; try discriminate. - destruct (Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate. - simpl in H1. - exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. - intros V1. rewrite V1. - exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb2. econstructor; eauto. - intros V2. rewrite V2. - simpl. - destruct (eq_block b0 b1); inv H1. - rewrite H3 in H5; inv H5. rewrite dec_eq_true. - decEq. apply Int.translate_cmpu. - eapply Mem.valid_pointer_inject_no_overflow; eauto. - eapply Mem.valid_pointer_inject_no_overflow; eauto. - exploit Mem.different_pointers_inject; eauto. intros P. - destruct (eq_block b3 b4); auto. - destruct P. contradiction. - destruct c; unfold eval_compare_mismatch in *; inv H2. - unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. - unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. + intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. Qed. -Ltac TrivialExists2 := - match goal with - | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => - exists v1; split; [auto | econstructor; eauto] - | _ => idtac - end. - Lemma eval_addressing_inject: forall addr vl1 vl2 v1, val_list_inject f vl1 vl2 -> @@ -926,15 +889,10 @@ Lemma eval_addressing_inject: eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - destruct (Genv.find_symbol genv i) as [] _eqn; inv H0. - TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. - destruct (Genv.find_symbol genv i) as [] _eqn; inv H0. - TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + intros. + rewrite eval_shift_stack_addressing. simpl. + eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. + exact symbol_address_inject. Qed. Lemma eval_operation_inject: @@ -946,102 +904,89 @@ Lemma eval_operation_inject: eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct op; simpl in *; FuncInv; InvInject; TrivialExists2. - exists v'; auto. - destruct (Genv.find_symbol genv i) as [] _eqn; inv H1. - TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - exists (Val.sign_ext 8 v'); split; auto. inv H4; simpl; auto. - exists (Val.zero_ext 8 v'); split; auto. inv H4; simpl; auto. - exists (Val.sign_ext 16 v'); split; auto. inv H4; simpl; auto. - exists (Val.zero_ext 16 v'); split; auto. inv H4; simpl; auto. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - rewrite Int.sub_add_l. auto. - destruct (eq_block b b0); inv H1. rewrite H3 in H5; inv H5. rewrite dec_eq_true. - rewrite Int.sub_shifted. TrivialExists2. - destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. - destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. - destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. - destruct (Int.ltu i0 Int.iwordsize); inv H2. TrivialExists2. - destruct (Int.ltu i0 Int.iwordsize); inv H2. TrivialExists2. - destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. - destruct (Int.ltu i Int.iwordsize); inv H1. TrivialExists2. - destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2. - destruct (Int.ltu i Int.iwordsize); inv H2. TrivialExists2. - destruct (Int.ltu i Int.iwordsize); inv H2. TrivialExists2. - destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. - exists (Val.singleoffloat v'); split; auto. inv H4; simpl; auto. - destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists2. - destruct (eval_condition c vl1 m1) as [] _eqn; try discriminate. - exploit eval_condition_inject; eauto. intros EQ; rewrite EQ. - destruct b; inv H1; TrivialExists2. + intros. + rewrite eval_shift_stack_operation. simpl. + eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. + exact symbol_address_inject. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. Qed. End EVAL_INJECT. -(** Transformation of addressing modes with two operands or more - into an equivalent arithmetic operation. This is used in the [Reload] - pass when a store instruction cannot be reloaded directly because - it runs out of temporary registers. *) - -(** For the PowerPC, there is only one binary addressing mode: [Aindexed2]. - The corresponding operation is [Oadd]. *) - -Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. - -Lemma eval_op_for_binary_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args v m, - (length args >= 2)%nat -> - eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. -Proof. - intros. - unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; - simpl; congruence. -Qed. - -Lemma type_op_for_binary_addressing: - forall addr, - (length (type_of_addressing addr) >= 2)%nat -> - type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). -Proof. - intros. destruct addr; simpl in H; reflexivity || omegaContradiction. -Qed. - -(** Two-address operations. There is only one: rotate-mask-insert. *) +(** * Masks for rotate and mask instructions *) + +(** Recognition of integers that are acceptable as immediate operands + to the [rlwim] PowerPC instruction. These integers are of the form + [000011110000] or [111100001111], that is, a run of one bits + surrounded by zero bits, or conversely. We recognize these integers by + running the following automaton on the bits. The accepting states are + 2, 3, 4, 5, and 6. +<< + 0 1 0 + / \ / \ / \ + \ / \ / \ / + -0--> [1] --1--> [2] --0--> [3] + / + [0] + \ + -1--> [4] --0--> [5] --1--> [6] + / \ / \ / \ + \ / \ / \ / + 1 0 1 +>> +*) -Definition two_address_op (op: operation) : bool := - match op with - | Oroli _ _ => true - | _ => false +Inductive rlw_state: Type := + | RLW_S0 : rlw_state + | RLW_S1 : rlw_state + | RLW_S2 : rlw_state + | RLW_S3 : rlw_state + | RLW_S4 : rlw_state + | RLW_S5 : rlw_state + | RLW_S6 : rlw_state + | RLW_Sbad : rlw_state. + +Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state := + match s, b with + | RLW_S0, false => RLW_S1 + | RLW_S0, true => RLW_S4 + | RLW_S1, false => RLW_S1 + | RLW_S1, true => RLW_S2 + | RLW_S2, false => RLW_S3 + | RLW_S2, true => RLW_S2 + | RLW_S3, false => RLW_S3 + | RLW_S3, true => RLW_Sbad + | RLW_S4, false => RLW_S5 + | RLW_S4, true => RLW_S4 + | RLW_S5, false => RLW_S5 + | RLW_S5, true => RLW_S6 + | RLW_S6, false => RLW_Sbad + | RLW_S6, true => RLW_S6 + | RLW_Sbad, _ => RLW_Sbad end. -(** Operations that are so cheap to recompute that CSE should not factor them out. *) - -Definition is_trivial_op (op: operation) : bool := - match op with - | Omove => true - | Ointconst _ => true - | Oaddrsymbol _ _ => true - | Oaddrstack _ => true - | _ => false +Definition rlw_accepting (s: rlw_state) : bool := + match s with + | RLW_S0 => false + | RLW_S1 => false + | RLW_S2 => true + | RLW_S3 => true + | RLW_S4 => true + | RLW_S5 => true + | RLW_S6 => true + | RLW_Sbad => false end. -(** Operations that depend on the memory state. *) - -Definition op_depends_on_memory (op: operation) : bool := - match op with - | Ocmp (Ccompu _) => true - | _ => false +Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := + match n with + | O => + rlw_accepting s + | S m => + let (b, y) := Int.Z_bin_decomp x in + is_rlw_mask_rec m (rlw_transition s b) y end. -Lemma op_depends_on_memory_correct: - forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, - op_depends_on_memory op = false -> - eval_operation ge sp op args m1 = eval_operation ge sp op args m2. -Proof. - intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; congruence. -Qed. +Definition is_rlw_mask (x: int) : bool := + is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x). -- cgit