From f4acbce30be2aecdfc491478a24c5eb551824f24 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 22 Mar 2019 16:50:48 +0000
Subject: 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.

---
 lib/arith.sail | 26 ++++++++++----------------
 lib/sail.c     | 21 +++++++++++++++++++++
 lib/sail.h     |  2 ++
 lib/smt.sail   | 13 +++++--------
 4 files changed, 38 insertions(+), 24 deletions(-)

(limited to 'lib')

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",
-- 
cgit v1.2.3