diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 6 | ||||
| -rw-r--r-- | lib/sail.c | 8 | ||||
| -rw-r--r-- | lib/sail.h | 1 |
3 files changed, 11 insertions, 4 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index a3a80fc5..b233048e 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -70,7 +70,11 @@ val _shl_int = "shl_int" : (int, int) -> int overload shl_int = {_shl8, _shl32, _shl_int} -val shr_int = "shr_int" : (int, int) -> int +val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} + +val _shr_int = "shr_int" : (int, int) -> int + +overload shr_int = {_shr32, _shr_int} // ***** div and mod ***** @@ -292,24 +292,26 @@ bool gteq(const mpz_t op1, const mpz_t op2) return mpz_cmp(op1, op2) >= 0; } -inline void shl_int(sail_int *rop, const sail_int op1, const sail_int op2) { mpz_mul_2exp(*rop, op1, mpz_get_ui(op2)); } -inline mach_int shl_mach_int(const mach_int op1, const mach_int op2) { return op1 << op2; } -inline void shr_int(sail_int *rop, const sail_int op1, const sail_int op2) { mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2)); } +mach_int shr_mach_int(const mach_int op1, const mach_int op2) +{ + return op1 >> op2; +} + inline void undefined_int(sail_int *rop, const int n) { @@ -116,6 +116,7 @@ bool gteq(const sail_int, const sail_int); * Left and right shift for integers */ mach_int shl_mach_int(const mach_int, const mach_int); +mach_int shr_mach_int(const mach_int, const mach_int); SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int); |
