From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Op.v | 327 +++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 230 insertions(+), 97 deletions(-) (limited to 'powerpc/Op.v') diff --git a/powerpc/Op.v b/powerpc/Op.v index 6f05e550..d4669613 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -32,6 +32,7 @@ Require Import Values. Require Import Memdata. Require Import Memory. Require Import Globalenvs. +Require Import Events. Set Implicit Arguments. @@ -141,27 +142,30 @@ Definition eval_compare_mismatch (c: comparison) : option bool := Definition eval_compare_null (c: comparison) (n: int) : option bool := if Int.eq n Int.zero then eval_compare_mismatch c else None. -Definition eval_condition (cond: condition) (vl: list val): +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) - | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if eq_block b1 b2 - then Some (Int.cmp c n1 n2) - else eval_compare_mismatch c - | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil => - eval_compare_null c n2 - | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => - eval_compare_null c n1 | 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) - | Ccompimm c n, Vptr b1 n1 :: nil => - eval_compare_null c 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 => @@ -182,7 +186,7 @@ Definition offset_sp (sp: val) (delta: int) : option val := Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) - (op: operation) (vl: list val): option 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) @@ -251,7 +255,7 @@ Definition eval_operation | Ofloatofwords, Vint i1 :: Vint i2 :: nil => Some (Vfloat (Float.from_words i1 i2)) | Ocmp c, _ => - match eval_condition c vl with + match eval_condition c vl m with | None => None | Some false => Some Vfalse | Some true => Some Vtrue @@ -327,21 +331,23 @@ Proof. Qed. Lemma eval_negate_condition: - forall (cond: condition) (vl: list val) (b: bool), - eval_condition cond vl = Some b -> - eval_condition (negate_condition cond) vl = Some (negb b). + 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 (eq_block b0 b1). rewrite Int.negate_cmp. congruence. + 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_cmpu. auto. rewrite Int.negate_cmp. auto. - apply eval_negate_compare_null; auto. rewrite Int.negate_cmpu. auto. + apply eval_negate_compare_null; auto. auto. rewrite negb_elim. auto. auto. @@ -362,8 +368,8 @@ 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, - eval_operation ge2 sp op vl = eval_operation ge1 sp op vl. + 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; @@ -483,9 +489,9 @@ Variable A V: Type. Variable genv: Genv.t A V. Lemma type_of_operation_sound: - forall op vl sp v, + forall op vl sp v m, op <> Omove -> - eval_operation genv sp op vl = Some v -> + eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). Proof. intros. @@ -643,14 +649,16 @@ Proof. Qed. Lemma eval_condition_weaken: - forall c vl b, - eval_condition c vl = Some b -> + forall c vl b m, + eval_condition c vl m = Some b -> eval_condition_total c vl = Val.of_bool b. 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. @@ -659,8 +667,8 @@ Proof. Qed. Lemma eval_operation_weaken: - forall sp op vl v, - eval_operation genv sp op vl = Some v -> + forall sp op vl v m, + eval_operation genv sp op vl m = Some v -> eval_operation_total sp op vl = v. Proof. intros. @@ -680,7 +688,7 @@ Proof. 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); intros; rewrite H0 in H. + 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. @@ -746,12 +754,20 @@ Ltac InvLessdef := end. Lemma eval_condition_lessdef: - forall cond vl1 vl2 b, + forall cond vl1 vl2 b m1 m2, Val.lessdef_list vl1 vl2 -> - eval_condition cond vl1 = Some b -> - eval_condition cond vl2 = Some b. + Mem.extends m1 m2 -> + 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. Qed. Ltac TrivialExists := @@ -762,33 +778,34 @@ Ltac TrivialExists := end. Lemma eval_operation_lessdef: - forall sp op vl1 vl2 v1, + forall sp op vl1 vl2 v1 m1 m2, Val.lessdef_list vl1 vl2 -> - eval_operation genv sp op vl1 = Some v1 -> - exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2. + Mem.extends m1 m2 -> + 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 H0. TrivialExists. + 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 H0. TrivialExists. - destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + 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 H0. TrivialExists. - caseEq (eval_condition c vl1); intros. rewrite H1 in H0. - rewrite (eval_condition_lessdef c H H1). - destruct b; inv H0; TrivialExists. - rewrite H1 in H0. discriminate. + 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. Qed. Lemma eval_addressing_lessdef: @@ -805,6 +822,159 @@ 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. + +Variable F V: Type. +Variable genv: Genv.t F V. +Variable f: meminj. +Hypothesis globals: meminj_preserves_globals genv f. +Variable sp1: block. +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. + +Lemma eval_condition_inject: + forall cond vl1 vl2 b m1 m2, + val_list_inject f vl1 vl2 -> + Mem.inject f m1 m2 -> + 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. +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 -> + eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> + exists v2, + 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. +Qed. + +Lemma eval_operation_inject: + forall op vl1 vl2 v1 m1 m2, + val_list_inject f vl1 vl2 -> + Mem.inject f m1 m2 -> + eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + exists v2, + 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. +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 @@ -816,10 +986,10 @@ End EVAL_LESSDEF. 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, + 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 = 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; @@ -849,57 +1019,20 @@ Definition is_trivial_op (op: operation) : bool := | _ => false end. -(** 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. +(** Operations that depend on the memory state. *) -Definition shift_stack_operation (delta: int) (op: operation) := +Definition op_depends_on_memory (op: operation) : bool := match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) - | _ => op + | Ocmp (Ccompu _) => true + | _ => false end. -Lemma shift_stack_eval_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args delta, - eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args = - eval_addressing ge sp addr args. -Proof. - intros. destruct addr; simpl; auto. - destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. - decEq. decEq. rewrite <- Int.add_assoc. decEq. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. - rewrite Int.sub_idem. apply Int.add_zero. -Qed. - -Lemma shift_stack_eval_operation: - forall (F V: Type) (ge: Genv.t F V) sp op args delta, - eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args = - eval_operation ge sp op args. +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. destruct op; simpl; auto. - destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. - decEq. decEq. rewrite <- Int.add_assoc. decEq. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. - rewrite Int.sub_idem. apply Int.add_zero. + intros until m2. destruct op; simpl; try congruence. + destruct c; simpl; congruence. Qed. - -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. - - - -- cgit