From bdbf444704c031a37039d4aeb2f19d05550afbd6 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Jun 2015 14:48:17 +0200
Subject: Signedness issue in specification of subtraction between two
 pointers.

---
 cfrontend/Cop.v               |  8 +++++---
 cfrontend/Cshmgen.v           |  2 +-
 cfrontend/Cshmgenproof.v      | 15 +++++++++++++--
 test/regression/Makefile      |  2 +-
 test/regression/Results/ptrs3 |  2 ++
 test/regression/ptrs3.c       | 10 ++++++++++
 6 files changed, 32 insertions(+), 7 deletions(-)
 create mode 100644 test/regression/Results/ptrs3
 create mode 100644 test/regression/ptrs3.c

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 6284660c..948ccaca 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -709,8 +709,10 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
       match v1,v2 with
       | Vptr b1 ofs1, Vptr b2 ofs2 =>
           if eq_block b1 b2 then
-            if Int.eq (Int.repr (sizeof cenv ty)) Int.zero then None
-            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof cenv ty))))
+            let sz := sizeof cenv ty in
+            if zlt 0 sz && zle sz Int.max_signed
+            then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz)))
+            else None
           else None
       | _, _ => None
       end
@@ -1216,7 +1218,7 @@ Proof.
   + inv H0; inv H1; inv H. TrivialInject.
     destruct (eq_block b1 b0); try discriminate. subst b1. 
     rewrite H0 in H2; inv H2. rewrite dec_eq_true. 
-    destruct (Int.eq (Int.repr (sizeof cenv ty)) Int.zero); inv H3.
+    destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3.
     rewrite Int.sub_shifted. TrivialInject.
   + inv H0; inv H1; inv H. TrivialInject.
     econstructor. eauto. rewrite Int.sub_add_l. auto.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index cb83731a..a80f4c15 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -260,7 +260,7 @@ Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2:
       OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
-      OK (Ebinop Odivu (Ebinop Osub e1 e2) n)
+      OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
   | sub_case_pl ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
       OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 025d7b66..c69d0c0a 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -490,8 +490,19 @@ Proof.
   destruct (classify_sub tya tyb); inv MAKE.
 - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - destruct va; try discriminate; destruct vb; inv SEM.
-  destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ce ty)) Int.zero) eqn:E; inv H0.
-  econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. 
+  destruct (eq_block b0 b1); try discriminate.
+  set (sz := sizeof ce ty) in *.
+  destruct (zlt 0 sz); try discriminate. 
+  destruct (zle sz Int.max_signed); simpl in H0; inv H0.
+  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. }
+  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. 
 - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 94c212d2..da7d5755 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \
   volatile1 volatile2 volatile3 \
   funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
   sizeof1 sizeof2 binops bool for1 switch switch2 compound \
-  decl1 interop1 bitfields9
+  decl1 interop1 bitfields9 ptrs3
 
 # Can run, but only in compiled mode, and have reference output in Results
 
diff --git a/test/regression/Results/ptrs3 b/test/regression/Results/ptrs3
new file mode 100644
index 00000000..17af0459
--- /dev/null
+++ b/test/regression/Results/ptrs3
@@ -0,0 +1,2 @@
+p - q = -9
+q - p = 9
diff --git a/test/regression/ptrs3.c b/test/regression/ptrs3.c
new file mode 100644
index 00000000..e0425af4
--- /dev/null
+++ b/test/regression/ptrs3.c
@@ -0,0 +1,10 @@
+#include <stdio.h>
+
+int main() { 
+  int a[10];
+  int *p = &a[0];
+  int *q = &a[9];
+  printf("p - q = %d\n", (int)(p - q));
+  printf("q - p = %d\n", (int)(q - p));
+  return 0;
+}
-- 
cgit