Merge pull request #1136 from GaloisInc/word-eval-refactor

Word eval refactor

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -31,11 +31,15 @@ import Numeric (showHex)
 import Cryptol.Backend.Monad
 import Cryptol.Backend.Concrete hiding (Concrete)
 import qualified Cryptol.Backend.Concrete as C
+import Cryptol.Backend.SeqMap (enumerateSeqMap)
+import Cryptol.Backend.WordValue (asWordVal)
 
 import Cryptol.Eval (evalSel)
 import Cryptol.Eval.Concrete (Value)
 import Cryptol.Eval.Type (TValue(..), tValTy)
-import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap)
+import Cryptol.Eval.Value (GenValue(..))
+
+
 import Cryptol.Parser
 import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type,
           ExportType(..))
@@ -389,7 +393,7 @@ readBack ty val =
         return Unit
       | contents == TVBit
       , VWord width wv <- val ->
-        do BV w v <- wv >>= asWordVal C.Concrete
+        do BV w v <- asWordVal C.Concrete wv
            let hexStr = T.pack $ showHex v ""
            let paddedLen = fromIntegral ((width `quot` 4) + (if width `rem` 4 == 0 then 0 else 1))
            return $ Num Hex (T.justifyRight paddedLen '0' hexStr) w

cryptol.cabal

@@ -164,8 +164,10 @@ library
                        Cryptol.Backend.Concrete,
                        Cryptol.Backend.FloatHelpers,
                        Cryptol.Backend.Monad,
+                       Cryptol.Backend.SeqMap,
                        Cryptol.Backend.SBV,
                        Cryptol.Backend.What4,
+                       Cryptol.Backend.WordValue,
 
                        Cryptol.Eval,
                        Cryptol.Eval.Concrete,

docs/CryptolPrims.md

@@ -20,6 +20,7 @@ a member of `Ring` and `Zero`.
 Literals
 -----------------------
     type Literal : # -> * -> Prop
+    type LiteralLessThan : # -> * -> Prop
 
     number : {val, rep} Literal val rep => rep
     length : {n, a, b} (fin n, Literal n b) => [n]a -> b
@@ -38,6 +39,11 @@ Literals
                    , lengthFromThenTo first next last == len) =>
                   [len]a
 
+    // '[a .. < b]` is syntactic sugar for 'fromToLessThan`{first=a,bound=b}'
+    fromToLessThan : {first, bound, a}
+         (fin first, bound >= first, LiteralLessThan bound a) =>
+         [bound - first]a
+
 Fractional Literals
 -------------------
 
@@ -48,7 +54,7 @@ or report an error if the number can't be represented exactly.
     type FLiteral : # -> # -> # -> * -> Prop
 
 
-Fractional literals are desugared into calles to the primitive `fraction`:
+Fractional literals are desugared into calls to the primitive `fraction`:
 
     fraction : { m, n, r, a } FLiteral m n r a => a
 
