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.

4 files changed, 112 insertions, 115 deletions

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.