From 20ad7e8e86b5242c397679908a7cce13a3ff9db9 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 19 Mar 2020 17:30:14 -0700
Subject: [PATCH] Remove the "round-to-zero" versions of integer division and
 modulus, since we're going to restrict signed division to bitvectors.

---
 src/Cryptol/Eval/Backend.hs        | 20 +-------------------
 src/Cryptol/Eval/Concrete/Value.hs |  6 ------
 src/Cryptol/Eval/Generic.hs        |  4 ++--
 src/Cryptol/Eval/SBV.hs            | 10 ----------
 4 files changed, 3 insertions(+), 37 deletions(-)

diff --git a/src/Cryptol/Eval/Backend.hs b/src/Cryptol/Eval/Backend.hs
index 4947f5a0..a505cef9 100644
--- a/src/Cryptol/Eval/Backend.hs
+++ b/src/Cryptol/Eval/Backend.hs
@@ -66,7 +66,7 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Merge the two given computations according to the predicate.
   mergeEval ::
      sym ->
-     (SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} -> 
+     (SBit sym -> a -> a -> SEval sym a) {- ^ A merge operation on values -} ->
      SBit sym {- ^ The condition -} ->
      SEval sym a {- ^ The "then" computation -} ->
      SEval sym a {- ^ The "else" computation -} ->
@@ -411,24 +411,6 @@ class MonadIO (SEval sym) => Backend sym where
     SInteger sym ->
     SEval sym (SInteger sym)
 
-  -- | Integer division, rounding toward zero. It is illegal to
-  --   call with a second argument concretely equal to 0.
-  --   Same semantics as Haskell's @quot@ operation.
-  intDivRTZ :: 
-    sym ->
-    SInteger sym ->
-    SInteger sym ->
-    SEval sym (SInteger sym)
-
-  -- | Integer modulus, with division rounding toward zero. It is illegal to
-  --   call with a second argument concretely equal to 0.
-  --   Same semantics as Haskell's @rem@ operation.
-  intModRTZ :: 
-    sym ->
-    SInteger sym ->
-    SInteger sym ->
-    SEval sym (SInteger sym)
-
   -- | Integer exponentiation.  The second argument must be non-negative.
   intExp ::
     sym ->
diff --git a/src/Cryptol/Eval/Concrete/Value.hs b/src/Cryptol/Eval/Concrete/Value.hs
index a889afd6..86b5e7a0 100644
--- a/src/Cryptol/Eval/Concrete/Value.hs
+++ b/src/Cryptol/Eval/Concrete/Value.hs
@@ -304,12 +304,6 @@ instance Backend Concrete where
   intMod sym x y =
     do assertSideCondition sym (y /= 0) DivideByZero
        pure $! x `mod` y
-  intDivRTZ sym x y =
-    do assertSideCondition sym (y /= 0) DivideByZero
-       pure $! x `quot` y
-  intModRTZ sym x y =
-    do assertSideCondition sym (y /= 0) DivideByZero
-       pure $! x `rem` y
   intExp sym x y =
     do assertSideCondition sym (y >= 0) NegativeExponent
        pure $! x ^ y
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index fee6b212..8359dad2 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -316,14 +316,14 @@ sdivV :: Backend sym => sym -> Binary sym
 sdivV sym = arithBinary sym opw opi opz
   where
     opw _w x y = wordSignedDiv sym x y
-    opi x y = intDivRTZ sym x y
+    opi x y = intDiv sym x y
     opz m x y = znDiv sym m x y
 
 smodV :: Backend sym => sym -> Binary sym
 smodV sym = arithBinary sym opw opi opz
   where
     opw _w x y = wordSignedMod sym x y
-    opi x y = intModRTZ sym x y
+    opi x y = intMod sym x y
     opz m x y = znMod sym m x y
 
 expV :: Backend sym => sym -> Binary sym
diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs
index 0853d9bb..e5f7f097 100644
--- a/src/Cryptol/Eval/SBV.hs
+++ b/src/Cryptol/Eval/SBV.hs
@@ -297,16 +297,6 @@ instance Backend SBV where
        assertSideCondition sym (svNot (svEqual b z)) DivideByZero
        pure $! svRem a b   -- TODO! Fix this: see issue #662
 
-  intDivRTZ sym a b =
-    do let z = svInteger KUnbounded 0
-       assertSideCondition sym (svNot (svEqual b z)) DivideByZero
-       pure $! svQuot a b  -- TODO! Fix this: see issue #662
-
-  intModRTZ sym a b =
-    do let z = svInteger KUnbounded 0
-       assertSideCondition sym (svNot (svEqual b z)) DivideByZero
-       pure $! svQuot a b  -- TODO! Fix this: see issue #662
-
   intExp sym  a b =
     do let z = svInteger KUnbounded 0
        assertSideCondition sym (svLessEq z b) NegativeExponent