Make min_int / -1 and min_int % -1 semantically undefined

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

16 files changed, 81 insertions, 44 deletions

diff --git a/Changelog b/Changelog
index d1e7e4c4..c63dc66c 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,12 @@
+
+- In accordance with ISO C standards, the signed division min_int / -1
+  and the signed remainder min_int % -1 (where min_int is the smallest
+  representable signed integer) now have undefined semantics and are
+  treated as "going wrong" behaviors.
+  (Previously, they were defined with results min_int and 0 respectively,
+  but this behavior requires unnatural code to be generated on IA32 and
+  PowerPC.)	
+
 Release 1.10, 2012-03-13
 ========================
 
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index c0a04f0b..0f06703c 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -112,8 +112,12 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1)
   | Orsubimm n, I n1 :: nil => I (Int.sub n n1)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
-  | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
-  | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
+  | Odiv, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else
+      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
+      else I(Int.divs n1 n2)
+  | Odivu, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
   | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
   | Oandshift s, I n1 :: I n2 :: nil => I(Int.and n1 (eval_static_shift s n2))
   | Oandimm n, I n1 :: nil => I(Int.and n1 n)
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 242f29b0..4c38d5ea 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -138,7 +138,8 @@ Proof.
   rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
   rewrite Val.sub_add_opp. rewrite Val.add_assoc. rewrite Int.sub_add_opp. auto.
   rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
-  destruct (Int.eq n2 Int.zero); inv H0. simpl; auto.
+  destruct (Int.eq n2 Int.zero). inv H0.
+    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
   destruct (Int.eq n2 Int.zero); inv H0. simpl; auto.
   destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
   destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
diff --git a/arm/Op.v b/arm/Op.v
index 3353416f..fa05288a 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -383,7 +383,8 @@ Proof with (try exact I).
   generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; intuition. destruct (zeq b0 b)...
   destruct v0...
   destruct v0; destruct v1...
-  destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
+  destruct v0; destruct v1; simpl in H0; inv H0.
+    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
   destruct v0; destruct v1; simpl in H0; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
   destruct v0; destruct v1...
   generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto.
@@ -841,7 +842,7 @@ Proof.
 
   inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
 
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index f7256624..9de6b326 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1459,11 +1459,13 @@ Proof.
     rewrite zeq_true. rewrite Int.sub_shifted. auto.
   inv H; inv H0; inv H1; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
