From 3c605199ab0d096cd66ba671a4e23eac9e79bbc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 6 Oct 2016 11:01:34 +0200 Subject: Regression: handling of integer + pointer in CompCert C During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented. On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does. --- cfrontend/Cop.v | 78 +++++++++++++++++++++++---------------- cfrontend/Cshmgen.v | 41 ++++++++++++--------- cfrontend/Cshmgenproof.v | 96 ++++++++++++++++++++---------------------------- cfrontend/Ctyping.v | 12 ++---- 4 files changed, 112 insertions(+), 115 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 8defd9d9..c395a2cb 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -627,20 +627,16 @@ Definition sem_binarith Inductive classify_add_cases : Type := | add_case_pi (ty: type) (si: signedness) (**r pointer, int *) | add_case_pl (ty: type) (**r pointer, long *) -(* | add_case_ip (si: signedness) (ty: type) (**r int, pointer *) | add_case_lp (ty: type) (**r long, pointer *) -*) | add_default. (**r numerical type, numerical type *) Definition classify_add (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with | Tpointer ty _, Tint _ si _ => add_case_pi ty si | Tpointer ty _, Tlong _ _ => add_case_pl ty -(* | Tint _ si _, Tpointer ty _ => add_case_ip si ty | Tlong _ _, Tpointer ty _ => add_case_lp ty -*) | _, _ => add_default end. @@ -650,32 +646,42 @@ Definition ptrofs_of_int (si: signedness) (n: int) : ptrofs := | Unsigned => Ptrofs.of_intu n end. +Definition sem_add_ptr_int (cenv: composite_env) (ty: type) (si: signedness) (v1 v2: val): option val := + match v1, v2 with + | Vptr b1 ofs1, Vint n2 => + let n2 := ptrofs_of_int si n2 in + Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) + | Vint n1, Vint n2 => + if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vint n2 => + let n2 := cast_int_long si n2 in + if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None + | _, _ => None + end. + +Definition sem_add_ptr_long (cenv: composite_env) (ty: type) (v1 v2: val): option val := + match v1, v2 with + | Vptr b1 ofs1, Vlong n2 => + let n2 := Ptrofs.of_int64 n2 in + Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) + | Vint n1, Vlong n2 => + let n2 := Int.repr (Int64.unsigned n2) in + if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vlong n2 => + if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None + | _, _ => None + end. + Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val := match classify_add t1 t2 with | add_case_pi ty si => (**r pointer plus integer *) - match v1, v2 with - | Vptr b1 ofs1, Vint n2 => - let n2 := ptrofs_of_int si n2 in - Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) - | Vint n1, Vint n2 => - if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | Vlong n1, Vint n2 => - let n2 := cast_int_long si n2 in - if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None - | _, _ => None - end - | add_case_pl ty => (**r pointer plus long *) - match v1, v2 with - | Vptr b1 ofs1, Vlong n2 => - let n2 := Ptrofs.of_int64 n2 in - Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) - | Vint n1, Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | Vlong n1, Vlong n2 => - if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None - | _, _ => None - end + sem_add_ptr_int cenv ty si v1 v2 + | add_case_pl ty => (**r pointer plus long *) + sem_add_ptr_long cenv ty v1 v2 + | add_case_ip si ty => (**r integer plus pointer *) + sem_add_ptr_int cenv ty si v2 v1 + | add_case_lp ty => (**r long plus pointer *) + sem_add_ptr_long cenv ty v2 v1 | add_default => sem_binarith (fun sg n1 n2 => Some(Vint(Int.add n1 n2))) @@ -1285,11 +1291,19 @@ Lemma sem_binary_operation_inj: Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) - unfold sem_add in *; destruct (classify_add ty1 ty2). - + inv H0; inv H1; TrivialInject. - econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. - + inv H0; inv H1; TrivialInject. - econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. + assert (A: forall cenv ty si v1' v2' tv1' tv2', + Val.inject f v1' tv1' -> Val.inject f v2' tv2' -> + sem_add_ptr_int cenv ty si v1' v2' = Some v -> + exists tv, sem_add_ptr_int cenv ty si tv1' tv2' = Some tv /\ Val.inject f v tv). + { intros. unfold sem_add_ptr_int in *; inv H2; inv H3; TrivialInject. + econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. } + assert (B: forall cenv ty v1' v2' tv1' tv2', + Val.inject f v1' tv1' -> Val.inject f v2' tv2' -> + sem_add_ptr_long cenv ty v1' v2' = Some v -> + exists tv, sem_add_ptr_long cenv ty tv1' tv2' = Some tv /\ Val.inject f v tv). + { intros. unfold sem_add_ptr_long in *; inv H2; inv H3; TrivialInject. + econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. } + unfold sem_add in *; destruct (classify_add ty1 ty2); eauto. + eapply sem_binarith_inject; eauto; intros; exact I. - (* sub *) unfold sem_sub in *; destruct (classify_sub ty1 ty2). diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 4e7aca8a..aeb31fe2 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -240,26 +240,31 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation) | bin_default => Error (msg "Cshmgen.make_binarith") end. +Definition make_add_ptr_int (ce: composite_env) (ty: type) (si: signedness) (e1 e2: expr) := + do sz <- sizeof ce ty; + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Oaddl e1 (Ebinop Omull n (make_longofint e2 si))) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Oadd e1 (Ebinop Omul n e2)). + +Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) := + do sz <- sizeof ce ty; + if Archi.ptr64 then + let n := make_longconst (Int64.repr sz) in + OK (Ebinop Oaddl e1 (Ebinop Omull n e2)) + else + let n := make_intconst (Int.repr sz) in + OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))). + Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with - | add_case_pi ty si => - do sz <- sizeof ce ty; - if Archi.ptr64 then - let n := make_longconst (Int64.repr sz) in - OK (Ebinop Oaddl e1 (Ebinop Omull n (make_longofint e2 si))) - else - let n := make_intconst (Int.repr sz) in - OK (Ebinop Oadd e1 (Ebinop Omul n e2)) - | add_case_pl ty => - do sz <- sizeof ce ty; - if Archi.ptr64 then - let n := make_longconst (Int64.repr sz) in - OK (Ebinop Oaddl e1 (Ebinop Omull n e2)) - else - let n := make_intconst (Int.repr sz) in - OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) - | add_default => - make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 + | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2 + | add_case_pl ty => make_add_ptr_long ce ty e1 e2 + | add_case_ip si ty => make_add_ptr_int ce ty si e2 e1 + | add_case_lp ty => make_add_ptr_long ce ty e2 e1 + | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 end. Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 4f8632f2..09e31cb2 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -619,66 +619,50 @@ 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. + assert (A: forall ty si a b c e le m va vb v, + make_add_ptr_int cunit.(prog_comp_env) ty si a b = OK c -> + eval_expr ge e le m a va -> eval_expr ge e le m b vb -> + sem_add_ptr_int (prog_comp_env prog) ty si va vb = Some v -> + eval_expr ge e le m c v). + { unfold make_add_ptr_int, sem_add_ptr_int; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE. + 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. f_equal. f_equal. 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. f_equal. f_equal. f_equal. + assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). + auto with ptrofs. + } + assert (B: forall ty a b c e le m va vb v, + make_add_ptr_long cunit.(prog_comp_env) ty a b = OK c -> + eval_expr ge e le m a va -> eval_expr ge e le m b vb -> + sem_add_ptr_long (prog_comp_env prog) ty va vb = Some v -> + eval_expr ge e le m c v). + { unfold make_add_ptr_long, sem_add_ptr_long; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE. + 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. f_equal. f_equal. f_equal. auto with ptrofs. + - destruct va; InvEval; destruct vb; inv SEM. + + eauto with cshm. + + econstructor; eauto with cshm. + simpl. rewrite SF. f_equal. f_equal. f_equal. + assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). + auto with ptrofs. + } red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_add tya tyb); try (monadInv MAKE). -- 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. apply f_equal. apply f_equal. apply 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. apply f_equal. apply f_equal. apply 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. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. -+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. - econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. - assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). - auto with ptrofs. + destruct (classify_add tya tyb); eauto. - eapply make_binarith_correct; eauto; intros; auto. Qed. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 521ae519..ba1d34fb 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -113,19 +113,13 @@ Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type := match op with | Oadd => match classify_add ty1 ty2 with - | add_case_pi ty _ (*| add_case_ip ty*) - | add_case_pl ty (*| add_case_lp ty*) => OK (Tpointer ty noattr) + | add_case_pi ty _ | add_case_ip _ ty + | add_case_pl ty | add_case_lp ty => OK (Tpointer ty noattr) | add_default => binarith_type ty1 ty2 "operator +" end | Osub => match classify_sub ty1 ty2 with | sub_case_pi ty _ | sub_case_pl ty => OK (Tpointer ty noattr) -(* - | sub_case_pp ty1 ty2 => - if type_eq (remove_attributes ty1) (remove_attributes ty2) - then OK (Tint I32 Signed noattr) - else Error (msg "operator - : incompatible pointer types") -*) | sub_case_pp ty => OK ptrdiff_t | sub_default => binarith_type ty1 ty2 "operator infix -" end @@ -1504,7 +1498,7 @@ Proof. intros until m; intros TY SEM WT1 WT2. destruct op; simpl in TY; simpl in SEM. - (* add *) - unfold sem_add in SEM; DestructCases; auto with ty. + unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty. eapply pres_sem_binarith; eauto; intros; exact I. - (* sub *) unfold sem_sub in SEM; DestructCases; auto with ty. -- cgit