From f3250c32ff42ae18fd03a5311c1f0caec3415aba Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Jun 2012 08:49:06 +0000 Subject: 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 --- ia32/Asmgenproof1.v | 2 +- ia32/ConstpropOp.vp | 10 ++++++++-- ia32/ConstpropOpproof.v | 6 ++++-- ia32/Op.v | 14 ++++++++------ ia32/PrintAsm.ml | 12 +----------- 5 files changed, 22 insertions(+), 22 deletions(-) (limited to 'ia32') 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) -> -- cgit