-    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+    destruct (Int.eq i0 Int.zero
+      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
     destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
-    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+    destruct (Int.eq i0 Int.zero
+      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
     destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
   inv H; inv H0; inv H1; TrivialExists.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 9087aa4c..ac7a58f6 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -300,7 +300,9 @@ Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   | div_case_ii Signed =>
       match v1,v2 with
        | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero then None else Some (Vint(Int.divs n1 n2))
+          if Int.eq n2 Int.zero
+          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
+          then None else Some (Vint(Int.divs n1 n2))
       | _,_ => None
       end
   | div_case_ff =>
@@ -333,7 +335,9 @@ Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   | binint_case_ii Signed =>
       match v1,v2 with
       | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
+          if Int.eq n2 Int.zero
+          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
+          then None else Some (Vint (Int.mods n1 n2))
       | _, _ => None
       end
   | binint_default =>
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 37f15cfe..76f08f31 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -367,15 +367,15 @@ Proof.
   unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
 (* div *)
   unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
   inv H11. constructor.
   inv H11. constructor.
   inv H11. constructor.
 (* mod *)
   unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
 (* and *)
   unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
 (* or *)
diff --git a/common/Values.v b/common/Values.v
index 1e274ad2..f0b125a1 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -218,14 +218,20 @@ Definition mul (v1 v2: val): val :=
 Definition divs (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some(Vint(Int.divs n1 n2))
+      if Int.eq n2 Int.zero
+      || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
+      then None
+      else Some(Vint(Int.divs n1 n2))
   | _, _ => None
   end.
 
 Definition mods (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some(Vint(Int.mods n1 n2))
+      if Int.eq n2 Int.zero
+      || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
+      then None
+      else Some(Vint(Int.mods n1 n2))
   | _, _ => None
   end.
 
@@ -656,7 +662,8 @@ Theorem mods_divs:
   mods x y = Some z -> exists v, divs x y = Some v /\ z = sub x (mul v y).
 Proof.
   intros. destruct x; destruct y; simpl in *; try discriminate.
-  destruct (Int.eq i0 Int.zero); inv H. 
+  destruct (Int.eq i0 Int.zero
+        || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H.
   exists (Vint (Int.divs i i0)); split; auto. 
   simpl. rewrite Int.mods_divs. auto.
 Qed.
@@ -679,7 +686,8 @@ Theorem divs_pow2:
   shrx x (Vint logn) = Some y.
 Proof.
   intros; destruct x; simpl in H1; inv H1.
-  destruct (Int.eq n Int.zero); inv H3. 
+  destruct (Int.eq n Int.zero
+         || Int.eq i (Int.repr Int.min_signed) && Int.eq n Int.mone); inv H3.
   simpl. rewrite H0. decEq. decEq. symmetry. apply Int.divs_pow2. auto.
 Qed.
 
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 5749a0b3..7b3427bc 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -744,7 +744,7 @@ Remark divs_mods_exist:
   end.
 Proof.
   intros. unfold Val.divs, Val.mods. destruct v1; auto. destruct v2; auto.
-  destruct (Int.eq i0 Int.zero); auto. 
+  destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto. 
 Qed.
 
 Remark divu_modu_exist:
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index b95ad669..a5e4e0d2 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -107,9 +107,15 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
   | Omulimm n, I n1 :: nil => I(Int.mul n1 n)
-  | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
+  | Odiv, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else
+      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
+      else I(Int.divs n1 n2)
   | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
-  | Omod, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.mods n1 n2)
+  | Omod, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else
+      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
+      else I(Int.mods n1 n2)
   | Omodu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.modu n1 n2)
   | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
   | Oandimm n, I n1 :: nil => I(Int.and n1 n)
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 1612bf69..ca38f6b8 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -143,9 +143,11 @@ Proof.
   InvVLMA; simpl in *; FuncInv; try subst v; auto.
   destruct (propagate_float_constants tt); simpl; auto.
   rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto.
+  destruct (Int.eq n2 Int.zero). inv H0. 
+    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
   destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
+  destruct (Int.eq n2 Int.zero). inv H0. 
+    destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
   destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
   destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
   destruct (Int.ltu n Int.iwordsize); simpl; auto.
diff --git a/ia32/Op.v b/ia32/Op.v
index 0b32b88e..9fdafe14 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -361,9 +361,11 @@ Proof with (try exact I).
   destruct v0; destruct v1... simpl. destruct (zeq b b0)...
   destruct v0; destruct v1...
   destruct v0...
+  destruct v0; destruct v1; simpl in *; inv H0.
+    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
   destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
-  destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
-  destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
+  destruct v0; destruct v1; simpl in *; inv H0.
+    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
   destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
   destruct v0; destruct v1...
   destruct v0...
@@ -837,12 +839,12 @@ Proof.
     rewrite Int.sub_shifted. auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
-  inv H4; inv H3; simpl in H1; inv H1. simpl. 
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
-  inv H4; inv H3; simpl in H1; inv H1. simpl. 
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
   inv H4; inv H2; simpl; auto.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index e9a44eb4..4e7c916c 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -591,18 +591,8 @@ let print_instruction oc = function
       fprintf oc "	xorl	%%edx, %%edx\n";
       fprintf oc "	divl	%a\n" ireg r1
   | Pidiv(r1) ->
-      let lbl1 = new_label() in
-      let lbl2 = new_label() in
-      fprintf oc "	cmpl	$-1, %a\n" ireg r1;
-      fprintf oc "	je	%a\n" label lbl1;
       fprintf oc "	cltd\n";
-      fprintf oc "	idivl	%a\n" ireg r1;
-      fprintf oc "	jmp	%a\n" label lbl2;
-      (* Division by -1 can cause an overflow trap if dividend = min_int.
-         Force x div (-1) = -x and x mod (-1) = 0. *)
-      fprintf oc "%a:	negl	%a\n" label lbl1 ireg EAX;
-      fprintf oc "	xorl	%a, %a\n" ireg EDX ireg EDX;
-      fprintf oc "%a:\n" label lbl2
+      fprintf oc "	idivl	%a\n" ireg r1
   | Pand_rr(rd, r1) ->
       fprintf oc "	andl	%a, %a\n" ireg r1 ireg rd
   | Pand_ri(rd, n) ->
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 60b5c63c..c39ccdb1 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -95,8 +95,12 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osubimm n, I n1 :: nil => I (Int.sub n n1)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
   | Omulimm n, I n1 :: nil => I(Int.mul n1 n)
-  | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
-  | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
+  | Odiv, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else
+      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
+      else I(Int.divs n1 n2)
+  | Odivu, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
   | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
   | Oandimm n, I n1 :: nil => I(Int.and n1 n)
   | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 1c050bdb..eef39448 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -139,7 +139,8 @@ Proof.
 
   rewrite Val.sub_add_opp. rewrite Val.add_assoc. simpl. rewrite Int.sub_add_opp. auto.
 
-  destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
+  destruct (Int.eq n2 Int.zero). inv H0. 
+  destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto.
   destruct (Int.eq n2 Int.zero); inv H0; simpl; auto.
 
   destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 986ea8c4..353c51c9 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -333,7 +333,9 @@ Proof with (try exact I).
   destruct v0...
   destruct v0; destruct v1...
   destruct v0...
-  destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
+  destruct v0; destruct v1; simpl in *; inv H0.
+    destruct (Int.eq i0 Int.zero
+         || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
   destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
   destruct v0; destruct v1...
   destruct v0...
@@ -758,7 +760,8 @@ Proof.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+    destruct (Int.eq i0 Int.zero
+         || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
   inv H4; inv H2; simpl; auto.