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, 10 insertions, 16 deletions

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",