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.

18 files changed, 123 insertions, 73 deletions

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index f4f7dc75..431ad1f7 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -284,17 +284,11 @@ val abs_real = {coq: "Rabs", _: "abs_real"} : real -> real
 
 overload abs = {abs_atom, abs_real}
 
-val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (nat, nat) -> nat
-
 val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
 
-val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
-
-overload operator / = {quotient_nat, quotient, quotient_real}
-
-val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
-
-overload operator % = {modulus}
+overload operator / = {ediv_int, quotient_real}
+overload div = {ediv_int}
+overload operator % = {emod_int}
 
 val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real
 
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index f125ec72..a9a78900 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -2201,7 +2201,7 @@ function clause execute ( Division((d,n,m,datasize as int('R),_unsigned)) ) = {
   if IsZero(operand2) then
     result = 0
   else
-    result = /* ARM: RoundTowardsZero*/ quot (_Int(operand1, _unsigned), _Int(operand2, _unsigned)); /* FIXME: does quot round towards zero? */
+    result = /* ARM: RoundTowardsZero*/ tdiv_int (_Int(operand1, _unsigned), _Int(operand2, _unsigned));
 
   wX(d) = to_bits(result) : (bits('R)) ; /* ARM: result[(datasize-1)..0] */
 }
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index 2dbd2bf4..f97c84a6 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -150,17 +150,9 @@ overload operator ^ = {xor_vec, int_power, concat_str}
 val mask : forall 'l 'm, 'l >= 0 & 'm >= 0. (implicit('l), bits('m)) -> bits('l)
 
 
-/* put this val spec into Sail lib for "%" */
-
-val mod = {
-  smt: "mod",
-  ocaml: "modulus",
-  lem: "integerMod",
-  c: "tmod_int",
-  coq: "Z.rem"
-} : forall 'M 'N. (int('M), int('N)) -> {'O, 0 <= 'O & 'O < N . int('O)}
-
-/* overload operator % = {mod_int} */
+overload operator % = {emod_int}
+overload operator / = {ediv_int}
+overload mod = {emod_int}
 
 val print = "print_endline" : string -> unit
 
diff --git a/lib/arith.sail b/lib/arith.sail
index 20231de1..798bde12 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -78,26 +78,20 @@ overload shr_int = {_shr32, _shr_int}
 
 // ***** div and mod *****
 
-val div_int = {
-  smt: "div",
-  ocaml: "quotient",
-  lem: "integerDiv",
-  c: "tdiv_int",
-  coq: "Z.quot"
+/*! Truncating division (rounds towards zero) */
+val tdiv_int = {
+  ocaml: "tdiv_int",
+  lem: "integerDiv_t",
+  c: "tdiv_int"
 } : (int, int) -> int
 
-overload operator / = {div_int}
-
-val mod_int = {
-  smt: "mod",
-  ocaml: "modulus",
-  lem: "integerMod",
-  c: "tmod_int",
-  coq: "Z.rem"
+/*! Remainder for truncating division (has sign of dividend) */
+val tmod_int = {
+  ocaml: "tmod_int",
+  lem: "integerMod_t",
+  c: "tmod_int"
 } : (int, int) -> nat
 
-overload operator % = {mod_int}
-
 val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
diff --git a/lib/sail.c b/lib/sail.c
index 6c71d7ae..2d47939e 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -350,6 +350,27 @@ void mult_int(sail_int *rop, const sail_int op1, const sail_int op2)
   mpz_mul(*rop, op1, op2);
 }
 
+
+inline
+void ediv_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  /* GMP doesn't have Euclidean division but we can emulate it using 
+     flooring and ceiling division. */
+  if (mpz_sgn(op2) >= 0) {
+    mpz_fdiv_q(*rop, op1, op2);
+  } else {
+    mpz_cdiv_q(*rop, op1, op2);
+  }
+}
+
+inline
+void emod_int(sail_int *rop, const sail_int op1, const sail_int op2)
+{
+  /* The documentation isn't that explicit but I think this is 
+     Euclidean mod. */
+  mpz_mod(*rop, op1, op2);
+}
+
 inline
 void tdiv_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
diff --git a/lib/sail.h b/lib/sail.h
index 5a7722de..666c75fe 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -138,6 +138,8 @@ SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(sub_nat, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(ediv_int, sail_int, const sail_int, const sail_int);
+SAIL_INT_FUNCTION(emod_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(fdiv_int, sail_int, const sail_int, const sail_int);
diff --git a/lib/smt.sail b/lib/smt.sail
index d886c127..4d250bef 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -3,24 +3,21 @@ $define _SMT
 
 // see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
 
-val div = {
+/*! Euclidean division */
+val ediv_int = {
   ocaml: "quotient",
   lem: "integerDiv",
-  c: "tdiv_int",
+  c: "ediv_int",
   coq: "ediv_with_eq"
 } : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
 
-overload operator / = {div}
-
-val mod = {
+val emod_int = {
   ocaml: "modulus",
   lem: "integerMod",
-  c: "tmod_int",
+  c: "emod_int",
   coq: "emod_with_eq"
 } : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 
-overload operator % = {mod}
-
 val abs_int = {
   ocaml: "abs_int",
   lem: "abs_int",
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
diff --git a/test/builtins/div_int.sail b/test/builtins/div_int.sail
index fed6de6e..e8da4f4b 100644
--- a/test/builtins/div_int.sail
+++ b/test/builtins/div_int.sail
@@ -5,6 +5,8 @@ $include <flow.sail>
 $include <vector_dec.sail>
 $include <arith.sail>
 
+overload div_int = {tdiv_int}
+
 function main (() : unit) -> unit = {
   assert(div_int(48240160, 8) == 6030020);
   assert(div_int(48240168, 8) == 6030021);
diff --git a/test/builtins/div_int2.sail b/test/builtins/div_int2.sail
index d3df278d..8ce97cc0 100644
--- a/test/builtins/div_int2.sail
+++ b/test/builtins/div_int2.sail
@@ -5,6 +5,8 @@ $include <flow.sail>
 $include <vector_dec.sail>
 $include <arith.sail>
 
+overload div_int = {tdiv_int}
+
 function main (() : unit) -> unit = {
   assert(div_int(0, 8) == 0);
   assert(div_int(1000, 12) == 83);
diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail
new file mode 100644
index 00000000..f9d7e7c5
--- /dev/null
+++ b/test/builtins/divmod.sail
@@ -0,0 +1,43 @@
+default Order dec
+
+$include <exception_basic.sail>
+$include <arith.sail>
+$include <smt.sail>
+
+function main (() : unit) -> unit = {
+  assert(ediv_int( 7 ,  5) ==  1);
+  assert(ediv_int( 7 , -5) == -1);
+  assert(ediv_int(-7 ,  5) == -2);
+  assert(ediv_int(-7 , -5) ==  2);
+  assert(ediv_int( 12 ,  3) ==  4);
+  assert(ediv_int( 12 , -3) == -4);
+  assert(ediv_int(-12 ,  3) == -4);
+  assert(ediv_int(-12 , -3) ==  4);
+  
+  assert(emod_int( 7 ,  5) ==  2);
+  assert(emod_int( 7 , -5) ==  2);
+  assert(emod_int(-7 ,  5) ==  3);
+  assert(emod_int(-7 , -5) ==  3);
+  assert(emod_int( 12 ,  3) == 0);
+  assert(emod_int( 12 , -3) == 0);
+  assert(emod_int(-12 ,  3) == 0);
+  assert(emod_int(-12 , -3) == 0);
+
+  assert(tdiv_int( 7 ,  5) ==  1);
+  assert(tdiv_int( 7 , -5) == -1);
+  assert(tdiv_int(-7 ,  5) == -1);
+  assert(tdiv_int(-7 , -5) ==  1);
+  assert(tdiv_int( 12 ,  3) ==  4);
+  assert(tdiv_int( 12 , -3) == -4);
+  assert(tdiv_int(-12 ,  3) == -4);
+  assert(tdiv_int(-12 , -3) ==  4);
+  
+  assert(tmod_int( 7 ,  5) ==  2);
+  assert(tmod_int( 7 , -5) ==  2);
+  assert(tmod_int(-7 ,  5) == -2);
+  assert(tmod_int(-7 , -5) == -2);
+  assert(tmod_int( 12 ,  3) == 0);
+  assert(tmod_int( 12 , -3) == 0);
+  assert(tmod_int(-12 ,  3) == 0);
+  assert(tmod_int(-12 , -3) == 0);
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
index 03954a9f..291b7e16 100644
--- a/test/typecheck/pass/Replicate.sail
+++ b/test/typecheck/pass/Replicate.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index 92c6d7cd..c40aa5ec 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -1,8 +1,8 @@
 Type error:
-[Replicate/v1.sail]:11:4-30
-11 |    replicate_bits(x, 'N / 'M)
+[Replicate/v1.sail]:14:4-30
+14 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
index 69f2bb6f..55627db5 100644
--- a/test/typecheck/pass/Replicate/v1.sail
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index 6afdac30..c2c15c12 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -1,8 +1,8 @@
 Type error:
-[Replicate/v2.sail]:10:4-30
-10 |    replicate_bits(x, 'N / 'M)
+[Replicate/v2.sail]:13:4-30
+13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
index e54b0af4..436ef24b 100644
--- a/test/typecheck/pass/Replicate/v2.sail
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -2,6 +2,9 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+overload operator % = {tmod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail
index 4aac2bed..594130a8 100644
--- a/test/typecheck/pass/guards.sail
+++ b/test/typecheck/pass/guards.sail
@@ -1,8 +1,9 @@
 default Order dec
 
 $include <prelude.sail>
+$include <smt.sail>
 
-overload operator / = {quotient}
+overload operator / = {ediv_int}
 
 union T = {C1 : int, C2 : int}
 
diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail
index 5ca85f53..cd3ca46c 100644
--- a/test/typecheck/pass/recursion.sail
+++ b/test/typecheck/pass/recursion.sail
@@ -2,6 +2,8 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+
 val log2 : int -> int
 
 function log2(n) =