Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.

1 files changed, 12 insertions, 21 deletions

diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 4bb004bf..39485769 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -187,36 +187,27 @@ let sint = function
 let add_int (x, y) = Big_int.add x y
 let sub_int (x, y) = Big_int.sub x y
 let mult (x, y) = Big_int.mul x y
+
+(* This is euclidian division from lem *)
 let quotient (x, y) = Big_int.div x y
 
-(* Big_int does not provide divide with rounding towards zero so roll
-   our own, assuming that division of positive integers rounds down *)
-let quot_round_zero (x, y) = 
-  let posX = Big_int.greater_equal x Big_int.zero in
-  let posY = Big_int.greater_equal y Big_int.zero in
-  let absX = Big_int.abs x in
-  let absY = Big_int.abs y in
-  let q = Big_int.div absX absY in
-  if posX != posY then
-    Big_int.negate q
-  else
-    q
+(* This is the same as tdiv_int, kept for compatibility with old preludes *)
+let quot_round_zero (x, y) =
+  Big_int.integerDiv_t x y
 
 (* The corresponding remainder function for above just respects the sign of x *)
-let rem_round_zero (x, y) = 
-  let posX = Big_int.greater_equal x Big_int.zero in
-  let absX = Big_int.abs x in
-  let absY = Big_int.abs y in
-  let r = Big_int.modulus absX absY in
-  if posX then
-    r
-  else
-    Big_int.negate r
+let rem_round_zero (x, y) =
+  Big_int.integerRem_t x y
 
+(* Lem provides euclidian modulo by default *)
 let modulus (x, y) = Big_int.modulus x y
 
 let negate x = Big_int.negate x
 
+let tdiv_int (x, y) = Big_int.integerDiv_t x y
+
+let tmod_int (x, y) = Big_int.integerRem_t x y
+
 let add_bit_with_carry (x, y, carry) =
   match x, y, carry with
   | B0, B0, B0 -> B0, B0