From b92d5a32c314eee0c68a70c33f1847545aabeb19 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 14 Jan 2020 23:07:49 +0100 Subject: 64-bit signed division by two code --- riscV/Asmgen.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'riscV/Asmgen.v') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 5952aa82..ffc7992c 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -597,11 +597,16 @@ Definition transl_op OK (Psrlil rd rs n :: k) | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrlil X31 rs (Int.repr 63) :: + Paddl X31 rs X31 :: + Psrail rd X31 Int.one :: k + else Psrail X31 rs (Int.repr 63) :: + Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: + Paddl X31 rs X31 :: + Psrail rd X31 n :: k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; -- cgit