From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- cfrontend/Cshmgenproof.v | 465 ++++++++++++++++++++++++++++++++--------------- 1 file changed, 323 insertions(+), 142 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 8bc97b99..3a35b87e 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -245,6 +245,19 @@ Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. +Lemma make_ptrofsconst_correct: + forall n e le m, + eval_expr ge e le m (make_ptrofsconst n) (Vptrofs (Ptrofs.repr n)). +Proof. + intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF. +- replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n). + apply make_longconst_correct. + symmetry; auto with ptrofs. +- replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n). + apply make_intconst_correct. + symmetry; auto with ptrofs. +Qed. + Lemma make_singleoffloat_correct: forall a n e le m, eval_expr ge e le m a (Vfloat n) -> @@ -276,38 +289,62 @@ Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correc Hint Constructors eval_expr eval_exprlist: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. -Lemma make_cmp_ne_zero_correct: +Lemma make_cmpu_ne_zero_correct: forall e le m a n, eval_expr ge e le m a (Vint n) -> - eval_expr ge e le m (make_cmp_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)). + eval_expr ge e le m (make_cmpu_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)). Proof. intros. - assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmp Cne) a (make_intconst Int.zero)) + assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) (Vint (if Int.eq n Int.zero then Int.zero else Int.one))). - econstructor; eauto with cshm. simpl. unfold Val.cmp, Val.cmp_bool. - unfold Int.cmp. destruct (Int.eq n Int.zero); auto. + { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Int.cmpu. destruct (Int.eq n Int.zero); auto. } assert (CMP: forall ob, Val.of_optbool ob = Vint n -> n = (if Int.eq n Int.zero then Int.zero else Int.one)). - intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. + { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. rewrite Int.eq_false. auto. apply Int.one_not_zero. - rewrite Int.eq_true. auto. + rewrite Int.eq_true. auto. } destruct a; simpl; auto. destruct b; auto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. inv H6. unfold Val.cmp in H0. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. inv H6. unfold Val.cmp in H0. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. inv H6. unfold Val.cmp in H0. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. - simpl in H6. unfold Val.cmpfs in H6. - destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. inv H6. eauto. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpl in H6. destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. +- inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmplu in H6. - destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [[]|]; inv H6; reflexivity. +Qed. + +Lemma make_cmpu_ne_zero_correct_ptr: + forall e le m a b i, + eval_expr ge e le m a (Vptr b i) -> + Archi.ptr64 = false -> + Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true -> + eval_expr ge e le m (make_cmpu_ne_zero a) Vone. +Proof. + intros. + assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone). + { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in H1. rewrite H0, H1. + rewrite Int.eq_true; auto. } + assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)). + { intros. destruct ob as [[]|]; discriminate. } + assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)). + { intros. destruct ob as [[]|]; discriminate. } + destruct a; simpl; auto. destruct b0; auto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_OPTBOOL; eauto. +- inv H; eelim OF_BOOL; eauto. +- inv H; eelim OF_BOOL; eauto. Qed. Lemma make_cast_int_correct: @@ -320,10 +357,27 @@ Proof. destruct si; eauto with cshm. destruct si; eauto with cshm. auto. - apply make_cmp_ne_zero_correct; auto. + apply make_cmpu_ne_zero_correct; auto. Qed. -Hint Resolve make_cast_int_correct: cshm. +Lemma make_longofint_correct: + forall e le m a n si, + eval_expr ge e le m a (Vint n) -> + eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)). +Proof. + intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. +Qed. + +Hint Resolve make_cast_int_correct make_longofint_correct: cshm. + +Ltac InvEval := + match goal with + | [ H: None = Some _ |- _ ] => discriminate + | [ H: Some _ = Some _ |- _ ] => inv H; InvEval + | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval + | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval + | _ => idtac + end. Lemma make_cast_correct: forall e le m a b v ty1 ty2 v', @@ -333,59 +387,51 @@ Lemma make_cast_correct: eval_expr ge e le m b v'. Proof. intros. unfold make_cast, sem_cast in *; - destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm. - (* single -> int *) + destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm. +- (* single -> int *) unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. - (* float -> int *) - destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. +- (* float -> int *) apply make_cast_int_correct. - unfold cast_float_int in E. unfold make_intoffloat. - destruct si2; econstructor; eauto; simpl; rewrite E; auto. - (* single -> int *) - destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2. + unfold cast_float_int in Heqo. unfold make_intoffloat. + destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto. +- (* single -> int *) apply make_cast_int_correct. - unfold cast_single_int in E. unfold make_intofsingle. - destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. - (* long -> int *) - unfold make_longofint, cast_int_long. destruct si1; eauto with cshm. - (* long -> float *) + unfold cast_single_int in Heqo. unfold make_intofsingle. + destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto. +- (* long -> float *) unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm. - (* long -> single *) +- (* long -> single *) unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm. - (* float -> long *) - destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. - unfold cast_float_long in E. unfold make_longoffloat. - destruct si2; econstructor; eauto; simpl; rewrite E; auto. - (* single -> long *) - destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2. - unfold cast_single_long in E. unfold make_longofsingle. - destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. - (* float -> bool *) +- (* float -> long *) + unfold cast_float_long in Heqo. unfold make_longoffloat. + destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto. +- (* single -> long *) + unfold cast_single_long in Heqo. unfold make_longofsingle. + destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto. +- (* int -> bool *) + apply make_cmpu_ne_zero_correct; auto. +- (* pointer (32 bits) -> bool *) + eapply make_cmpu_ne_zero_correct_ptr; eauto. +- (* long -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. + destruct (Int64.eq i Int64.zero); auto. +- (* pointer (64 bits) -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1. + rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity. +- (* float -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f Float.zero); auto. - (* single -> bool *) +- (* single -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f Float32.zero); auto. - (* long -> bool *) - econstructor; eauto with cshm. - simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp. - destruct (Int64.eq i Int64.zero); auto. - (* int -> bool *) - econstructor; eauto with cshm. - simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. - destruct (Int.eq i Int.zero); auto. - (* pointer -> bool *) - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2. - econstructor; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true. - unfold Mem.weak_valid_pointer in VALID; rewrite VALID. - auto. - (* struct *) - destruct (ident_eq id1 id2); inv H2; auto. - (* union *) - destruct (ident_eq id1 id2); inv H2; auto. +- (* struct *) + destruct (ident_eq id1 id2); inv H1; auto. +- (* union *) + destruct (ident_eq id1 id2); inv H1; auto. Qed. Lemma make_boolean_correct: @@ -397,29 +443,28 @@ Lemma make_boolean_correct: /\ Val.bool_of_val vb b. Proof. intros. unfold make_boolean. unfold bool_val in H0. - destruct (classify_bool ty); destruct v; inv H0. -(* int *) - econstructor; split. apply make_cmp_ne_zero_correct with (n := i); auto. + destruct (classify_bool ty); destruct v; InvEval. +- (* int *) + econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto. destruct (Int.eq i Int.zero); simpl; constructor. -(* float *) +- (* ptr 32 bits *) + exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. +- (* long *) + econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto. + destruct (Int64.eq i Int64.zero); simpl; constructor. +- (* ptr 64 bits *) + exists Vone; split. + econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. + unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity. + constructor. +- (* float *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero); constructor. -(* single *) +- (* single *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. destruct (Float32.cmp Cne f Float32.zero); constructor. -(* pointer *) - econstructor; split. econstructor; eauto with cshm. simpl. eauto. - unfold Val.cmpu, Val.cmpu_bool. simpl. - destruct (Int.eq i Int.zero); simpl; constructor. - econstructor; split. econstructor; eauto with cshm. simpl. eauto. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. - unfold Val.cmpu, Val.cmpu_bool. simpl. - unfold Mem.weak_valid_pointer in V; rewrite V. constructor. -(* long *) - econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. - destruct (Int64.eq i Int64.zero); simpl; constructor. Qed. Lemma make_neg_correct: @@ -454,11 +499,24 @@ Lemma make_notbool_correct: eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. - unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; - destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. - econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. - unfold Mem.weak_valid_pointer in V; rewrite V. auto. + unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1. + destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval. +- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. + destruct (Int.eq i Int.zero); auto. +- destruct Archi.ptr64 eqn:SF; inv SEM. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto. +- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. + destruct (Int64.eq i Int64.zero); auto. +- destruct Archi.ptr64 eqn:SF; inv SEM. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. + unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto. +- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. + destruct (Float.cmp Ceq f Float.zero); auto. +- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. + destruct (Float32.cmp Ceq f Float32.zero); auto. Qed. Lemma make_notint_correct: @@ -561,19 +619,66 @@ End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. +(* +Lemma eqm_ptrofs_of_int: + forall si i, + Ptrofs.eqm (Ptrofs.unsigned (ptrofs_of_int si i)) + (match si with Signed => Int.signed i | Unsigned => Int.unsigned i end). +Proof. + intros. unfold ptrofs_of_int. destruct si; apply Ptrofs.eqm_sym; apply Ptrofs.eqm_unsigned_repr. +Qed. + +Lemma ptrofs_mul_32: + forall si n i, + Archi.ptr64 = false -> + Ptrofs.of_int (Int.mul (Int.repr n) i) = Ptrofs.mul (Ptrofs.repr n) (ptrofs_of_int si i). +Proof. + intros. apply Ptrofs.eqm_samerepr. + eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ]. + apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Ptrofs.eqm_sym. eapply Ptrofs.eqm_trans. apply eqm_ptrofs_of_int. + apply -> Val.ptrofs_eqm_32; auto. destruct si. apply Int.eqm_signed_unsigned. apply Int.eqm_refl. +Qed. + +Lemma ptrofs_mul_32_64: + forall n i, + Archi.ptr64 = false -> + Ptrofs.of_int (Int.mul (Int.repr n) (Int64.loword i)) = Ptrofs.mul (Ptrofs.repr n) (Ptrofs.of_int64 i). +Proof. + intros. apply Ptrofs.eqm_samerepr. + eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ]. + apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r. + unfold Int64.loword. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. +Qed. +*) + Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)). Proof. red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_add tya tyb); try (monadInv MAKE). -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). + { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } + auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). + auto with ptrofs. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). + auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -582,25 +687,61 @@ Proof. red; unfold make_sub, sem_sub; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_sub tya tyb); try (monadInv MAKE). -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM. - destruct (eq_block b0 b1); try discriminate. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). + { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } + auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). + auto with ptrofs. +- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *. + destruct va; InvEval; destruct vb; InvEval. + destruct (eq_block b0 b1); try discriminate. destruct (zlt 0 sz); try discriminate. - destruct (zle sz Int.max_signed); simpl in H0; inv H0. + destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM. + assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz). + { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. } + destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c. ++ assert (E: Int64.signed (Int64.repr sz) = sz). + { apply Int64.signed_repr. + replace Int64.max_signed with Ptrofs.max_signed. + generalize Int64.min_signed_neg; omega. + unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. } econstructor; eauto with cshm. - rewrite dec_eq_true; simpl. - assert (E: Int.signed (Int.repr sz) = sz). - { apply Int.signed_repr. generalize Int.min_signed_neg; omega. } + rewrite SF, dec_eq_true. simpl. + predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero. + rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction. + predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone. + rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction. + rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal. + symmetry. auto with ptrofs. ++ assert (E: Int.signed (Int.repr sz) = sz). + { apply Int.signed_repr. + replace Int.max_signed with Ptrofs.max_signed. + generalize Int.min_signed_neg; omega. + unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. + } + econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. - rewrite andb_false_r; auto. -- rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. + rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal. + symmetry. auto with ptrofs. +- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. + simpl. rewrite SF. do 3 f_equal. + auto with ptrofs. ++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal. + assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). + auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -716,25 +857,61 @@ Proof. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. +Lemma make_cmp_ptr_correct: + forall cmp e le m a va b vb v, + cmp_ptr m cmp va vb = Some v -> + eval_expr ge e le m a va -> + eval_expr ge e le m b vb -> + eval_expr ge e le m (make_cmp_ptr cmp a b) v. +Proof. + unfold cmp_ptr, make_cmp_ptr; intros. + destruct Archi.ptr64. +- econstructor; eauto. +- econstructor; eauto. simpl. unfold Val.cmpu. + destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto. +Qed. + +Remark make_ptrofs_of_int_correct: + forall e le m a i si, + eval_expr ge e le m a (Vint i) -> + eval_expr ge e le m (if Archi.ptr64 then make_longofint a si else a) (Vptrofs (ptrofs_of_int si i)). +Proof. + intros. unfold Vptrofs, ptrofs_of_int. destruct Archi.ptr64 eqn:SF. +- unfold make_longofint. destruct si. ++ replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)). + eauto with cshm. + apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. ++ replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)). + eauto with cshm. + apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. +- destruct si. ++ replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto. + symmetry. auto with ptrofs. ++ replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto. + symmetry. auto with ptrofs. +Qed. + +Remark make_ptrofs_of_int64_correct: + forall e le m a i, + eval_expr ge e le m a (Vlong i) -> + eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (Vptrofs (Ptrofs.of_int64 i)). +Proof. + intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF. +- replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto. + symmetry. auto with ptrofs. +- econstructor; eauto. simpl. do 2 f_equal. + apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr. +Qed. + Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp). Proof. red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). -- inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; - simpl in SEM; inv SEM. - econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto. -- inv MAKE. destruct vb; try discriminate. - set (vb := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; - simpl in SEM; inv SEM. - econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb. - unfold Val.cmpu. rewrite E. auto. -- inv MAKE. destruct va; try discriminate. - set (va := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; - simpl in SEM; inv SEM. - econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va. - unfold Val.cmpu. rewrite E. auto. +- inv MAKE. eapply make_cmp_ptr_correct; eauto. +- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct. +- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct. +- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct. +- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -1042,49 +1219,53 @@ Lemma transl_expr_lvalue_correct: Csharpminor.eval_expr tge te le m ta (Vptr b ofs)). Proof. apply eval_expr_lvalue_ind; intros; try (monadInv TR). -(* const int *) +- (* const int *) apply make_intconst_correct. -(* const float *) +- (* const float *) apply make_floatconst_correct. -(* const single *) +- (* const single *) apply make_singleconst_correct. -(* const long *) +- (* const long *) apply make_longconst_correct. -(* temp var *) +- (* temp var *) constructor; auto. -(* addrof *) +- (* addrof *) simpl in TR. auto. -(* unop *) +- (* unop *) eapply transl_unop_correct; eauto. -(* binop *) +- (* binop *) eapply transl_binop_correct; eauto. -(* cast *) +- (* cast *) eapply make_cast_correct; eauto. -(* sizeof *) - rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct. -(* alignof *) - rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct. -(* rvalue out of lvalue *) +- (* sizeof *) + rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct. +- (* alignof *) + rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct. +- (* rvalue out of lvalue *) exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. eapply make_load_correct; eauto. -(* var local *) +- (* var local *) exploit (me_local _ _ MENV); eauto. intros EQ. econstructor. eapply eval_var_addr_local. eauto. -(* var global *) +- (* var global *) econstructor. eapply eval_var_addr_global. eapply match_env_globals; eauto. rewrite symbols_preserved. auto. -(* deref *) +- (* deref *) simpl in TR. eauto. -(* field struct *) +- (* field struct *) unfold make_field_access in EQ0. rewrite H1 in EQ0. destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0. exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. - rewrite <- B in EQ1. - eapply eval_Ebinop; eauto. - apply make_intconst_correct. - simpl. unfold ge in *; simpl in *. congruence. -(* field union *) + rewrite <- B in EQ1. + assert (x0 = delta) by (unfold ge in *; simpl in *; congruence). + subst x0. + destruct Archi.ptr64 eqn:SF. ++ eapply eval_Ebinop; eauto using make_longconst_correct. + simpl. rewrite SF. do 3 f_equal. auto with ptrofs. ++ eapply eval_Ebinop; eauto using make_intconst_correct. + simpl. rewrite SF. do 3 f_equal. auto with ptrofs. +- (* field union *) unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0. auto. Qed. -- cgit