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 --- Changelog | 9 +++++++++ arm/ConstpropOp.vp | 8 ++++++-- arm/ConstpropOpproof.v | 3 ++- arm/Op.v | 5 +++-- cfrontend/Cminorgenproof.v | 6 ++++-- cfrontend/Csem.v | 8 ++++++-- cfrontend/Initializersproof.v | 8 ++++---- common/Values.v | 16 ++++++++++++---- ia32/Asmgenproof1.v | 2 +- ia32/ConstpropOp.vp | 10 ++++++++-- ia32/ConstpropOpproof.v | 6 ++++-- ia32/Op.v | 14 ++++++++------ ia32/PrintAsm.ml | 12 +----------- powerpc/ConstpropOp.vp | 8 ++++++-- powerpc/ConstpropOpproof.v | 3 ++- powerpc/Op.v | 7 +++++-- 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. -- cgit