From d1883caa6aaca666384f6928782c9cac8d1d5709 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 10 Sep 2021 16:59:54 -0700
Subject: [PATCH] Add primitive `toSignedInteger`.

---
 lib/Cryptol.cry                 |  5 +++++
 src/Cryptol/Backend.hs          |  6 ++++++
 src/Cryptol/Backend/Concrete.hs |  1 +
 src/Cryptol/Backend/SBV.hs      |  1 +
 src/Cryptol/Backend/What4.hs    |  1 +
 src/Cryptol/Eval/Generic.hs     | 10 ++++++++++
 6 files changed, 24 insertions(+)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index 14b79f73..8264abf4 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -734,6 +734,11 @@ primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
  */
 primitive lg2 : {n} (fin n) => [n] -> [n]
 
+/**
+ * Convert a signed 2's complement bitvector to an integer.
+ */
+primitive toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer
+
 
 // Rational specific operations ----------------------------------------------
 
diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs
index 5526b119..d132e5b6 100644
--- a/src/Cryptol/Backend.hs
+++ b/src/Cryptol/Backend.hs
@@ -614,6 +614,12 @@ class MonadIO (SEval sym) => Backend sym where
     SWord sym ->
     SEval sym (SInteger sym)
 
+  -- | Construct a signed integer value from the given packed word.
+  wordToSignedInt ::
+    sym ->
+    SWord sym ->
+    SEval sym (SInteger sym)
+
   -- ==== Integer operations ====
 
   -- | Addition of unbounded integers.
diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs
index 3a800fe4..348ef63b 100644
--- a/src/Cryptol/Backend/Concrete.hs
+++ b/src/Cryptol/Backend/Concrete.hs
@@ -185,6 +185,7 @@ instance Backend Concrete where
   integerAsLit _ = Just
 
   wordToInt _ (BV _ x) = pure x
+  wordToSignedInt _ (BV w x) = pure $! signedValue w x
   wordFromInt _ w x = pure $! mkBv w x
 
   packWord _ bits = pure $! BV (toInteger w) a
diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs
index e18a195d..5ad5bd1d 100644
--- a/src/Cryptol/Backend/SBV.hs
+++ b/src/Cryptol/Backend/SBV.hs
@@ -293,6 +293,7 @@ instance Backend SBV where
   wordLg2 _ a = sLg2 a
 
   wordToInt _ x = pure $! svToInteger x
+  wordToSignedInt _ x = pure $! svToInteger (svSign x)
   wordFromInt _ w i = pure $! svFromInteger w i
 
   intEq _ a b = pure $! svEqual a b
diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs
index 11731522..fe0f9c1a 100644
--- a/src/Cryptol/Backend/What4.hs
+++ b/src/Cryptol/Backend/What4.hs
@@ -362,6 +362,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
         liftIO (SW.bvSRem (w4 sym) x y)
 
   wordToInt sym x = liftIO (SW.bvToInteger (w4 sym) x)
+  wordToSignedInt sym x = liftIO (SW.sbvToInteger (w4 sym) x)
   wordFromInt sym width i = liftIO (SW.integerToBV (w4 sym) i width)
 
   intPlus   sym x y  = liftIO $ W4.intAdd (w4 sym) x y
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 005bc875..6045d4e3 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -716,6 +716,13 @@ smodV sym  =
   PWordFun \y ->
   PPrim (VWord w . wordVal <$> wordSignedMod sym x y)
 
+{-# SPECIALIZE toSignedIntegerV :: Concrete -> Prim Concrete #-}
+toSignedIntegerV :: Backend sym => sym -> Prim sym
+toSignedIntegerV sym =
+  PFinPoly \_w ->
+  PWordFun \x ->
+  PPrim (VInteger <$> wordToSignedInt sym x)
+
 -- Cmp -------------------------------------------------------------------------
 
 {-# SPECIALIZE cmpValue ::
@@ -2031,6 +2038,9 @@ genericPrimTable sym getEOpts =
                     unary (roundToEvenV sym))
 
     -- Bitvector specific operations
+  , ("toSignedInteger"
+                  , {-# SCC "Prelude::toSignedInteger" #-}
+                    toSignedIntegerV sym)
   , ("/$"         , {-# SCC "Prelude::(/$)" #-}
                     sdivV sym)
   , ("%$"         , {-# SCC "Prelude::(%$)" #-}