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 --- backend/Selectionproof.v | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d997015..d475f26 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -86,7 +86,7 @@ Lemma eval_base_condition_of_expr: eval_expr ge sp e m le a v -> Val.bool_of_val v b -> eval_condexpr ge sp e m le - (CEcond (Ccompimm Cne Int.zero) (a ::: Enil)) + (CEcond (Ccompuimm Cne Int.zero) (a ::: Enil)) b. Proof. intros. @@ -97,7 +97,7 @@ Qed. Lemma is_compare_neq_zero_correct: forall c v b, is_compare_neq_zero c = true -> - eval_condition c (v :: nil) = Some b -> + eval_condition c (v :: nil) m = Some b -> Val.bool_of_val v b. Proof. intros. @@ -107,17 +107,18 @@ Proof. simpl in H0. destruct v; inv H0. generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. constructor. + subst i; constructor. constructor; auto. simpl in H0. destruct v; inv H0. generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. subst i; constructor. constructor; auto. + constructor. Qed. Lemma is_compare_eq_zero_correct: forall c v b, is_compare_eq_zero c = true -> - eval_condition c (v :: nil) = Some b -> + eval_condition c (v :: nil) m = Some b -> Val.bool_of_val v (negb b). Proof. intros. apply is_compare_neq_zero_correct with (negate_condition c). @@ -145,8 +146,8 @@ Proof. eapply eval_base_condition_of_expr; eauto. inv H0. simpl in H7. - assert (eval_condition c vl = Some b). - destruct (eval_condition c vl); try discriminate. + assert (eval_condition c vl m = Some b). + destruct (eval_condition c vl m); try discriminate. destruct b0; inv H7; inversion H1; congruence. assert (eval_condexpr ge sp e m le (CEcond c e0) b). eapply eval_CEcond; eauto. @@ -230,7 +231,7 @@ Lemma eval_sel_binop: forall le op a1 a2 v1 v2 v, eval_expr ge sp e m le a1 v1 -> eval_expr ge sp e m le a2 v2 -> - eval_binop op v1 v2 = Some v -> + eval_binop op v1 v2 m = Some v -> eval_expr ge sp e m le (sel_binop op a1 a2) v. Proof. destruct op; simpl; intros; FuncInv; try subst v. @@ -263,13 +264,15 @@ Proof. apply eval_subf; auto. apply eval_mulf; auto. apply eval_divf; auto. - apply eval_comp_int; auto. - eapply eval_comp_int_ptr; eauto. - eapply eval_comp_ptr_int; eauto. + apply eval_comp; auto. + eapply eval_compu_int; eauto. + eapply eval_compu_int_ptr; eauto. + eapply eval_compu_ptr_int; eauto. + destruct (Mem.valid_pointer m b (Int.unsigned i) && + Mem.valid_pointer m b0 (Int.unsigned i0)) as [] _eqn; try congruence. destruct (eq_block b b0); inv H1. - eapply eval_comp_ptr_ptr; eauto. - eapply eval_comp_ptr_ptr_2; eauto. - eapply eval_compu; eauto. + eapply eval_compu_ptr_ptr; eauto. + eapply eval_compu_ptr_ptr_2; eauto. eapply eval_compf; eauto. Qed. -- cgit v1.2.3