From 41b7ecb127b93b1aecc29a298ec21dc94603e6fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Jul 2013 12:10:11 +0000 Subject: Optimize integer divisions by positive constants, turning them into multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 6 +- Changelog | 2 + Makefile | 4 +- arm/Asm.v | 28 +- arm/Asmgen.v | 18 +- arm/Asmgenproof1.v | 7 +- arm/ConstpropOp.vp | 3 + arm/Op.v | 10 + arm/PrintAsm.ml | 10 +- arm/SelectOp.vp | 41 +- arm/SelectOpproof.v | 108 +-- backend/SelectDiv.vp | 156 ++++ backend/SelectDivproof.v | 547 ++++++++++++++ backend/SelectLongproof.v | 2 +- backend/Selection.v | 1 + backend/Selectionproof.v | 2 + common/Values.v | 12 + ia32/Asm.v | 8 + ia32/Asmgen.v | 8 + ia32/Asmgenproof1.v | 4 + ia32/ConstpropOp.vp | 2 + ia32/Machregs.v | 6 + ia32/Op.v | 10 + ia32/PrintAsm.ml | 4 + ia32/SelectOp.vp | 11 +- ia32/SelectOpproof.v | 41 +- lib/Integers.v | 28 + powerpc/Asm.v | 6 + powerpc/Asmgen.v | 6 + powerpc/ConstpropOp.vp | 2 + powerpc/Op.v | 10 + powerpc/PrintAsm.ml | 4 + powerpc/SelectOp.vp | 32 +- powerpc/SelectOpproof.v | 74 +- test/regression/Results/int32 | 1620 +++++++++++++++++++++++++++++++++++++++++ test/regression/int32.c | 12 + 36 files changed, 2663 insertions(+), 182 deletions(-) create mode 100644 backend/SelectDiv.vp create mode 100644 backend/SelectDivproof.v diff --git a/.depend b/.depend index 17db282..ca707a4 100644 --- a/.depend +++ b/.depend @@ -30,11 +30,13 @@ backend/Cminor.vo backend/Cminor.glob backend/Cminor.v.beautified: backend/Cmino $(ARCH)/Op.vo $(ARCH)/Op.glob $(ARCH)/Op.v.beautified: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)/SelectOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo +backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo -backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo +backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo $(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo -backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectLongproof.vo +backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo backend/Registers.vo backend/Registers.glob backend/Registers.v.beautified: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo backend/RTL.vo backend/RTL.glob backend/RTL.v.beautified: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTLgen.vo backend/RTLgen.glob backend/RTLgen.v.beautified: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo diff --git a/Changelog b/Changelog index a7151c6..657cb03 100644 --- a/Changelog +++ b/Changelog @@ -1,6 +1,8 @@ Development trunk: ================== +- Optimize integer divisions by positive constants, turning them into + multiply-high and shifts. - Avoid double rounding issues in conversion from 64-bit integers to single-precision floats. - PowerPC: more efficient implementation of division on 64-bit integers. diff --git a/Makefile b/Makefile index 76938b4..1694457 100644 --- a/Makefile +++ b/Makefile @@ -75,8 +75,8 @@ COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ BACKEND=\ Cminor.v Op.v CminorSel.v \ - SelectOp.v SelectLong.v Selection.v \ - SelectOpproof.v SelectLongproof.v Selectionproof.v \ + SelectOp.v SelectDiv.v SelectLong.v Selection.v \ + SelectOpproof.v SelectDivproof.v SelectLongproof.v Selectionproof.v \ Registers.v RTL.v \ RTLgen.v RTLgenspec.v RTLgenproof.v \ Tailcall.v Tailcallproof.v \ diff --git a/arm/Asm.v b/arm/Asm.v index 43a1435..76e8196 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -157,9 +157,11 @@ Inductive instruction : Type := | Pstr: ireg -> ireg -> shift_addr -> instruction (**r int32 store *) | Pstrb: ireg -> ireg -> shift_addr -> instruction (**r int8 store *) | Pstrh: ireg -> ireg -> shift_addr -> instruction (**r int16 store *) - | Psdiv: ireg -> ireg -> ireg -> instruction (**r signed division *) + | Psdiv: instruction (**r signed division *) + | Psmull: ireg -> ireg -> ireg -> ireg -> instruction (**r signed multiply long *) | Psub: ireg -> ireg -> shift_op -> instruction (**r integer subtraction *) - | Pudiv: ireg -> ireg -> ireg -> instruction (**r unsigned division *) + | Pudiv: instruction (**r unsigned division *) + | Pumull: ireg -> ireg -> ireg -> ireg -> instruction (**r unsigned multiply long *) (* Floating-point coprocessor instructions (VFP double scalar operations) *) | Pfcpyd: freg -> freg -> instruction (**r float move *) | Pfabsd: freg -> freg -> instruction (**r float absolute value *) @@ -559,18 +561,28 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out exec_store Mint8unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m | Pstrh r1 r2 sa => exec_store Mint16unsigned (Val.add rs#r2 (eval_shift_addr sa rs)) r1 rs m - | Psdiv rd r1 r2 => - match Val.divs rs#r1 rs#r2 with - | Some v => Next (nextinstr (rs#rd <- v)) m + | Psdiv => + match Val.divs rs#IR0 rs#IR1 with + | Some v => Next (nextinstr (rs#IR0 <- v + #IR1 <- Vundef #IR2 <- Vundef + #IR3 <- Vundef #IR12 <- Vundef)) m | None => Stuck end + | Psmull rdl rdh r1 r2 => + Next (nextinstr (rs#rdl <- (Val.mul rs#r1 rs#r2) + #rdh <- (Val.mulhs rs#r1 rs#r2))) m | Psub r1 r2 so => Next (nextinstr (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m - | Pudiv rd r1 r2 => - match Val.divu rs#r1 rs#r2 with - | Some v => Next (nextinstr (rs#rd <- v)) m + | Pudiv => + match Val.divu rs#IR0 rs#IR1 with + | Some v => Next (nextinstr (rs#IR0 <- v + #IR1 <- Vundef #IR2 <- Vundef + #IR3 <- Vundef #IR12 <- Vundef)) m | None => Stuck end + | Pumull rdl rdh r1 r2 => + Next (nextinstr (rs#rdl <- (Val.mul rs#r1 rs#r2) + #rdh <- (Val.mulhu rs#r1 rs#r2))) m (* Floating-point coprocessor instructions *) | Pfcpyd r1 r2 => Next (nextinstr (rs#r1 <- (rs#r2))) m diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 6645149..3707b7f 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -299,12 +299,22 @@ Definition transl_op OK (if negb (ireg_eq r r1) then Pmla r r1 r2 r3 :: k else if negb (ireg_eq r r2) then Pmla r r2 r1 r3 :: k else Pmla IR14 r1 r2 r3 :: Pmov r (SOreg IR14) :: k) - | Odiv, a1 :: a2 :: nil => + | Omulhs, a1 :: a2 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psdiv r r1 r2 :: k) - | Odivu, a1 :: a2 :: nil => + OK (Psmull IR14 r r1 r2 :: k) + | Omulhu, a1 :: a2 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pudiv r r1 r2 :: k) + OK (Pumull IR14 r r1 r2 :: k) + | Odiv, a1 :: a2 :: nil => + assertion (mreg_eq res R0); + assertion (mreg_eq a1 R0); + assertion (mreg_eq a2 R1); + OK (Psdiv :: k) + | Odivu, a1 :: a2 :: nil => + assertion (mreg_eq res R0); + assertion (mreg_eq a1 R0); + assertion (mreg_eq a2 R1); + OK (Pudiv :: k) | Oand, a1 :: a2 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pand r r1 (SOreg r2) :: k) diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index d77006a..21d2b73 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -942,11 +942,12 @@ Proof. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. intuition Simpl. (* divs *) - econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. - intuition Simpl. +Local Transparent destroyed_by_op. + econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. + split. Simpl. simpl; intros. intuition Simpl. (* divu *) econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. - intuition Simpl. + split. Simpl. simpl; intros. intuition Simpl. (* Oandimm *) generalize (andimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 9bf066b..caf0da6 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -112,6 +112,9 @@ 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) + | Omla, I n1 :: I n2 :: I n3 :: nil => I(Int.add (Int.mul n1 n2) n3) + | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2) + | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu 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 diff --git a/arm/Op.v b/arm/Op.v index af3ccdb..fe97d36 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -82,6 +82,8 @@ Inductive operation : Type := | Orsubimm: int -> operation (**r [rd = n - r1] *) | Omul: operation (**r [rd = r1 * r2] *) | Omla: operation (**r [rd = r1 * r2 + r3] *) + | Omulhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omulhu: operation (**r [rd = high part of r1 * r2, unsigned] *) | Odiv: operation (**r [rd = r1 / r2] (signed) *) | Odivu: operation (**r [rd = r1 / r2] (unsigned) *) | Oand: operation (**r [rd = r1 & r2] *) @@ -226,6 +228,8 @@ Definition eval_operation | Orsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) | Omla, v1 :: v2 :: v3 :: nil => Some (Val.add (Val.mul v1 v2) v3) + | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) + | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) | Odiv, v1 :: v2 :: nil => Val.divs v1 v2 | Odivu, v1 :: v2 :: nil => Val.divu v1 v2 | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2) @@ -319,6 +323,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Orsubimm _ => (Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) | Omla => (Tint :: Tint :: Tint :: nil, Tint) + | Omulhs => (Tint :: Tint :: nil, Tint) + | Omulhu => (Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) | Odivu => (Tint :: Tint :: nil, Tint) | Oand => (Tint :: Tint :: nil, Tint) @@ -396,6 +402,8 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... destruct v1... destruct v2... + destruct v0; destruct v1... + destruct v0; destruct v1... 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... @@ -823,6 +831,8 @@ Proof. inv H4; inv H2; simpl; auto. apply Values.val_add_inject; auto. inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; 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. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index d700326..c0e2687 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -599,14 +599,16 @@ let print_instruction oc = function fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 - | Psdiv(r1, r2, r3) -> - assert (r1 = IR0 && r2 = IR0 && r3 = IR1); + | Psdiv -> fprintf oc " bl __aeabi_idiv\n"; 1 + | Psmull(r1, r2, r3, r4) -> + fprintf oc " smull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 | Psub(r1, r2, so) -> fprintf oc " sub %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 - | Pudiv(r1, r2, r3) -> - assert (r1 = IR0 && r2 = IR0 && r3 = IR1); + | Pudiv -> fprintf oc " bl __aeabi_uidiv\n"; 1 + | Pumull(r1, r2, r3, r4) -> + fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 (* Floating-point coprocessor instructions *) | Pfcpyd(r1, r2) -> fprintf oc " fcpyd %a, %a\n" freg r1 freg r2; 1 diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index d81328b..4cd09d1 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -272,33 +272,20 @@ Definition mod_aux (divop: operation) (e1 e2: expr) := Enil) ::: Enil))). -Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). - -Definition mods := mod_aux Odiv. - -Definition divuimm (e: expr) (n: int) := - match Int.is_power2 n with - | Some l => shruimm e l - | None => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil) - end. - -Nondetfunction divu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => divuimm e1 n2 - | _ => Eop Odivu (e1:::e2:::Enil) - end. - -Definition moduimm (e: expr) (n: int) := - match Int.is_power2 n with - | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil) - | None => mod_aux Odivu e (Eop (Ointconst n) Enil) - end. - -Nondetfunction modu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => moduimm e1 n2 - | _ => mod_aux Odivu e1 e2 - end. +Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). +Definition mods_base := mod_aux Odiv. +Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). +Definition modu_base := mod_aux Odivu. + +Definition shrximm (e1: expr) (n2: int) := + if Int.eq n2 Int.zero + then e1 + else Elet e1 + (shrimm + (add (Eletvar O) + (shruimm (shrimm (Eletvar O) (Int.repr 31)) + (Int.sub Int.iwordsize n2))) + n2). (** ** General shifts *) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index a71ead7..9beb1ad 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -468,83 +468,103 @@ Proof. reflexivity. Qed. -Theorem eval_divs: +Theorem eval_divs_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divs x y = Some z -> - exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divs. exists z; split. EvalOp. auto. + intros. unfold divs_base. exists z; split. EvalOp. auto. Qed. -Theorem eval_mods: +Theorem eval_mods_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.mods x y = Some z -> - exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold mods. + intros; unfold mods_base. exploit Val.mods_divs; eauto. intros [v [A B]]. subst. econstructor; split; eauto. apply eval_mod_aux with (semdivop := Val.divs); auto. Qed. -Theorem eval_divuimm: - forall le n a x z, - eval_expr ge sp e m le a x -> - Val.divu x (Vint n) = Some z -> - exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v. -Proof. - intros; unfold divuimm. - destruct (Int.is_power2 n) eqn:?. - replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto. - eapply Val.divu_pow2; eauto. - TrivialExists. - econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. -Qed. - -Theorem eval_divu: +Theorem eval_divu_base: forall le a x b y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divu x y = Some z -> - exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. - intros until z. unfold divu; destruct (divu_match b); intros; InvEval. - eapply eval_divuimm; eauto. - TrivialExists. + intros. unfold divu_base. exists z; split. EvalOp. auto. Qed. -Theorem eval_moduimm: - forall le n a x z, +Theorem eval_modu_base: + forall le a x b y z, eval_expr ge sp e m le a x -> - Val.modu x (Vint n) = Some z -> - exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v. + eval_expr ge sp e m le b y -> + Val.modu x y = Some z -> + exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold moduimm. - destruct (Int.is_power2 n) eqn:?. - replace z with (Val.and x (Vint (Int.sub n Int.one))). TrivialExists. - eapply Val.modu_pow2; eauto. + intros; unfold modu_base. exploit Val.modu_divu; eauto. intros [v [A B]]. subst. econstructor; split; eauto. apply eval_mod_aux with (semdivop := Val.divu); auto. - EvalOp. Qed. -Theorem eval_modu: - forall le a x b y z, +Theorem eval_shrximm: + forall le a n x z, eval_expr ge sp e m le a x -> - eval_expr ge sp e m le b y -> - Val.modu x y = Some z -> - exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v. + Val.shrx x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v. Proof. - intros until y; unfold modu; case (modu_match b); intros; InvEval. - eapply eval_moduimm; eauto. - exploit Val.modu_divu; eauto. intros [v [A B]]. - subst. econstructor; split; eauto. - apply eval_mod_aux with (semdivop := Val.divu); auto. + intros. unfold shrximm. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. exists x; split; auto. + destruct x; simpl in H0; try discriminate. + destruct (Int.ltu Int.zero (Int.repr 31)); inv H0. + replace (Int.shrx i Int.zero) with i. auto. + unfold Int.shrx, Int.divs. rewrite Int.shl_zero. + change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. +- destruct x; simpl in H0; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT31; inv H0. + assert (A: eval_expr ge sp e m (Vint i :: le) (Eletvar 0) (Vint i)) + by (constructor; auto). + exploit (eval_shrimm (Int.repr 31)). eexact A. + intros [v [B LD]]. simpl in LD. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. + simpl in LD; inv LD. + exploit (eval_shruimm (Int.sub Int.iwordsize n)). eexact B. + intros [v [C LD]]. simpl in LD. + assert (RANGE: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true). + { + generalize (Int.ltu_inv _ _ LT31). intros. + unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. + rewrite Int.unsigned_repr. apply zlt_true. + assert (Int.unsigned n <> 0). + { red; intros; elim H1. rewrite <- (Int.repr_unsigned n). rewrite H2; reflexivity. } + omega. + change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. + generalize Int.wordsize_max_unsigned; omega. + } + rewrite RANGE in LD. inv LD. + exploit eval_add. eexact A. eexact C. intros [v [D LD]]. + simpl in LD. inv LD. + exploit (eval_shrimm n). eexact D. intros [v [E LD]]. + simpl in LD. + assert (RANGE2: Int.ltu n Int.iwordsize = true). + { + generalize (Int.ltu_inv _ _ LT31). intros. + unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true. + change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. + omega. + } + rewrite RANGE2 in LD. inv LD. + econstructor; split. econstructor. eassumption. eexact E. + rewrite Int.shrx_shr_2 by auto. + auto. Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp new file mode 100644 index 0000000..e60a97d --- /dev/null +++ b/backend/SelectDiv.vp @@ -0,0 +1,156 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for integer division and modulus *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +(** We try to turn divisions by a constant into a multiplication by + a pseudo-inverse of the divisor. The approach is described in +- Torbjörn Granlund, Peter L. Montgomery: "Division by Invariant + Integers using Multiplication". PLDI 1994. +- Henry S. Warren, Jr: "Hacker's Delight". Addison-Wesley. Chapter 10. +*) + +Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z) := + match fuel with + | O => None + | S fuel' => + let twp := two_p p in + if zlt (nc * (d - twp mod d)) twp + then Some(p - 32, (twp + d - twp mod d) / d) + else find_div_mul_params fuel' nc d (p + 1) + end. + +Definition divs_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int.wordsize + (Int.half_modulus - Int.half_modulus mod d - 1) + d 32 with + | None => None + | Some(p, m) => + if zlt 0 d + && zlt (two_p (32 + p)) (m * d) + && zle (m * d) (two_p (32 + p) + two_p (p + 1)) + && zle 0 m && zlt m Int.modulus + && zle 0 p && zlt p 32 + then Some(p, m) else None + end. + +Definition divu_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int.wordsize + (Int.modulus - Int.modulus mod d - 1) + d 32 with + | None => None + | Some(p, m) => + if zlt 0 d + && zle (two_p (32 + p)) (m * d) + && zle (m * d) (two_p (32 + p) + two_p p) + && zle 0 m && zlt m Int.modulus + && zle 0 p && zlt p 32 + then Some(p, m) else None + end. + +Definition divu_mul (p: Z) (m: Z) := + shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil)) + (Int.repr p). + +Definition divuimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => shruimm e1 l + | None => + match divu_mul_params (Int.unsigned n2) with + | None => divu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divu_mul p m) + end + end. + +Nondetfunction divu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divuimm e1 n2 + | _ => divu_base e1 e2 + end. + +Definition mod_from_div (equo: expr) (n: int) := + Eop Osub (Eletvar O ::: mulimm n equo ::: Enil). + +Definition moduimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => andimm (Int.sub n2 Int.one) e1 + | None => + match divu_mul_params (Int.unsigned n2) with + | None => modu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) + end + end. + +Nondetfunction modu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => moduimm e1 n2 + | _ => modu_base e1 e2 + end. + +Definition divs_mul (p: Z) (m: Z) := + let e2 := + Eop Omulhs (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil) in + let e3 := + if zlt m Int.half_modulus then e2 else add e2 (Eletvar O) in + add (shrimm e3 (Int.repr p)) + (shruimm (Eletvar O) (Int.repr (Int.zwordsize - 1))). + +Definition divsimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => + if Int.ltu l (Int.repr 31) + then shrximm e1 l + else divs_base e1 (Eop (Ointconst n2) Enil) + | None => + match divs_mul_params (Int.signed n2) with + | None => divs_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divs_mul p m) + end + end. + +Nondetfunction divs (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divsimm e1 n2 + | _ => divs_base e1 e2 + end. + +Definition modsimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => + if Int.ltu l (Int.repr 31) + then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2) + else mods_base e1 (Eop (Ointconst n2) Enil) + | None => + match divs_mul_params (Int.signed n2) with + | None => mods_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) + end + end. + +Nondetfunction mods (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => modsimm e1 n2 + | _ => mods_base e1 e2 + end. + diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v new file mode 100644 index 0000000..4d8f96a --- /dev/null +++ b/backend/SelectDivproof.v @@ -0,0 +1,547 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness of instruction selection for integer division *) + +Require Import Coqlib. +Require Import Zquot. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Cminor. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. +Require Import SelectOpproof. +Require Import SelectDiv. + +Open Local Scope cminorsel_scope. + +(** * Main approximation theorems *) + +Section Z_DIV_MUL. + +Variable N: Z. (**r number of relevant bits *) +Hypothesis N_pos: N >= 0. +Variable d: Z. (**r divisor *) +Hypothesis d_pos: d > 0. + +(** This is theorem 4.2 from Granlund and Montgomery, PLDI 1994. *) + +Lemma Zdiv_mul_pos: + forall m l, + l >= 0 -> + two_p (N+l) <= m * d <= two_p (N+l) + two_p l -> + forall n, + 0 <= n < two_p N -> + Zdiv n d = Zdiv (m * n) (two_p (N + l)). +Proof. + intros m l l_pos [LO HI] n RANGE. + exploit (Z_div_mod_eq n d). auto. + set (q := n / d). + set (r := n mod d). + intro EUCL. + assert (0 <= r <= d - 1). + unfold r. generalize (Z_mod_lt n d d_pos). omega. + assert (0 <= m). + apply Zmult_le_0_reg_r with d. auto. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + set (k := m * d - two_p (N + l)). + assert (0 <= k <= two_p l). + unfold k; omega. + assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). + unfold k. rewrite EUCL. ring. + assert (0 <= k * n). + apply Zmult_le_0_compat; omega. + assert (k * n <= two_p (N + l) - two_p l). + apply Zle_trans with (two_p l * n). + apply Zmult_le_compat_r. omega. omega. + replace (N + l) with (l + N) by omega. + rewrite two_p_is_exp. + replace (two_p l * two_p N - two_p l) + with (two_p l * (two_p N - 1)) + by ring. + apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. + omega. omega. + assert (0 <= two_p (N + l) * r). + apply Zmult_le_0_compat. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + omega. + assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). + replace (two_p (N + l) * d - two_p (N + l)) + with (two_p (N + l) * (d - 1)) by ring. + apply Zmult_le_compat_l. + omega. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + assert (0 <= m * n - two_p (N + l) * q). + apply Zmult_le_reg_r with d. auto. + replace (0 * d) with 0 by ring. rewrite H2. omega. + assert (m * n - two_p (N + l) * q < two_p (N + l)). + apply Zmult_lt_reg_r with d. omega. + rewrite H2. + apply Zle_lt_trans with (two_p (N + l) * d - two_p l). + omega. + exploit (two_p_gt_ZERO l). omega. omega. + symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). + ring. omega. +Qed. + +Lemma Zdiv_unique_2: + forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1. +Proof. + intros. apply Zdiv_unique with (x - (q - 1) * y). ring. + replace ((q - 1) * y) with (y * q - y) by ring. omega. +Qed. + +Lemma Zdiv_mul_opp: + forall m l, + l >= 0 -> + two_p (N+l) < m * d <= two_p (N+l) + two_p l -> + forall n, + 0 < n <= two_p N -> + Zdiv n d = - Zdiv (m * (-n)) (two_p (N + l)) - 1. +Proof. + intros m l l_pos [LO HI] n RANGE. + replace (m * (-n)) with (- (m * n)) by ring. + exploit (Z_div_mod_eq n d). auto. + set (q := n / d). + set (r := n mod d). + intro EUCL. + assert (0 <= r <= d - 1). + unfold r. generalize (Z_mod_lt n d d_pos). omega. + assert (0 <= m). + apply Zmult_le_0_reg_r with d. auto. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1). + omega. + apply Zdiv_unique_2. + apply two_p_gt_ZERO. omega. + replace (two_p (N + l) * - q - - (m * n)) + with (m * n - two_p (N + l) * q) + by ring. + set (k := m * d - two_p (N + l)). + assert (0 < k <= two_p l). + unfold k; omega. + assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). + unfold k. rewrite EUCL. ring. + split. + apply Zmult_lt_reg_r with d. omega. + replace (0 * d) with 0 by omega. + rewrite H2. + assert (0 < k * n). apply Zmult_lt_0_compat; omega. + assert (0 <= two_p (N + l) * r). + apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega. + omega. + apply Zmult_le_reg_r with d. omega. + rewrite H2. + assert (k * n <= two_p (N + l)). + rewrite Zplus_comm. rewrite two_p_is_exp; try omega. + apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. + apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. + assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). + replace (two_p (N + l) * d - two_p (N + l)) + with (two_p (N + l) * (d - 1)) + by ring. + apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega. + omega. +Qed. + +(** This is theorem 5.1 from Granlund and Montgomery, PLDI 1994. *) + +Lemma Zquot_mul: + forall m l, + l >= 0 -> + two_p (N+l) < m * d <= two_p (N+l) + two_p l -> + forall n, + - two_p N <= n < two_p N -> + Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). +Proof. + intros. destruct (zlt n 0). + exploit (Zdiv_mul_opp m l H H0 (-n)). omega. + replace (- - n) with n by ring. + replace (Z.quot n d) with (- Z.quot (-n) d). + rewrite Zquot_Zdiv_pos by omega. omega. + rewrite Z.quot_opp_l by omega. ring. + rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. + apply Zdiv_mul_pos; omega. +Qed. + +End Z_DIV_MUL. + +(** * Correctness of the division parameters *) + +Lemma divs_mul_params_sound: + forall d m p, + divs_mul_params d = Some(p, m) -> + 0 <= m < Int.modulus /\ 0 <= p < 32 /\ + forall n, + Int.min_signed <= n <= Int.max_signed -> + Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). +Proof with (try discriminate). + unfold divs_mul_params; intros d m' p' EQ. + destruct (find_div_mul_params Int.wordsize + (Int.half_modulus - Int.half_modulus mod d - 1) d 32) + as [[p m] | ]... + destruct (zlt 0 d)... + destruct (zlt (two_p (32 + p)) (m * d))... + destruct (zle (m * d) (two_p (32 + p) + two_p (p + 1)))... + destruct (zle 0 m)... + destruct (zlt m Int.modulus)... + destruct (zle 0 p)... + destruct (zlt p 32)... + simpl in EQ. inv EQ. + split. auto. split. auto. intros. + replace (32 + p') with (31 + (p' + 1)) by omega. + apply Zquot_mul; try omega. + replace (31 + (p' + 1)) with (32 + p') by omega. omega. + change (Int.min_signed <= n < Int.half_modulus). + unfold Int.max_signed in H. omega. +Qed. + +Lemma divu_mul_params_sound: + forall d m p, + divu_mul_params d = Some(p, m) -> + 0 <= m < Int.modulus /\ 0 <= p < 32 /\ + forall n, + 0 <= n < Int.modulus -> + Zdiv n d = Zdiv (m * n) (two_p (32 + p)). +Proof with (try discriminate). + unfold divu_mul_params; intros d m' p' EQ. + destruct (find_div_mul_params Int.wordsize + (Int.modulus - Int.modulus mod d - 1) d 32) + as [[p m] | ]... + destruct (zlt 0 d)... + destruct (zle (two_p (32 + p)) (m * d))... + destruct (zle (m * d) (two_p (32 + p) + two_p p))... + destruct (zle 0 m)... + destruct (zlt m Int.modulus)... + destruct (zle 0 p)... + destruct (zlt p 32)... + simpl in EQ. inv EQ. + split. auto. split. auto. intros. + apply Zdiv_mul_pos; try omega. assumption. +Qed. + +Lemma divs_mul_shift_gen: + forall x y m p, + divs_mul_params (Int.signed y) = Some(p, m) -> + 0 <= m < Int.modulus /\ 0 <= p < 32 /\ + Int.divs x y = Int.add (Int.shr (Int.repr ((Int.signed x * m) / Int.modulus)) (Int.repr p)) + (Int.shru x (Int.repr 31)). +Proof. + intros. set (n := Int.signed x). set (d := Int.signed y) in *. + exploit divs_mul_params_sound; eauto. intros (A & B & C). + split. auto. split. auto. + unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). + rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add. + rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. + rewrite Int.unsigned_repr. f_equal. + rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring. + cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). + unfold Int.max_signed; omega. + apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. + apply Int.modulus_pos. + split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. + apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto. + apply Zle_lt_trans with (Int.half_modulus * m). + apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto. + apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. + assert (32 < Int.max_unsigned) by (compute; auto). omega. + unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. + apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. omega. +Qed. + +Theorem divs_mul_shift_1: + forall x y m p, + divs_mul_params (Int.signed y) = Some(p, m) -> + m < Int.half_modulus -> + 0 <= p < 32 /\ + Int.divs x y = Int.add (Int.shr (Int.mulhs x (Int.repr m)) (Int.repr p)) + (Int.shru x (Int.repr 31)). +Proof. + intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). + intros (A & B & C). split. auto. rewrite C. + unfold Int.mulhs. rewrite Int.signed_repr. auto. + generalize Int.min_signed_neg; unfold Int.max_signed; omega. +Qed. + +Theorem divs_mul_shift_2: + forall x y m p, + divs_mul_params (Int.signed y) = Some(p, m) -> + m >= Int.half_modulus -> + 0 <= p < 32 /\ + Int.divs x y = Int.add (Int.shr (Int.add (Int.mulhs x (Int.repr m)) x) (Int.repr p)) + (Int.shru x (Int.repr 31)). +Proof. + intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). + intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. + rewrite Int.add_signed. unfold Int.mulhs. set (n := Int.signed x). + transitivity (Int.repr (n * (m - Int.modulus) / Int.modulus + n)). + f_equal. + replace (n * (m - Int.modulus)) with (n * m + (-n) * Int.modulus) by ring. + rewrite Z_div_plus. ring. apply Int.modulus_pos. + apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. + apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. + rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. + apply zlt_false. omega. +Qed. + +Theorem divu_mul_shift: + forall x y m p, + divu_mul_params (Int.unsigned y) = Some(p, m) -> + 0 <= p < 32 /\ + Int.divu x y = Int.shru (Int.mulhu x (Int.repr m)) (Int.repr p). +Proof. + intros. exploit divu_mul_params_sound; eauto. intros (A & B & C). + split. auto. + rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. + unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range. + rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). + f_equal. rewrite (Int.unsigned_repr m). + rewrite Int.unsigned_repr. f_equal. ring. + cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus). + unfold Int.max_unsigned; omega. + apply Zdiv_interval_1. omega. compute; auto. compute; auto. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. + apply Zle_lt_trans with (Int.modulus * m). + apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. + apply Zmult_lt_compat_l. compute; auto. omega. + unfold Int.max_unsigned; omega. + assert (32 < Int.max_unsigned) by (compute; auto). omega. +Qed. + +(** * Correctness of the smart constructors for division and modulus *) + +Section CMCONSTRS. + +Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. + +Lemma eval_divu_mul: + forall le x y p M, + divu_mul_params (Int.unsigned y) = Some(p, M) -> + nth_error le O = Some (Vint x) -> + eval_expr ge sp e m le (divu_mul p M) (Vint (Int.divu x y)). +Proof. + intros. unfold divu_mul. exploit (divu_mul_shift x); eauto. intros [A B]. + assert (eval_expr ge sp e m le + (Eop Omulhu (Eletvar 0 ::: Eop (Ointconst (Int.repr M)) Enil ::: Enil)) + (Vint (Int.mulhu x (Int.repr M)))). + { EvalOp. econstructor. econstructor; eauto. econstructor. EvalOp. simpl; reflexivity. constructor. + auto. } + exploit eval_shruimm. eexact H1. instantiate (1 := Int.repr p). + intros [v [P Q]]. simpl in Q. + replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. + inv Q. rewrite B. auto. + unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. + assert (32 < Int.max_unsigned) by (compute; auto). omega. +Qed. + +Theorem eval_divuimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.divu x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (divuimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold divuimm; intros. generalize H0; intros DIV. + destruct x; simpl in DIV; try discriminate. + destruct (Int.eq n2 Int.zero) eqn:Z2; inv DIV. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- erewrite Int.divu_pow2 by eauto. + replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). + apply eval_shruimm; auto. + simpl. erewrite Int.is_power2_range; eauto. +- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + + exists (Vint (Int.divu i n2)); split; auto. + econstructor; eauto. eapply eval_divu_mul; eauto. + + eapply eval_divu_base; eauto. EvalOp. +Qed. + +Theorem eval_divu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divu x y = Some z -> + exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v. +Proof. + unfold divu; intros until b. destruct (divu_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_divuimm; eauto. +- eapply eval_divu_base; eauto. +Qed. + +Lemma eval_mod_from_div: + forall le a n x y, + eval_expr ge sp e m le a (Vint y) -> + nth_error le O = Some (Vint x) -> + eval_expr ge sp e m le (mod_from_div a n) (Vint (Int.sub x (Int.mul y n))). +Proof. + unfold mod_from_div; intros. + exploit eval_mulimm; eauto. instantiate (1 := n). intros [v [A B]]. + simpl in B. inv B. EvalOp. +Qed. + +Theorem eval_moduimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.modu x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (moduimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold moduimm; intros. generalize H0; intros MOD. + destruct x; simpl in MOD; try discriminate. + destruct (Int.eq n2 Int.zero) eqn:Z2; inv MOD. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- erewrite Int.modu_and by eauto. + change (Vint (Int.and i (Int.sub n2 Int.one))) + with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))). + apply eval_andimm. auto. +- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + + econstructor; split. + econstructor; eauto. eapply eval_mod_from_div. + eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. + rewrite Int.modu_divu. auto. + red; intros; subst n2; discriminate. + + eapply eval_modu_base; eauto. EvalOp. +Qed. + +Theorem eval_modu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modu x y = Some z -> + exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v. +Proof. + unfold modu; intros until b. destruct (modu_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_moduimm; eauto. +- eapply eval_modu_base; eauto. +Qed. + +Lemma eval_divs_mul: + forall le x y p M, + divs_mul_params (Int.signed y) = Some(p, M) -> + nth_error le O = Some (Vint x) -> + eval_expr ge sp e m le (divs_mul p M) (Vint (Int.divs x y)). +Proof. + intros. unfold divs_mul. + assert (V: eval_expr ge sp e m le (Eletvar O) (Vint x)). + { constructor; auto. } + assert (X: eval_expr ge sp e m le + (Eop Omulhs (Eletvar 0 ::: Eop (Ointconst (Int.repr M)) Enil ::: Enil)) + (Vint (Int.mulhs x (Int.repr M)))). + { EvalOp. econstructor. eauto. econstructor. EvalOp. simpl; reflexivity. constructor. + auto. } + exploit eval_shruimm. eexact V. instantiate (1 := Int.repr (Int.zwordsize - 1)). + intros [v1 [Y LD]]. simpl in LD. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. + simpl in LD. inv LD. + assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true). + { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. + assert (32 < Int.max_unsigned) by (compute; auto). omega. } + destruct (zlt M Int.half_modulus). +- exploit (divs_mul_shift_1 x); eauto. intros [A B]. + exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]]. + simpl in LD. rewrite RANGE in LD by auto. inv LD. + exploit eval_add. eexact Z. eexact Y. intros [v1 [W LD]]. + simpl in LD. inv LD. + rewrite B. exact W. +- exploit (divs_mul_shift_2 x); eauto. intros [A B]. + exploit eval_add. eexact X. eexact V. intros [v1 [Z LD]]. + simpl in LD. inv LD. + exploit eval_shrimm. eexact Z. instantiate (1 := Int.repr p). intros [v1 [U LD]]. + simpl in LD. rewrite RANGE in LD by auto. inv LD. + exploit eval_add. eexact U. eexact Y. intros [v1 [W LD]]. + simpl in LD. inv LD. + rewrite B. exact W. +Qed. + +Theorem eval_divsimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.divs x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (divsimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold divsimm; intros. generalize H0; intros DIV. + destruct x; simpl in DIV; try discriminate. + destruct (Int.eq n2 Int.zero + || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto. + + eapply eval_divs_base; eauto. EvalOp. +- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + exists (Vint (Int.divs i n2)); split; auto. + econstructor; eauto. eapply eval_divs_mul; eauto. + + eapply eval_divs_base; eauto. EvalOp. +Qed. + +Theorem eval_divs: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divs x y = Some z -> + exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v. +Proof. + unfold divs; intros until b. destruct (divs_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_divsimm; eauto. +- eapply eval_divs_base; eauto. +Qed. + +Theorem eval_modsimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.mods x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (modsimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold modsimm; intros. + exploit Val.mods_divs; eauto. intros [y [A B]]. + generalize A; intros DIV. + destruct x; simpl in DIV; try discriminate. + destruct (Int.eq n2 Int.zero + || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)). + constructor. simpl; eauto. eapply Val.divs_pow2; eauto. + intros [v1 [X LD]]. inv LD. + econstructor; split. econstructor. eauto. + apply eval_mod_from_div. eexact X. simpl; eauto. + simpl. auto. + + eapply eval_mods_base; eauto. EvalOp. +- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + econstructor; split. + econstructor. eauto. apply eval_mod_from_div with (x := i); auto. + eapply eval_divs_mul with (x := i); eauto. + simpl. auto. + + eapply eval_mods_base; eauto. EvalOp. +Qed. + +Theorem eval_mods: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.mods x y = Some z -> + exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v. +Proof. + unfold mods; intros until b. destruct (mods_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_modsimm; eauto. +- eapply eval_mods_base; eauto. +Qed. + +End CMCONSTRS. diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index 3978828..26f33da 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness of instruction selection for 64-bit integer operations *) +(** Correctness of instruction selection for integer division *) Require Import Coqlib. Require Import AST. diff --git a/backend/Selection.v b/backend/Selection.v index b35c891..f62a888 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -31,6 +31,7 @@ Require Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import SelectDiv. Require Import SelectLong. Open Local Scope cminorsel_scope. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e94f85d..c292b49 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -26,9 +26,11 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import SelectDiv. Require Import SelectLong. Require Import Selection. Require Import SelectOpproof. +Require Import SelectDivproof. Require Import SelectLongproof. Open Local Scope cminorsel_scope. diff --git a/common/Values.v b/common/Values.v index 05749b7..670f785 100644 --- a/common/Values.v +++ b/common/Values.v @@ -222,6 +222,18 @@ Definition mul (v1 v2: val): val := | _, _ => Vundef end. +Definition mulhs (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.mulhs n1 n2) + | _, _ => Vundef + end. + +Definition mulhu (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.mulhu n1 n2) + | _, _ => Vundef + end. + Definition divs (v1 v2: val): option val := match v1, v2 with | Vint n1, Vint n2 => diff --git a/ia32/Asm.v b/ia32/Asm.v index d86ff19..78c4c3b 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -145,6 +145,8 @@ Inductive instruction: Type := | Psub_rr (rd: ireg) (r1: ireg) | Pimul_rr (rd: ireg) (r1: ireg) | Pimul_ri (rd: ireg) (n: int) + | Pimul_r (r1: ireg) + | Pmul_r (r1: ireg) | Pdiv (r1: ireg) | Pidiv (r1: ireg) | Pand_rr (rd: ireg) (r1: ireg) @@ -540,6 +542,12 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd rs#r1))) m | Pimul_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd (Vint n)))) m + | Pimul_r r1 => + Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1) + #EDX <- (Val.mulhs rs#EAX rs#r1))) m + | Pmul_r r1 => + Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1) + #EDX <- (Val.mulhu rs#EAX rs#r1))) m | Pdiv r1 => let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in match Val.divu vn vd, Val.modu vn vd with diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 4543ac9..0410057 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -311,6 +311,14 @@ Definition transl_op | Omulimm n, a1 :: nil => assertion (mreg_eq a1 res); do r <- ireg_of res; OK (Pimul_ri r n :: k) + | Omulhs, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res DX); + do r2 <- ireg_of a2; OK (Pimul_r r2 :: k) + | Omulhu, a1 :: a2 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res DX); + do r2 <- ireg_of a2; OK (Pmul_r r2 :: k) | Odiv, a1 :: a2 :: nil => assertion (mreg_eq a1 AX); assertion (mreg_eq a2 CX); diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 728617e..9ddc463 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -922,6 +922,10 @@ Transparent destroyed_by_op. apply SAME. eapply mk_intconv_correct; eauto. (* cast16unsigned *) apply SAME. eapply mk_intconv_correct; eauto. +(* mulhs *) + apply SAME. TranslOp. destruct H1. Simplifs. +(* mulhu *) + apply SAME. TranslOp. destruct H1. Simplifs. (* div *) apply SAME. specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index fea0afd..a29b450 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -107,6 +107,8 @@ 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) + | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2) + | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu 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 diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 528e9ed..826dadf 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -75,6 +75,8 @@ Definition destroyed_by_op (op: operation): list mreg := match op with | Omove => FP0 :: nil | Ocast8signed | Ocast8unsigned | Ocast16signed | Ocast16unsigned => AX :: nil + | Omulhs => AX :: DX :: nil + | Omulhu => AX :: DX :: nil | Odiv => AX :: DX :: nil | Odivu => AX :: DX :: nil | Omod => AX :: DX :: nil @@ -136,6 +138,8 @@ Definition temp_for_parent_frame: mreg := Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := match op with + | Omulhs => (Some AX :: None :: nil, Some DX) + | Omulhu => (Some AX :: None :: nil, Some DX) | Odiv => (Some AX :: Some CX :: nil, Some AX) | Odivu => (Some AX :: Some CX :: nil, Some AX) | Omod => (Some AX :: Some CX :: nil, Some DX) @@ -192,6 +196,8 @@ Definition two_address_op (op: operation) : bool := | Osub => true | Omul => true | Omulimm _ => true + | Omulhs => false + | Omulhu => false | Odiv => false | Odivu => false | Omod => false diff --git a/ia32/Op.v b/ia32/Op.v index 509938e..f2e6b13 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -78,6 +78,8 @@ Inductive operation : Type := | Osub: operation (**r [rd = r1 - r2] *) | Omul: operation (**r [rd = r1 * r2] *) | Omulimm: int -> operation (**r [rd = r1 * n] *) + | Omulhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omulhu: operation (**r [rd = high part of r1 * r2, unsigned] *) | Odiv: operation (**r [rd = r1 / r2] (signed) *) | Odivu: operation (**r [rd = r1 / r2] (unsigned) *) | Omod: operation (**r [rd = r1 % r2] (signed) *) @@ -216,6 +218,8 @@ Definition eval_operation | Osub, v1::v2::nil => Some (Val.sub v1 v2) | Omul, v1::v2::nil => Some (Val.mul v1 v2) | Omulimm n, v1::nil => Some (Val.mul v1 (Vint n)) + | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) + | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) | Odiv, v1::v2::nil => Val.divs v1 v2 | Odivu, v1::v2::nil => Val.divu v1 v2 | Omod, v1::v2::nil => Val.mods v1 v2 @@ -305,6 +309,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osub => (Tint :: Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) | Omulimm _ => (Tint :: nil, Tint) + | Omulhs => (Tint :: Tint :: nil, Tint) + | Omulhu => (Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) | Odivu => (Tint :: Tint :: nil, Tint) | Omod => (Tint :: Tint :: nil, Tint) @@ -387,6 +393,8 @@ Proof with (try exact I). destruct v0; destruct v1... simpl. destruct (eq_block b b0)... destruct v0; destruct v1... destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... 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... @@ -796,6 +804,8 @@ Proof. rewrite Int.sub_shifted. auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; 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. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 9c8f963..5fb2568 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -606,6 +606,10 @@ let print_instruction oc = function fprintf oc " imull %a, %a\n" ireg r1 ireg rd | Pimul_ri(rd, n) -> fprintf oc " imull $%a, %a\n" coqint n ireg rd + | Pimul_r(r1) -> + fprintf oc " imull %a\n" ireg r1 + | Pmul_r(r1) -> + fprintf oc " mull %a\n" ireg r1 | Pdiv(r1) -> fprintf oc " xorl %%edx, %%edx\n"; fprintf oc " divl %a\n" ireg r1 diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 2d1ab48..209147e 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -299,10 +299,13 @@ Nondetfunction xor (e1: expr) (e2: expr) := (** ** Integer division and modulus *) -Definition divu (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). -Definition modu (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). -Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). -Definition mods (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). +Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). +Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). +Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). +Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). + +Definition shrximm (e1: expr) (n2: int) := + if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). (** ** General shifts *) diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 8c9c7e6..85802b6 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -471,44 +471,61 @@ Proof. TrivialExists. Qed. -Theorem eval_divs: +Theorem eval_divs_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divs x y = Some z -> - exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divs. exists z; split. EvalOp. auto. + intros. unfold divs_base. exists z; split. EvalOp. auto. Qed. -Theorem eval_divu: +Theorem eval_divu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divu x y = Some z -> - exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divu. exists z; split. EvalOp. auto. + intros. unfold divu_base. exists z; split. EvalOp. auto. Qed. -Theorem eval_mods: +Theorem eval_mods_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.mods x y = Some z -> - exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold mods. exists z; split. EvalOp. auto. + intros. unfold mods_base. exists z; split. EvalOp. auto. Qed. -Theorem eval_modu: +Theorem eval_modu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modu x y = Some z -> - exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold modu. exists z; split. EvalOp. auto. + intros. unfold modu_base. exists z; split. EvalOp. auto. +Qed. + +Theorem eval_shrximm: + forall le a n x z, + eval_expr ge sp e m le a x -> + Val.shrx x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v. +Proof. + intros. unfold shrximm. + predSpec Int.eq Int.eq_spec n Int.zero. + subst n. exists x; split; auto. + destruct x; simpl in H0; try discriminate. + destruct (Int.ltu Int.zero (Int.repr 31)); inv H0. + replace (Int.shrx i Int.zero) with i. auto. + unfold Int.shrx, Int.divs. rewrite Int.shl_zero. + change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. + econstructor; split. EvalOp. auto. Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. diff --git a/lib/Integers.v b/lib/Integers.v index 23f2294..cbbf28c 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -286,6 +286,11 @@ Definition rolm (x a m: int): int := and (rol x a) m. Definition shrx (x y: int): int := divs x (shl one y). +(** High half of full multiply. *) + +Definition mulhu (x y: int): int := repr ((unsigned x * unsigned y) / modulus). +Definition mulhs (x y: int): int := repr ((signed x * signed y) / modulus). + (** Condition flags *) Definition negative (x: int): int := @@ -4275,6 +4280,19 @@ Qed. Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y). +Lemma mul'_mulhu: + forall x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y). +Proof. + intros. + rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul. + set (p := Int.unsigned x * Int.unsigned y). + set (ph := p / Int.modulus). set (pl := p mod Int.modulus). + transitivity (repr (ph * Int.modulus + pl)). +- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. +- apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints. + rewrite Int.unsigned_repr_eq. apply eqm_refl. +Qed. + Lemma decompose_mul: forall xh xl yh yl, mul (ofwords xh xl) (ofwords yh yl) = @@ -4310,6 +4328,16 @@ Proof. f_equal. ring. Qed. +Lemma decompose_mul_2: + forall xh xl yh yl, + mul (ofwords xh xl) (ofwords yh yl) = + ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl)) + (Int.mul xl yl). +Proof. + intros. rewrite decompose_mul. rewrite mul'_mulhu. + rewrite hi_ofwords, lo_ofwords. auto. +Qed. + Lemma decompose_ltu: forall xh xl yh yl, ltu (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.ltu xh yh. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index bbe2d3e..e6e9d76 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -193,6 +193,8 @@ Inductive instruction : Type := | Pmtlr: ireg -> instruction (**r move ireg to LR *) | Pmulli: ireg -> ireg -> constant -> instruction (**r integer multiply immediate *) | Pmullw: ireg -> ireg -> ireg -> instruction (**r integer multiply *) + | Pmulhw: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) + | Pmulhwu: ireg -> ireg -> ireg -> instruction (**r multiply high signed *) | Pnand: ireg -> ireg -> ireg -> instruction (**r bitwise not-and *) | Pnor: ireg -> ireg -> ireg -> instruction (**r bitwise not-or *) | Por: ireg -> ireg -> ireg -> instruction (**r bitwise or *) @@ -702,6 +704,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m | Pmullw rd r1 r2 => Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m + | Pmulhw rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.mulhs rs#r1 rs#r2))) m + | Pmulhwu rd r1 r2 => + Next (nextinstr (rs#rd <- (Val.mulhu rs#r1 rs#r2))) m | Pnand rd r1 r2 => Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m | Pnor rd r1 r2 => diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 2b6d80d..cc9a51c 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -371,6 +371,12 @@ Definition transl_op Pmulli r r1 (Cint n) :: k else loadimm GPR0 n (Pmullw r r1 GPR0 :: k)) + | Omulhs, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmulhw r r1 r2 :: k) + | Omulhu, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + OK (Pmulhwu r r1 r2 :: k) | Odiv, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; OK (Pdivw r r1 r2 :: k) diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index e7e4095..d0322c1 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -95,6 +95,8 @@ 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) + | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2) + | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu 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 diff --git a/powerpc/Op.v b/powerpc/Op.v index 1952304..085a098 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -65,6 +65,8 @@ Inductive operation : Type := | Osubimm: int -> operation (**r [rd = n - r1] *) | Omul: operation (**r [rd = r1 * r2] *) | Omulimm: int -> operation (**r [rd = r1 * n] *) + | Omulhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omulhu: operation (**r [rd = high part of r1 * r2, unsigned] *) | Odiv: operation (**r [rd = r1 / r2] (signed) *) | Odivu: operation (**r [rd = r1 / r2] (unsigned) *) | Oand: operation (**r [rd = r1 & r2] *) @@ -185,6 +187,8 @@ Definition eval_operation | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1) | Omul, v1::v2::nil => Some (Val.mul v1 v2) | Omulimm n, v1::nil => Some (Val.mul v1 (Vint n)) + | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) + | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2) | Odiv, v1::v2::nil => Val.divs v1 v2 | Odivu, v1::v2::nil => Val.divu v1 v2 | Oand, v1::v2::nil => Some(Val.and v1 v2) @@ -276,6 +280,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubimm _ => (Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) | Omulimm _ => (Tint :: nil, Tint) + | Omulhs => (Tint :: Tint :: nil, Tint) + | Omulhu => (Tint :: Tint :: nil, Tint) | Odiv => (Tint :: Tint :: nil, Tint) | Odivu => (Tint :: Tint :: nil, Tint) | Oand => (Tint :: Tint :: nil, Tint) @@ -351,6 +357,8 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... 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... @@ -759,6 +767,8 @@ Proof. inv H4; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; 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. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 879d755..08438df 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -818,6 +818,10 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c | Pmullw(r1, r2, r3) -> fprintf oc " mullw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhw(r1, r2, r3) -> + fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhwu(r1, r2, r3) -> + fprintf oc " mulhwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pnand(r1, r2, r3) -> fprintf oc " nand %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pnor(r1, r2, r3) -> diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 7b15ccc..bc9b677 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -290,8 +290,6 @@ Nondetfunction xor (e1: expr) (e2: expr) := (** ** Integer division and modulus *) -Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). - Definition mod_aux (divop: operation) (e1 e2: expr) := Elet e1 (Elet (lift e2) @@ -301,31 +299,13 @@ Definition mod_aux (divop: operation) (e1 e2: expr) := Enil) ::: Enil))). -Definition mods := mod_aux Odiv. - -Definition divuimm (e: expr) (n: int) := - match Int.is_power2 n with - | Some l => shruimm e l - | None => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil) - end. - -Nondetfunction divu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => divuimm e1 n2 - | _ => Eop Odivu (e1:::e2:::Enil) - end. - -Definition moduimm (e: expr) (n: int) := - match Int.is_power2 n with - | Some l => andimm (Int.sub n Int.one) e - | None => mod_aux Odivu e (Eop (Ointconst n) Enil) - end. +Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). +Definition mods_base := mod_aux Odiv. +Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). +Definition modu_base := mod_aux Odivu. -Nondetfunction modu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => moduimm e1 n2 - | _ => mod_aux Odivu e1 e2 - end. +Definition shrximm (e1: expr) (n2: int) := + if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). (** ** General shifts *) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 5a0a903..177d64a 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -465,14 +465,14 @@ Proof. TrivialExists. Qed. -Theorem eval_divs: +Theorem eval_divs_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divs x y = Some z -> - exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divs. exists z; split. EvalOp. auto. + intros. unfold divs_base. exists z; split. EvalOp. auto. Qed. Lemma eval_mod_aux: @@ -501,73 +501,57 @@ Proof. reflexivity. Qed. -Theorem eval_mods: +Theorem eval_mods_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.mods x y = Some z -> - exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold mods. + intros; unfold mods_base. exploit Val.mods_divs; eauto. intros [v [A B]]. subst. econstructor; split; eauto. apply eval_mod_aux with (semdivop := Val.divs); auto. Qed. -Theorem eval_divuimm: - forall le n a x z, - eval_expr ge sp e m le a x -> - Val.divu x (Vint n) = Some z -> - exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v. -Proof. - intros; unfold divuimm. - destruct (Int.is_power2 n) eqn:?. - replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto. - eapply Val.divu_pow2; eauto. - TrivialExists. - econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. -Qed. - -Theorem eval_divu: - forall le a x b y z, +Theorem eval_divu_base: + forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divu x y = Some z -> - exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. - intros until z. unfold divu; destruct (divu_match b); intros; InvEval. - eapply eval_divuimm; eauto. - TrivialExists. + intros. unfold divu_base. exists z; split. EvalOp. auto. Qed. -Theorem eval_moduimm: - forall le n a x z, +Theorem eval_modu_base: + forall le a b x y z, eval_expr ge sp e m le a x -> - Val.modu x (Vint n) = Some z -> - exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v. + eval_expr ge sp e m le b y -> + Val.modu x y = Some z -> + exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros; unfold moduimm. - destruct (Int.is_power2 n) eqn:?. - replace z with (Val.and x (Vint (Int.sub n Int.one))). apply eval_andimm; auto. - eapply Val.modu_pow2; eauto. + intros; unfold modu_base. exploit Val.modu_divu; eauto. intros [v [A B]]. subst. econstructor; split; eauto. apply eval_mod_aux with (semdivop := Val.divu); auto. - EvalOp. Qed. -Theorem eval_modu: - forall le a x b y z, +Theorem eval_shrximm: + forall le a n x z, eval_expr ge sp e m le a x -> - eval_expr ge sp e m le b y -> - Val.modu x y = Some z -> - exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v. + Val.shrx x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v. Proof. - intros until y; unfold modu; case (modu_match b); intros; InvEval. - eapply eval_moduimm; eauto. - exploit Val.modu_divu; eauto. intros [v [A B]]. - subst. econstructor; split; eauto. - apply eval_mod_aux with (semdivop := Val.divu); auto. + intros. unfold shrximm. + predSpec Int.eq Int.eq_spec n Int.zero. + subst n. exists x; split; auto. + destruct x; simpl in H0; try discriminate. + destruct (Int.ltu Int.zero (Int.repr 31)); inv H0. + replace (Int.shrx i Int.zero) with i. auto. + unfold Int.shrx, Int.divs. rewrite Int.shl_zero. + change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. + econstructor; split. EvalOp. auto. Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. diff --git a/test/regression/Results/int32 b/test/regression/Results/int32 index e0fafc4..1223a5b 100644 --- a/test/regression/Results/int32 +++ b/test/regression/Results/int32 @@ -8,6 +8,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 ~x = ffffffff x & y = 0 x | y = 0 @@ -32,6 +44,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 ~x = ffffffff x & y = 0 x | y = 1 @@ -56,6 +80,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 ~x = ffffffff x & y = 0 x | y = ffffffff @@ -80,6 +116,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 ~x = ffffffff x & y = 0 x | y = 7fffffff @@ -104,6 +152,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 ~x = ffffffff x & y = 0 x | y = 80000000 @@ -128,6 +188,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = 0 +x /u 5 = 0 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = 0 +x /u 11 = 0 +x %u 11 = 0 +x /s 11 = 0 +x %s 11 = 0 ~x = ffffffff x & y = 0 x | y = 6255 @@ -152,6 +224,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 228b7b22 +x %u 3 = 0 +x /s 3 = 228b7b22 +x %s 3 = 0 +x /u 5 = 14ba16ae +x %u 5 = 0 +x /s 5 = 14ba16ae +x %s 5 = 0 +x /u 11 = 96bdbc3 +x %u 11 = 5 +x /s 11 = 96bdbc3 +x %s 11 = 5 ~x = 985d8e99 x & y = 0 x | y = 67a27166 @@ -176,6 +260,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 ~x = fffffffe x & y = 0 x | y = 1 @@ -200,6 +296,18 @@ x /u y = 1 x %u y = 0 x /s y = 1 x %s y = 0 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 ~x = fffffffe x & y = 1 x | y = 1 @@ -224,6 +332,18 @@ x /u y = 0 x %u y = 1 x /s y = ffffffff x %s y = 0 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 ~x = fffffffe x & y = 1 x | y = ffffffff @@ -248,6 +368,18 @@ x /u y = 0 x %u y = 1 x /s y = 0 x %s y = 1 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 ~x = fffffffe x & y = 1 x | y = 7fffffff @@ -272,6 +404,18 @@ x /u y = 0 x %u y = 1 x /s y = 0 x %s y = 1 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 ~x = fffffffe x & y = 0 x | y = 80000001 @@ -296,6 +440,18 @@ x /u y = 0 x %u y = 1 x /s y = 0 x %s y = 1 +x /u 3 = 0 +x %u 3 = 1 +x /s 3 = 0 +x %s 3 = 1 +x /u 5 = 0 +x %u 5 = 1 +x /s 5 = 0 +x %s 5 = 1 +x /u 11 = 0 +x %u 11 = 1 +x /s 11 = 0 +x %s 11 = 1 ~x = fffffffe x & y = 1 x | y = ae3d5f03 @@ -320,6 +476,18 @@ x /u y = 3fb9ebc x %u y = 0 x /s y = 3fb9ebc x %s y = 0 +x /u 3 = 153df94 +x %u 3 = 0 +x /s 3 = 153df94 +x %s 3 = 0 +x /u 5 = cbec8c +x %u 5 = 0 +x /s 5 = cbec8c +x %s 5 = 0 +x /u 11 = 5cb156 +x %u 11 = a +x /s 11 = 5cb156 +x %s 11 = a ~x = fc046143 x & y = 0 x | y = 3fb9ebd @@ -344,6 +512,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 55555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffff +x /u 5 = 33333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffff +x /u 11 = 1745d174 +x %u 11 = 3 +x /s 11 = 0 +x %s 11 = ffffffff ~x = 0 x & y = 0 x | y = ffffffff @@ -368,6 +548,18 @@ x /u y = ffffffff x %u y = 0 x /s y = ffffffff x %s y = 0 +x /u 3 = 55555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffff +x /u 5 = 33333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffff +x /u 11 = 1745d174 +x %u 11 = 3 +x /s 11 = 0 +x %s 11 = ffffffff ~x = 0 x & y = 1 x | y = ffffffff @@ -392,6 +584,18 @@ x /u y = 1 x %u y = 0 x /s y = 1 x %s y = 0 +x /u 3 = 55555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffff +x /u 5 = 33333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffff +x /u 11 = 1745d174 +x %u 11 = 3 +x /s 11 = 0 +x %s 11 = ffffffff ~x = 0 x & y = ffffffff x | y = ffffffff @@ -416,6 +620,18 @@ x /u y = 2 x %u y = 1 x /s y = 0 x %s y = ffffffff +x /u 3 = 55555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffff +x /u 5 = 33333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffff +x /u 11 = 1745d174 +x %u 11 = 3 +x /s 11 = 0 +x %s 11 = ffffffff ~x = 0 x & y = 7fffffff x | y = ffffffff @@ -440,6 +656,18 @@ x /u y = 1 x %u y = 7fffffff x /s y = 0 x %s y = ffffffff +x /u 3 = 55555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffff +x /u 5 = 33333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffff +x /u 11 = 1745d174 +x %u 11 = 3 +x /s 11 = 0 +x %s 11 = ffffffff ~x = 0 x & y = 80000000 x | y = ffffffff @@ -464,6 +692,18 @@ x /u y = 1 x %u y = 69b5f51e x /s y = 0 x %s y = ffffffff +x /u 3 = 55555555 +x %u 3 = 0 +x /s 3 = 0 +x %s 3 = ffffffff +x /u 5 = 33333333 +x %u 5 = 0 +x /s 5 = 0 +x %s 5 = ffffffff +x /u 11 = 1745d174 +x %u 11 = 3 +x /s 11 = 0 +x %s 11 = ffffffff ~x = 0 x & y = 964a0ae1 x | y = ffffffff @@ -488,6 +728,18 @@ x /u y = 0 x %u y = 26b98582 x /s y = d9467a7e x %s y = 0 +x /u 3 = ce881d6 +x %u 3 = 0 +x /s 3 = ce881d6 +x %s 3 = 0 +x /u 5 = 7beb44d +x %u 5 = 1 +x /s 5 = 7beb44d +x %s 5 = 1 +x /u 11 = 3853aae +x %u 11 = 8 +x /s 11 = 3853aae +x %s 11 = 8 ~x = d9467a7d x & y = 26b98582 x | y = ffffffff @@ -512,6 +764,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 ~x = 80000000 x & y = 0 x | y = 7fffffff @@ -536,6 +800,18 @@ x /u y = 7fffffff x %u y = 0 x /s y = 7fffffff x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 ~x = 80000000 x & y = 1 x | y = 7fffffff @@ -560,6 +836,18 @@ x /u y = 0 x %u y = 7fffffff x /s y = 80000001 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 ~x = 80000000 x & y = 7fffffff x | y = ffffffff @@ -584,6 +872,18 @@ x /u y = 1 x %u y = 0 x /s y = 1 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 ~x = 80000000 x & y = 7fffffff x | y = 7fffffff @@ -608,6 +908,18 @@ x /u y = 0 x %u y = 7fffffff x /s y = 0 x %s y = 7fffffff +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 ~x = 80000000 x & y = 0 x | y = ffffffff @@ -632,6 +944,18 @@ x /u y = 0 x %u y = 7fffffff x /s y = fffffff6 x %s y = 682f655 +x /u 3 = 2aaaaaaa +x %u 3 = 1 +x /s 3 = 2aaaaaaa +x %s 3 = 1 +x /u 5 = 19999999 +x %u 5 = 2 +x /s 5 = 19999999 +x %s 5 = 2 +x /u 11 = ba2e8ba +x %u 11 = 1 +x /s 11 = ba2e8ba +x %s 11 = 1 ~x = 80000000 x & y = 73d9e56f x | y = ffffffff @@ -656,6 +980,18 @@ x /u y = 0 x %u y = 3b92bf38 x /s y = 0 x %s y = 3b92bf38 +x /u 3 = 13db9512 +x %u 3 = 2 +x /s 3 = 13db9512 +x %s 3 = 2 +x /u 5 = bea263e +x %u 5 = 2 +x /s 5 = bea263e +x %s 5 = 2 +x /u 11 = 56a6e79 +x %u 11 = 5 +x /s 11 = 56a6e79 +x %s 11 = 5 ~x = c46d40c7 x & y = 3b92bf38 x | y = 7fffffff @@ -680,6 +1016,18 @@ x /u y = 0 x %u y = 0 x /s y = 0 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = d5555556 +x %s 3 = fffffffe +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = e6666667 +x %s 5 = fffffffd +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = f45d1746 +x %s 11 = fffffffe ~x = 7fffffff x & y = 0 x | y = 80000000 @@ -704,6 +1052,18 @@ x /u y = 80000000 x %u y = 0 x /s y = 80000000 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = d5555556 +x %s 3 = fffffffe +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = e6666667 +x %s 5 = fffffffd +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = f45d1746 +x %s 11 = fffffffe ~x = 7fffffff x & y = 0 x | y = 80000001 @@ -728,6 +1088,18 @@ x /u y = 0 x %u y = 80000000 x /s y = 0 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = d5555556 +x %s 3 = fffffffe +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = e6666667 +x %s 5 = fffffffd +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = f45d1746 +x %s 11 = fffffffe ~x = 7fffffff x & y = 80000000 x | y = ffffffff @@ -752,6 +1124,18 @@ x /u y = 1 x %u y = 1 x /s y = ffffffff x %s y = ffffffff +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = d5555556 +x %s 3 = fffffffe +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = e6666667 +x %s 5 = fffffffd +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = f45d1746 +x %s 11 = fffffffe ~x = 7fffffff x & y = 0 x | y = ffffffff @@ -776,6 +1160,18 @@ x /u y = 1 x %u y = 0 x /s y = 1 x %s y = 0 +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = d5555556 +x %s 3 = fffffffe +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = e6666667 +x %s 5 = fffffffd +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = f45d1746 +x %s 11 = fffffffe ~x = 7fffffff x & y = 80000000 x | y = 80000000 @@ -800,6 +1196,18 @@ x /u y = 0 x %u y = 80000000 x /s y = 5 x %s y = fac93d1f +x /u 3 = 2aaaaaaa +x %u 3 = 2 +x /s 3 = d5555556 +x %s 3 = fffffffe +x /u 5 = 19999999 +x %u 5 = 3 +x /s 5 = e6666667 +x %s 5 = fffffffd +x /u 11 = ba2e8ba +x %u 11 = 2 +x /s 11 = f45d1746 +x %s 11 = fffffffe ~x = 7fffffff x & y = 80000000 x | y = e7715a2d @@ -824,6 +1232,18 @@ x /u y = 0 x %u y = 7186e15e x /s y = 0 x %s y = 7186e15e +x /u 3 = 25d7a074 +x %u 3 = 2 +x /s 3 = 25d7a074 +x %s 3 = 2 +x /u 5 = 16b49379 +x %u 5 = 1 +x /s 5 = 16b49379 +x %s 5 = 1 +x /u 11 = a52147c +x %u 11 = a +x /s 11 = a52147c +x %s 11 = a ~x = 8e791ea1 x & y = 0 x | y = f186e15e @@ -848,6 +1268,18 @@ x /u y = 1 x %u y = 2164c327 x /s y = 0 x %s y = a3d2a09b +x /u 3 = 369b8ade +x %u 3 = 1 +x /s 3 = e1463589 +x %s 3 = 0 +x /u 5 = 20c3b9b8 +x %u 5 = 3 +x /s 5 = ed908686 +x %s 5 = fffffffd +x /u 11 = ee49a3c +x %u 11 = 7 +x /s 11 = f79ec8c9 +x %s 11 = fffffff8 ~x = 5c2d5f64 x & y = 82408010 x | y = a3fffdff @@ -872,6 +1304,18 @@ x /u y = 1 x %u y = 247f3b3f x /s y = 0 x %s y = e3ad9c39 +x /u 3 = 4be48968 +x %u 3 = 1 +x /s 3 = f68f3413 +x %s 3 = 0 +x /u 5 = 2d891f3e +x %u 5 = 3 +x /s 5 = fa55ec0c +x %s 5 = fffffffd +x /u 11 = 14b2b11c +x %u 11 = 5 +x /s 11 = fd6cdfa9 +x %s 11 = fffffff6 ~x = 1c5263c6 x & y = a32c0038 x | y = ffaffcfb @@ -896,6 +1340,18 @@ x /u y = a x %u y = 50aa627 x /s y = fffffffe x %s y = fd712767 +x /u 3 = 46ae3ed7 +x %u 3 = 2 +x /s 3 = f158e983 +x %s 3 = fffffffe +x /u 5 = 2a688c1b +x %u 5 = 0 +x /s 5 = f73558e8 +x %s 5 = ffffffff +x /u 11 = 1346cb52 +x %u 11 = 1 +x /s 11 = fc00f9de +x %s 11 = fffffffd ~x = 2bf54378 x & y = 14023400 x | y = d4bbbdf7 @@ -920,6 +1376,18 @@ x /u y = 0 x %u y = e2a8dd05 x /s y = 2 x %s y = ffb99c59 +x /u 3 = 4b8d9f01 +x %u 3 = 2 +x /s 3 = f63849ad +x %s 3 = fffffffe +x /u 5 = 2d54f901 +x %u 5 = 0 +x /s 5 = fa21c5ce +x %s 5 = ffffffff +x /u 11 = 149afcd1 +x %u 11 = a +x /s 11 = fd552b5e +x %s 11 = fffffffb ~x = 1d5722fa x & y = e0208004 x | y = f3fffd57 @@ -944,6 +1412,18 @@ x /u y = 0 x %u y = 10462533 x /s y = 0 x %s y = 10462533 +x /u 3 = 56cb711 +x %u 3 = 0 +x /s 3 = 56cb711 +x %s 3 = 0 +x /u 5 = 3413aa3 +x %u 5 = 4 +x /s 5 = 3413aa3 +x %s 5 = 4 +x /u 11 = 17abd90 +x %u 11 = 3 +x /s 11 = 17abd90 +x %s 11 = 3 ~x = efb9dacc x & y = 10420120 x | y = bd46e73f @@ -968,6 +1448,18 @@ x /u y = 1 x %u y = 5121ed1f x /s y = 0 x %s y = b58be891 +x /u 3 = 3c83f830 +x %u 3 = 1 +x /s 3 = e72ea2db +x %s 3 = 0 +x /u 5 = 244f2e83 +x %u 5 = 2 +x /s 5 = f11bfb51 +x %s 5 = fffffffc +x /u 11 = 10811524 +x %u 11 = 5 +x /s 11 = f93b43b1 +x %s 11 = fffffff6 ~x = 4a74176e x & y = 2409e810 x | y = f5ebfbf3 @@ -992,6 +1484,18 @@ x /u y = 3 x %u y = cfebea7 x /s y = 0 x %s y = c615869f +x /u 3 = 42072cdf +x %u 3 = 2 +x /s 3 = ecb1d78b +x %s 3 = fffffffe +x /u 5 = 279de7b9 +x %u 5 = 2 +x /s 5 = f46ab487 +x %s 5 = fffffffc +x /u 11 = 1201f4f7 +x %u 11 = 2 +x /s 11 = fabc2383 +x %s 11 = fffffffe ~x = 39ea7960 x & y = 4100288 x | y = ffb7c6bf @@ -1016,6 +1520,18 @@ x /u y = 0 x %u y = b7ca4add x /s y = 1 x %s y = fa21bc8f +x /u 3 = 3d436e49 +x %u 3 = 2 +x /s 3 = e7ee18f5 +x %s 3 = fffffffe +x /u 5 = 24c20ef9 +x %u 5 = 0 +x /s 5 = f18edbc6 +x %s 5 = ffffffff +x /u 11 = 10b54c9f +x %u 11 = 8 +x /s 11 = f96f7b2c +x %s 11 = fffffff9 ~x = 4835b522 x & y = b5880a4c x | y = bfeacedf @@ -1040,6 +1556,18 @@ x /u y = 1 x %u y = 11791ce7 x /s y = 0 x %s y = fd824ccb +x /u 3 = 5480c443 +x %u 3 = 2 +x /s 3 = ff2b6eef +x %s 3 = fffffffe +x /u 5 = 32b3a8f5 +x %u 5 = 2 +x /s 5 = ff8075c3 +x %s 5 = fffffffc +x /u 11 = 170bd86f +x %u 11 = 6 +x /s 11 = ffc606fc +x %s 11 = fffffff7 ~x = 27db334 x & y = ec000cc0 x | y = fd8b6fef @@ -1064,6 +1592,18 @@ x /u y = 0 x %u y = aaae4fe9 x /s y = 2 x %s y = fb91e615 +x /u 3 = 38e4c54d +x %u 3 = 2 +x /s 3 = e38f6ff9 +x %s 3 = fffffffe +x /u 5 = 2222dcc8 +x %u 5 = 1 +x /s 5 = eeefa995 +x %s 5 = 0 +x /u 11 = f8435cf +x %u 11 = 4 +x /s 11 = f83e645b +x %s 11 = 0 ~x = 5551b016 x & y = 828e04e8 x | y = ffae7feb @@ -1088,6 +1628,18 @@ x /u y = 0 x %u y = a7aa3b7 x /s y = 0 x %s y = a7aa3b7 +x /u 3 = 37e3692 +x %u 3 = 1 +x /s 3 = 37e3692 +x %s 3 = 1 +x /u 5 = 2188724 +x %u 5 = 3 +x /s 5 = 2188724 +x %s 5 = 3 +x /u 11 = f3e056 +x %u 11 = 5 +x /s 11 = f3e056 +x %s 11 = 5 ~x = f5855c48 x & y = 23882a0 x | y = 4a7ee7f7 @@ -1112,6 +1664,18 @@ x /u y = 1 x %u y = 39b786f x /s y = 0 x %s y = e7a503b5 +x /u 3 = 4d37013c +x %u 3 = 1 +x /s 3 = f7e1abe7 +x %s 3 = 0 +x /u 5 = 2e5433f1 +x %u 5 = 0 +x /s 5 = fb2100be +x %s 5 = ffffffff +x /u 11 = 150f0056 +x %u 11 = 3 +x /s 11 = fdc92ee2 +x %s 11 = ffffffff ~x = 185afc4a x & y = e4010304 x | y = e7ad8bf7 @@ -1136,6 +1700,18 @@ x /u y = 0 x %u y = a2fd7763 x /s y = 2 x %s y = ec25702b +x /u 3 = 36547d21 +x %u 3 = 0 +x /s 3 = e0ff27cc +x %s 3 = ffffffff +x /u 5 = 209917e0 +x %u 5 = 3 +x /s 5 = ed65e4ae +x %s 5 = fffffffd +x /u 11 = ed13966 +x %u 11 = 1 +x /s 11 = f78b67f2 +x %s 11 = fffffffd ~x = 5d02889c x & y = 826c0300 x | y = fbfd77ff @@ -1160,6 +1736,18 @@ x /u y = 0 x %u y = 354a3241 x /s y = 0 x %s y = 354a3241 +x /u 3 = 11c36615 +x %u 3 = 2 +x /s 3 = 11c36615 +x %s 3 = 2 +x /u 5 = aa87073 +x %u 5 = 2 +x /s 5 = aa87073 +x %s 5 = 2 +x /u 11 = 4d8331d +x %u 11 = 2 +x /s 11 = 4d8331d +x %s 11 = 2 ~x = cab5cdbe x & y = 21082040 x | y = b77aff63 @@ -1184,6 +1772,18 @@ x /u y = 4 x %u y = 1a97eb6f x /s y = fffffffc x %s y = f174fc2f +x /u 3 = 2cacd145 +x %u 3 = 0 +x /s 3 = d7577bf0 +x %s 3 = ffffffff +x /u 5 = 1ace1729 +x %u 5 = 2 +x /s 5 = e79ae3f7 +x %s 5 = fffffffc +x /u 11 = c2f21cd +x %u 11 = 0 +x /s 11 = f4e95059 +x %s 11 = fffffffc ~x = 79f98c30 x & y = 2022208 x | y = 9edff3df @@ -1208,6 +1808,18 @@ x /u y = 1 x %u y = 16df04f x /s y = 1 x %s y = 16df04f +x /u 3 = 191177d9 +x %u 3 = 2 +x /s 3 = 191177d9 +x %s 3 = 2 +x /u 5 = f0a7b1c +x %u 5 = 1 +x /s 5 = f0a7b1c +x %s 5 = 1 +x /u 11 = 6d637f5 +x %u 11 = 6 +x /s 11 = 6d637f5 +x %s 11 = 6 ~x = b4cb9872 x & y = 4904670c x | y = 4bf677bf @@ -1232,6 +1844,18 @@ x /u y = 1 x %u y = 2687e6a7 x /s y = 0 x %s y = 9f3a04fb +x /u 3 = 351356fe +x %u 3 = 1 +x /s 3 = dfbe01a9 +x %s 3 = 0 +x /u 5 = 1fd86765 +x %u 5 = 2 +x /s 5 = eca53433 +x %s 5 = fffffffc +x /u 11 = e79a35c +x %u 11 = 7 +x /s 11 = f733d1e9 +x %s 11 = fffffff8 ~x = 60c5fb04 x & y = 18320450 x | y = ffba1eff @@ -1256,6 +1880,18 @@ x /u y = 1 x %u y = 5d7ceabf x /s y = 0 x %s y = d080ef99 +x /u 3 = 45804fdd +x %u 3 = 2 +x /s 3 = f02afa89 +x %s 3 = fffffffe +x /u 5 = 29b3631e +x %u 5 = 3 +x /s 5 = f6802fec +x %s 5 = fffffffd +x /u 11 = 12f472df +x %u 11 = 4 +x /s 11 = fbaea16b +x %s 11 = 0 ~x = 2f7f1066 x & y = 50000498 x | y = f384efdb @@ -1280,6 +1916,18 @@ x /u y = 1 x %u y = 22dda297 x /s y = 1 x %s y = 22dda297 +x /u 3 = 1bc5c7a2 +x %u 3 = 1 +x /s 3 = 1bc5c7a2 +x %s 3 = 1 +x /u 5 = 10a9de2e +x %u 5 = 1 +x /s 5 = 10a9de2e +x %s 5 = 1 +x /u 11 = 79307e6 +x %u 11 = 5 +x /s 11 = 79307e6 +x %s 11 = 5 ~x = acaea918 x & y = 10511440 x | y = 7373f6f7 @@ -1304,6 +1952,18 @@ x /u y = 1 x %u y = 2658a42f x /s y = 1 x %s y = 2658a42f +x /u 3 = 205ff221 +x %u 3 = 2 +x /s 3 = 205ff221 +x %s 3 = 2 +x /u 5 = 136cc47a +x %u 5 = 3 +x /s 5 = 136cc47a +x %s 5 = 3 +x /u 11 = 8d4594f +x %u 11 = 0 +x /s 11 = 8d4594f +x %s 11 = 0 ~x = 9ee0299a x & y = 20071224 x | y = 7bdff677 @@ -1328,6 +1988,18 @@ x /u y = 0 x %u y = 61465593 x /s y = ffffffff x %s y = 2e84b59f +x /u 3 = 206cc731 +x %u 3 = 0 +x /s 3 = 206cc731 +x %s 3 = 0 +x /u 5 = 13747783 +x %u 5 = 4 +x /s 5 = 13747783 +x %s 5 = 4 +x /u 11 = 8d7d93b +x %u 11 = a +x /s 11 = 8d7d93b +x %s 11 = a ~x = 9eb9aa6c x & y = 41064000 x | y = ed7e759f @@ -1352,6 +2024,18 @@ x /u y = 2 x %u y = 2fd5314d x /s y = 0 x %s y = e5dfe7f1 +x /u 3 = 4c9ff7fb +x %u 3 = 0 +x /s 3 = f74aa2a6 +x %s 3 = ffffffff +x /u 5 = 2df994c9 +x %u 5 = 4 +x /s 5 = fac66197 +x %s 5 = fffffffe +x /u 11 = 14e5cf44 +x %u 11 = 5 +x /s 11 = fd9ffdd1 +x %s 11 = fffffff6 ~x = 1a20180e x & y = 41054350 x | y = ffdffff3 @@ -1376,6 +2060,18 @@ x /u y = 0 x %u y = 843facff x /s y = 2 x %s y = e4b3f1ef +x /u 3 = 2c1539aa +x %u 3 = 1 +x /s 3 = d6bfe455 +x %s 3 = 0 +x /u 5 = 1a732299 +x %u 5 = 2 +x /s 5 = e73fef67 +x %s 5 = fffffffc +x /u 11 = c05c9e8 +x %u 11 = 7 +x /s 11 = f4bff875 +x %s 11 = fffffff8 ~x = 7bc05300 x & y = 84058c88 x | y = cffffdff @@ -1400,6 +2096,18 @@ x /u y = 0 x %u y = 4b3ab03d x /s y = fffffffd x %s y = 6c984c7 +x /u 3 = 19139014 +x %u 3 = 1 +x /s 3 = 19139014 +x %s 3 = 1 +x /u 5 = f0bbcd9 +x %u 5 = 0 +x /s 5 = f0bbcd9 +x %s 5 = 0 +x /u 11 = 6d6ca34 +x %u 11 = 1 +x /s 11 = 6d6ca34 +x %s 11 = 1 ~x = b4c54fc2 x & y = 492a902c x | y = eb3fbc3f @@ -1424,6 +2132,18 @@ x /u y = 1 x %u y = 582d2067 x /s y = 0 x %s y = c23cc92b +x /u 3 = 40beedb9 +x %u 3 = 0 +x /s 3 = eb699864 +x %s 3 = ffffffff +x /u 5 = 26d8f508 +x %u 5 = 3 +x /s 5 = f3a5c1d6 +x %s 5 = fffffffd +x /u 11 = 11a86f61 +x %u 11 = 0 +x /s 11 = fa629ded +x %s 11 = fffffffc ~x = 3dc336d4 x & y = 420c8800 x | y = ea3fe9ef @@ -1448,6 +2168,18 @@ x /u y = 6 x %u y = 707968d x /s y = 6 x %s y = 707968d +x /u 3 = 20f57e6d +x %u 3 = 2 +x /s 3 = 20f57e6d +x %s 3 = 2 +x /u 5 = 13c67f0e +x %u 5 = 3 +x /s 5 = 13c67f0e +x %s 5 = 3 +x /u 11 = 8fd227b +x %u 11 = 0 +x /s 11 = 8fd227b +x %s 11 = 0 ~x = 9d1f84b6 x & y = 2405048 x | y = 6feefbcb @@ -1472,6 +2204,18 @@ x /u y = 1 x %u y = 692d857 x /s y = 1 x %s y = 692d857 +x /u 3 = 6809cb2 +x %u 3 = 1 +x /s 3 = 6809cb2 +x %s 3 = 1 +x /u 5 = 3e6c46b +x %u 5 = 0 +x /s 5 = 3e6c46b +x %s 5 = 0 +x /u 11 = 1c5fc30 +x %u 11 = 7 +x /s 11 = 1c5fc30 +x %s 11 = 7 ~x = ec7e29e8 x & y = 80d400 x | y = 1fefffd7 @@ -1496,6 +2240,18 @@ x /u y = 0 x %u y = 7c045515 x /s y = fffffffd x %s y = 12a31487 +x /u 3 = 2956c707 +x %u 3 = 0 +x /s 3 = 2956c707 +x %s 3 = 0 +x /u 5 = 18cdaa9d +x %u 5 = 4 +x /s 5 = 18cdaa9d +x %s 5 = 4 +x /u 11 = b463647 +x %u 11 = 8 +x /s 11 = b463647 +x %s 11 = 8 ~x = 83fbaaea x & y = 5c041504 x | y = fcdfd537 @@ -1520,6 +2276,18 @@ x /u y = 3 x %u y = 501364f x /s y = 0 x %s y = cec3bfc3 +x /u 3 = 44ebea96 +x %u 3 = 1 +x /s 3 = ef969541 +x %s 3 = 0 +x /u 5 = 295a598d +x %u 5 = 2 +x /s 5 = f627265b +x %s 5 = fffffffc +x /u 11 = 12cbfa29 +x %u 11 = 0 +x /s 11 = fb8628b5 +x %s 11 = fffffffc ~x = 313c403c x & y = 42409840 x | y = cfc3ffff @@ -1544,6 +2312,18 @@ x /u y = 16 x %u y = 2ee15f5 x /s y = 0 x %s y = fe6809a1 +x /u 3 = 54cd588b +x %u 3 = 0 +x /s 3 = ff780336 +x %s 3 = ffffffff +x /u 5 = 32e19b86 +x %u 5 = 3 +x /s 5 = ffae6854 +x %s 5 = fffffffd +x /u 11 = 1720bb0e +x %u 11 = 7 +x /s 11 = ffdae99b +x %s 11 = fffffff8 ~x = 197f65e x & y = a680100 x | y = ff6e4de3 @@ -1568,6 +2348,18 @@ x /u y = 0 x %u y = 614322f x /s y = 0 x %s y = 614322f +x /u 3 = 206bb65 +x %u 3 = 0 +x /s 3 = 206bb65 +x %s 3 = 0 +x /u 5 = 1373d3c +x %u 5 = 3 +x /s 5 = 1373d3c +x %s 5 = 3 +x /u 11 = 8d78ed +x %u 11 = 0 +x /s 11 = 8d78ed +x %s 11 = 0 ~x = f9ebcdd0 x & y = 6043028 x | y = 16f7f6ff @@ -1592,6 +2384,18 @@ x /u y = 0 x %u y = 142824ed x /s y = 0 x %s y = 142824ed +x /u 3 = 6b80c4f +x %u 3 = 0 +x /s 3 = 6b80c4f +x %s 3 = 0 +x /u 5 = 4080762 +x %u 5 = 3 +x /s 5 = 4080762 +x %s 5 = 3 +x /u 11 = 1d51aa1 +x %u 11 = 2 +x /s 11 = 1d51aa1 +x %s 11 = 2 ~x = ebd7db12 x & y = 1020240c x | y = 56fafdff @@ -1616,6 +2420,18 @@ x /u y = 0 x %u y = c08d995b x /s y = e x %s y = ff124483 +x /u 3 = 402f331e +x %u 3 = 1 +x /s 3 = ead9ddc9 +x %s 3 = 0 +x /u 5 = 2682b845 +x %u 5 = 2 +x /s 5 = f34f8513 +x %s 5 = fffffffc +x /u 11 = 11813c7c +x %u 11 = 7 +x /s 11 = fa3b6b09 +x %s 11 = fffffff8 ~x = 3f7266a4 x & y = c0888910 x | y = fb8ddf7f @@ -1640,6 +2456,18 @@ x /u y = 0 x %u y = 2e47f2f9 x /s y = 0 x %s y = 2e47f2f9 +x /u 3 = f6d50fd +x %u 3 = 2 +x /s 3 = f6d50fd +x %s 3 = 2 +x /u 5 = 94196fe +x %u 5 = 3 +x /s 5 = 94196fe +x %s 5 = 3 +x /u 11 = 4351616 +x %u 11 = 7 +x /s 11 = 4351616 +x %s 11 = 7 ~x = d1b80d06 x & y = 284590b8 x | y = afeffafb @@ -1664,6 +2492,18 @@ x /u y = 0 x %u y = bcbf2147 x /s y = d x %s y = fd75d7d7 +x /u 3 = 3eea606d +x %u 3 = 0 +x /s 3 = e9950b18 +x %s 3 = ffffffff +x /u 5 = 25bfd374 +x %u 5 = 3 +x /s 5 = f28ca042 +x %s 5 = fffffffd +x /u 11 = 1128a5ef +x %u 11 = 2 +x /s 11 = f9e2d47b +x %s 11 = fffffffe ~x = 4340deb8 x & y = b8052100 x | y = ffbfa377 @@ -1688,6 +2528,18 @@ x /u y = 1 x %u y = 62bbcbaf x /s y = 0 x %s y = effd7fc5 +x /u 3 = 4fff2a97 +x %u 3 = 0 +x /s 3 = faa9d542 +x %s 3 = ffffffff +x /u 5 = 2fff7ff4 +x %u 5 = 1 +x /s 5 = fccc4cc1 +x %s 5 = 0 +x /u 11 = 15d13a29 +x %u 11 = 2 +x /s 11 = fe8b68b5 +x %s 11 = fffffffe ~x = 1002803a x & y = 8d413404 x | y = effdffd7 @@ -1712,6 +2564,18 @@ x /u y = 0 x %u y = 27d8b5f3 x /s y = 0 x %s y = 27d8b5f3 +x /u 3 = d483ca6 +x %u 3 = 1 +x /s 3 = d483ca6 +x %s 3 = 1 +x /u 5 = 7f82463 +x %u 5 = 4 +x /s 5 = 7f82463 +x %s 5 = 4 +x /u 11 = 39f565b +x %u 11 = a +x /s 11 = 39f565b +x %s 11 = a ~x = d8274a0c x & y = 79824e0 x | y = bffafdff @@ -1736,6 +2600,18 @@ x /u y = 4 x %u y = 1d72ea89 x /s y = ffffffff x %s y = f8904283 +x /u 3 = 443f3270 +x %u 3 = 1 +x /s 3 = eee9dd1b +x %s 3 = 0 +x /u 5 = 28f2b7dd +x %u 5 = 0 +x /s 5 = f5bf84aa +x %s 5 = ffffffff +x /u 11 = 129cdf35 +x %u 11 = a +x /s 11 = fb570dc2 +x %s 11 = fffffffb ~x = 334268ae x & y = 8908310 x | y = efffbf73 @@ -1760,6 +2636,18 @@ x /u y = 0 x %u y = 7597035f x /s y = fffffffe x %s y = 2688d42f +x /u 3 = 27325675 +x %u 3 = 0 +x /s 3 = 27325675 +x %s 3 = 0 +x /u 5 = 17849a46 +x %u 5 = 1 +x /s 5 = 17849a46 +x %s 5 = 1 +x /u 11 = ab0a337 +x %u 11 = 2 +x /s 11 = ab0a337 +x %s 11 = 2 ~x = 8a68fca0 x & y = 50100048 x | y = fdffeb7f @@ -1784,6 +2672,18 @@ x /u y = 5 x %u y = ba9c357 x /s y = 5 x %s y = ba9c357 +x /u 3 = 21ad41df +x %u 3 = 0 +x /s 3 = 21ad41df +x %s 3 = 0 +x /u 5 = 1434c11f +x %u 5 = 2 +x /s 5 = 1434c11f +x %s 5 = 2 +x /u 11 = 92f4082 +x %u 11 = 7 +x /s 11 = 92f4082 +x %s 11 = 7 ~x = 9af83a62 x & y = 107800c x | y = 75dfdf9f @@ -1808,6 +2708,18 @@ x /u y = 0 x %u y = 44ef758b x /s y = ffffffff x %s y = 1734072f +x /u 3 = 16fa7c83 +x %u 3 = 2 +x /s 3 = 16fa7c83 +x %s 3 = 2 +x /u 5 = dc97de8 +x %u 5 = 3 +x /s 5 = dc97de8 +x %s 5 = 3 +x /u 11 = 6445081 +x %u 11 = 0 +x /s 11 = 6445081 +x %s 11 = 0 ~x = bb108a74 x & y = 40441180 x | y = d6eff5af @@ -1832,6 +2744,18 @@ x /u y = 0 x %u y = 6df256a9 x /s y = ffffffff x %s y = 1e11b353 +x /u 3 = 24a61ce3 +x %u 3 = 0 +x /s 3 = 24a61ce3 +x %s 3 = 0 +x /u 5 = 15fd4488 +x %u 5 = 1 +x /s 5 = 15fd4488 +x %s 5 = 1 +x /u 11 = 9fec20f +x %u 11 = 4 +x /s 11 = 9fec20f +x %s 11 = 4 ~x = 920da956 x & y = 201254a8 x | y = fdff5eab @@ -1856,6 +2780,18 @@ x /u y = 1 x %u y = 79ad93d7 x /s y = 0 x %s y = fd7c3877 +x /u 3 = 547ebd7d +x %u 3 = 0 +x /s 3 = ff296828 +x %s 3 = ffffffff +x /u 5 = 32b271b1 +x %u 5 = 2 +x /s 5 = ff7f3e7f +x %s 5 = fffffffc +x /u 11 = 170b4af3 +x %u 11 = 6 +x /s 11 = ffc57980 +x %s 11 = fffffff7 ~x = 283c788 x & y = 814c2020 x | y = fffebcf7 @@ -1880,6 +2816,18 @@ x /u y = 0 x %u y = af765675 x /s y = 2 x %s y = fa3d3869 +x /u 3 = 3a7cc77c +x %u 3 = 1 +x /s 3 = e5277227 +x %s 3 = 0 +x /u 5 = 2317aae4 +x %u 5 = 1 +x /s 5 = efe477b1 +x %s 5 = 0 +x /u 11 = ff37c39 +x %u 11 = 2 +x /s 11 = f8adaac5 +x %s 11 = fffffffe ~x = 5089a98a x & y = 8a140604 x | y = fffedf77 @@ -1904,6 +2852,18 @@ x /u y = 1 x %u y = 2af61ac7 x /s y = ffffffff x %s y = f85a557f +x /u 3 = 308d680b +x %u 3 = 2 +x /s 3 = db3812b7 +x %s 3 = fffffffe +x /u 5 = 1d21a4d3 +x %u 5 = 4 +x /s 5 = e9ee71a1 +x %s 5 = fffffffe +x /u 11 = d3dd68e +x %u 11 = 9 +x /s 11 = f5f8051b +x %s 11 = fffffffa ~x = 6e57c7dc x & y = a01800 x | y = f7ba3d7f @@ -1928,6 +2888,18 @@ x /u y = 3 x %u y = 1386e99b x /s y = 3 x %s y = 1386e99b +x /u 3 = 21d3db00 +x %u 3 = 1 +x /s 3 = 21d3db00 +x %s 3 = 1 +x /u 5 = 144be9cd +x %u 5 = 0 +x /s 5 = 144be9cd +x %s 5 = 0 +x /u 11 = 939c75d +x %u 11 = 2 +x /s 11 = 939c75d +x %s 11 = 2 ~x = 9a846efe x & y = 1518100 x | y = 7f7b9d23 @@ -1952,6 +2924,18 @@ x /u y = 0 x %u y = 919b208f x /s y = 1 x %s y = f72b68b7 +x /u 3 = 30890ada +x %u 3 = 1 +x /s 3 = db33b585 +x %s 3 = 0 +x /u 5 = 1d1f0683 +x %u 5 = 0 +x /s 5 = e9ebd350 +x %s 5 = ffffffff +x /u 11 = d3ca5de +x %u 11 = 5 +x /s 11 = f5f6d46b +x %s 11 = fffffff6 ~x = 6e64df70 x & y = 900b2088 x | y = 9bffb7df @@ -1976,6 +2960,18 @@ x /u y = 0 x %u y = fa4924d x /s y = 0 x %s y = fa4924d +x /u 3 = 536db6f +x %u 3 = 0 +x /s 3 = 536db6f +x %s 3 = 0 +x /u 5 = 320ea0f +x %u 5 = 2 +x /s 5 = 320ea0f +x %s 5 = 2 +x /u 11 = 16c0d4c +x %u 11 = 9 +x /s 11 = 16c0d4c +x %s 11 = 9 ~x = f05b6db2 x & y = 484124c x | y = 7fa4f2ff @@ -2000,6 +2996,18 @@ x /u y = 1 x %u y = dbb6da7 x /s y = 1 x %s y = dbb6da7 +x /u 3 = 28f71f3e +x %u 3 = 1 +x /s 3 = 28f71f3e +x %s 3 = 1 +x /u 5 = 189445f2 +x %u 5 = 1 +x /s 5 = 189445f2 +x %s 5 = 1 +x /u 11 = b2c1fcb +x %u 11 = 2 +x /s 11 = b2c1fcb +x %s 11 = 2 ~x = 851aa244 x & y = 68215010 x | y = 7fedfdbf @@ -2024,6 +3032,18 @@ x /u y = 0 x %u y = 7bdaa659 x /s y = fffffff9 x %s y = 4106e8f +x /u 3 = 2948e21d +x %u 3 = 2 +x /s 3 = 2948e21d +x %s 3 = 2 +x /u 5 = 18c55478 +x %u 5 = 1 +x /s 5 = 18c55478 +x %s 5 = 1 +x /u 11 = b426c36 +x %u 11 = 7 +x /s 11 = b426c36 +x %s 11 = 7 ~x = 842559a6 x & y = 6ac20418 x | y = fffbbedb @@ -2048,6 +3068,18 @@ x /u y = 27 x %u y = 1e4cb37 x /s y = fffffffe x %s y = fd2e1fc7 +x /u 3 = 504eb3e2 +x %u 3 = 1 +x /s 3 = faf95e8d +x %s 3 = 0 +x /u 5 = 302f38bb +x %u 5 = 0 +x /s 5 = fcfc0588 +x %s 5 = ffffffff +x /u 11 = 15e6eb3d +x %u 11 = 8 +x /s 11 = fea119ca +x %s 11 = fffffff9 ~x = f13e458 x & y = 200200 x | y = f6ed1bb7 @@ -2072,6 +3104,18 @@ x /u y = 9 x %u y = d41837f x /s y = fffffffa x %s y = f3d4bce9 +x /u 3 = 32889db7 +x %u 3 = 0 +x /s 3 = dd334862 +x %s 3 = ffffffff +x /u 5 = 1e51f83a +x %u 5 = 3 +x /s 5 = eb1ec508 +x %s 5 = fffffffd +x /u 11 = dc82b03 +x %u 11 = 4 +x /s 11 = f682598f +x %s 11 = 0 ~x = 686626da x & y = 7190124 x | y = 9fdffdf7 @@ -2096,6 +3140,18 @@ x /u y = 0 x %u y = 4a154653 x /s y = 0 x %s y = 4a154653 +x /u 3 = 18b1c21b +x %u 3 = 2 +x /s 3 = 18b1c21b +x %s 3 = 2 +x /u 5 = ed10e10 +x %u 5 = 3 +x /s 5 = ed10e10 +x %s 5 = 3 +x /u 11 = 6bc1daa +x %u 11 = 5 +x /s 11 = 6bc1daa +x %s 11 = 5 ~x = b5eab9ac x & y = 8044040 x | y = efffefdf @@ -2120,6 +3176,18 @@ x /u y = 5 x %u y = b5f57 x /s y = 5 x %s y = b5f57 +x /u 3 = 1bfefce5 +x %u 3 = 2 +x /s 3 = 1bfefce5 +x %s 3 = 2 +x /u 5 = 10cc3156 +x %u 5 = 3 +x /s 5 = 10cc3156 +x %s 5 = 3 +x /u 11 = 7a2a210 +x %u 11 = 1 +x /s 11 = 7a2a210 +x %s 11 = 1 ~x = ac03094e x & y = 10c8e210 x | y = 53fdffb3 @@ -2144,6 +3212,18 @@ x /u y = 0 x %u y = 9db389bf x /s y = 6 x %s y = fa9f360f +x /u 3 = 34912dea +x %u 3 = 1 +x /s 3 = df3bd895 +x %s 3 = 0 +x /u 5 = 1f8a4ebf +x %u 5 = 4 +x /s 5 = ec571b8d +x %s 5 = fffffffe +x /u 11 = e5623cb +x %u 11 = 6 +x /s 11 = f7105258 +x %s 11 = fffffff7 ~x = 624c7640 x & y = 90830108 x | y = fdb3ebff @@ -2168,6 +3248,18 @@ x /u y = 1 x %u y = 2b59030f x /s y = 0 x %s y = a8898afd +x /u 3 = 382dd8ff +x %u 3 = 0 +x /s 3 = e2d883aa +x %s 3 = ffffffff +x /u 5 = 21b51bcc +x %u 5 = 1 +x /s 5 = ee81e899 +x %s 5 = 0 +x /u 11 = f525274 +x %u 11 = 1 +x /s 11 = f80c8100 +x %s 11 = fffffffd ~x = 57767502 x & y = 280082ec x | y = fdb98fff @@ -2192,6 +3284,18 @@ x /u y = 0 x %u y = 3eb251eb x /s y = 0 x %s y = 3eb251eb +x /u 3 = 14e61b4e +x %u 3 = 1 +x /s 3 = 14e61b4e +x %s 3 = 1 +x /u 5 = c8a1062 +x %u 5 = 1 +x /s 5 = c8a1062 +x %s 5 = 1 +x /u 11 = 5b31eb8 +x %u 11 = 3 +x /s 11 = 5b31eb8 +x %s 11 = 3 ~x = c14dae14 x & y = 14924080 x | y = befffbef @@ -2216,6 +3320,18 @@ x /u y = 0 x %u y = 80bbe209 x /s y = 1 x %s y = fdc4097f +x /u 3 = 2ae94b58 +x %u 3 = 1 +x /s 3 = d593f603 +x %s 3 = 0 +x /u 5 = 19bf2d35 +x %u 5 = 0 +x /s 5 = e68bfa02 +x %s 5 = ffffffff +x /u 11 = bb3fd46 +x %u 11 = 7 +x /s 11 = f46e2bd3 +x %s 11 = fffffff8 ~x = 7f441df6 x & y = 80b3c008 x | y = 82fffa8b @@ -2240,6 +3356,18 @@ x /u y = 2 x %u y = 1da53d7 x /s y = 2 x %s y = 1da53d7 +x /u 3 = 1a55ee47 +x %u 3 = 2 +x /s 3 = 1a55ee47 +x %s 3 = 2 +x /u 5 = fcd2891 +x %u 5 = 2 +x /s 5 = fcd2891 +x %s 5 = 2 +x /u 11 = 72eb559 +x %u 11 = 4 +x /s 11 = 72eb559 +x %s 11 = 4 ~x = b0fe3528 x & y = 6018a80 x | y = 6f93fbd7 @@ -2264,6 +3392,18 @@ x /u y = 0 x %u y = 205307d5 x /s y = 0 x %s y = 205307d5 +x /u 3 = ac657f1 +x %u 3 = 2 +x /s 3 = ac657f1 +x %s 3 = 2 +x /u 5 = 6770191 +x %u 5 = 0 +x /s 5 = 6770191 +x %s 5 = 0 +x /u 11 = 2f04687 +x %u 11 = 8 +x /s 11 = 2f04687 +x %s 11 = 8 ~x = dfacf82a x & y = 201000c4 x | y = 21fb7ff7 @@ -2288,6 +3428,18 @@ x /u y = 1 x %u y = 4acb0e47 x /s y = 0 x %s y = d7c2e083 +x /u 3 = 47eba02b +x %u 3 = 2 +x /s 3 = f2964ad7 +x %s 3 = fffffffe +x /u 5 = 2b26f9b3 +x %u 5 = 4 +x /s 5 = f7f3c681 +x %s 5 = fffffffe +x /u 11 = 139d5a3a +x %u 11 = 5 +x /s 11 = fc5788c7 +x %s 11 = fffffff6 ~x = 283d1f7c x & y = 84c2c000 x | y = dff7f2bf @@ -2312,6 +3464,18 @@ x /u y = 6 x %u y = 93c2a55 x /s y = 6 x %s y = 93c2a55 +x /u 3 = 18c99820 +x %u 3 = 1 +x /s 3 = 18c99820 +x %s 3 = 1 +x /u 5 = edf5b46 +x %u 5 = 3 +x /s 5 = edf5b46 +x %s 5 = 3 +x /u 11 = 6c29dda +x %u 11 = 3 +x /s 11 = 6c29dda +x %s 11 = 3 ~x = b5a3379e x & y = a58c000 x | y = 4adecd63 @@ -2336,6 +3500,18 @@ x /u y = 0 x %u y = 92333eef x /s y = 5 x %s y = f55ca957 +x /u 3 = 30bbbfa5 +x %u 3 = 0 +x /s 3 = db666a50 +x %s 3 = ffffffff +x /u 5 = 1d3d72fc +x %u 5 = 3 +x /s 5 = ea0a3fca +x %s 5 = fffffffd +x /u 11 = d4a7a15 +x %u 11 = 8 +x /s 11 = f604a8a2 +x %s 11 = fffffff9 ~x = 6dccc110 x & y = 80222aa8 x | y = fe3bfeff @@ -2360,6 +3536,18 @@ x /u y = 0 x %u y = 3701afad x /s y = ffffffff x %s y = 8f4888b +x /u 3 = 1255e539 +x %u 3 = 2 +x /s 3 = 1255e539 +x %s 3 = 2 +x /u 5 = b005655 +x %u 5 = 4 +x /s 5 = b005655 +x %s 5 = 4 +x /u 11 = 500273e +x %u 11 = 3 +x /s 11 = 500273e +x %s 11 = 3 ~x = c8fe5052 x & y = 1100888c x | y = f7f3ffff @@ -2384,6 +3572,18 @@ x /u y = 0 x %u y = 4d59521b x /s y = ffffffff x %s y = 1926d30f +x /u 3 = 19c870b3 +x %u 3 = 2 +x /s 3 = 19c870b3 +x %s 3 = 2 +x /u 5 = f78439f +x %u 5 = 0 +x /s 5 = f78439f +x %s 5 = 0 +x /u 11 = 7081ebc +x %u 11 = 7 +x /s 11 = 7081ebc +x %s 11 = 7 ~x = b2a6ade4 x & y = 49490010 x | y = cfddd2ff @@ -2408,6 +3608,18 @@ x /u y = 0 x %u y = 241109b9 x /s y = 0 x %s y = 241109b9 +x /u 3 = c05ade8 +x %u 3 = 1 +x /s 3 = c05ade8 +x %s 3 = 1 +x /u 5 = 7369b8b +x %u 5 = 2 +x /s 5 = 7369b8b +x %s 5 = 2 +x /u 11 = 3475df9 +x %u 11 = 6 +x /s 11 = 3475df9 +x %s 11 = 6 ~x = dbeef646 x & y = 100038 x | y = ecdd99fb @@ -2432,6 +3644,18 @@ x /u y = 2 x %u y = 1d74a427 x /s y = ffffffff x %s y = dbee16f7 +x /u 3 = 34256cad +x %u 3 = 0 +x /s 3 = ded01758 +x %s 3 = ffffffff +x /u 5 = 1f49a79b +x %u 5 = 0 +x /s 5 = ec167468 +x %s 5 = ffffffff +x /u 11 = e38c08c +x %u 11 = 3 +x /s 11 = f6f2ef18 +x %s 11 = ffffffff ~x = 638fb9f8 x & y = 1c704000 x | y = bf7dd6f7 @@ -2456,6 +3680,18 @@ x /u y = 0 x %u y = c4ce285 x /s y = 0 x %s y = c4ce285 +x /u 3 = 419a0d7 +x %u 3 = 0 +x /s 3 = 419a0d7 +x %s 3 = 0 +x /u 5 = 275c6e7 +x %u 5 = 2 +x /s 5 = 275c6e7 +x %s 5 = 2 +x /u 11 = 11e4323 +x %u 11 = 4 +x /s 11 = 11e4323 +x %s 11 = 4 ~x = f3b31d7a x & y = 48284 x | y = afdfe7d7 @@ -2480,6 +3716,18 @@ x /u y = 0 x %u y = 3a1406b3 x /s y = 0 x %s y = 3a1406b3 +x /u 3 = 135c023b +x %u 3 = 2 +x /s 3 = 135c023b +x %s 3 = 2 +x /u 5 = b9d9af0 +x %u 5 = 3 +x /s 5 = b9d9af0 +x %s 5 = 3 +x /u 11 = 547a384 +x %u 11 = 7 +x /s 11 = 547a384 +x %s 11 = 7 ~x = c5ebf94c x & y = 81006a0 x | y = bf17d6bf @@ -2504,6 +3752,18 @@ x /u y = 1 x %u y = 1192eb1f x /s y = 0 x %s y = d1760611 +x /u 3 = 45d20205 +x %u 3 = 2 +x /s 3 = f07cacb1 +x %s 3 = fffffffe +x /u 5 = 29e4679d +x %u 5 = 0 +x /s 5 = f6b1346a +x %s 5 = ffffffff +x /u 11 = 130ababb +x %u 11 = 8 +x /s 11 = fbc4e948 +x %s 11 = fffffff9 ~x = 2e89f9ee x & y = 91620210 x | y = fff71ef3 @@ -2528,6 +3788,18 @@ x /u y = 0 x %u y = 4c2d401f x /s y = 0 x %s y = 4c2d401f +x /u 3 = 19646ab5 +x %u 3 = 0 +x /s 3 = 19646ab5 +x %s 3 = 0 +x /u 5 = f3c4006 +x %u 5 = 1 +x /s 5 = f3c4006 +x %s 5 = 1 +x /u 11 = 6ecd748 +x %u 11 = 7 +x /s 11 = 6ecd748 +x %s 11 = 7 ~x = b3d2bfe0 x & y = c0d4008 x | y = ccbd4e3f @@ -2552,6 +3824,18 @@ x /u y = 1 x %u y = 387d9a8f x /s y = 0 x %s y = e518005d +x /u 3 = 4c5d5574 +x %u 3 = 1 +x /s 3 = f708001f +x %s 3 = 0 +x /u 5 = 2dd199ac +x %u 5 = 1 +x /s 5 = fa9e6679 +x %s 5 = 0 +x /u 11 = 14d3a2f1 +x %u 11 = 2 +x /s 11 = fd8dd17d +x %s 11 = fffffffe ~x = 1ae7ffa2 x & y = a418004c x | y = ed9a65df @@ -2576,6 +3860,18 @@ x /u y = 0 x %u y = 749d5e4b x /s y = ffffffff x %s y = 32b711af +x /u 3 = 26df1f6e +x %u 3 = 1 +x /s 3 = 26df1f6e +x %s 3 = 1 +x /u 5 = 1752ac75 +x %u 5 = 2 +x /s 5 = 1752ac75 +x %s 5 = 2 +x /u 11 = a99f14c +x %u 11 = 7 +x /s 11 = a99f14c +x %s 11 = 7 ~x = 8b62a1b4 x & y = 34191240 x | y = fe9dff6f @@ -2600,6 +3896,18 @@ x /u y = 0 x %u y = 3c151d69 x /s y = 0 x %s y = 3c151d69 +x /u 3 = 140709cd +x %u 3 = 2 +x /s 3 = 140709cd +x %s 3 = 2 +x /u 5 = c043915 +x %u 5 = 0 +x /s 5 = c043915 +x %s 5 = 0 +x /u 11 = 576487d +x %u 11 = a +x /s 11 = 576487d +x %s 11 = a ~x = c3eae296 x & y = c100468 x | y = 7cd55d6b @@ -2624,6 +3932,18 @@ x /u y = 0 x %u y = 5aaa8d37 x /s y = ffffffff x %s y = 2ba0cf97 +x /u 3 = 1e38d9bd +x %u 3 = 0 +x /s 3 = 1e38d9bd +x %s 3 = 0 +x /u 5 = 12221c3e +x %u 5 = 1 +x /s 5 = 12221c3e +x %s 5 = 1 +x /u 11 = 83e0cd6 +x %u 11 = 5 +x /s 11 = 83e0cd6 +x %s 11 = 5 ~x = a55572c8 x & y = 50a20020 x | y = dafecf77 @@ -2648,6 +3968,18 @@ x /u y = 0 x %u y = 18f26935 x /s y = 0 x %s y = 18f26935 +x /u 3 = 850cdbc +x %u 3 = 1 +x /s 3 = 850cdbc +x %s 3 = 1 +x /u 5 = 4fd483d +x %u 5 = 4 +x /s 5 = 4fd483d +x %s 5 = 4 +x /u 11 = 2449533 +x %u 11 = 4 +x /s 11 = 2449533 +x %s 11 = 4 ~x = e70d96ca x & y = 10a24004 x | y = bafb7bf7 @@ -2672,6 +4004,18 @@ x /u y = 0 x %u y = 192bb8e3 x /s y = 0 x %s y = 192bb8e3 +x /u 3 = 863e84b +x %u 3 = 2 +x /s 3 = 863e84b +x %s 3 = 2 +x /u 5 = 508be93 +x %u 5 = 4 +x /s 5 = 508be93 +x %s 5 = 4 +x /u 11 = 249cafd +x %u 11 = 4 +x /s 11 = 249cafd +x %s 11 = 4 ~x = e6d4471c x & y = 1909b000 x | y = 196bffff @@ -2696,6 +4040,18 @@ x /u y = 1 x %u y = 6ae1c2df x /s y = 0 x %s y = f8e3afc1 +x /u 3 = 52f68feb +x %u 3 = 0 +x /s 3 = fda13a96 +x %s 3 = ffffffff +x /u 5 = 31c72326 +x %u 5 = 3 +x /s 5 = fe93eff4 +x %s 5 = fffffffd +x /u 11 = 16a055cb +x %u 11 = 8 +x /s 11 = ff5a8458 +x %s 11 = fffffff9 ~x = 71c503e x & y = 8801acc0 x | y = fee3efe3 @@ -2720,6 +4076,18 @@ x /u y = 4 x %u y = 22e56ef x /s y = ffffffff x %s y = ec461ae7 +x /u 3 = 3f26d9c5 +x %u 3 = 0 +x /s 3 = e9d18470 +x %s 3 = ffffffff +x /u 5 = 25e41c43 +x %u 5 = 0 +x /s 5 = f2b0e910 +x %s 5 = ffffffff +x /u 11 = 1139241e +x %u 11 = 5 +x /s 11 = f9f352ab +x %s 11 = fffffff6 ~x = 428b72b0 x & y = 2c508d08 x | y = bff58ddf @@ -2744,6 +4112,18 @@ x /u y = 0 x %u y = af977d0d x /s y = 1 x %s y = e4e14e4f +x /u 3 = 3a87d459 +x %u 3 = 2 +x /s 3 = e5327f05 +x %s 3 = fffffffe +x /u 5 = 231e4c35 +x %u 5 = 4 +x /s 5 = efeb1903 +x %s 5 = fffffffe +x /u 11 = ff67fbb +x %u 11 = 4 +x /s 11 = f8b0ae47 +x %s 11 = 0 ~x = 506882f2 x & y = 8a962c0c x | y = efb77fbf @@ -2768,6 +4148,18 @@ x /u y = 1 x %u y = 1155f4a7 x /s y = 0 x %s y = c301767b +x /u 3 = 41007cd3 +x %u 3 = 2 +x /s 3 = ebab277f +x %s 3 = fffffffe +x /u 5 = 27004ae5 +x %u 5 = 2 +x /s 5 = f3cd17b3 +x %s 5 = fffffffc +x /u 11 = 11ba5096 +x %u 11 = 9 +x /s 11 = fa747f23 +x %s 11 = fffffffa ~x = 3cfe8984 x & y = 81010050 x | y = f3abf7ff @@ -2792,6 +4184,18 @@ x /u y = 0 x %u y = 7dc31d19 x /s y = ffffffff x %s y = 38951173 +x /u 3 = 29ebb45d +x %u 3 = 2 +x /s 3 = 29ebb45d +x %s 3 = 2 +x /u 5 = 192705d1 +x %u 5 = 4 +x /s 5 = 192705d1 +x %s 5 = 4 +x /u 11 = b6ed419 +x %u 11 = 6 +x /s 11 = b6ed419 +x %s 11 = 6 ~x = 823ce2e6 x & y = 38c11418 x | y = ffd3fd5b @@ -2816,6 +4220,18 @@ x /u y = 0 x %u y = 37e3a067 x /s y = fffffffd x %s y = a5fcfd7 +x /u 3 = 12a13577 +x %u 3 = 2 +x /s 3 = 12a13577 +x %s 3 = 2 +x /u 5 = b2d867b +x %u 5 = 0 +x /s 5 = b2d867b +x %s 5 = 0 +x /u 11 = 514b17d +x %u 11 = 8 +x /s 11 = 514b17d +x %s 11 = 8 ~x = c81c5f98 x & y = 30c00040 x | y = f7f7aff7 @@ -2840,6 +4256,18 @@ x /u y = 0 x %u y = ae6e9be5 x /s y = 3 x %s y = f5460ec3 +x /u 3 = 3a24dea1 +x %u 3 = 2 +x /s 3 = e4cf894d +x %s 3 = fffffffe +x /u 5 = 22e2ebfa +x %u 5 = 3 +x /s 5 = efafb8c8 +x %s 5 = fffffffd +x /u 11 = fdb8289 +x %u 11 = 2 +x /s 11 = f895b115 +x %s 11 = fffffffe ~x = 5191641a x & y = a86299a4 x | y = ee6edbf7 @@ -2864,6 +4292,18 @@ x /u y = 1 x %u y = 78bc387 x /s y = 0 x %s y = f5ecf713 +x /u 3 = 51f9a7b1 +x %u 3 = 0 +x /s 3 = fca4525c +x %s 3 = ffffffff +x /u 5 = 312f649d +x %u 5 = 2 +x /s 5 = fdfc316b +x %s 5 = fffffffc +x /u 11 = 165b5c47 +x %u 11 = 6 +x /s 11 = ff158ad4 +x %s 11 = fffffff7 ~x = a1308ec x & y = e4603300 x | y = ffedf79f @@ -2888,6 +4328,18 @@ x /u y = 0 x %u y = 700c571 x /s y = 0 x %s y = 700c571 +x /u 3 = 2559725 +x %u 3 = 2 +x /s 3 = 2559725 +x %s 3 = 2 +x /u 5 = 1668de3 +x %u 5 = 2 +x /s 5 = 1668de3 +x %s 5 = 2 +x /u 11 = a2faad +x %u 11 = 2 +x /s 11 = a2faad +x %s 11 = 2 ~x = f8ff3a8e x & y = 3000050 x | y = 6f16fff3 @@ -2912,6 +4364,18 @@ x /u y = 0 x %u y = 1c9c267f x /s y = fffffff5 x %s y = 10d69d7 +x /u 3 = 989622a +x %u 3 = 1 +x /s 3 = 989622a +x %s 3 = 1 +x /u 5 = 5b8d47f +x %u 5 = 4 +x /s 5 = 5b8d47f +x %s 5 = 4 +x /u 11 = 299d4f4 +x %u 11 = 3 +x /s 11 = 299d4f4 +x %s 11 = 3 ~x = e363d980 x & y = 1c1c2008 x | y = fdfeaf7f @@ -2936,6 +4400,18 @@ x /u y = 0 x %u y = 160b25bd x /s y = 0 x %s y = 160b25bd +x /u 3 = 7590c94 +x %u 3 = 1 +x /s 3 = 7590c94 +x %s 3 = 1 +x /u 5 = 468a125 +x %u 5 = 4 +x /s 5 = 468a125 +x %s 5 = 4 +x /u 11 = 201036e +x %u 11 = 3 +x /s 11 = 201036e +x %s 11 = 3 ~x = e9f4da42 x & y = 140121ac x | y = 5f9f37bf @@ -2960,6 +4436,18 @@ x /u y = 0 x %u y = b7c89aab x /s y = 7 x %s y = fca324cf +x /u 3 = 3d42de39 +x %u 3 = 0 +x /s 3 = e7ed88e4 +x %s 3 = ffffffff +x /u 5 = 24c1b888 +x %u 5 = 3 +x /s 5 = f18e8556 +x %s 5 = fffffffd +x /u 11 = 10b52555 +x %u 11 = 4 +x /s 11 = f96f53e1 +x %s 11 = 0 ~x = 48376554 x & y = b6088800 x | y = f7e9feef @@ -2984,6 +4472,18 @@ x /u y = 0 x %u y = 2cd608c9 x /s y = 0 x %s y = 2cd608c9 +x /u 3 = ef202ed +x %u 3 = 2 +x /s 3 = ef202ed +x %s 3 = 2 +x /u 5 = 8f79b5b +x %u 5 = 2 +x /s 5 = 8f79b5b +x %s 5 = 2 +x /u 11 = 4137529 +x %u 11 = 6 +x /s 11 = 4137529 +x %s 11 = 6 ~x = d329f736 x & y = c800048 x | y = eef6a8cb @@ -3008,6 +4508,18 @@ x /u y = 0 x %u y = 3f0e7f97 x /s y = 0 x %s y = 3f0e7f97 +x /u 3 = 1504d532 +x %u 3 = 1 +x /s 3 = 1504d532 +x %s 3 = 1 +x /u 5 = c9c7feb +x %u 5 = 0 +x /s 5 = c9c7feb +x %s 5 = 0 +x /u 11 = 5bb7ff6 +x %u 11 = 5 +x /s 11 = 5bb7ff6 +x %s 11 = 5 ~x = c0f18068 x & y = 3a0e3900 x | y = bfae7fd7 @@ -3032,6 +4544,18 @@ x /u y = 1 x %u y = 45bf5def x /s y = ffffffff x %s y = d999973b +x /u 3 = 2fe428dc +x %u 3 = 1 +x /s 3 = da8ed387 +x %s 3 = 0 +x /u 5 = 1cbc1884 +x %u 5 = 1 +x /s 5 = e988e551 +x %s 5 = 0 +x /u 11 = d0fae0d +x %u 11 = 6 +x /s 11 = f5c9dc9a +x %s 11 = fffffff7 ~x = 7053856a x & y = 9ac1884 x | y = cfed7eb7 @@ -3056,6 +4580,18 @@ x /u y = 0 x %u y = 59fac143 x /s y = 0 x %s y = 59fac143 +x /u 3 = 1dfe406b +x %u 3 = 2 +x /s 3 = 1dfe406b +x %s 3 = 2 +x /u 5 = 11fef373 +x %u 5 = 4 +x /s 5 = 11fef373 +x %s 5 = 4 +x /u 11 = 82e1191 +x %u 11 = 8 +x /s 11 = 82e1191 +x %s 11 = 8 ~x = a6053ebc x & y = 8e08140 x | y = dbfacbff @@ -3080,6 +4616,18 @@ x /u y = 0 x %u y = 28e84721 x /s y = 0 x %s y = 28e84721 +x /u 3 = da2c260 +x %u 3 = 1 +x /s 3 = da2c260 +x %s 3 = 1 +x /u 5 = 82e74a0 +x %u 5 = 1 +x /s 5 = 82e74a0 +x %s 5 = 1 +x /u 11 = 3b80677 +x %u 11 = 4 +x /s 11 = 3b80677 +x %s 11 = 4 ~x = d717b8de x & y = a80400 x | y = fcff47e3 @@ -3104,6 +4652,18 @@ x /u y = 0 x %u y = 14f70baf x /s y = 0 x %s y = 14f70baf +x /u 3 = 6fd03e5 +x %u 3 = 0 +x /s 3 = 6fd03e5 +x %s 3 = 0 +x /u 5 = 43168bc +x %u 5 = 3 +x /s 5 = 43168bc +x %s 5 = 3 +x /u 11 = 1e7e9ca +x %u 11 = 1 +x /s 11 = 1e7e9ca +x %s 11 = 1 ~x = eb08f450 x & y = 130028 x | y = 75ffabff @@ -3128,6 +4688,18 @@ x /u y = 0 x %u y = cabdfa6d x /s y = 9 x %s y = fe43e0df +x /u 3 = 4394a8cf +x %u 3 = 0 +x /s 3 = ee3f537a +x %s 3 = ffffffff +x /u 5 = 288c6549 +x %u 5 = 0 +x /s 5 = f5593216 +x %s 5 = ffffffff +x /u 11 = 126e5c95 +x %u 11 = 6 +x /s 11 = fb288b22 +x %s 11 = fffffff7 ~x = 35420592 x & y = ca04700c x | y = fafffeff @@ -3152,6 +4724,18 @@ x /u y = 1 x %u y = 1df9d827 x /s y = 1 x %s y = 1df9d827 +x /u 3 = 2651ee49 +x %u 3 = 0 +x /s 3 = 2651ee49 +x %s 3 = 0 +x /u 5 = 16fdf55f +x %u 5 = 0 +x /s 5 = 16fdf55f +x %s 5 = 0 +x /u 11 = a736f88 +x %u 11 = 3 +x /s 11 = a736f88 +x %s 11 = 3 ~x = 8d0a3524 x & y = 50f1c290 x | y = 76fffaff @@ -3176,6 +4760,18 @@ x /u y = 3 x %u y = 9707cb x /s y = 0 x %s y = cbc8e079 +x /u 3 = 43eda028 +x %u 3 = 1 +x /s 3 = ee984ad3 +x %s 3 = 0 +x /u 5 = 28c1c67e +x %u 5 = 3 +x /s 5 = f58e934c +x %s 5 = fffffffd +x /u 11 = 1286a00b +x %u 11 = 0 +x /s 11 = fb40ce97 +x %s 11 = fffffffc ~x = 34371f86 x & y = 43884038 x | y = cbfbe87b @@ -3200,6 +4796,18 @@ x /u y = 0 x %u y = 7de2ac7 x /s y = 0 x %s y = 7de2ac7 +x /u 3 = 29f6397 +x %u 3 = 2 +x /s 3 = 29f6397 +x %s 3 = 2 +x /u 5 = 192d55b +x %u 5 = 0 +x /s 5 = 192d55b +x %s 5 = 0 +x /u 11 = b71b29 +x %u 11 = 4 +x /s 11 = b71b29 +x %s 11 = 4 ~x = f821d538 x & y = 7da2a80 x | y = bfdfbef7 @@ -3224,6 +4832,18 @@ x /u y = 2 x %u y = 19e4ce19 x /s y = fffffffe x %s y = fac93c71 +x /u 3 = 2e1d01c1 +x %u 3 = 2 +x /s 3 = d8c7ac6d +x %s 3 = fffffffe +x /u 5 = 1bab010d +x %u 5 = 4 +x /s 5 = e877cddb +x %s 5 = fffffffe +x /u 11 = c938c1d +x %u 11 = 6 +x /s 11 = f54dbaaa +x %s 11 = fffffff7 ~x = 75a8faba x & y = 8110104 x | y = ba7f1fd7 diff --git a/test/regression/int32.c b/test/regression/int32.c index bec50f0..d7b6c9e 100644 --- a/test/regression/int32.c +++ b/test/regression/int32.c @@ -48,6 +48,18 @@ static void test1(u32 x, u32 y) printf("x %%u y = %x\n", safe_umod32(x, y)); printf("x /s y = %x\n", safe_sdiv32(x, y)); printf("x %%s y = %x\n", safe_smod32(x, y)); + printf("x /u 3 = %x\n", x / 3); + printf("x %%u 3 = %x\n", x % 3); + printf("x /s 3 = %x\n", (s32)x / 3); + printf("x %%s 3 = %x\n", (s32)x % 3); + printf("x /u 5 = %x\n", x / 5); + printf("x %%u 5 = %x\n", x % 5); + printf("x /s 5 = %x\n", (s32)x / 5); + printf("x %%s 5 = %x\n", (s32)x % 5); + printf("x /u 11 = %x\n", x / 11); + printf("x %%u 11 = %x\n", x % 11); + printf("x /s 11 = %x\n", (s32)x / 11); + printf("x %%s 11 = %x\n", (s32)x % 11); printf("~x = %x\n", ~x); printf("x & y = %x\n", x & y); printf("x | y = %x\n", x | y); -- cgit v1.2.3