@@ -274,15 +280,15 @@ Sequences
     updates    : {n,k,ix,a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
     updatesEnd : {n,k,ix,d} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
 
-    take       : {front,back,elem} (fin front) => [front + back]elem -> [front]elem
+    take       : {front,back,elem} [front + back]elem -> [front]elem
     drop       : {front,back,elem} (fin front) => [front + back]elem -> [back]elem
     head       : {a, b} [1 + a]b -> b
     tail       : {a, b} [1 + a]b -> [a]b
     last       : {a, b} [1 + a]b -> b
 
     // Declarations of the form 'x @ i = e' are syntactic
     // sugar for 'x = generate (\i -> e)'.
-    generate   : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a
+    generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
 
     groupBy    : {each,parts,elem} (fin each) => [parts * each]elem -> [parts][each]elem
 

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -790,7 +790,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:822:14--822:20
+  (Cryptol::@) called at Cryptol:820:14--820:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9
@@ -2109,12 +2109,13 @@ \subsection{Predicates}
 \restartrepl
 \begin{replPrompt}
   Cryptol> :t take
-  take : {front, back, a} (fin front) => [front + back]a -> [front]a
+  take : {front, back, a} [front + back]a -> [front]a
 \end{replPrompt}
 
 The type of {\tt take} says that it is parameterized over {\tt front}
-and {\tt back}, {\tt front} must be a finite value,\indFin it takes a
-sequence {\tt front + back} long, and returns a sequence {\tt front} long.
+and {\tt back} and a type {\tt a}, it takes a sequence
+{\tt front + back} long of elements of type {\tt a}, and returns a
+sequence {\tt front} long.
 
 The impact of this predicate shows up when we try to take more than
 what is available:

lib/Cryptol.cry

@@ -717,8 +717,9 @@ primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a
  * Splits a sequence into a pair of sequences.
  * 'splitAt z = (x, y)' iff 'x # y = z'.
  */
-primitive splitAt : {front, back, a} (fin front) => [front + back]a
-                                                 -> ([front]a, [back]a)
+splitAt : {front, back, a} (fin front) => [front + back]a
+                                       -> ([front]a, [back]a)
+splitAt xs = (take`{front,back} xs, drop`{front,back} xs)
 
 /**
  * Concatenates a list of sequences.
@@ -745,18 +746,15 @@ primitive reverse : {n, a} (fin n) => [n]a -> [n]a
  */
 primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
 
-
 /**
  * Select the first (left-most) 'front' elements of a sequence.
  */
-take : {front, back, a} (fin front) => [front + back]a -> [front]a
-take (x # _) = x
+primitive take : {front, back, a} [front + back]a -> [front]a
 
 /**
  * Select all the elements after (to the right of) the 'front' elements of a sequence.
  */
-drop : {front, back, a} (fin front) => [front + back]a -> [back]a
-drop ((_ : [front] _) # y) = y
+primitive drop : {front, back, a} (fin front) => [front + back]a -> [back]a
 
 /**
  * Drop the first (left-most) element of a sequence.

lib/SuiteB.cry

@@ -205,7 +205,7 @@ private
     type sha2_padded_size w L = sha2_num_blocks w L * sha2_block_size w
 
     sha2pad : {w, L} (fin w, fin L, w >= 1) => [L] -> [sha2_padded_size w L]
-    sha2pad M = M # 0b1 # zero # ((fromInteger `L) : [2*w])
+    sha2pad M = rnf (M # 0b1 # zero # ((fromInteger `L) : [2*w]))
 
     sha2blocks : {w, L} (fin w, fin L, w >= 1) =>
       [L] -> [sha2_num_blocks w L][16][w]

src/Cryptol/Backend.hs

@@ -7,6 +7,10 @@ module Cryptol.Backend
   , cryUserError
   , cryNoPrimError
   , FPArith2
+  , IndexDirection(..)
+
+  , enumerateIntBits
+  , enumerateIntBits'
 
     -- * Rationals
   , SRational(..)
@@ -29,14 +33,20 @@ module Cryptol.Backend
   , iteRational
   ) where
 
+import qualified Control.Exception as X
 import Control.Monad.IO.Class
 import Data.Kind (Type)
 
 import Cryptol.Backend.FloatHelpers (BF)
 import Cryptol.Backend.Monad
-  ( EvalError(..), CallStack, pushCallFrame )
+  ( EvalError(..), Unsupported(..), CallStack, pushCallFrame )
 import Cryptol.ModuleSystem.Name(Name)
 import Cryptol.Parser.Position
+import Cryptol.TypeCheck.Solver.InfNat(Nat'(..),widthInteger)
+
+data IndexDirection
+  = IndexForward
+  | IndexBackward
 
 invalidIndex :: Backend sym => sym -> Integer -> SEval sym a
 invalidIndex sym i = raiseError sym (InvalidIndex (Just i))
@@ -191,6 +201,31 @@ iteRational :: Backend sym => sym -> SBit sym -> SRational sym -> SRational sym
 iteRational sym p (SRational a b) (SRational c d) =
   SRational <$> iteInteger sym p a c <*> iteInteger sym p b d
 
+-- | Compute the list of bits in an integer in big-endian order.
+--   The integer argument is a concrete upper bound for
+--   the symbolic integer.
+enumerateIntBits' :: Backend sym =>
+  sym ->
+  Integer ->
+  SInteger sym ->
+  SEval sym (Integer, [SBit sym])
+enumerateIntBits' sym n idx =
+  do let width = widthInteger n
+     w <- wordFromInt sym width idx
+     bs <- unpackWord sym w
+     pure (width, bs)
+
+-- | Compute the list of bits in an integer in big-endian order.
+--   Fails if neither the sequence length nor the type value
+--   provide an upper bound for the integer.
+enumerateIntBits :: Backend sym =>
+  sym ->
+  Nat' ->
+  SInteger sym ->
+  SEval sym (Integer, [SBit sym])
+enumerateIntBits sym (Nat n) idx = enumerateIntBits' sym n idx
+enumerateIntBits _sym Inf _ = liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer shifting"))
+
 -- | This type class defines a collection of operations on bits, words and integers that
 --   are necessary to define generic evaluator primitives that operate on both concrete
 --   and symbolic values uniformly.
@@ -205,7 +240,7 @@ class MonadIO (SEval sym) => Backend sym where
 
   -- | Check if an operation is "ready", which means its
   --   evaluation will be trivial.
-  isReady :: sym -> SEval sym a -> Bool
+  isReady :: sym -> SEval sym a -> SEval sym (Maybe a)
 
   -- | Produce a thunk value which can be filled with its associated computation
   --   after the fact.  A preallocated thunk is returned, along with an operation to
@@ -488,6 +523,51 @@ class MonadIO (SEval sym) => Backend sym where
     SWord sym ->
     SEval sym (SWord sym)
 
+  -- | Shift a bitvector left by the specified amount.
+  --   The shift amount is considered as an unsigned value.
+  --   Shifting by more than the word length results in 0.
+  wordShiftLeft ::
+    sym ->
+    SWord sym {- ^ value to shift -} ->
+    SWord sym {- ^ amount to shift by -} ->
+    SEval sym (SWord sym)
+
+  -- | Shift a bitvector right by the specified amount.
+  --   This is a logical shift, which shifts in 0 values
+  --   on the left. The shift amount is considered as an
+  --   unsigned value. Shifting by more than the word length
+  --   results in 0.
+  wordShiftRight ::
+    sym ->
+    SWord sym {- ^ value to shift -} ->
+    SWord sym {- ^ amount to shift by -} ->
+    SEval sym (SWord sym)
+
+  -- | Shift a bitvector right by the specified amount.  This is an
+  --   arithmetic shift, which shifts in copies of the high bit on the
+  --   left. The shift amount is considered as an unsigned
+  --   value. Shifting by more than the word length results in filling
+  --   the bitvector with the high bit.
+  wordSignedShiftRight ::
+    sym ->
+    SWord sym {- ^ value to shift -} ->
+    SWord sym {- ^ amount to shift by -} ->
+    SEval sym (SWord sym)
+
+  wordRotateLeft ::
+    sym ->
+    SWord sym {- ^ value to rotate -} ->
+    SWord sym {- ^ amount to rotate by -} ->
+    SEval sym (SWord sym)
+
+  wordRotateRight ::
+    sym ->
+    SWord sym {- ^ value to rotate -} ->
+    SWord sym {- ^ amount to rotate by -} ->
+    SEval sym (SWord sym)
+
+
+
   -- | 2's complement negation of bitvectors
   wordNegate ::
     sym ->

src/Cryptol/Backend/Concrete.hs

@@ -152,8 +152,7 @@ instance Backend Concrete where
   wordUpdate _ (BV w x) idx True  = pure $! BV w (setBit   x (fromInteger (w - 1 - idx)))
   wordUpdate _ (BV w x) idx False = pure $! BV w (clearBit x (fromInteger (w - 1 - idx)))
 
-  isReady _ (Ready _) = True
-  isReady _ _ = False
+  isReady _ = maybeReady
 
   mergeEval _sym f c mx my =
     do x <- mx
@@ -285,6 +284,33 @@ instance Backend Concrete where
            pure $! mkBv i (sx `rem` sy)
     | otherwise = panic "Attempt to mod words of different sizes: wordSignedMod" [show i, show j]
 
+  wordShiftLeft _sym (BV w ival) (BV _ by)
+    | by >= w   = pure $! BV w 0
+    | by > toInteger (maxBound :: Int) = panic "shl" ["Shift amount too large", show by]
+    | otherwise = pure $! mkBv w (shiftL ival (fromInteger by))
+
+  wordShiftRight _sym (BV w ival) (BV _ by)
+    | by >= w   = pure $! BV w 0
+    | by > toInteger (maxBound :: Int) = panic "lshr" ["Shift amount too large", show by]
+    | otherwise = pure $! BV w (shiftR ival (fromInteger by))
+
+  wordSignedShiftRight _sym (BV w ival) (BV _ by) =
+    let by' = min w by in
+    if by' > toInteger (maxBound :: Int) then
+      panic "wordSignedShiftRight" ["Shift amount too large", show by]
+    else
+      pure $! mkBv w (shiftR (signedValue w ival) (fromInteger by'))
+
+  wordRotateRight _sym (BV 0 i) _ = pure (BV 0 i)
+  wordRotateRight _sym (BV w i) (BV _ by) =
+      pure . mkBv w $! (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))
+    where b = fromInteger (by `mod` w)
+
+  wordRotateLeft _sym (BV 0 i) _ = pure (BV 0 i)
+  wordRotateLeft _sym (BV w i) (BV _ by) =
+      pure . mkBv w $! (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))
+    where b = fromInteger (by `mod` w)
+
   wordLg2 _ (BV i x) = pure $! mkBv i (lg2 x)
 
   intEq _ x y = pure $! x == y

src/Cryptol/Backend/Monad.hs

@@ -328,13 +328,15 @@ modifyCallStack f m =
   Eval $ \stk ->
     do let stk' = f stk
        -- putStrLn $ unwords ["Pushing call stack", show (displayCallStack stk')]
-       runEval stk' m
+       seq stk' (runEval stk' m)
+{-# INLINE modifyCallStack #-}
 
 -- | Execute the given evaluation action.
 runEval :: CallStack -> Eval a -> IO a
 runEval _   (Ready a)  = return a
 runEval stk (Eval x)   = x stk
 runEval _   (Thunk tv) = unDelay tv
+{-# INLINE runEval #-}
 
 {-# INLINE evalBind #-}
 evalBind :: Eval a -> (a -> Eval b) -> Eval b

src/Cryptol/Backend/SBV.hs

@@ -48,7 +48,7 @@ import Cryptol.Backend.Concrete ( integerToChar )
 import Cryptol.Backend.Monad
   ( Eval(..), blackhole, delayFill, evalSpark
   , EvalError(..), EvalErrorEx(..), Unsupported(..)
-  , modifyCallStack, getCallStack
+  , modifyCallStack, getCallStack, maybeReady
   )
 
 import Cryptol.Utils.Panic (panic)
@@ -162,8 +162,10 @@ instance Backend SBV where
     | Just False <- svAsBool cond = raiseError sym err
     | otherwise = SBVEval (pure (SBVResult cond ()))
 
-  isReady _ (SBVEval (Ready _)) = True
-  isReady _ _ = False
+  isReady _ (SBVEval m) = SBVEval $
+    maybeReady m >>= \case
+      Just x  -> pure (Just <$> x)
+      Nothing -> pure (pure Nothing)
 
   sDelayFill _ m retry msg = SBVEval $
     do m' <- delayFill (sbvEval m) (sbvEval <$> retry) msg
@@ -262,6 +264,12 @@ instance Backend SBV where
   wordMult  _ a b = pure $! svTimes a b
   wordNegate _ a  = pure $! svUNeg a
 
+  wordShiftLeft _ a b   = pure $! shl a b
+  wordShiftRight _ a b  = pure $! lshr a b
+  wordRotateLeft _ a b  = pure $! SBV.svRotateLeft a b
+  wordRotateRight _ a b = pure $! SBV.svRotateRight a b
+  wordSignedShiftRight _ a b = pure $! ashr a b
+
   wordDiv sym a b =
     do let z = literalSWord (intSizeOf b) 0
        assertSideCondition sym (svNot (svEqual b z)) DivideByZero