Commit bdbf4447 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Signedness issue in specification of subtraction between two pointers.

parent ff625877
......@@ -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.
......
......@@ -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)))
......
......@@ -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.
......
......@@ -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
......
#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;
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment