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

5 files changed, 22 insertions, 22 deletions

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) ->