cryptol 2.11.0 → 2.12.0

raw patch · 79 files changed

+6573/−4328 lines, 79 filesdep +prettyprinterdep −prettydep −randomdep ~sbvdep ~simple-smtdep ~what4PVP ok

version bump matches the API change (PVP)

Dependencies added: prettyprinter

Dependencies removed: pretty, random

Dependency ranges changed: sbv, simple-smt, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +78/−0
• cryptol.cabal +17/−9
• cryptol/Main.hs +4/−10
• cryptol/REPL/Haskeline.hs +2/−2
• lib/Array.cry +44/−0
• lib/Cryptol.cry +102/−24
• lib/CryptolTC.z3 +14/−8
• lib/SuiteB.cry +1/−1
• src/Cryptol/Backend.hs +88/−2
• src/Cryptol/Backend/Concrete.hs +30/−3
• src/Cryptol/Backend/Monad.hs +43/−8
• src/Cryptol/Backend/SBV.hs +12/−3
• src/Cryptol/Backend/SeqMap.hs +301/−0
• src/Cryptol/Backend/What4.hs +13/−6
• src/Cryptol/Backend/WordValue.hs +759/−0
• src/Cryptol/Eval.hs +33/−202
• src/Cryptol/Eval/Concrete.hs +56/−181
• src/Cryptol/Eval/Env.hs +0/−2
• src/Cryptol/Eval/Generic.hs +398/−583
• src/Cryptol/Eval/Reference.lhs +83/−25
• src/Cryptol/Eval/SBV.hs +59/−201
• src/Cryptol/Eval/Value.hs +123/−296
• src/Cryptol/Eval/What4.hs +62/−236
• src/Cryptol/F2.hs +2/−1
• src/Cryptol/ModuleSystem.hs +11/−4
• src/Cryptol/ModuleSystem/Base.hs +76/−67
• src/Cryptol/ModuleSystem/Env.hs +93/−101
• src/Cryptol/ModuleSystem/Exports.hs +48/−31
• src/Cryptol/ModuleSystem/InstantiateModule.hs +33/−14
• src/Cryptol/ModuleSystem/Interface.hs +80/−67
• src/Cryptol/ModuleSystem/Monad.hs +16/−19
• src/Cryptol/ModuleSystem/Name.hs +74/−66
• src/Cryptol/ModuleSystem/NamingEnv.hs +213/−135
• src/Cryptol/ModuleSystem/Renamer.hs +514/−485
• src/Cryptol/ModuleSystem/Renamer/Error.hs +205/−0
• src/Cryptol/ModuleSystem/Renamer/Monad.hs +342/−0
• src/Cryptol/Parser.y +84/−23
• src/Cryptol/Parser/AST.hs +158/−64
• src/Cryptol/Parser/Layout.hs +237/−0
• src/Cryptol/Parser/Lexer.x +16/−1
• src/Cryptol/Parser/LexerUtils.hs +6/−215
• src/Cryptol/Parser/Name.hs +2/−2
• src/Cryptol/Parser/Names.hs +22/−19
• src/Cryptol/Parser/NoInclude.hs +13/−7
• src/Cryptol/Parser/NoPat.hs +20/−2
• src/Cryptol/Parser/ParserUtils.hs +82/−24
• src/Cryptol/Parser/Position.hs +5/−3
• src/Cryptol/Parser/Selector.hs +5/−5
• src/Cryptol/Parser/Token.hs +119/−0
• src/Cryptol/REPL/Browse.hs +155/−0
• src/Cryptol/REPL/Command.hs +75/−263
• src/Cryptol/REPL/Monad.hs +150/−32
• src/Cryptol/Symbolic.hs +27/−5
• src/Cryptol/Symbolic/What4.hs +248/−79
• src/Cryptol/Testing/Random.hs +10/−8
• src/Cryptol/Transform/MonoValues.hs +5/−5
• src/Cryptol/Transform/Specialize.hs +3/−2
• src/Cryptol/TypeCheck.hs +47/−32
• src/Cryptol/TypeCheck/AST.hs +71/−66
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +17/−4
• src/Cryptol/TypeCheck/Depends.hs +0/−214
• src/Cryptol/TypeCheck/Error.hs +64/−52
• src/Cryptol/TypeCheck/Infer.hs +177/−88
• src/Cryptol/TypeCheck/InferTypes.hs +38/−24
• src/Cryptol/TypeCheck/Interface.hs +73/−0
• src/Cryptol/TypeCheck/Monad.hs +222/−134
• src/Cryptol/TypeCheck/Parseable.hs +20/−8
• src/Cryptol/TypeCheck/SimpType.hs +13/−2
• src/Cryptol/TypeCheck/SimpleSolver.hs +1/−2
• src/Cryptol/TypeCheck/Solver/InfNat.hs +9/−10
• src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +2/−2
• src/Cryptol/TypeCheck/Solver/SMT.hs +23/−12
• src/Cryptol/TypeCheck/Solver/Selector.hs +6/−6
• src/Cryptol/TypeCheck/Subst.hs +8/−0
• src/Cryptol/TypeCheck/TCon.hs +3/−3
• src/Cryptol/TypeCheck/Type.hs +66/−29
• src/Cryptol/TypeCheck/TypeOf.hs +26/−3
• src/Cryptol/Utils/Ident.hs +82/−2
• src/Cryptol/Utils/PP.hs +134/−84

@@ -1,3 +1,81 @@+# 2.12.0++## Language changes+* Updates to the layout rule.  We simplified the specification and made+  some minor changes, in particular:+    - Paren blocks nested in a layout block need to respect the indentation+      if the layout block+    - We allow nested layout blocks to have the same indentation, which is+      convenient when writing `private` declarations as they don't need to+      be indented as long as they are at the end of the file.++* New enumeration forms `[x .. y by n]`, `[x .. <y by n]`,+  `[x .. y down by n]` and `[x .. >y down by n]` have been+  implemented. These new forms let the user explicitly specify+  the stride for an enumeration, as opposed to the previous+  `[x, y .. z]` form (where the stride was computed from `x` and `y`).++* Nested modules are now available (from pull request #1048). For example, the following is now valid Cryptol:++        module SubmodTest where++        import submodule B as C++        submodule A where+          propA = C::y > 5++        submodule B where+          y : Integer+          y = 42++## New features++* What4 prover backends now feature an improved multi-SAT procedure+  which is significantly faster than the old algorithm. Thanks to+  Levent Erkök for the suggestion.++* There is a new `w4-abc` solver option, which communicates to ABC+  as an external process via What4.++* Expanded support for declaration forms in the REPL. You can now+  define infix operators, type synonyms and mutually-recursive functions,+  and state signatures and fixity declarations. Multiple declarations+  can be combined into a single line by separating them with `;`,+  which is necessary for stating a signature together with a+  definition, etc.+  +* There is a new `:set path` REPL option that provides an alternative to+  `CRYPTOLPATH` for controlling where to search for imported modules+  (issue #631).++* The `cryptol-remote-api` server now natively supports HTTPS (issue+  #1008), `newtype` values (issue #1033), and safety checking (issue+  #1166).++* Releases optionally include solvers (issue #1111). See the+  `*-with-solvers*` files in the assets list for this release.++## Bug fixes++* Closed issues #422, #436, #619, #631, #633, #640, #680, #734, #735,+  #759, #760, #764, #849, #996, #1000, #1008, #1019, #1032, #1033,+  #1034, #1043, #1047, #1060, #1064, #1083, #1084, #1087, #1102, #1111,+  #1113, #1117, #1125, #1133, #1142, #1144, #1145, #1146, #1157, #1160,+  #1163, #1166, #1169, #1175, #1179, #1182, #1190, #1191, #1196, #1197,+  #1204, #1209, #1210, #1213, #1216, #1223, #1226, #1238, #1239, #1240,+  #1241, #1250, #1256, #1259, #1261, #1266, #1274, #1275, #1283, and+  #1291.++* Merged pull requests #1048, #1128, #1129, #1130, #1131, #1135, #1136,+  #1137, #1139, #1148, #1149, #1150, #1152, #1154, #1156, #1158, #1159,+  #1161, #1164, #1165, #1168, #1170, #1171, #1172, #1173, #1174, #1176,+  #1181, #1183, #1186, #1188, #1192, #1193, #1194, #1195, #1199, #1200,+  #1202, #1203, #1205, #1207, #1211, #1214, #1215, #1218, #1219, #1221,+  #1224, #1225, #1227, #1228, #1230, #1231, #1232, #1234, #1242, #1243,+  #1244, #1245, #1246, #1247, #1248, #1251, #1252, #1254, #1255, #1258,+  #1263, #1265, #1268, #1269, #1270, #1271, #1272, #1273, #1276, #1281,+  #1282, #1284, #1285, #1286, #1287, #1288, #1293, #1294, and #1295.+ # 2.11.0  ## Language changes

@@ -1,6 +1,6 @@ Cabal-version:       2.4 Name:                cryptol-Version:             2.11.0+Version:             2.12.0 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD-3-Clause@@ -25,7 +25,8 @@ source-repository this   type:     git   location: https://github.com/GaloisInc/cryptol.git-  tag:      2.11.0+  -- add a tag on release branches+  tag:      2.12.0   flag static@@ -61,11 +62,10 @@                        monad-control     >= 1.0,                        monadLib          >= 3.7.2,                        parameterized-utils >= 2.0.2,-                       pretty            >= 1.1,+                       prettyprinter     >= 1.7.0,                        process           >= 1.2,-                       random            >= 1.0.1,-                       sbv               >= 8.6 && < 8.13,-                       simple-smt        >= 0.7.1,+                       sbv               >= 8.6 && < 8.17,+                       simple-smt        >= 0.9.7,                        stm               >= 2.4,                        strict,                        text              >= 1.1,@@ -74,13 +74,15 @@                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.1 && < 1.2+                       what4             >= 1.2 && < 1.3    Build-tool-depends:  alex:alex, happy:happy   hs-source-dirs:      src    Exposed-modules:     Cryptol.Parser,                        Cryptol.Parser.Lexer,+                       Cryptol.Parser.Token,+                       Cryptol.Parser.Layout,                        Cryptol.Parser.AST,                        Cryptol.Parser.Position,                        Cryptol.Parser.Names,@@ -110,9 +112,11 @@                        Cryptol.ModuleSystem.Monad,                        Cryptol.ModuleSystem.Name,                        Cryptol.ModuleSystem.NamingEnv,-                       Cryptol.ModuleSystem.Renamer,                        Cryptol.ModuleSystem.Exports,                        Cryptol.ModuleSystem.InstantiateModule,+                       Cryptol.ModuleSystem.Renamer,+                       Cryptol.ModuleSystem.Renamer.Monad,+                       Cryptol.ModuleSystem.Renamer.Error,                         Cryptol.TypeCheck,                        Cryptol.TypeCheck.Type,@@ -125,12 +129,12 @@                        Cryptol.TypeCheck.Infer,                        Cryptol.TypeCheck.CheckModuleInstance,                        Cryptol.TypeCheck.InferTypes,+                       Cryptol.TypeCheck.Interface,                        Cryptol.TypeCheck.Error,                        Cryptol.TypeCheck.Kind,                        Cryptol.TypeCheck.Subst,                        Cryptol.TypeCheck.Instantiate,                        Cryptol.TypeCheck.Unify,-                       Cryptol.TypeCheck.Depends,                        Cryptol.TypeCheck.PP,                        Cryptol.TypeCheck.Solve,                        Cryptol.TypeCheck.Default,@@ -162,8 +166,10 @@                        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,@@ -188,6 +194,7 @@                        Cryptol.Symbolic.What4,                         Cryptol.REPL.Command,+                       Cryptol.REPL.Browse,                        Cryptol.REPL.Monad,                        Cryptol.REPL.Trie @@ -224,6 +231,7 @@                      , directory                      , filepath                      , haskeline >= 0.7 && < 0.9+                     , exceptions                      , monad-control                      , text                      , transformers

@@ -15,7 +15,7 @@  import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandExitCode(..)) import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,-                   io,prependSearchPath,setSearchPath)+                   io,prependSearchPath,setSearchPath,parseSearchPath) import qualified Cryptol.REPL.Monad as REPL import Cryptol.ModuleSystem.Env(ModulePath(..)) @@ -32,7 +32,7 @@ import System.Directory (getTemporaryDirectory, removeFile) import System.Environment (getArgs, getProgName, lookupEnv) import System.Exit (exitFailure,exitSuccess)-import System.FilePath (searchPathSeparator, splitSearchPath, takeDirectory)+import System.FilePath (searchPathSeparator, takeDirectory) import System.IO (hClose, hPutStr, openTempFile)  @@ -256,14 +256,8 @@   mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"   case mCryptolPath of     Nothing -> return ()-    Just path | optCryptolPathOnly opts -> setSearchPath path'-              | otherwise               -> prependSearchPath path'-#if defined(mingw32_HOST_OS) || defined(__MINGW32__)-      -- Windows paths search from end to beginning-      where path' = reverse (splitSearchPath path)-#else-      where path' = splitSearchPath path-#endif+    Just path | optCryptolPathOnly opts -> setSearchPath (parseSearchPath path)+              | otherwise               -> prependSearchPath (parseSearchPath path)   smoke <- REPL.smokeTest   case smoke of     [] -> return ()

@@ -16,7 +16,7 @@ import           Cryptol.REPL.Command import           Cryptol.REPL.Monad import           Cryptol.REPL.Trie-import           Cryptol.Utils.PP+import           Cryptol.Utils.PP hiding ((</>)) import           Cryptol.Utils.Logger(stdoutLogger) import           Cryptol.Utils.Ident(modNameToText, interactiveName) @@ -99,7 +99,7 @@ getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []   where   loop ls prompt =-    do mb <- getInputLine prompt+    do mb <- fmap (filter (/= '\r')) <$> getInputLine prompt        let newPropmpt = map (\_ -> ' ') prompt        case mb of          Nothing -> return NoMoreLines

@@ -11,3 +11,47 @@ primitive arrayLookup : {a, b} (Array a b) -> a -> b primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b) +/**+ * Copy elements from the source array to the destination array.+ *+ * 'arrayCopy dest_arr dest_idx src_arr src_idx len' copies the+ * elements from 'src_arr' at indices '[src_idx ..< (src_idx + len)]' into+ * 'dest_arr' at indices '[dest_idx ..< (dest_idx + len)]'.+ *+ * The result is undefined if either 'dest_idx + len' or 'src_idx + len'+ * wraps around.+ */+primitive arrayCopy : {n, a} (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n] -> (Array [n] a)+/**+ * Set elements of the given array.+ *+ * 'arraySet' arr idx val len' sets the elements of 'arr' at indices+ * '[idx ..< (idx + len)]' to 'val'.+ *+ * The result is undefined if 'idx + len' wraps around.+ */+primitive arraySet : {n, a} (Array [n] a) -> [n] -> a -> [n] -> (Array [n] a)+/**+ * Check whether the lhs array and rhs array are equal at a range of+ * indices.+ *+ * 'arrayRangeEq sym lhs_arr lhs_idx rhs_arr rhs_idx len' checks whether+ * the elements of 'lhs_arr' at indices '[lhs_idx ..< (lhs_idx + len)]' and+ * the elements of 'rhs_arr' at indices '[rhs_idx ..< (rhs_idx + len)]' are+ * equal.+ *+ * The result is undefined if either 'lhs_idx + len' or 'rhs_idx + len'+ * wraps around.+ */+primitive arrayRangeEqual : {n, a} (Array [n] a) -> [n] -> (Array [n] a) -> [n] -> [n] -> Bool++arrayRangeLookup : {a, b, n} (Integral a, fin n, LiteralLessThan n a) => (Array a b) -> a -> [n]b+arrayRangeLookup arr idx = res+  where+    res @ i = arrayLookup arr (idx + i)++arrayRangeUpdate : {a, b, n} (Integral a, fin n, LiteralLessThan n a) => (Array a b) -> a -> [n]b -> (Array a b)+arrayRangeUpdate arr idx vals = arrs ! 0+  where+    arrs = [arr] # [ arrayUpdate acc (idx + i) val | acc <- arrs | i <- [0 ..< n] | val <- vals ]+

@@ -32,7 +32,7 @@ /**  * 'Z n' is the type of integers, modulo 'n'.  *- * The values of 'Z n' may be thought of as equivalance+ * The values of 'Z n' may be thought of as equivalence  * classes of integers according to the equivalence  * 'x ~ y' iff 'n' divides 'x - y'.  'Z n' naturally  * forms a ring, but does not support integral division@@ -41,9 +41,9 @@  * However, you may use the 'fromZ' operation  * to project values in 'Z n' into the integers if such operations  * are required.  This will compute the reduced representative- * of the equivalance class. In other words, 'fromZ' computes+ * of the equivalence class. In other words, 'fromZ' computes  * the (unique) integer value 'i'  where '0 <= i < n' and- * 'i' is in the given equivalance class.+ * 'i' is in the given equivalence class.  *  * If the modulus 'n' is prime, 'Z n' also  * supports computing inverses and forms a field.@@ -131,13 +131,13 @@ /** Divide numeric types, rounding up. */ primitive type   { m : #, n : # }-  (fin m, fin n, n >= 1) =>+  (fin n, n >= 1) =>   m /^ n : #  /** How much we need to add to make a proper multiple of the second argument. */ primitive type   { m : #, n : # }-  (fin m, fin n, n >= 1) =>+  (fin n, n >= 1) =>   m %^ n : #  /** The length of an enumeration. */@@ -195,26 +195,76 @@ /**  * A finite sequence counting up from 'first' to 'last'.  *- * '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.+ * '[x .. y]' is syntactic sugar for 'fromTo`{first=x,last=y}'.  */-primitive fromTo : {first, last, a} (fin last, last >= first,-                                    Literal first a, Literal last a) =>-                                    [1 + (last - first)]a+primitive fromTo : {first, last, a}+  (fin last, last >= first, Literal last a) =>+  [1 + (last - first)]a  /**  * A possibly infinite sequence counting up from 'first' up to (but not including) 'bound'.  *- * Note that if 'first' = 'bound' then the sequence will be empty.+ * '[ x ..< y ]' is syntactic sugar for 'fromToLessThan`{first=x,bound=y}'.+ *+ * Note that if 'first' = 'bound' then the sequence will be empty.  If 'bound = inf'+ * then the sequence will be infinite, and will eventually wrap around for bounded types.  */ primitive fromToLessThan :-  {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => [bound - first]a+  {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) =>+  [bound - first]a +/**+ * A finite sequence counting up from 'first' to 'last' by 'stride'.+ * Note that 'last' will only be an element of the enumeration if+ * 'stride' divides 'last - first' evenly.+ *+ * '[x .. y by n]' is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'.+ */+primitive fromToBy : {first, last, stride, a}+  (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>+  [1 + (last - first)/stride]a  /**+ * A finite sequence counting from 'first' up to (but not including) 'bound'+ * by 'stride'.  Note that if 'first = bound' then the sequence will+ * be empty.  If 'bound = inf' then the sequence will be infinite, and will+ * eventually wrap around for bounded types.+ *+ * '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=x,bound=y,stride=n}'.+ */+primitive fromToByLessThan : {first, bound, stride, a}+  (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>+  [(bound - first)/^stride]a++/**+ * A finite sequence counting from 'first' down to 'last' by 'stride'.+ * Note that 'last' will only be an element of the enumeration if+ * 'stride' divides 'first - last' evenly.+ *+ * '[x .. y down by n]' is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'.+ */+primitive fromToDownBy : {first, last, stride, a}+  (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>+  [1 + (first - last)/stride]a++/**+ * A finite sequence counting from 'first' down to (but not including)+ * 'bound' by 'stride'.+ *+ * '[x ..> y down by n]' is syntactic sugar for+ * 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.+ *+ * Note that if 'first = bound' the sequence will be empty.+ */+primitive fromToDownByGreaterThan : {first, bound, stride, a}+  (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>+  [(first - bound)/^stride]a++/**  * A finite arithmetic sequence starting with 'first' and 'next',  * stopping when the values reach or would skip over 'last'.  *- * '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.+ * '[x,y..z]' is syntactic sugar for 'fromThenTo`{first=x,next=y,last=z}'.  */ primitive fromThenTo : {first, next, last, a, len}                        ( fin first, fin next, fin last@@ -224,12 +274,12 @@  // Fractional Literals --------------------- -/** 'FLiteral m n r a' asserts that the type `a' contains the-fraction `m/n`.  The flag `r` indicates if we should round (`r >= 1`)+/** 'FLiteral m n r a' asserts that the type 'a' contains the+fraction 'm/n'.  The flag 'r' indicates if we should round ('r >= 1') or report an error if the number can't be represented exactly. */ primitive type FLiteral : # -> # -> # -> * -> Prop -/** A fractional literal corresponding to `m/n` */+/** A fractional literal corresponding to 'm/n' */ primitive   fraction : { m, n, r, a } FLiteral m n r a => a @@ -387,7 +437,7 @@  /**  * Value types that correspond to a field; that is,- * a ring also posessing multiplicative inverses for+ * a ring also possessing multiplicative inverses for  * non-zero elements.  *  * Floating-point values are only approximately a field,@@ -684,7 +734,12 @@  */ 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 ----------------------------------------------  /**@@ -717,8 +772,9 @@  * 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 +801,15 @@  */ 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.@@ -899,6 +952,31 @@ generate f = [ f i | i <- [0 .. <n] ]  +/**+ * Sort a sequence of elements. Equivalent to 'sortBy (<=)'.+ */+sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a+sort = sortBy (<=)++/**+ * Sort a sequence according to the given less-than-or-equal relation.+ * The sorting is stable, so it preserves the relative position of any+ * pair of elements that are equivalent according to the order relation.+ */+sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a+sortBy le vs =+  if `n == (0 : Integer) then vs+  else drop`{1 - min 1 n} (insertBy (vs@0) (sortBy le (drop`{min 1 n} vs)))+  where+    insertBy : {k} (fin k) => a -> [k]a -> [k+1]a+    insertBy x0 ys = xys.0 # [last xs]+      where+        xs : [k+1]a+        xs = [x0] # xys.1+        xys : [k](a, a)+        xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ]++ // GF_2^n polynomial computations -------------------------------------------  /**@@ -920,7 +998,7 @@  /**  * Parallel map.  The given function is applied to each element in the- * given finite seqeuence, and the results are computed in parallel.+ * given finite sequence, and the results are computed in parallel.  * The values in the resulting sequence are reduced to normal form,  * as is done with the deepseq operation.  *

@@ -267,10 +267,12 @@   )) ) -- (declare-fun cryExpUnknown (Int Int) Int) +(assert (forall ((x Int) (y Int))+  (=> (and (> y 0) (> x 0))+      (>= (cryExpUnknown x y) x))))+ (define-fun cryExpTable ((x Int) (y Int)) Int   (ite (= y 0) 1   (ite (= y 1) x@@ -291,15 +293,19 @@ )  (define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat-  (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr-  (ite (= (value y) 0) cryErr (cryNat (- (div (- (value x)) (value y)))))-  )+  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr+  (ite (= (value y) 0) cryErr+  (ite (not (isFin x)) cryInf+    (cryNat (- (div (- (value x)) (value y))))+  ))) )  (define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat-  (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr-  (ite (= (value y) 0) cryErr (cryNat (mod (- (value x)) (value y))))-  )+  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr+  (ite (= (value y) 0) cryErr+  (ite (not (isFin x)) (cryNat 0)+    (cryNat (mod (- (value x)) (value y)))+  ))) )  (define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat

@@ -205,7 +205,7 @@     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]

@@ -7,7 +7,11 @@   , cryUserError   , cryNoPrimError   , FPArith2+  , IndexDirection(..) +  , enumerateIntBits+  , enumerateIntBits'+     -- * Rationals   , SRational(..)   , intToRational@@ -29,15 +33,21 @@   , 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 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 @@    -- | 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 @@     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 ->@@ -530,6 +610,12 @@    -- | Construct an integer value from the given packed word.   wordToInt ::+    sym ->+    SWord sym ->+    SEval sym (SInteger sym)++  -- | Construct a signed integer value from the given packed word.+  wordToSignedInt ::     sym ->     SWord sym ->     SEval sym (SInteger sym)

@@ -114,7 +114,7 @@   prefix = case base of     2  -> text "0b" <.> padding 1     8  -> text "0o" <.> padding 3-    10 -> empty+    10 -> mempty     16 -> text "0x" <.> padding 4     _  -> text "0"  <.> char '<' <.> int base <.> char '>' @@ -152,8 +152,7 @@   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@@ -186,6 +185,7 @@   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@@ -284,6 +284,33 @@                sy = signedValue i y            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) 

@@ -63,12 +63,33 @@  -- | The type of dynamic call stacks for the interpreter. --   New frames are pushed onto the right side of the sequence.-type CallStack = Seq (Name, Range)+data CallStack+  = EmptyCallStack+  | CombineCallStacks !CallStack !CallStack+  | PushCallFrame !Name !Range !CallStack +instance Semigroup CallStack where+  (<>) = CombineCallStacks++instance Monoid CallStack where+  mempty = EmptyCallStack++type CallStack' = Seq (Name, Range)++evalCallStack :: CallStack -> CallStack'+evalCallStack stk =+  case stk of+    EmptyCallStack -> mempty+    CombineCallStacks appstk fnstk -> combineCallStacks' (evalCallStack appstk) (evalCallStack fnstk)+    PushCallFrame n r stk1 -> pushCallFrame' n r (evalCallStack stk1)+ -- | Pretty print a call stack with each call frame on a separate --   line, with most recent call frames at the top. displayCallStack :: CallStack -> Doc-displayCallStack = vcat . map f . toList . Seq.reverse+displayCallStack = displayCallStack' . evalCallStack++displayCallStack' :: CallStack' -> Doc+displayCallStack' = vcat . map f . toList . Seq.reverse   where   f (nm,rng)     | rng == emptyRange = pp nm@@ -92,7 +113,15 @@   CallStack {- ^ call stack of the application context -} ->   CallStack {- ^ call stack of the function being applied -} ->   CallStack-combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk+combineCallStacks appstk EmptyCallStack = appstk+combineCallStacks EmptyCallStack fnstk = fnstk+combineCallStacks appstk fnstk = CombineCallStacks appstk fnstk++combineCallStacks' ::+  CallStack' {- ^ call stack of the application context -} ->+  CallStack' {- ^ call stack of the function being applied -} ->+  CallStack'+combineCallStacks' appstk fnstk = appstk <> dropCommonPrefix appstk fnstk   where   dropCommonPrefix _  Seq.Empty = Seq.Empty   dropCommonPrefix Seq.Empty fs = fs@@ -102,9 +131,12 @@  -- | Add a call frame to the top of a call stack pushCallFrame :: Name -> Range -> CallStack -> CallStack-pushCallFrame nm rng stk@( _ Seq.:|> (nm',rng'))+pushCallFrame nm rng stk = PushCallFrame nm rng stk++pushCallFrame' :: Name -> Range -> CallStack' -> CallStack'+pushCallFrame' nm rng stk@( _ Seq.:|> (nm',rng'))   | nm == nm', rng == rng' = stk-pushCallFrame nm rng stk = stk Seq.:|> (nm,rng)+pushCallFrame' nm rng stk = stk Seq.:|> (nm,rng)   -- | The monad for Cryptol evaluation.@@ -328,13 +360,15 @@   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@@ -415,11 +449,12 @@  deriving Typeable  instance PP EvalErrorEx where-  ppPrec _ (EvalErrorEx stk ex) = vcat ([ pp ex ] ++ callStk)+  ppPrec _ (EvalErrorEx stk0 ex) = vcat ([ pp ex ] ++ callStk)     where+    stk = evalCallStack stk0     callStk | Seq.null stk = []-            | otherwise = [ text "-- Backtrace --", displayCallStack stk ]+            | otherwise = [ text "-- Backtrace --", displayCallStack' stk ]  instance Show EvalErrorEx where   show = show . pp

@@ -48,7 +48,7 @@ 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 @@     | 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 @@   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@@ -285,6 +293,7 @@   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

@@ -0,0 +1,301 @@+-- |+-- Module      :  Cryptol.Backend.SeqMap+-- Copyright   :  (c) 2013-2021 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}++module Cryptol.Backend.SeqMap+  ( -- * Sequence Maps+    SeqMap+  , indexSeqMap+  , lookupSeqMap+  , finiteSeqMap+  , infiniteSeqMap+  , enumerateSeqMap+  , streamSeqMap+  , reverseSeqMap+  , updateSeqMap+  , dropSeqMap+  , concatSeqMap+  , splitSeqMap+  , memoMap+  , delaySeqMap+  , zipSeqMap+  , mapSeqMap+  , mergeSeqMap+  , barrelShifter+  , shiftSeqByInteger++  , IndexSegment(..)+  ) where++import qualified Control.Exception as X+import Control.Monad+import Control.Monad.IO.Class+import Data.Bits+import Data.List+import Data.IORef+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map++import Cryptol.Backend+import Cryptol.Backend.Concrete (Concrete)+import Cryptol.Backend.Monad (Unsupported(..))++import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))+import Cryptol.Utils.Panic++-- | A sequence map represents a mapping from nonnegative integer indices+--   to values.  These are used to represent both finite and infinite sequences.+data SeqMap sym a+  = IndexSeqMap  !(Integer -> SEval sym a)+  | UpdateSeqMap !(Map Integer (SEval sym a))+                 !(SeqMap sym a)+  | MemoSeqMap+     !Nat'+     !(IORef (Map Integer a))+     !(IORef (Integer -> SEval sym a))++indexSeqMap :: (Integer -> SEval sym a) -> SeqMap sym a+indexSeqMap = IndexSeqMap++lookupSeqMap :: Backend sym => SeqMap sym a -> Integer -> SEval sym a+lookupSeqMap (IndexSeqMap f) i = f i+lookupSeqMap (UpdateSeqMap m xs) i =+  case Map.lookup i m of+    Just x  -> x+    Nothing -> lookupSeqMap xs i+lookupSeqMap (MemoSeqMap sz cache eval) i =+  do mz <- liftIO (Map.lookup i <$> readIORef cache)+     case mz of+       Just z  -> return z+       Nothing ->+         do f <- liftIO (readIORef eval)+            v <- f i+            msz <- liftIO $ atomicModifyIORef' cache (\m ->+                        let m' = Map.insert i v m in (m', Map.size m'))+            -- If we memoize the entire map, overwrite the evaluation closure to let+            -- the garbage collector reap it+            when (case sz of Inf -> False; Nat sz' -> toInteger msz >= sz')+                 (liftIO (writeIORef eval+                    (\j -> panic "lookupSeqMap" ["Messed up size accounting", show sz, show j])))+            return v++instance Backend sym => Functor (SeqMap sym) where+  fmap f xs = IndexSeqMap (\i -> f <$> lookupSeqMap xs i)++-- | Generate a finite sequence map from a list of values+finiteSeqMap :: Backend sym => sym -> [SEval sym a] -> SeqMap sym a+finiteSeqMap sym xs =+   UpdateSeqMap+      (Map.fromList (zip [0..] xs))+      (IndexSeqMap (\i -> invalidIndex sym i))++-- | Generate an infinite sequence map from a stream of values+infiniteSeqMap :: Backend sym => sym -> [SEval sym a] -> SEval sym (SeqMap sym a)+infiniteSeqMap sym xs =+   -- TODO: use an int-trie?+   memoMap sym Inf (IndexSeqMap $ \i -> genericIndex xs i)++-- | Create a finite list of length @n@ of the values from @[0..n-1]@ in+--   the given the sequence emap.+enumerateSeqMap :: (Backend sym, Integral n) => n -> SeqMap sym a -> [SEval sym a]+enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]++-- | Create an infinite stream of all the values in a sequence map+streamSeqMap :: Backend sym => SeqMap sym a -> [SEval sym a]+streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]++-- | Reverse the order of a finite sequence map+reverseSeqMap :: Backend sym =>+  Integer {- ^ Size of the sequence map -} ->+  SeqMap sym a ->+  SeqMap sym a+reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)++updateSeqMap :: SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a+updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm+updateSeqMap xs i x = UpdateSeqMap (Map.singleton i x) xs++-- | Concatenate the first @n@ values of the first sequence map onto the+--   beginning of the second sequence map.+concatSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a -> SeqMap sym a+concatSeqMap n x y =+    IndexSeqMap $ \i ->+       if i < n+         then lookupSeqMap x i+         else lookupSeqMap y (i-n)++-- | Given a number @n@ and a sequence map, return two new sequence maps:+--   the first containing the values from @[0..n-1]@ and the next containing+--   the values from @n@ onward.+splitSeqMap :: Backend sym => Integer -> SeqMap sym a -> (SeqMap sym a, SeqMap sym a)+splitSeqMap n xs = (hd,tl)+  where+  hd = xs+  tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)++-- | Drop the first @n@ elements of the given 'SeqMap'.+dropSeqMap :: Backend sym => Integer -> SeqMap sym a -> SeqMap sym a+dropSeqMap 0 xs = xs+dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)++delaySeqMap :: Backend sym => sym -> SEval sym (SeqMap sym a) -> SEval sym (SeqMap sym a)+delaySeqMap sym xs =+  do xs' <- sDelay sym xs+     pure $ IndexSeqMap $ \i -> do m <- xs'; lookupSeqMap m i++-- | Given a sequence map, return a new sequence map that is memoized using+--   a finite map memo table.+memoMap :: Backend sym => sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)++-- Sequence is alreay memoized, just return it+memoMap _sym _sz x@(MemoSeqMap{}) = pure x++memoMap sym sz x = do+  stk <- sGetCallStack sym+  cache <- liftIO $ newIORef $ Map.empty+  evalRef <- liftIO $ newIORef $ eval stk+  return (MemoSeqMap sz cache evalRef)++  where+    eval stk i = sWithCallStack sym stk (lookupSeqMap x i)+++-- | Apply the given evaluation function pointwise to the two given+--   sequence maps.+zipSeqMap ::+  Backend sym =>+  sym ->+  (a -> a -> SEval sym a) ->+  Nat' ->+  SeqMap sym a ->+  SeqMap sym a ->+  SEval sym (SeqMap sym a)+zipSeqMap sym f sz x y =+  memoMap sym sz (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))++-- | Apply the given function to each value in the given sequence map+mapSeqMap ::+  Backend sym =>+  sym ->+  (a -> SEval sym a) ->+  Nat' ->+  SeqMap sym a ->+  SEval sym (SeqMap sym a)+mapSeqMap sym f sz x =+  memoMap sym sz (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)+++{-# INLINE mergeSeqMap #-}+mergeSeqMap :: Backend sym =>+  sym ->+  (SBit sym -> a -> a -> SEval sym a) ->+  SBit sym ->+  SeqMap sym a ->+  SeqMap sym a ->+  SeqMap sym a+mergeSeqMap sym f c x y =+  IndexSeqMap $ \i -> mergeEval sym f c (lookupSeqMap x i) (lookupSeqMap y i)+++{-# INLINE shiftSeqByInteger #-}+shiftSeqByInteger :: Backend sym =>+  sym ->+  (SBit sym -> a -> a -> SEval sym a)+     {- ^ if/then/else operation of values -} ->+  (Integer -> Integer -> Maybe Integer)+     {- ^ reindexing operation -} ->+  SEval sym a {- ^ zero value -} ->+  Nat' {- ^ size of the sequence -} ->+  SeqMap sym a {- ^ sequence to shift -} ->+  SInteger sym {- ^ shift amount, assumed to be in range [0,len] -} ->+  SEval sym (SeqMap sym a)+shiftSeqByInteger sym merge reindex zro m xs idx+  | Just j <- integerAsLit sym idx = shiftOp xs j+  | otherwise =+      do (n, idx_bits) <- enumerateIntBits sym m idx+         barrelShifter sym merge shiftOp m xs n (map BitIndexSegment idx_bits)+ where+   shiftOp vs shft =+     pure $ indexSeqMap $ \i ->+       case reindex i shft of+         Nothing -> zro+         Just i' -> lookupSeqMap vs i'+++data IndexSegment sym+  = BitIndexSegment (SBit sym)+  | WordIndexSegment (SWord sym)++{-# SPECIALIZE+  barrelShifter ::+  Concrete ->+  (SBit Concrete -> a -> a -> SEval Concrete a) ->+  (SeqMap Concrete a -> Integer -> SEval Concrete (SeqMap Concrete a)) ->+  Nat' ->+  SeqMap Concrete a ->+  Integer ->+  [IndexSegment Concrete] ->+  SEval Concrete (SeqMap Concrete a)+ #-}+barrelShifter :: Backend sym =>+  sym ->+  (SBit sym -> a -> a -> SEval sym a)+     {- ^ if/then/else operation of values -} ->+  (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))+     {- ^ concrete shifting operation -} ->+  Nat' {- ^ Size of the map being shifted -} ->+  SeqMap sym a {- ^ initial value -} ->+  Integer {- Number of bits in shift amount -} ->+  [IndexSegment sym]  {- ^ segments of the shift amount, in big-endian order -} ->+  SEval sym (SeqMap sym a)+barrelShifter sym mux shift_op sz x0 n0 bs0+  | n0 >= toInteger (maxBound :: Int) =+      liftIO (X.throw (UnsupportedSymbolicOp ("Barrel shifter with too many bits in shift amount: " ++ show n0)))+  | otherwise = go x0 (fromInteger n0) bs0++  where+  go x !_n [] = return x++  go x !n (WordIndexSegment w:bs) =+    let n' = n - fromInteger (wordLen sym w) in+    case wordAsLit sym w of+      Just (_,0) -> go x n' bs+      Just (_,j) ->+        do x_shft <- shift_op x (j * bit n')+           go x_shft n' bs+      Nothing ->+        do wbs <- unpackWord sym w+           go x n (map BitIndexSegment wbs ++ bs)++  go x !n (BitIndexSegment b:bs) =+    let n' = n - 1 in+    case bitAsLit sym b of+      Just False -> go x n' bs+      Just True ->+        do x_shft <- shift_op x (bit n')+           go x_shft n' bs+      Nothing ->+        do x_shft <- shift_op x (bit n')+           x' <- memoMap sym sz (mergeSeqMap sym mux b x_shft x)+           go x' n' bs

@@ -39,7 +39,7 @@ import Cryptol.Backend.Monad    ( Eval(..), EvalError(..), EvalErrorEx(..)    , Unsupported(..), delayFill, blackhole, evalSpark-   , modifyCallStack, getCallStack+   , modifyCallStack, getCallStack, maybeReady    ) import Cryptol.Utils.Panic @@ -76,7 +76,7 @@   | W4Result !(W4.Pred sym) !a     -- ^ safety predicate and result: the result only makes sense when     -- the predicate holds.-+ deriving Functor  -------------------------------------------------------------------------------- -- Moving between the layers@@ -215,10 +215,10 @@     | Just False <- W4.asConstantPred cond = evalError err     | otherwise = addSafety cond -  isReady sym m =-    case w4Eval m (w4 sym) of-      Ready _ -> True-      _ -> False+  isReady sym m = W4Eval $ W4Conn $ \_ ->+    maybeReady (w4Eval m (w4 sym)) >>= \case+      Just x  -> pure (Just <$> x)+      Nothing -> pure (W4Result (W4.backendPred (w4 sym) True) Nothing)    sDelayFill _ m retry msg =     total@@ -342,6 +342,12 @@   wordNegate sym x   = liftIO (SW.bvNeg (w4 sym) x)   wordLg2    sym x   = sLg2 (w4 sym) x  +  wordShiftLeft   sym x y = w4bvShl (w4 sym) x y+  wordShiftRight  sym x y = w4bvLshr (w4 sym) x y+  wordRotateLeft  sym x y = w4bvRol (w4 sym) x y+  wordRotateRight sym x y = w4bvRor (w4 sym) x y+  wordSignedShiftRight sym x y = w4bvAshr (w4 sym) x y+   wordDiv sym x y =      do assertBVDivisor sym y         liftIO (SW.bvUDiv (w4 sym) x y)@@ -356,6 +362,7 @@         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

@@ -0,0 +1,759 @@+-- |+-- Module      :  Cryptol.Backend.WordValue+-- Copyright   :  (c) 2013-2021 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DoAndIfThenElse #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}++module Cryptol.Backend.WordValue+  ( -- * WordValue+    WordValue+  , wordVal+  , bitmapWordVal+  , asWordList+  , asWordVal+  , asBitsMap+  , joinWordVal+  , takeWordVal+  , dropWordVal+  , extractWordVal+  , wordValLogicOp+  , wordValUnaryOp+  , assertWordValueInBounds+  , enumerateWordValue+  , enumerateWordValueRev+  , enumerateIndexSegments+  , wordValueSize+  , indexWordValue+  , updateWordValue+  , delayWordValue+  , joinWords+  , shiftSeqByWord+  , shiftWordByInteger+  , shiftWordByWord+  , wordValAsLit+  , reverseWordVal+  , forceWordValue+  , wordValueEqualsInteger+  , updateWordByWord++  , mergeWord+  , mergeWord'+  ) where++import Control.Monad (unless)+import Data.Bits+import GHC.Generics (Generic)++import Cryptol.Backend+import Cryptol.Backend.Concrete (Concrete(..))+import Cryptol.Backend.Monad (EvalError(..))+import Cryptol.Backend.SeqMap++import Cryptol.TypeCheck.Solver.InfNat(widthInteger, Nat'(..))++-- | Force the evaluation of a word value+forceWordValue :: Backend sym => WordValue sym -> SEval sym ()+forceWordValue (WordVal w)  = seq w (return ())+forceWordValue (ThunkWordVal _ m)  = forceWordValue =<< m+forceWordValue (BitmapVal _n packed _) = do w <- packed; seq w (return ())++-- | An arbitrarily-chosen number of elements where we switch from a dense+--   sequence representation of bit-level words to 'SeqMap' representation.+largeBitSize :: Integer+largeBitSize = bit 32++-- | For efficiency reasons, we handle finite sequences of bits as special cases+--   in the evaluator.  In cases where we know it is safe to do so, we prefer to+--   used a "packed word" representation of bit sequences.  This allows us to rely+--   directly on Integer types (in the concrete evaluator) and SBV's Word types (in+--   the symbolic simulator).+--+--   However, if we cannot be sure all the bits of the sequence+--   will eventually be forced, we must instead rely on an explicit sequence of bits+--   representation.+data WordValue sym+  = ThunkWordVal Integer !(SEval sym (WordValue sym))+  | WordVal !(SWord sym)                      -- ^ Packed word representation for bit sequences.+  | BitmapVal+       !Integer -- ^ Length of the word+       !(SEval sym (SWord sym)) -- ^ Thunk for packing the word+       !(SeqMap sym (SBit sym)) -- ^+ deriving (Generic)++wordVal :: SWord sym -> WordValue sym+wordVal = WordVal++packBitmap :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (SWord sym)+packBitmap sym sz bs = packWord sym =<< sequence (enumerateSeqMap sz bs)++unpackBitmap :: Backend sym => sym -> SWord sym -> SeqMap sym (SBit sym)+unpackBitmap sym w = indexSeqMap $ \i -> wordBit sym w i++bitmapWordVal :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)+bitmapWordVal sym sz bs =+  do packed <- sDelay sym (packBitmap sym sz bs)+     pure (BitmapVal sz packed bs)++{-# INLINE joinWordVal #-}+joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)+joinWordVal sym wv1 wv2 =+  let fallback = fallbackWordJoin sym wv1 wv2 in+  case (wv1, wv2) of+    (WordVal w1, WordVal w2) ->+      WordVal <$> joinWord sym w1 w2++    (ThunkWordVal _ m1, _) ->+      isReady sym m1 >>= \case+        Just x -> joinWordVal sym x wv2+        Nothing -> fallback++    (_,ThunkWordVal _ m2) ->+      isReady sym m2 >>= \case+        Just x   -> joinWordVal sym wv1 x+        Nothing  -> fallback++    (WordVal w1, BitmapVal _ packed2 _) ->+      isReady sym packed2 >>= \case+        Just w2 -> WordVal <$> joinWord sym w1 w2+        Nothing  -> fallback++    (BitmapVal _ packed1 _, WordVal w2) ->+      isReady sym packed1 >>= \case+        Just w1 -> WordVal <$> joinWord sym w1 w2+        Nothing -> fallback++    (BitmapVal _ packed1 _, BitmapVal _ packed2 _) ->+      do r1 <- isReady sym packed1+         r2 <- isReady sym packed2+         case (r1,r2) of+           (Just w1, Just w2) -> WordVal <$> joinWord sym w1 w2+           _ -> fallback++{-# INLINE fallbackWordJoin #-}+fallbackWordJoin :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)+fallbackWordJoin sym w1 w2 =+  do let n1 = wordValueSize sym w1+     let n2 = wordValueSize sym w2+     let len = n1 + n2+     packed <- sDelay sym+                 (do a <- asWordVal sym w1+                     b <- asWordVal sym w2+                     joinWord sym a b)+     let bs = concatSeqMap n1 (asBitsMap sym w1) (asBitsMap sym w2)+     pure (BitmapVal len packed bs)+++{-# INLINE takeWordVal #-}+takeWordVal ::+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  WordValue sym ->+  SEval sym (WordValue sym)+takeWordVal sym leftWidth rigthWidth (WordVal w) =+  do (lw, _rw) <- splitWord sym leftWidth rigthWidth w+     pure (WordVal lw)++takeWordVal sym leftWidth rightWidth (ThunkWordVal _ m) =+  isReady sym m >>= \case+    Just w -> takeWordVal sym leftWidth rightWidth w+    Nothing ->+      do m' <- sDelay sym (takeWordVal sym leftWidth rightWidth =<< m)+         return (ThunkWordVal leftWidth m')++takeWordVal sym leftWidth rightWidth (BitmapVal _n packed xs) =+  isReady sym packed >>= \case+    Just w -> do (lw, _rw) <- splitWord sym leftWidth rightWidth w+                 pure (WordVal lw)+    Nothing -> bitmapWordVal sym leftWidth xs++{-# INLINE dropWordVal #-}+dropWordVal ::+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  WordValue sym ->+  SEval sym (WordValue sym)+dropWordVal sym leftWidth rigthWidth (WordVal w) =+  do (_lw, rw) <- splitWord sym leftWidth rigthWidth w+     pure (WordVal rw)++dropWordVal sym leftWidth rightWidth (ThunkWordVal _ m) =+  isReady sym m >>= \case+    Just w -> dropWordVal sym leftWidth rightWidth w+    Nothing ->+      do m' <- sDelay sym (dropWordVal sym leftWidth rightWidth =<< m)+         return (ThunkWordVal rightWidth m')++dropWordVal sym leftWidth rightWidth (BitmapVal _n packed xs) =+  isReady sym packed >>= \case+    Just w -> do (_lw, rw) <- splitWord sym leftWidth rightWidth w+                 pure (WordVal rw)+    Nothing ->+      do let rxs = dropSeqMap leftWidth xs+         bitmapWordVal sym rightWidth rxs++{-# INLINE extractWordVal #-}++-- | Extract a subsequence of bits from a @WordValue@.+--   The first integer argument is the number of bits in the+--   resulting word.  The second integer argument is the+--   number of less-significant digits to discard.  Stated another+--   way, the operation `extractWordVal n i w` is equivalent to+--   first shifting `w` right by `i` bits, and then truncating to+--   `n` bits.+extractWordVal ::+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  WordValue sym ->+  SEval sym (WordValue sym)+extractWordVal sym len start (WordVal w) =+   WordVal <$> extractWord sym len start w+extractWordVal sym len start (ThunkWordVal _n m) =+  isReady sym m >>= \case+    Just w -> extractWordVal sym len start w+    Nothing ->+      do m' <- sDelay sym (extractWordVal sym len start =<< m)+         pure (ThunkWordVal len m')+extractWordVal sym len start (BitmapVal n packed xs) =+  isReady sym packed >>= \case+    Just w -> WordVal <$> extractWord sym len start w+    Nothing ->+      do let xs' = dropSeqMap (n - start - len) xs+         bitmapWordVal sym len xs'++{-# INLINE wordValLogicOp #-}++wordValLogicOp ::+  Backend sym =>+  sym ->+  (SBit sym -> SBit sym -> SEval sym (SBit sym)) ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->+  WordValue sym ->+  WordValue sym ->+  SEval sym (WordValue sym)+wordValLogicOp _sym _ wop (WordVal w1) (WordVal w2) = WordVal <$> wop w1 w2++wordValLogicOp sym bop wop (WordVal w1) (BitmapVal n2 packed2 bs2) =+  isReady sym packed2 >>= \case+    Just w2 -> WordVal <$> wop w1 w2+    Nothing -> bitmapWordVal sym n2 =<< zipSeqMap sym bop (Nat n2) (unpackBitmap sym w1) bs2++wordValLogicOp sym bop wop (BitmapVal n1 packed1 bs1) (WordVal w2) =+  isReady sym packed1 >>= \case+    Just w1 -> WordVal <$> wop w1 w2+    Nothing -> bitmapWordVal sym n1 =<< zipSeqMap sym bop (Nat n1) bs1 (unpackBitmap sym w2)++wordValLogicOp sym bop wop (BitmapVal n1 packed1 bs1) (BitmapVal _n2 packed2 bs2) =+  do r1 <- isReady sym packed1+     r2 <- isReady sym packed2+     case (r1,r2) of+       (Just w1, Just w2) -> WordVal <$> wop w1 w2+       _ -> bitmapWordVal sym n1 =<< zipSeqMap sym bop (Nat n1) bs1 bs2++wordValLogicOp sym bop wop (ThunkWordVal _ m1) w2 =+  do w1 <- m1+     wordValLogicOp sym bop wop w1 w2++wordValLogicOp sym bop wop w1 (ThunkWordVal _ m2) =+  do w2 <- m2+     wordValLogicOp sym bop wop w1 w2++{-# INLINE wordValUnaryOp #-}+wordValUnaryOp ::+  Backend sym =>+  sym ->+  (SBit sym -> SEval sym (SBit sym)) ->+  (SWord sym -> SEval sym (SWord sym)) ->+  WordValue sym ->+  SEval sym (WordValue sym)+wordValUnaryOp _ _ wop (WordVal w)  = WordVal <$> wop w+wordValUnaryOp sym bop wop (ThunkWordVal _ m) = wordValUnaryOp sym bop wop =<< m+wordValUnaryOp sym bop wop (BitmapVal n packed xs) =+  isReady sym packed >>= \case+    Just w  -> WordVal <$> wop w+    Nothing -> bitmapWordVal sym n =<< mapSeqMap sym bop (Nat n) xs++{-# SPECIALIZE joinWords ::+  Concrete ->+  Integer ->+  Integer ->+  SeqMap Concrete (WordValue Concrete)->+  SEval Concrete (WordValue Concrete)+  #-}+joinWords :: forall sym.+  Backend sym =>+  sym ->+  Integer ->+  Integer ->+  SeqMap sym (WordValue sym) ->+  SEval sym (WordValue sym)++-- small enough to pack+joinWords sym nParts nEach xs | nParts * nEach < largeBitSize =+  do z <- wordLit sym 0 0+     loop (wordVal z) (enumerateSeqMap nParts xs)++ where+ loop :: WordValue sym -> [SEval sym (WordValue sym)] -> SEval sym (WordValue sym)+ loop !wv [] = pure wv+ loop !wv (w : ws) =+    do w'  <- delayWordValue sym nEach w+       wv' <- joinWordVal sym wv w'+       loop wv' ws++-- too large to pack+joinWords sym nParts nEach xs = bitmapWordVal sym (nParts * nEach) zs+  where+    zs = indexSeqMap $ \i ->+            do let (q,r) = divMod i nEach+               ys <- lookupSeqMap xs q+               indexWordValue sym ys r++reverseWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (WordValue sym)+reverseWordVal sym w =+  let m = wordValueSize sym w in+  bitmapWordVal sym m <$> reverseSeqMap m $ asBitsMap sym w++wordValAsLit :: Backend sym => sym -> WordValue sym -> SEval sym (Maybe Integer)+wordValAsLit sym (WordVal w) = pure (snd <$> wordAsLit sym w)+wordValAsLit sym (ThunkWordVal _ m) =+  isReady sym m >>= \case+    Just v  -> wordValAsLit sym v+    Nothing -> pure Nothing+wordValAsLit sym (BitmapVal _ packed _) =+  isReady sym packed >>= \case+    Just w  -> pure (snd <$> wordAsLit sym w)+    Nothing -> pure Nothing++-- | Force a word value into packed word form+asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)+asWordVal _   (WordVal w)            = return w+asWordVal sym (ThunkWordVal _ m)     = asWordVal sym =<< m+asWordVal _   (BitmapVal _ packed _) = packed++wordValueEqualsInteger :: forall sym. Backend sym =>+  sym ->+  WordValue sym ->+  Integer ->+  SEval sym (SBit sym)+wordValueEqualsInteger sym wv i+  | wordValueSize sym wv < widthInteger i = return (bitLit sym False)+  | otherwise = loop wv++ where+   loop (ThunkWordVal _ m) = loop =<< m+   loop (WordVal w) = wordEq sym w =<< wordLit sym (wordLen sym w) i+   loop (BitmapVal n packed bs) =+     isReady sym packed >>= \case+       Just w  -> loop (WordVal w)+       Nothing -> bitsAre i =<< sequence (enumerateSeqMap n (reverseSeqMap n bs))++   -- NB little-endian sequence of bits+   bitsAre :: Integer -> [SBit sym] -> SEval sym (SBit sym)+   bitsAre !n [] = return (bitLit sym (n == 0))+   bitsAre !n (b:bs) =+     do pb  <- bitIs (testBit n 0) b+        pbs <- bitsAre (n `shiftR` 1) bs+        bitAnd sym pb pbs++   bitIs :: Bool -> SBit sym -> SEval sym (SBit sym)+   bitIs b x = if b then pure x else bitComplement sym x++asWordList :: forall sym. Backend sym => sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])+asWordList sym = loop id+ where+   loop :: ([SWord sym] -> [SWord sym]) -> [WordValue sym] -> SEval sym (Maybe [SWord sym])+   loop f [] = pure (Just (f []))+   loop f (WordVal x : vs) = loop (f . (x:)) vs+   loop f (ThunkWordVal _ m : vs) =+     isReady sym m >>= \case+       Just m' -> loop f (m' : vs)+       Nothing -> pure Nothing+   loop f (BitmapVal _ packed _ : vs) =+     isReady sym packed >>= \case+       Just x -> loop (f . (x:)) vs+       Nothing -> pure Nothing++-- | Force a word value into a sequence of bits+asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (SBit sym)+asBitsMap _   (BitmapVal _ _ xs)  = xs+asBitsMap sym (WordVal w)         = indexSeqMap $ \i -> wordBit sym w i+asBitsMap sym (ThunkWordVal _ m)  =+  indexSeqMap $ \i ->+    do mp <- asBitsMap sym <$> (unwindThunks m)+       lookupSeqMap mp i++-- | Turn a word value into a sequence of bits, forcing each bit.+--   The sequence is returned in big-endian order.+enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]+enumerateWordValue sym (WordVal w) = unpackWord sym w+enumerateWordValue sym (ThunkWordVal _ m) = enumerateWordValue sym =<< m+  -- TODO? used the packed value if it is ready?+enumerateWordValue _ (BitmapVal n _ xs) = sequence (enumerateSeqMap n xs)++-- | Turn a word value into a sequence of bits, forcing each bit.+--   The sequence is returned in reverse of the usual order, which is little-endian order.+enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]+enumerateWordValueRev sym (WordVal w)  = reverse <$> unpackWord sym w+enumerateWordValueRev sym (ThunkWordVal _ m)  = enumerateWordValueRev sym =<< m+  -- TODO? used the packed value if it is ready?+enumerateWordValueRev _   (BitmapVal n _ xs) = sequence (enumerateSeqMap n (reverseSeqMap n xs))+++enumerateIndexSegments :: Backend sym => sym -> WordValue sym -> SEval sym [IndexSegment sym]+enumerateIndexSegments _sym (WordVal w) = pure [WordIndexSegment w]+enumerateIndexSegments sym (ThunkWordVal _ m) = enumerateIndexSegments sym =<< m+enumerateIndexSegments sym (BitmapVal n packed xs) =+  isReady sym packed >>= \case+    Just w  -> pure [WordIndexSegment w]+    Nothing -> traverse (BitIndexSegment <$>) (enumerateSeqMap n xs)++{-# SPECIALIZE bitsValueLessThan ::+  Concrete ->+  Integer ->+  [SBit Concrete] ->+  Integer ->+  SEval Concrete (SBit Concrete)+  #-}+bitsValueLessThan ::+  Backend sym =>+  sym ->+  Integer {- ^ bit-width -} ->+  [SBit sym] {- ^ big-endian list of index bits -} ->+  Integer {- ^ Upper bound to test against -} ->+  SEval sym (SBit sym)+bitsValueLessThan sym _w [] _n = pure $ bitLit sym False+bitsValueLessThan sym w (b:bs) n+  | nbit =+      do notb <- bitComplement sym b+         bitOr sym notb =<< bitsValueLessThan sym (w-1) bs n+  | otherwise =+      do notb <- bitComplement sym b+         bitAnd sym notb =<< bitsValueLessThan sym (w-1) bs n+ where+ nbit = testBit n (fromInteger (w-1))+++assertWordValueInBounds ::+  Backend sym => sym -> Integer -> WordValue sym -> SEval sym ()++-- Can't index out of bounds for a sequence that is+-- longer than the expressible index values+assertWordValueInBounds sym n idx+  | n >= 2^(wordValueSize sym idx)+  = return ()++assertWordValueInBounds sym n (WordVal idx)+  | Just (_w,i) <- wordAsLit sym idx+  = unless (i < n) (raiseError sym (InvalidIndex (Just i)))++-- If the index is a packed word, test that it+-- is less than the concrete value of n, which+-- fits into w bits because of the above test.+assertWordValueInBounds sym n (WordVal idx) =+  do n' <- wordLit sym (wordLen sym idx) n+     p <- wordLessThan sym idx n'+     assertSideCondition sym p (InvalidIndex Nothing)++-- Force thunks+assertWordValueInBounds sym n (ThunkWordVal _ m) =+  assertWordValueInBounds sym n =<< m++-- If the index is an unpacked word, force all the bits+-- and compute the unsigned less-than test directly.+assertWordValueInBounds sym n (BitmapVal sz packed bits) =+  isReady sym packed >>= \case+    Just w -> assertWordValueInBounds sym n (WordVal w)+    Nothing ->+      do bitsList <- sequence (enumerateSeqMap sz bits)+         p <- bitsValueLessThan sym sz bitsList n+         assertSideCondition sym p (InvalidIndex Nothing)++delayWordValue :: Backend sym => sym -> Integer -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)+delayWordValue sym sz m =+  isReady sym m >>= \case+    Just w  -> pure w+    Nothing -> ThunkWordVal sz <$> sDelay sym (unwindThunks m)++-- If we are calling this, we know the spine of the word value has been+-- demanded, so we unwind any chains of `ThunkWordValue` that may have built up.+unwindThunks :: Backend sym => SEval sym (WordValue sym) -> SEval sym (WordValue sym)+unwindThunks m =+  m >>= \case+    ThunkWordVal _ m' -> unwindThunks m'+    x -> pure x++{-# INLINE shiftWordByInteger #-}+shiftWordByInteger ::+  Backend sym =>+  sym ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym)) +    {- ^ operation on word values -} ->+  (Integer -> Integer -> Maybe Integer)+    {- ^ reindexing operation -} ->+  WordValue sym {- ^ word value to shift -} ->+  SInteger sym {- ^ shift amount, assumed to be in range [0,len] -} ->+  SEval sym (WordValue sym)++shiftWordByInteger sym wop reindex x idx =+  case x of+    ThunkWordVal w wm ->+      isReady sym wm >>= \case+        Just x' -> shiftWordByInteger sym wop reindex x' idx+        Nothing ->+         do m' <- sDelay sym+                     (do x' <- wm+                         shiftWordByInteger sym wop reindex x' idx)+            return (ThunkWordVal w m')++    WordVal x' -> WordVal <$> (wop x' =<< wordFromInt sym (wordLen sym x') idx)++    BitmapVal n packed bs0 ->+      isReady sym packed >>= \case+        Just w -> shiftWordByInteger sym wop reindex (WordVal w) idx+        Nothing ->+          bitmapWordVal sym n =<<+            shiftSeqByInteger sym (iteBit sym) reindex (pure (bitLit sym False)) (Nat n) bs0 idx+++{-# INLINE shiftWordByWord #-}+shiftWordByWord ::+  Backend sym =>+  sym ->+  (SWord sym -> SWord sym -> SEval sym (SWord sym))+    {- ^ operation on word values -} ->+  (Integer -> Integer -> Maybe Integer)+    {- ^ reindexing operation -} ->+  WordValue sym {- ^ value to shift -} ->+  WordValue sym {- ^ amount to shift -} ->+  SEval sym (WordValue sym)+shiftWordByWord sym wop reindex x idx =+  case x of+    ThunkWordVal w wm ->+      isReady sym wm >>= \case+        Just wm' -> shiftWordByWord sym wop reindex wm' idx+        Nothing ->+         do m' <- sDelay sym (do wm' <- wm+                                 shiftWordByWord sym wop reindex wm' idx)+            return (ThunkWordVal w m')++    WordVal x' -> WordVal <$> (wop x' =<< asWordVal sym idx)++    BitmapVal n packed bs0 ->+      isReady sym packed >>= \case+        Just w -> shiftWordByWord sym wop reindex (WordVal w) idx+        Nothing ->+          bitmapWordVal sym n =<<+            shiftSeqByWord sym (iteBit sym) reindex (pure (bitLit sym False)) (Nat n) bs0 idx+++{-# INLINE updateWordByWord #-}+updateWordByWord ::+  Backend sym =>+  sym ->+  IndexDirection ->+  WordValue sym {- ^ value to update -} ->+  WordValue sym {- ^ index to update at -} ->+  SEval sym (SBit sym) {- ^ fresh bit -} ->+  SEval sym (WordValue sym)+updateWordByWord sym dir w0 idx bitval =+  wordValAsLit sym idx >>= \case+    Just j ->+      let sz = wordValueSize sym w0 in+      case dir of+        IndexForward  -> updateWordValue sym w0 j bitval+        IndexBackward -> updateWordValue sym w0 (sz - j - 1) bitval+    Nothing -> loop w0++ where+   loop (ThunkWordVal sz m) =+     isReady sym m >>= \case+       Just w' -> loop w'+       Nothing -> delayWordValue sym sz (loop =<< m)++   loop (BitmapVal sz packed bs) =+     isReady sym packed >>= \case+       Just w -> loop (WordVal w)+       Nothing ->+         case dir of+           IndexForward ->+             bitmapWordVal sym sz $ indexSeqMap $ \i ->+               do b <- wordValueEqualsInteger sym idx i+                  mergeEval sym (iteBit sym) b bitval (lookupSeqMap bs i)+           IndexBackward ->+             bitmapWordVal sym sz $ indexSeqMap $ \i ->+               do b <- wordValueEqualsInteger sym idx (sz - i - 1)+                  mergeEval sym (iteBit sym) b bitval (lookupSeqMap bs i)++   loop (WordVal wv) = WordVal <$>+      -- TODO, this is too strict in bit+      do let sz = wordLen sym wv+         b <- bitval+         msk <- case dir of+                  IndexForward ->+                    do highbit <- wordLit sym sz (bit (fromInteger (sz-1)))+                       wordShiftRight sym highbit =<< asWordVal sym idx+                  IndexBackward ->+                    do lowbit <- wordLit sym sz 1+                       wordShiftLeft sym lowbit =<< asWordVal sym idx+         case bitAsLit sym b of+           Just True  -> wordOr  sym wv msk+           Just False -> wordAnd sym wv =<< wordComplement sym msk+           Nothing ->+             do zro <- wordLit sym sz 0+                one <- wordComplement sym zro+                q   <- iteWord sym b one zro+                w'  <- wordAnd sym wv =<< wordComplement sym msk+                wordXor sym w' =<< wordAnd sym msk q+++{-# INLINE shiftSeqByWord #-}+shiftSeqByWord  ::+  Backend sym =>+  sym ->+  (SBit sym -> a -> a -> SEval sym a)+     {- ^ if/then/else operation of values -} ->+  (Integer -> Integer -> Maybe Integer)+     {- ^ reindexing operation -} ->+  SEval sym a  {- ^ zero value -} ->+  Nat' {- ^ size of the sequence -} ->+  SeqMap sym a {- ^ sequence to shift -} ->+  WordValue sym {- ^ shift amount -} ->+  SEval sym (SeqMap sym a)+shiftSeqByWord sym merge reindex zro sz xs idx =+  wordValAsLit sym idx >>= \case+    Just j -> shiftOp xs j+    Nothing ->+      do idx_segs <- enumerateIndexSegments sym idx+         barrelShifter sym merge shiftOp sz xs idx_bits idx_segs+  where+   idx_bits = wordValueSize sym idx++   shiftOp vs shft =+     pure $ indexSeqMap $ \i ->+       case reindex i shft of+         Nothing -> zro+         Just i' -> lookupSeqMap vs i'++-- | Compute the size of a word value+-- TODO, can we get rid of this? If feels like it should be+--  unnecessary.+wordValueSize :: Backend sym => sym -> WordValue sym -> Integer+wordValueSize sym (WordVal w)  = wordLen sym w+wordValueSize _ (ThunkWordVal n _) = n+wordValueSize _ (BitmapVal n _ _) = n++-- | Select an individual bit from a word value+indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)+indexWordValue sym (ThunkWordVal _ m) idx = do m' <- m ; indexWordValue sym m' idx+indexWordValue sym (WordVal w) idx+   | 0 <= idx && idx < wordLen sym w = wordBit sym w idx+   | otherwise = invalidIndex sym idx+indexWordValue sym (BitmapVal n _packed xs) idx+   | 0 <= idx && idx < n = lookupSeqMap xs idx+   | otherwise = invalidIndex sym idx++-- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the+--   given bit value.+updateWordValue :: Backend sym =>+  sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)+updateWordValue sym wv0 idx b = loop wv0+  where+    loop (ThunkWordVal sz m) =+      isReady sym m >>= \case+        Just w  -> loop w+        Nothing -> delayWordValue sym sz (loop =<< m)++    loop (WordVal w)+      | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx+      | otherwise =+          isReady sym b >>= \case+            Just b' -> WordVal <$> wordUpdate sym w idx b'+            Nothing ->+              do let bs = unpackBitmap sym w+                 bitmapWordVal sym (wordLen sym w) $ updateSeqMap bs idx b++    loop (BitmapVal sz packed bs)+      | 0 <= idx && idx < sz =+          isReady sym packed >>= \case+            Just w  -> loop (WordVal w)+            Nothing -> bitmapWordVal sym sz $ updateSeqMap bs idx b+      | otherwise = invalidIndex sym idx++{-# INLINE mergeWord #-}+mergeWord :: Backend sym =>+  sym ->+  SBit sym ->+  WordValue sym ->+  WordValue sym ->+  SEval sym (WordValue sym)+mergeWord sym c (ThunkWordVal _ m1) (ThunkWordVal _ m2) =+  mergeWord' sym c (unwindThunks m1) (unwindThunks m2)+mergeWord sym c (ThunkWordVal _ m1) w2 =+  mergeWord' sym c (unwindThunks m1) (pure w2)+mergeWord sym c w1 (ThunkWordVal _ m2) =+  mergeWord' sym c (pure w1) (unwindThunks m2)++mergeWord sym c (WordVal w1) (WordVal w2) =+  WordVal <$> iteWord sym c w1 w2++mergeWord sym c (BitmapVal n1 packed1 bs1) (WordVal w2) =+  isReady sym packed1 >>= \case+    Just w1 -> WordVal <$> iteWord sym c w1 w2+    Nothing -> mergeBitmaps sym c n1 bs1 (unpackBitmap sym w2)++mergeWord sym c (WordVal w1) (BitmapVal n2 packed2 bs2) =+  isReady sym packed2 >>= \case+    Just w2 -> WordVal <$> iteWord sym c w1 w2+    Nothing -> mergeBitmaps sym c n2 (unpackBitmap sym w1) bs2++mergeWord sym c (BitmapVal n1 packed1 bs1) (BitmapVal _n2 packed2 bs2) =+  do r1 <- isReady sym packed1+     r2 <- isReady sym packed2+     case (r1,r2) of+       (Just w1, Just w2) -> WordVal <$> iteWord sym c w1 w2+       _ -> mergeBitmaps sym c n1 bs1 bs2++mergeBitmaps :: Backend sym =>+  sym ->+  SBit sym ->+  Integer ->+  SeqMap sym (SBit sym) ->+  SeqMap sym (SBit sym) ->+  SEval sym (WordValue sym)+mergeBitmaps sym c sz bs1 bs2 =+  do bs <- memoMap sym (Nat sz) (mergeSeqMap sym (iteBit sym) c bs1 bs2)+     bitmapWordVal sym sz bs++{-# INLINE mergeWord' #-}+mergeWord' :: Backend sym =>+  sym ->+  SBit sym ->+  SEval sym (WordValue sym) ->+  SEval sym (WordValue sym) ->+  SEval sym (WordValue sym)+mergeWord' sym c x y+  | Just b <- bitAsLit sym c = if b then x else y+  | otherwise = mergeEval sym (mergeWord sym) c x y

@@ -40,7 +40,9 @@ import Cryptol.Backend import Cryptol.Backend.Concrete( Concrete(..) ) import Cryptol.Backend.Monad-import Cryptol.Eval.Generic ( iteValue )+import Cryptol.Backend.SeqMap+import Cryptol.Backend.WordValue+ import Cryptol.Eval.Env import Cryptol.Eval.Prims import Cryptol.Eval.Type@@ -122,14 +124,14 @@     -- NB, even if the list cannot be packed, we must use `VWord`     -- when the element type is `Bit`.     | isTBit tyv -> {-# SCC "evalExpr->Elist/bit" #-}-        return $ VWord len $-          case tryFromBits sym vs of-            Just w  -> WordVal <$> w-            Nothing -> do xs <- mapM (sDelay sym) vs-                          return $ LargeBitsVal len $ finiteSeqMap xs+        VWord len <$>+          (tryFromBits sym vs >>= \case+             Just w  -> pure (wordVal w)+             Nothing -> do xs <- mapM (\x -> sDelay sym (fromVBit <$> x)) vs+                           bitmapWordVal sym len $ finiteSeqMap sym xs)     | otherwise -> {-# SCC "evalExpr->EList" #-} do         xs <- mapM (sDelay sym) vs-        return $ VSeq len $ finiteSeqMap xs+        return $ VSeq len $ finiteSeqMap sym xs    where     tyv = evalValType (envTypes env) ty     vs  = map eval es@@ -362,186 +364,12 @@   GenEvalEnv sym ->   (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) ->   SEval sym ()-fillHole sym env (nm, sch, _, fill) = do+fillHole _sym env (nm, _sch, _, fill) = do   case lookupVar nm env of-    Just (Right v)-     | isValueType env sch ->-               fill =<< sDelayFill sym v-                          (Just (etaDelay sym env sch v))-                          (show (ppLocName nm))--     | otherwise -> fill (etaDelay sym env sch v)-+    Just (Right v) -> fill v     _ -> evalPanic "fillHole" ["Recursive definition not completed", show (ppLocName nm)] --- | 'Value' types are non-polymorphic types recursive constructed from---   bits, finite sequences, tuples and records.  Types of this form can---   be implemented rather more efficiently than general types because we can---   rely on the 'delayFill' operation to build a thunk that falls back on performing---   eta-expansion rather than doing it eagerly.-isValueType :: GenEvalEnv sym -> Schema -> Bool-isValueType env Forall{ sVars = [], sProps = [], sType = t0 }-   = go (evalValType (envTypes env) t0)- where-  go TVBit = True-  go (TVSeq _ x)  = go x-  go (TVTuple xs) = and (map go xs)-  go (TVRec xs)   = and (fmap go xs)-  go (TVNewtype _ _ xs) = and (fmap go xs)-  go _            = False -isValueType _ _ = False---{-# SPECIALIZE etaWord  ::-  Concrete ->-  Integer ->-  SEval Concrete (GenValue Concrete) ->-  SEval Concrete (WordValue Concrete)-  #-}---- | Eta-expand a word value.  This forces an unpacked word representation.-etaWord  ::-  Backend sym =>-  sym ->-  Integer ->-  SEval sym (GenValue sym) ->-  SEval sym (WordValue sym)-etaWord sym n val = do-  w <- sDelay sym (fromWordVal "during eta-expansion" =<< val)-  xs <- memoMap sym $ IndexSeqMap $ \i ->-          do w' <- w; VBit <$> indexWordValue sym w' i-  pure $ LargeBitsVal n xs--{-# SPECIALIZE etaDelay ::-  Concrete ->-  GenEvalEnv Concrete ->-  Schema ->-  SEval Concrete (GenValue Concrete) ->-  SEval Concrete (GenValue Concrete)-  #-}---- | Given a simulator value and its type, fully eta-expand the value.  This---   is a type-directed pass that always produces a canonical value of the---   expected shape.  Eta expansion of values is sometimes necessary to ensure---   the correct evaluation semantics of recursive definitions.  Otherwise,---   expressions that should be expected to produce well-defined values in the---   denotational semantics will fail to terminate instead.-etaDelay ::-  Backend sym =>-  sym ->-  GenEvalEnv sym ->-  Schema ->-  SEval sym (GenValue sym) ->-  SEval sym (GenValue sym)-etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0-  where-  goTpVars env []     val =-     do stk <- sGetCallStack sym-        go stk (evalValType (envTypes env) tp0) val-  goTpVars env (v:vs) val =-    case tpKind v of-      KType -> tlam sym $ \t ->-                  goTpVars (bindType (tpVar v) (Right t) env) vs ( ($t) . fromVPoly sym =<< val )-      KNum  -> nlam sym $ \n ->-                  goTpVars (bindType (tpVar v) (Left n) env) vs ( ($n) . fromVNumPoly sym =<< val )-      k     -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k]--  go stk tp x | isReady sym x = x >>= \case-      VBit{}      -> x-      VInteger{}  -> x-      VWord{}     -> x-      VRational{} -> x-      VFloat{}    -> x-      VSeq n xs ->-        case tp of-          TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go stk el (lookupSeqMap xs i)-          _ -> evalPanic "type mismatch during eta-expansion" ["Expected sequence type, but got " ++ show tp]--      VStream xs ->-        case tp of-          TVStream el -> return $ VStream $ IndexSeqMap $ \i -> go stk el (lookupSeqMap xs i)-          _ -> evalPanic "type mismatch during eta-expansion" ["Expected stream type, but got " ++ show tp]--      VTuple xs ->-        case tp of-          TVTuple ts | length ts == length xs -> return $ VTuple (zipWith (go stk) ts xs)-          _ -> evalPanic "type mismatch during eta-expansion" ["Expected tuple type with " ++ show (length xs)-                                   ++ " elements, but got " ++ show tp]--      VRecord fs ->-        case tp of-          TVNewtype _ _ fts ->-            do let res = zipRecords (\_ v t -> go stk t v) fs fts-               case res of-                 Left (Left f)  -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f]-                 Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f]-                 Right fs' -> return (VRecord fs')-          TVRec fts ->-            do let res = zipRecords (\_ v t -> go stk t v) fs fts-               case res of-                 Left (Left f)  -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f]-                 Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f]-                 Right fs' -> return (VRecord fs')-          _ -> evalPanic "type mismatch during eta-expansion" ["Expected record type, but got " ++ show tp]--      f@VFun{} ->-        case tp of-          TVFun _t1 t2 -> lam sym $ \a -> go stk t2 (fromVFun sym f a)-          _ -> evalPanic "type mismatch during eta-expansion" ["Expected function type but got " ++ show tp]--      VPoly{} ->-        evalPanic "type mismatch during eta-expansion" ["Encountered polymorphic value"]--      VNumPoly{} ->-        evalPanic "type mismatch during eta-expansion" ["Encountered numeric polymorphic value"]--  go stk tp v = sWithCallStack sym stk $-    case tp of-      TVBit -> v-      TVInteger -> v-      TVFloat {} -> v-      TVIntMod _ -> v-      TVRational -> v-      TVArray{} -> v--      TVSeq n TVBit ->-          do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (Just (etaWord sym n v)) ""-             return $ VWord n w--      TVSeq n el ->-          do x' <- sDelay sym (fromSeq "during eta-expansion" =<< v)-             return $ VSeq n $ IndexSeqMap $ \i -> do-               go stk el (flip lookupSeqMap i =<< x')--      TVStream el ->-          do x' <- sDelay sym (fromSeq "during eta-expansion" =<< v)-             return $ VStream $ IndexSeqMap $ \i ->-               go stk el (flip lookupSeqMap i =<< x')--      TVFun _t1 t2 ->-          do v' <- sDelay sym (fromVFun sym <$> v)-             lam sym $ \a -> go stk t2 ( ($a) =<< v' )--      TVTuple ts ->-          do let n = length ts-             v' <- sDelay sym (fromVTuple <$> v)-             return $ VTuple $-                [ go stk t =<< (flip genericIndex i <$> v')-                | i <- [0..(n-1)]-                | t <- ts-                ]--      TVRec fs ->-          do v' <- sDelay sym (fromVRecord <$> v)-             let err f = evalPanic "expected record value with field" [show f]-             let eta f t = go stk t =<< (fromMaybe (err f) . lookupField f <$> v')-             return $ VRecord (mapWithFieldName eta fs)--      TVAbstract {} -> v--      TVNewtype _ _ body -> go stk (TVRec body) v- {-# SPECIALIZE declHole ::   Concrete ->   Decl ->@@ -600,9 +428,11 @@   SEval Concrete (GenValue Concrete)   #-} --- | Apply the the given "selector" form to the given value.  This function pushes---   tuple and record selections pointwise down into other value constructs---   (e.g., streams and functions).+-- | Apply the the given "selector" form to the given value.  Note that+--   selectors are expected to apply only to values of the right type,+--   e.g. tuple selectors expect only tuple values.  The lifting of+--   tuple an record selectors over functions and sequences has already+--   been resolved earlier in the typechecker. evalSel ::   Backend sym =>   sym ->@@ -636,7 +466,7 @@     case v of       VSeq _ vs       -> lookupSeqMap vs (toInteger n)       VStream vs      -> lookupSeqMap vs (toInteger n)-      VWord _ wv      -> VBit <$> (flip (indexWordValue sym) (toInteger n) =<< wv)+      VWord _ wv      -> VBit <$> indexWordValue sym wv (toInteger n)       _               -> do vdoc <- ppValue sym defaultPPOpts val                             evalPanic "Cryptol.Eval.evalSel"                               [ "Unexpected value in list selection"@@ -685,8 +515,7 @@     case e of       VSeq i mp  -> pure $ VSeq i  $ updateSeqMap mp n v       VStream mp -> pure $ VStream $ updateSeqMap mp n v-      VWord i m  -> pure $ VWord i $ do m1 <- m-                                        updateWordValue sym m1 n asBit+      VWord i m  -> VWord i <$> updateWordValue sym m n asBit       _ -> bad "Sequence update on a non-sequence."    asBit = do res <- v@@ -776,7 +605,7 @@   SEval sym (GenValue sym) evalComp sym env len elty body ms =        do lenv <- mconcat <$> mapM (branchEnvs sym (toListEnv env)) ms-          mkSeq len elty <$> memoMap sym (IndexSeqMap $ \i -> do+          mkSeq sym len elty =<< memoMap sym len (indexSeqMap $ \i -> do               evalExpr sym (evalListEnv lenv i) body)  {-# SPECIALIZE branchEnvs ::@@ -794,24 +623,24 @@   ListEnv sym ->   [Match] ->   SEval sym (ListEnv sym)-branchEnvs sym env matches = foldM (evalMatch sym) env matches+branchEnvs sym env matches = snd <$> foldM (evalMatch sym) (1, env) matches  {-# SPECIALIZE evalMatch ::   (?range :: Range, ConcPrims) =>   Concrete ->-  ListEnv Concrete ->+  (Integer, ListEnv Concrete) ->   Match ->-  SEval Concrete (ListEnv Concrete)+  SEval Concrete (Integer, ListEnv Concrete)   #-}  -- | Turn a match into the list of environments it represents. evalMatch ::   (?range :: Range, EvalPrims sym) =>   sym ->-  ListEnv sym ->+  (Integer, ListEnv sym) ->   Match ->-  SEval sym (ListEnv sym)-evalMatch sym lenv m = case m of+  SEval sym (Integer, ListEnv sym)+evalMatch sym (lsz, lenv) m = seq lsz $ case m of    -- many envs   From n l _ty expr ->@@ -819,16 +648,16 @@       -- Select from a sequence of finite length.  This causes us to 'stutter'       -- through our previous choices `nLen` times.       Nat nLen -> do-        vss <- memoMap sym $ IndexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr+        vss <- memoMap sym (Nat lsz) $ indexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr         let stutter xs = \i -> xs (i `div` nLen)         let lenv' = lenv { leVars = fmap stutter (leVars lenv) }         let vs i = do let (q, r) = i `divMod` nLen                       lookupSeqMap vss q >>= \case-                        VWord _ w   -> VBit <$> (flip (indexWordValue sym) r =<< w)+                        VWord _ w   -> VBit <$> indexWordValue sym w r                         VSeq _ xs'  -> lookupSeqMap xs' r                         VStream xs' -> lookupSeqMap xs' r                         _           -> evalPanic "evalMatch" ["Not a list value"]-        return $ bindVarList n vs lenv'+        return (lsz * nLen, bindVarList n vs lenv')        -- Select from a sequence of infinite length.  Note that this means we       -- will never need to backtrack into previous branches.  Thus, we can convert@@ -842,11 +671,13 @@         let env   = EvalEnv allvars (leTypes lenv)         xs <- evalExpr sym env expr         let vs i = case xs of-                     VWord _ w   -> VBit <$> (flip (indexWordValue sym) i =<< w)+                     VWord _ w   -> VBit <$> indexWordValue sym w i                      VSeq _ xs'  -> lookupSeqMap xs' i                      VStream xs' -> lookupSeqMap xs' i                      _           -> evalPanic "evalMatch" ["Not a list value"]-        return $ bindVarList n vs lenv'+        -- Selecting from an infinite list effectively resets the length of the+        -- list environment, so return 1 as the length+        return (1, bindVarList n vs lenv')      where       len  = evalNumType (leTypes lenv) l@@ -854,7 +685,7 @@   -- XXX we don't currently evaluate these as though they could be recursive, as   -- they are typechecked that way; the read environment to evalExpr is the same   -- as the environment to bind a new name in.-  Let d -> return $ bindVarList (dName d) (\i -> f (evalListEnv lenv i)) lenv+  Let d -> return (lsz, bindVarList (dName d) (\i -> f (evalListEnv lenv i)) lenv)     where       f env =           case dDefinition d of

@@ -26,7 +26,6 @@   ) where  import Control.Monad (guard, zipWithM, foldM, mzero)-import Data.Bits (Bits(..)) import Data.Ratio(numerator,denominator) import Data.Word(Word32, Word64) import MonadLib( ChoiceT, findOne, lift )@@ -42,8 +41,10 @@ import Cryptol.Backend.Concrete import Cryptol.Backend.FloatHelpers import Cryptol.Backend.Monad+import Cryptol.Backend.SeqMap+import Cryptol.Backend.WordValue -import Cryptol.Eval.Generic hiding (logicShift)+import Cryptol.Eval.Generic import Cryptol.Eval.Prims import Cryptol.Eval.Type import Cryptol.Eval.Value@@ -110,7 +111,7 @@         do ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))            pure $ EList ses (tValTy b)       (TVSeq n TVBit, VWord _ wval) ->-        do BV _ v <- lift (asWordVal Concrete =<< wval)+        do BV _ v <- lift (asWordVal Concrete wval)            pure $ ETApp (ETApp (prim "number") (tNum v)) (tWord (tNum n))        (_,VStream{})  -> mzero@@ -125,7 +126,7 @@            panic "Cryptol.Eval.Concrete.toExpr"              ["type mismatch:"              , pretty (tValTy ty)-             , render doc+             , show doc              ]  floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr@@ -159,24 +160,11 @@    Map.fromList $ map (\(n, v) -> (prelPrim n, v)) -  [ (">>$"        , {-# SCC "Prelude::(>>$)" #-}-                    sshrV)--    -- Shifts and rotates-  , ("<<"         , {-# SCC "Prelude::(<<)" #-}-                    logicShift shiftLW shiftLS)-  , (">>"         , {-# SCC "Prelude::(>>)" #-}-                    logicShift shiftRW shiftRS)-  , ("<<<"        , {-# SCC "Prelude::(<<<)" #-}-                    logicShift rotateLW rotateLS)-  , (">>>"        , {-# SCC "Prelude::(>>>)" #-}-                    logicShift rotateRW rotateRS)--    -- Indexing and updates-  , ("@"          , {-# SCC "Prelude::(@)" #-}-                    indexPrim sym indexFront_int indexFront_bits indexFront)+  [ -- Indexing and updates+    ("@"          , {-# SCC "Prelude::(@)" #-}+                    indexPrim sym IndexForward indexFront_int indexFront_segs)   , ("!"          , {-# SCC "Prelude::(!)" #-}-                    indexPrim sym indexBack_int indexBack_bits indexBack)+                    indexPrim sym IndexBackward indexFront_int indexFront_segs)    , ("update"     , {-# SCC "Prelude::update" #-}                     updatePrim sym updateFront_word updateFront)@@ -194,7 +182,7 @@                       F2.pmult (fromInteger (u+1)) x y                     else                       F2.pmult (fromInteger (v+1)) y x-             in return . VWord (1+u+v) . pure . WordVal . mkBv (1+u+v) $! z)+             in return . VWord (1+u+v) . wordVal . mkBv (1+u+v) $! z)     , ("pmod",         PFinPoly \_u ->@@ -203,7 +191,7 @@         PWordFun \(BV _ m) ->         PPrim           do assertSideCondition sym (m /= 0) DivideByZero-             return . VWord v . pure . WordVal . mkBv v $! F2.pmod (fromInteger w) x m)+             return . VWord v . wordVal . mkBv v $! F2.pmod (fromInteger w) x m)    , ("pdiv",         PFinPoly \_u ->@@ -212,7 +200,7 @@         PWordFun \(BV _ m) ->         PPrim           do assertSideCondition sym (m /= 0) DivideByZero-             return . VWord w . pure . WordVal . mkBv w $! F2.pdiv (fromInteger w) x m)+             return . VWord w . wordVal . mkBv w $! F2.pdiv (fromInteger w) x m)   ]  @@ -230,7 +218,7 @@        PFinPoly \p ->        PFun     \s ->        PFun     \t ->-       PPrim +       PPrim           do s' <- toProjectivePoint =<< s              t' <- toProjectivePoint =<< t              let r = PrimeEC.ec_add_nonzero (PrimeEC.primeModulus p) s' t'@@ -285,8 +273,8 @@               foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))                     SHA.initialSHA224State blks            let f :: Word32 -> Eval Value-               f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger-               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5,w6])+               f = pure . VWord 32 . wordVal . BV 32 . toInteger+               zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6])            seq zs (pure (VSeq 7 zs)))    , ("processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-}@@ -298,8 +286,8 @@              foldM (\st blk -> seq st (SHA.processSHA256Block st <$> (toSHA256Block =<< blk)))                    SHA.initialSHA256State blks            let f :: Word32 -> Eval Value-               f = pure . VWord 32 . pure . WordVal . BV 32 . toInteger-               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5,w6,w7])+               f = pure . VWord 32 . wordVal . BV 32 . toInteger+               zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])            seq zs (pure (VSeq 8 zs)))    , ("processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-}@@ -311,8 +299,8 @@              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))                    SHA.initialSHA384State blks            let f :: Word64 -> Eval Value-               f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger-               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5])+               f = pure . VWord 64 . wordVal . BV 64 . toInteger+               zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5])            seq zs (pure (VSeq 6 zs)))    , ("processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-}@@ -324,8 +312,8 @@              foldM (\st blk -> seq st (SHA.processSHA512Block st <$> (toSHA512Block =<< blk)))                    SHA.initialSHA512State blks            let f :: Word64 -> Eval Value-               f = pure . VWord 64 . pure . WordVal . BV 64 . toInteger-               zs = finiteSeqMap (map f [w0,w1,w2,w3,w4,w5,w6,w7])+               f = pure . VWord 64 . wordVal . BV 64 . toInteger+               zs = finiteSeqMap Concrete (map f [w0,w1,w2,w3,w4,w5,w6,w7])            seq zs (pure (VSeq 8 zs)))    , ("AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-}@@ -336,11 +324,11 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInfKeyExpand" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger             kws <- mapM toWord [0 .. k-1]             let ws = AES.keyExpansionWords k kws             let len = 4*(k+7)-            pure (VSeq len (finiteSeqMap (map fromWord ws))))+            pure (VSeq len (finiteSeqMap Concrete (map fromWord ws))))    , ("AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-}       PFun \st ->@@ -349,10 +337,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESInvMixColumns" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.invMixColumns ws-            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')    , ("AESEncRound", {-# SCC "SuiteB::AESEncRound" #-}       PFun \st ->@@ -361,10 +349,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesRound ws-            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')    , ("AESEncFinalRound", {-# SCC "SuiteB::AESEncFinalRound" #-}      PFun \st ->@@ -373,10 +361,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESEncFinalRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesFinalRound ws-            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')    , ("AESDecRound", {-# SCC "SuiteB::AESDecRound" #-}       PFun \st ->@@ -385,10 +373,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesInvRound ws-            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')    , ("AESDecFinalRound", {-# SCC "SuiteB::AESDecFinalRound" #-}      PFun \st ->@@ -397,10 +385,10 @@             let toWord :: Integer -> Eval Word32                 toWord i = fromInteger. bvVal <$> (fromVWord Concrete "AESDecFinalRound" =<< lookupSeqMap ss i)             let fromWord :: Word32 -> Eval Value-                fromWord = pure . VWord 32 . pure . WordVal . BV 32 . toInteger+                fromWord = pure . VWord 32 . wordVal . BV 32 . toInteger             ws <- mapM toWord [0,1,2,3]             let ws' = AES.aesInvFinalRound ws-            pure . VSeq 4 . finiteSeqMap . map fromWord $ ws')+            pure . VSeq 4 . finiteSeqMap Concrete . map fromWord $ ws')   ]  @@ -449,152 +437,39 @@         (toWord 14) <*>         (toWord 15) --------------------------------------------------------------------------------- -sshrV :: Prim Concrete-sshrV =-  PNumPoly \_n ->-  PTyPoly  \ix ->-  PWordFun \(BV w x) ->-  PFun     \y ->-  PPrim-   do idx <- y >>= asIndex Concrete ">>$" ix >>= \case-                 Left idx -> pure idx-                 Right wv -> bvVal <$> asWordVal Concrete wv-      return $ VWord w $ pure $ WordVal $ mkBv w $ signedShiftRW w x idx--logicShift :: (Integer -> Integer -> Integer -> Integer)-              -- ^ The function may assume its arguments are masked.-              -- It is responsible for masking its result if needed.-           -> (Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)-           -> Prim Concrete-logicShift opW opS =-  PNumPoly \a ->-  PTyPoly  \_ix ->-  PTyPoly  \c ->-  PFun     \l ->-  PFun     \r ->-  PPrim-     do i <- r >>= \case-          VInteger i -> pure i-          VWord _ wval -> bvVal <$> (asWordVal Concrete =<< wval)-          _ -> evalPanic "logicShift" ["not an index"]-        l >>= \case-          VWord w wv -> return $ VWord w $ wv >>= \case-                          WordVal (BV _ x) -> return $ WordVal (BV w (opW w x i))-                          LargeBitsVal n xs -> return $ LargeBitsVal n $ opS (Nat n) c xs i--          _ -> mkSeq a c <$> (opS a c <$> (fromSeq "logicShift" =<< l) <*> return i)---- Left shift for words.-shiftLW :: Integer -> Integer -> Integer -> Integer-shiftLW w ival by-  | by <  0   = shiftRW w ival (negate by)-  | by >= w   = 0-  | by > toInteger (maxBound :: Int) = panic "shiftLW" ["Shift amount too large", show by]-  | otherwise = mask w (shiftL ival (fromInteger by))---- Right shift for words-shiftRW :: Integer -> Integer -> Integer -> Integer-shiftRW w ival by-  | by <  0   = shiftLW w ival (negate by)-  | by >= w   = 0-  | by > toInteger (maxBound :: Int) = panic "shiftRW" ["Shift amount too large", show by]-  | otherwise = shiftR ival (fromInteger by)---- signed right shift for words-signedShiftRW :: Integer -> Integer -> Integer -> Integer-signedShiftRW w ival by-  | by < 0    = shiftLW w ival (negate by)-  | otherwise =-     let by' = min w by in-     if by' > toInteger (maxBound :: Int) then-       panic "signedShiftRW" ["Shift amount too large", show by]-     else-       shiftR (signedValue w ival) (fromInteger by')--shiftLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete-shiftLS w ety vs by-  | by < 0 = shiftRS w ety vs (negate by)--shiftLS w ety vs by = IndexSeqMap $ \i ->-  case w of-    Nat len-      | i+by < len -> lookupSeqMap vs (i+by)-      | i    < len -> zeroV Concrete ety-      | otherwise  -> evalPanic "shiftLS" ["Index out of bounds"]-    Inf            -> lookupSeqMap vs (i+by)--shiftRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete-shiftRS w ety vs by-  | by < 0 = shiftLS w ety vs (negate by)--shiftRS w ety vs by = IndexSeqMap $ \i ->-  case w of-    Nat len-      | i >= by   -> lookupSeqMap vs (i-by)-      | i < len   -> zeroV Concrete ety-      | otherwise -> evalPanic "shiftLS" ["Index out of bounds"]-    Inf-      | i >= by   -> lookupSeqMap vs (i-by)-      | otherwise -> zeroV Concrete ety----- XXX integer doesn't implement rotateL, as there's no bit bound-rotateLW :: Integer -> Integer -> Integer -> Integer-rotateLW 0 i _  = i-rotateLW w i by = mask w $ (i `shiftL` b) .|. (i `shiftR` (fromInteger w - b))-  where b = fromInteger (by `mod` w)--rotateLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete-rotateLS w _ vs by = IndexSeqMap $ \i ->-  case w of-    Nat len -> lookupSeqMap vs ((by + i) `mod` len)-    _ -> panic "Cryptol.Eval.Prim.rotateLS" [ "unexpected infinite sequence" ]---- XXX integer doesn't implement rotateR, as there's no bit bound-rotateRW :: Integer -> Integer -> Integer -> Integer-rotateRW 0 i _  = i-rotateRW w i by = mask w $ (i `shiftR` b) .|. (i `shiftL` (fromInteger w - b))-  where b = fromInteger (by `mod` w)--rotateRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete-rotateRS w _ vs by = IndexSeqMap $ \i ->-  case w of-    Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)-    _ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]-- -- Sequence Primitives --------------------------------------------------------- -indexFront :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value-indexFront _mblen _a vs _ix (bvVal -> ix) = lookupSeqMap vs ix--indexFront_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value-indexFront_bits mblen a vs ix bs = indexFront mblen a vs ix =<< packWord Concrete bs--indexFront_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value+indexFront_int :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> Eval Value indexFront_int _mblen _a vs _ix idx = lookupSeqMap vs idx -indexBack :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value-indexBack mblen a vs ix (bvVal -> idx) = indexBack_int mblen a vs ix idx--indexBack_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value-indexBack_bits mblen a vs ix bs = indexBack mblen a vs ix =<< packWord Concrete bs+indexFront_segs :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> [IndexSegment Concrete] -> Eval Value+indexFront_segs _mblen _a vs _ix idx_bits segs = lookupSeqMap vs $! packSegments idx_bits segs -indexBack_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value-indexBack_int mblen _a vs _ix idx =-  case mblen of-    Nat len -> lookupSeqMap vs (len - idx - 1)-    Inf     -> evalPanic "indexBack" ["unexpected infinite sequence"]+packSegments :: Integer -> [IndexSegment Concrete] -> Integer+packSegments = loop 0+  where+  loop !val !n segs =+    case segs of+      [] -> val+      [WordIndexSegment (BV _ x)] -> val + x+      WordIndexSegment (BV xlen x) : bs ->+        let n' = n - xlen+         in loop (val + (x*2^n')) n' bs+      BitIndexSegment True : bs ->+        let n' = n - 1+         in loop (val + 2^n') n' bs+      BitIndexSegment False : bs ->+        let n' = n - 1+         in loop val n' bs  updateFront ::   Nat'               {- ^ length of the sequence -} ->   TValue             {- ^ type of values in the sequence -} ->-  SeqMap Concrete    {- ^ sequence to update -} ->+  SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->   Either Integer (WordValue Concrete) {- ^ index -} ->   Eval Value         {- ^ new value at index -} ->-  Eval (SeqMap Concrete)+  Eval (SeqMap Concrete (GenValue Concrete)) updateFront _len _eltTy vs (Left idx) val = do   return $ updateSeqMap vs idx val @@ -619,10 +494,10 @@ updateBack ::   Nat'               {- ^ length of the sequence -} ->   TValue             {- ^ type of values in the sequence -} ->-  SeqMap Concrete    {- ^ sequence to update -} ->+  SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->   Either Integer (WordValue Concrete) {- ^ index -} ->   Eval Value         {- ^ new value at index -} ->-  Eval (SeqMap Concrete)+  Eval (SeqMap Concrete (GenValue Concrete)) updateBack Inf _eltTy _vs _w _val =   evalPanic "Unexpected infinite sequence in updateEnd" [] updateBack (Nat n) _eltTy vs (Left idx) val = do

@@ -6,8 +6,6 @@ -- Stability   :  provisional -- Portability :  portable -{-# LANGUAGE Safe #-}- {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveAnyClass #-}

@@ -19,25 +19,28 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE BangPatterns #-}+ {-# OPTIONS_GHC -fno-warn-orphans #-} module Cryptol.Eval.Generic where  import qualified Control.Exception as X+import Control.Monad(join) import Control.Monad.IO.Class (MonadIO(..))-import Control.Monad (join, unless) import System.Random.TF.Gen (seedTFGen) -import Data.Bits (testBit, (.&.), shiftR)+import Data.Bits ((.&.), shiftR) import Data.Maybe (fromMaybe) import qualified Data.Map.Strict as Map import Data.Map(Map) import Data.Ratio ((%))  import Cryptol.TypeCheck.AST-import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,widthInteger)+import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul) import Cryptol.Backend import Cryptol.Backend.Concrete (Concrete(..)) import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )+import Cryptol.Backend.SeqMap+import Cryptol.Backend.WordValue import Cryptol.Testing.Random( randomValue )  import Cryptol.Eval.Prims@@ -63,7 +66,7 @@       | m == 0                   -> evalPanic "mkLit" ["0 modulus not allowed"]       | otherwise                -> VInteger <$> integerLit sym (i `mod` m)     TVFloat e p                  -> VFloat <$> fpLit sym e p (fromInteger i)-    TVSeq w TVBit                -> pure $ word sym w i+    TVSeq w TVBit                -> word sym w i     TVRational                   -> VRational <$> (intToRational sym =<< integerLit sym i)     _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"                                     [ "Invalid type for number" ]@@ -217,14 +220,14 @@                   lw <- fromVWord sym "ringLeft" l                   rw <- fromVWord sym "ringRight" r                   stk <- sGetCallStack sym-                  return $ VWord w (WordVal <$> (sWithCallStack sym stk (opw w lw rw)))-      | otherwise -> VSeq w <$> (join (zipSeqMap sym (loop a) <$>+                  VWord w . wordVal <$> (sWithCallStack sym stk (opw w lw rw))+      | otherwise -> VSeq w <$> (join (zipSeqMap sym (loop a) (Nat w) <$>                                       (fromSeq "ringBinary left" l) <*>                                       (fromSeq "ringBinary right" r)))      TVStream a ->       -- streams-      VStream <$> (join (zipSeqMap sym (loop a) <$>+      VStream <$> (join (zipSeqMap sym (loop a) Inf <$>                              (fromSeq "ringBinary left" l) <*>                              (fromSeq "ringBinary right" r))) @@ -303,11 +306,11 @@       | isTBit a -> do               wx <- fromVWord sym "ringUnary" v               stk <- sGetCallStack sym-              return $ VWord w (WordVal <$> sWithCallStack sym stk (opw w wx))-      | otherwise -> VSeq w <$> (mapSeqMap sym (loop a) =<< fromSeq "ringUnary" v)+              VWord w . wordVal <$> sWithCallStack sym stk (opw w wx)+      | otherwise -> VSeq w <$> (mapSeqMap sym (loop a) (Nat w) =<< fromSeq "ringUnary" v)      TVStream a ->-      VStream <$> (mapSeqMap sym (loop a) =<< fromSeq "ringUnary" v)+      VStream <$> (mapSeqMap sym (loop a) Inf =<< fromSeq "ringUnary" v)      -- functions     TVFun _ ety ->@@ -372,14 +375,14 @@           -- words and finite sequences           | isTBit a ->              do stk <- sGetCallStack sym-                pure $ VWord w $ (WordVal <$> sWithCallStack sym stk (opw w))+                VWord w . wordVal <$> sWithCallStack sym stk (opw w)           | otherwise ->              do v <- sDelay sym (loop a)-                pure $ VSeq w $ IndexSeqMap \_i -> v+                pure $ VSeq w $ indexSeqMap \_i -> v          TVStream a ->              do v <- sDelay sym (loop a)-                pure $ VStream $ IndexSeqMap \_i -> v+                pure $ VStream $ indexSeqMap \_i -> v          TVFun _ b ->              do v <- sDelay sym (loop b)@@ -420,7 +423,7 @@           do wl <- fromVWord sym "integralBinary left" l              wr <- fromVWord sym "integralBinary right" r              stk <- sGetCallStack sym-             return $ VWord w (WordVal <$> sWithCallStack sym stk (opw w wl wr))+             VWord w . wordVal <$> sWithCallStack sym stk (opw w wl wr)      _ -> evalPanic "integralBinary" [show ty ++ " not int class `Integral`"] @@ -509,7 +512,7 @@                       intV sym onei aty                  | n > 0 ->-                    do ebits <- enumerateIntBits' sym n ei+                    do (_,ebits) <- enumerateIntBits' sym n ei                        computeExponent sym aty a ebits                  | otherwise -> raiseError sym NegativeExponent@@ -517,7 +520,7 @@               Nothing -> liftIO (X.throw (UnsupportedSymbolicOp "integer exponentiation"))            TVSeq _w el | isTBit el ->-            do ebits <- enumerateWordValue sym =<< fromWordVal "(^^)" e+            do ebits <- enumerateWordValue sym (fromWordVal "(^^)" e)                computeExponent sym aty a ebits            _ -> evalPanic "expV" [show ety ++ " not int class `Integral`"]@@ -695,7 +698,7 @@ lg2V sym =   PFinPoly \w ->   PWordFun \x ->-  PVal (VWord w (WordVal <$> wordLg2 sym x))+  PPrim (VWord w . wordVal <$> wordLg2 sym x)  {-# SPECIALIZE sdivV :: Concrete -> Prim Concrete #-} sdivV :: Backend sym => sym -> Prim sym@@ -703,7 +706,7 @@   PFinPoly \w ->   PWordFun \x ->   PWordFun \y ->-  PVal (VWord w (WordVal <$> wordSignedDiv sym x y))+  PPrim (VWord w . wordVal <$> wordSignedDiv sym x y)  {-# SPECIALIZE smodV :: Concrete -> Prim Concrete #-} smodV :: Backend sym => sym -> Prim sym@@ -711,8 +714,15 @@   PFinPoly \w ->   PWordFun \x ->   PWordFun \y ->-  PVal (VWord w (WordVal <$> wordSignedMod sym x 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 ::@@ -915,14 +925,14 @@    -- sequences   TVSeq w ety-      | isTBit ety -> pure $ word sym w 0+      | isTBit ety -> word sym w 0       | otherwise  ->            do z <- sDelay sym (zeroV sym ety)-              pure $ VSeq w (IndexSeqMap \_i -> z)+              pure $ VSeq w (indexSeqMap \_i -> z)    TVStream ety ->      do z <- sDelay sym (zeroV sym ety)-        pure $ VStream (IndexSeqMap \_i -> z)+        pure $ VStream (indexSeqMap \_i -> z)    -- functions   TVFun _ bty ->@@ -943,52 +953,13 @@    TVNewtype {} -> evalPanic "zeroV" [ "Newtype not in `Zero`" ] ---  | otherwise = evalPanic "zeroV" ["invalid type for zero"] -{-# INLINE joinWordVal #-}-joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)-joinWordVal sym (WordVal w1) (WordVal w2)-  | wordLen sym w1 + wordLen sym w2 < largeBitSize-  = WordVal <$> joinWord sym w1 w2-joinWordVal sym w1 w2-  = pure $ LargeBitsVal (n1+n2) (concatSeqMap n1 (asBitsMap sym w1) (asBitsMap sym w2))- where n1 = wordValueSize sym w1-       n2 = wordValueSize sym w2---{-# SPECIALIZE joinWords ::-  Concrete ->-  Integer ->-  Integer ->-  SeqMap Concrete ->-  SEval Concrete (GenValue Concrete)-  #-}-joinWords :: forall sym.-  Backend sym =>-  sym ->-  Integer ->-  Integer ->-  SeqMap sym ->-  SEval sym (GenValue sym)-joinWords sym nParts nEach xs =-  loop (WordVal <$> wordLit sym 0 0) (enumerateSeqMap nParts xs)-- where- loop :: SEval sym (WordValue sym) -> [SEval sym (GenValue sym)] -> SEval sym (GenValue sym)- loop !wv [] =-    VWord (nParts * nEach) <$> sDelay sym wv- loop !wv (w : ws) =-    w >>= \case-      VWord _ w' ->-        loop (join (joinWordVal sym <$> wv <*> w')) ws-      _ -> evalPanic "joinWords: expected word value" []- {-# SPECIALIZE joinSeq ::   Concrete ->   Nat' ->   Integer ->   TValue ->-  SeqMap Concrete ->+  SEval Concrete (SeqMap Concrete (GenValue Concrete)) ->   SEval Concrete (GenValue Concrete)   #-} joinSeq ::@@ -997,35 +968,32 @@   Nat' ->   Integer ->   TValue ->-  SeqMap sym ->+  SEval sym (SeqMap sym (GenValue sym)) ->   SEval sym (GenValue sym)  -- Special case for 0 length inner sequences.-joinSeq sym _parts 0 a _xs+joinSeq sym _parts 0 a _val   = zeroV sym (TVSeq 0 a)  -- finite sequence of words-joinSeq sym (Nat parts) each TVBit xs-  | parts * each < largeBitSize-  = joinWords sym parts each xs-  | otherwise-  = do let zs = IndexSeqMap $ \i ->-                  do let (q,r) = divMod i each-                     ys <- fromWordVal "join seq" =<< lookupSeqMap xs q-                     VBit <$> indexWordValue sym ys r-       return $ VWord (parts * each) $ pure $ LargeBitsVal (parts * each) zs+joinSeq sym (Nat parts) each TVBit val+  = do w <- delayWordValue sym (parts*each)+              (joinWords sym parts each . fmap (fromWordVal "joinV") =<< val)+       pure (VWord (parts*each) w)  -- infinite sequence of words-joinSeq sym Inf each TVBit xs-  = return $ VStream $ IndexSeqMap $ \i ->+joinSeq sym Inf each TVBit val+  = return $ VStream $ indexSeqMap $ \i ->       do let (q,r) = divMod i each-         ys <- fromWordVal "join seq" =<< lookupSeqMap xs q+         xs <- val+         ys <- fromWordVal "join seq" <$> lookupSeqMap xs q          VBit <$> indexWordValue sym ys r  -- finite or infinite sequence of non-words-joinSeq _sym parts each _a xs-  = return $ vSeq $ IndexSeqMap $ \i -> do+joinSeq _sym parts each _a val+  = return $ vSeq $ indexSeqMap $ \i -> do       let (q,r) = divMod i each+      xs <- val       ys <- fromSeq "join seq" =<< lookupSeqMap xs q       lookupSeqMap ys r   where@@ -1044,146 +1012,115 @@   Nat' ->   Integer ->   TValue ->-  GenValue sym ->+  SEval sym (GenValue sym) ->   SEval sym (GenValue sym)-joinV sym parts each a val = joinSeq sym parts each a =<< fromSeq "joinV" val---{-# INLINE splitWordVal #-}--splitWordVal ::-  Backend sym =>-  sym ->-  Integer ->-  Integer ->-  WordValue sym ->-  SEval sym (WordValue sym, WordValue sym)-splitWordVal sym leftWidth rightWidth (WordVal w) =-  do (lw, rw) <- splitWord sym leftWidth rightWidth w-     pure (WordVal lw, WordVal rw)-splitWordVal _ leftWidth rightWidth (LargeBitsVal _n xs) =-  let (lxs, rxs) = splitSeqMap leftWidth xs-   in pure (LargeBitsVal leftWidth lxs, LargeBitsVal rightWidth rxs)+joinV sym parts each a val =+  do xs <- sDelay sym (fromSeq "joinV" =<< val)+     joinSeq sym parts each a xs -{-# INLINE splitAtV #-}-splitAtV ::+{-# INLINE takeV #-}+takeV ::   Backend sym =>   sym ->   Nat' ->   Nat' ->   TValue ->-  GenValue sym ->+  SEval sym (GenValue sym) ->   SEval sym (GenValue sym)-splitAtV sym front back a val =-  case back of--    Nat rightWidth | aBit -> do-          ws <- sDelay sym (splitWordVal sym leftWidth rightWidth =<< fromWordVal "splitAtV" val)-          return $ VTuple-                   [ VWord leftWidth  . pure . fst <$> ws-                   , VWord rightWidth . pure . snd <$> ws-                   ]--    Inf | aBit -> do-       vs <- sDelay sym (fromSeq "splitAtV" val)-       ls <- sDelay sym (fst . splitSeqMap leftWidth <$> vs)-       rs <- sDelay sym (snd . splitSeqMap leftWidth <$> vs)-       return $ VTuple [ return $ VWord leftWidth (LargeBitsVal leftWidth <$> ls)-                       , VStream <$> rs-                       ]--    _ -> do-       vs <- sDelay sym (fromSeq "splitAtV" val)-       ls <- sDelay sym (fst . splitSeqMap leftWidth <$> vs)-       rs <- sDelay sym (snd . splitSeqMap leftWidth <$> vs)-       return $ VTuple [ VSeq leftWidth <$> ls-                       , mkSeq back a <$> rs-                       ]--  where-  aBit = isTBit a--  leftWidth = case front of-    Nat n -> n-    _     -> evalPanic "splitAtV" ["invalid `front` len"]+takeV sym front back a val =+  case front of+    Inf -> val+    Nat front' ->+      case back of+        Nat back' | isTBit a ->+          do w <- delayWordValue sym front' (takeWordVal sym front' back' =<< (fromWordVal "takeV" <$> val))+             pure (VWord front' w) +        Inf | isTBit a ->+          do w <- delayWordValue sym front' (bitmapWordVal sym front' . fmap fromVBit =<< (fromSeq "takeV" =<< val))+             pure (VWord front' w) -{-# INLINE extractWordVal #-}+        _ ->+          do xs <- delaySeqMap sym (fromSeq "takeV" =<< val)+             pure (VSeq front' xs) --- | Extract a subsequence of bits from a @WordValue@.---   The first integer argument is the number of bits in the---   resulting word.  The second integer argument is the---   number of less-significant digits to discard.  Stated another---   way, the operation `extractWordVal n i w` is equivalent to---   first shifting `w` right by `i` bits, and then truncating to---   `n` bits.-extractWordVal ::+{-# INLINE dropV #-}+dropV ::   Backend sym =>   sym ->   Integer ->-  Integer ->-  WordValue sym ->-  SEval sym (WordValue sym)-extractWordVal sym len start (WordVal w) =-   WordVal <$> extractWord sym len start w-extractWordVal _ len start (LargeBitsVal n xs) =-   let xs' = dropSeqMap (n - start - len) xs-    in pure $ LargeBitsVal len xs'+  Nat' ->+  TValue ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym)+dropV sym front back a val =+  case back of+    Nat back' | isTBit a ->+      do w <- delayWordValue sym back' (dropWordVal sym front back' =<< (fromWordVal "dropV" <$> val))+         pure (VWord back' w) -{-# INLINE ecSplitV #-}+    _ ->+      do xs <- delaySeqMap sym (dropSeqMap front <$> (fromSeq "dropV" =<< val))+         mkSeq sym back a xs ++{-# INLINE splitV #-}+ -- | Split implementation.-ecSplitV :: Backend sym => sym -> Prim sym-ecSplitV sym =-  PNumPoly \parts ->-  PNumPoly \each ->-  PTyPoly  \a ->-  PFun     \val ->-  PPrim+splitV :: Backend sym =>+  sym ->+  Nat' ->+  Integer ->+  TValue ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym)+splitV sym parts each a val =     case (parts, each) of-       (Nat p, Nat e) | isTBit a -> do-          ~(VWord _ val') <- val-          return $ VSeq p $ IndexSeqMap $ \i ->-            pure $ VWord e (extractWordVal sym e ((p-i-1)*e) =<< val')-       (Inf, Nat e) | isTBit a -> do-          val' <- sDelay sym (fromSeq "ecSplitV" =<< val)-          return $ VStream $ IndexSeqMap $ \i ->-            return $ VWord e $ return $ LargeBitsVal e $ IndexSeqMap $ \j ->+       (Nat p, e) | isTBit a -> do+          val' <- sDelay sym (fromWordVal "splitV" <$> val)+          return $ VSeq p $ indexSeqMap $ \i ->+            VWord e <$> (extractWordVal sym e ((p-i-1)*e) =<< val')+       (Inf, e) | isTBit a -> do+          val' <- sDelay sym (fromSeq "splitV" =<< val)+          return $ VStream $ indexSeqMap $ \i ->+            VWord e <$> bitmapWordVal sym e (indexSeqMap $ \j ->               let idx = i*e + toInteger j                in idx `seq` do                       xs <- val'-                      lookupSeqMap xs idx-       (Nat p, Nat e) -> do-          val' <- sDelay sym (fromSeq "ecSplitV" =<< val)-          return $ VSeq p $ IndexSeqMap $ \i ->-            return $ VSeq e $ IndexSeqMap $ \j -> do+                      fromVBit <$> lookupSeqMap xs idx)+       (Nat p, e) -> do+          val' <- sDelay sym (fromSeq "splitV" =<< val)+          return $ VSeq p $ indexSeqMap $ \i ->+            return $ VSeq e $ indexSeqMap $ \j -> do               xs <- val'               lookupSeqMap xs (e * i + j)-       (Inf  , Nat e) -> do-          val' <- sDelay sym (fromSeq "ecSplitV" =<< val)-          return $ VStream $ IndexSeqMap $ \i ->-            return $ VSeq e $ IndexSeqMap $ \j -> do+       (Inf  , e) -> do+          val' <- sDelay sym (fromSeq "splitV" =<< val)+          return $ VStream $ indexSeqMap $ \i ->+            return $ VSeq e $ indexSeqMap $ \j -> do               xs <- val'               lookupSeqMap xs (e * i + j)-       _              -> evalPanic "splitV" ["invalid type arguments to split"] + {-# INLINE reverseV #-}  reverseV :: forall sym.   Backend sym =>   sym ->-  GenValue sym ->+  Integer ->+  TValue ->+  SEval sym (GenValue sym) ->   SEval sym (GenValue sym)-reverseV _ (VSeq n xs) =-  return $ VSeq n $ reverseSeqMap n xs-reverseV sym (VWord n x) = return (VWord n (revword <$> x))- where- revword wv =-   let m = wordValueSize sym wv in-   LargeBitsVal m $ reverseSeqMap m $ asBitsMap sym wv-reverseV _ _ =-  evalPanic "reverseV" ["Not a finite sequence"] +reverseV sym n TVBit val =+  do w <- delayWordValue sym n (reverseWordVal sym . fromWordVal "reverseV" =<< val)+     pure (VWord n w)++reverseV sym n _a val =+  do xs <- delaySeqMap sym (reverseSeqMap n <$> (fromSeq "reverseV" =<< val))+     pure (VSeq n xs)++ {-# INLINE transposeV #-}  transposeV ::@@ -1196,28 +1133,28 @@   SEval sym (GenValue sym) transposeV sym a b c xs   | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit-      return $ bseq $ IndexSeqMap $ \bi ->-        return $ VWord na $ return $ LargeBitsVal na $ IndexSeqMap $ \ai ->+      return $ bseq $ indexSeqMap $ \bi ->+        VWord na <$> bitmapWordVal sym na (indexSeqMap $ \ai ->          do xs' <- fromSeq "transposeV" xs             ys <- lookupSeqMap xs' ai             case ys of-              VStream ys' -> lookupSeqMap ys' bi-              VWord _ wv  -> VBit <$> (flip (indexWordValue sym) bi =<< wv)-              _ -> evalPanic "transpose" ["expected sequence of bits"]+              VStream ys' -> fromVBit <$> lookupSeqMap ys' bi+              VWord _ wv  -> indexWordValue sym wv bi+              _ -> evalPanic "transpose" ["expected sequence of bits"])    | isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit-      return $ bseq $ IndexSeqMap $ \bi ->-        return $ VStream $ IndexSeqMap $ \ai ->+      return $ bseq $ indexSeqMap $ \bi ->+        return $ VStream $ indexSeqMap $ \ai ->          do xs' <- fromSeq "transposeV" xs             ys  <- lookupSeqMap xs' ai             case ys of               VStream ys' -> lookupSeqMap ys' bi-              VWord _ wv  -> VBit <$> (flip (indexWordValue sym) bi =<< wv)+              VWord _ wv  -> VBit <$> indexWordValue sym wv bi               _ -> evalPanic "transpose" ["expected sequence of bits"]    | otherwise = -- [a][b]c -> [b][a]c-      return $ bseq $ IndexSeqMap $ \bi ->-        return $ aseq $ IndexSeqMap $ \ai -> do+      return $ bseq $ indexSeqMap $ \bi ->+        return $ aseq $ indexSeqMap $ \ai -> do           xs' <- fromSeq "transposeV 1" xs           ys  <- fromSeq "transposeV 2" =<< lookupSeqMap xs' ai           z   <- lookupSeqMap ys bi@@ -1239,54 +1176,52 @@ ccatV ::   Backend sym =>   sym ->-  Nat' ->+  Integer ->   Nat' ->   TValue ->-  (GenValue sym) ->-  (GenValue sym) ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym) ->   SEval sym (GenValue sym) -ccatV sym _front _back _elty (VWord m l) (VWord n r) =-  return $ VWord (m+n) (join (joinWordVal sym <$> l <*> r))+-- Finite bitvectors+ccatV sym front (Nat back) TVBit l r =+  do ml <- isReady sym l+     mr <- isReady sym r+     case (ml, mr) of+       (Just l', Just r') ->+         VWord (front+back) <$>+           joinWordVal sym (fromWordVal "ccatV left" l') (fromWordVal "ccatV right" r')+       _ ->+         VWord (front+back) <$> delayWordValue sym (front+back)+                (do l' <- fromWordVal "ccatV left"  <$> l+                    r' <- fromWordVal "ccatV right" <$> r+                    joinWordVal sym l' r') -ccatV sym _front _back _elty (VWord m l) (VStream r) = do-  l' <- sDelay sym l-  return $ VStream $ IndexSeqMap $ \i ->-    if i < m then-      VBit <$> (flip (indexWordValue sym) i =<< l')-    else-      lookupSeqMap r (i-m)+-- Infinite bitstream+ccatV sym front Inf TVBit l r =+  do l'' <- sDelay sym (asBitsMap sym  . fromWordVal "ccatV left" <$> l)+     r'' <- sDelay sym (fromSeq "ccatV right" =<< r)+     pure $ VStream $ indexSeqMap $ \i ->+      if i < front then do+        ls <- l''+        VBit <$> lookupSeqMap ls i+      else do+        rs <- r''+        lookupSeqMap rs (i-front) -ccatV sym front back elty l r = do-       l'' <- sDelay sym (fromSeq "ccatV left" l)-       r'' <- sDelay sym (fromSeq "ccatV right" r)-       let Nat n = front-       mkSeq (evalTF TCAdd [front,back]) elty <$> return (IndexSeqMap $ \i ->-        if i < n then do-         ls <- l''-         lookupSeqMap ls i-        else do-         rs <- r''-         lookupSeqMap rs (i-n))+-- streams/sequences of nonbits+ccatV sym front back elty l r =+  do l'' <- sDelay sym (fromSeq "ccatV left" =<< l)+     r'' <- sDelay sym (fromSeq "ccatV right" =<< r)+     mkSeq sym (evalTF TCAdd [Nat front,back]) elty $ indexSeqMap $ \i ->+      if i < front then do+        ls <- l''+        lookupSeqMap ls i+      else do+        rs <- r''+        lookupSeqMap rs (i-front) -{-# INLINE wordValLogicOp #-} -wordValLogicOp ::-  Backend sym =>-  sym ->-  (SBit sym -> SBit sym -> SEval sym (SBit sym)) ->-  (SWord sym -> SWord sym -> SEval sym (SWord sym)) ->-  WordValue sym ->-  WordValue sym ->-  SEval sym (WordValue sym)-wordValLogicOp _sym _ wop (WordVal w1) (WordVal w2) = WordVal <$> wop w1 w2--wordValLogicOp sym bop _ w1 w2 = LargeBitsVal (wordValueSize sym w1) <$> zs-     where zs = memoMap sym $ IndexSeqMap $ \i -> join (op <$> (lookupSeqMap xs i) <*> (lookupSeqMap ys i))-           xs = asBitsMap sym w1-           ys = asBitsMap sym w2-           op x y = VBit <$> (bop (fromVBit x) (fromVBit y))- {-# SPECIALIZE logicBinary ::   Concrete ->   (SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)) ->@@ -1325,20 +1260,19 @@     TVSeq w aty          -- words          | isTBit aty-              -> do v <- sDelay sym $ join-                            (wordValLogicOp sym opb opw <$>-                                    fromWordVal "logicBinary l" l <*>-                                    fromWordVal "logicBinary r" r)-                    return $ VWord w v+              -> VWord w <$> delayWordValue sym w+                               (wordValLogicOp sym opb opw+                                    (fromWordVal "logicBinary l" l)+                                    (fromWordVal "logicBinary r" r))           -- finite sequences          | otherwise -> VSeq w <$>-                           (join (zipSeqMap sym (loop aty) <$>+                           (join (zipSeqMap sym (loop aty) (Nat w) <$>                                     (fromSeq "logicBinary left" l)                                     <*> (fromSeq "logicBinary right" r)))      TVStream aty ->-        VStream <$> (join (zipSeqMap sym (loop aty) <$>+        VStream <$> (join (zipSeqMap sym (loop aty) Inf <$>                           (fromSeq "logicBinary left" l) <*>                           (fromSeq "logicBinary right" r))) @@ -1362,18 +1296,6 @@     TVNewtype {} -> evalPanic "logicBinary"                         [ "Newtype not in `Logic`" ] -{-# INLINE wordValUnaryOp #-}-wordValUnaryOp ::-  Backend sym =>-  sym ->-  (SBit sym -> SEval sym (SBit sym)) ->-  (SWord sym -> SEval sym (SWord sym)) ->-  WordValue sym ->-  SEval sym (WordValue sym)-wordValUnaryOp _ _ wop (WordVal w)  = WordVal <$> (wop w)-wordValUnaryOp sym bop _ (LargeBitsVal n xs) = LargeBitsVal n <$> mapSeqMap sym f xs-  where f x = VBit <$> (bop (fromVBit x))- {-# SPECIALIZE logicUnary ::   Concrete ->   (SBit Concrete -> SEval Concrete (SBit Concrete)) ->@@ -1405,16 +1327,15 @@     TVSeq w ety          -- words          | isTBit ety-              -> do v <- sDelay sym (wordValUnaryOp sym opb opw =<< fromWordVal "logicUnary" val)-                    return $ VWord w v+              -> VWord w <$> delayWordValue sym w (wordValUnaryOp sym opb opw (fromWordVal "logicUnary" val))           -- finite sequences          | otherwise-              -> VSeq w <$> (mapSeqMap sym (loop ety) =<< fromSeq "logicUnary" val)+              -> VSeq w <$> (mapSeqMap sym (loop ety) (Nat w) =<< fromSeq "logicUnary" val)           -- streams     TVStream ety ->-         VStream <$> (mapSeqMap sym (loop ety) =<< fromSeq "logicUnary" val)+         VStream <$> (mapSeqMap sym (loop ety) Inf =<< fromSeq "logicUnary" val)      TVTuple etys ->       do as <- mapM (sDelay sym) (fromVTuple val)@@ -1433,32 +1354,7 @@      TVNewtype {} -> evalPanic "logicUnary" [ "Newtype not in `Logic`" ] -{-# SPECIALIZE bitsValueLessThan ::-  Concrete ->-  Integer ->-  [SBit Concrete] ->-  Integer ->-  SEval Concrete (SBit Concrete)-  #-}-bitsValueLessThan ::-  Backend sym =>-  sym ->-  Integer {- ^ bit-width -} ->-  [SBit sym] {- ^ big-endian list of index bits -} ->-  Integer {- ^ Upper bound to test against -} ->-  SEval sym (SBit sym)-bitsValueLessThan sym _w [] _n = pure $ bitLit sym False-bitsValueLessThan sym w (b:bs) n-  | nbit =-      do notb <- bitComplement sym b-         bitOr sym notb =<< bitsValueLessThan sym (w-1) bs n-  | otherwise =-      do notb <- bitComplement sym b-         bitAnd sym notb =<< bitsValueLessThan sym (w-1) bs n- where- nbit = testBit n (fromInteger (w-1)) - {-# INLINE assertIndexInBounds #-} assertIndexInBounds ::   Backend sym =>@@ -1486,30 +1382,8 @@  -- Can't index out of bounds for a sequence that is -- longer than the expressible index values-assertIndexInBounds sym (Nat n) (Right idx)-  | n >= 2^(wordValueSize sym idx)-  = return ()---- If the index is concrete, test it directly-assertIndexInBounds sym (Nat n) (Right (WordVal idx))-  | Just (_w,i) <- wordAsLit sym idx-  = unless (i < n) (raiseError sym (InvalidIndex (Just i)))---- If the index is a packed word, test that it--- is less than the concrete value of n, which--- fits into w bits because of the above test.-assertIndexInBounds sym (Nat n) (Right (WordVal idx)) =-  do n' <- wordLit sym (wordLen sym idx) n-     p <- wordLessThan sym idx n'-     assertSideCondition sym p (InvalidIndex Nothing)---- If the index is an unpacked word, force all the bits--- and compute the unsigned less-than test directly.-assertIndexInBounds sym (Nat n) (Right (LargeBitsVal w bits)) =-  do bitsList <- traverse (fromVBit <$>) (enumerateSeqMap w bits)-     p <- bitsValueLessThan sym w bitsList n-     assertSideCondition sym p (InvalidIndex Nothing)-+assertIndexInBounds sym (Nat n) (Right idx) =+  assertWordValueInBounds sym n idx  -- | Indexing operations. @@ -1517,11 +1391,11 @@ indexPrim ::   Backend sym =>   sym ->-  (Nat' -> TValue -> SeqMap sym -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->-  (Nat' -> TValue -> SeqMap sym -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) ->-  (Nat' -> TValue -> SeqMap sym -> TValue -> SWord sym -> SEval sym (GenValue sym)) ->+  IndexDirection ->+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) ->+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> Integer -> [IndexSegment sym] -> SEval sym (GenValue sym)) ->   Prim sym-indexPrim sym int_op bits_op word_op =+indexPrim sym dir int_op word_op =   PNumPoly \len ->   PTyPoly  \eltTy ->   PTyPoly  \ix ->@@ -1529,16 +1403,19 @@   PFun     \idx ->   PPrim    do vs <- xs >>= \case-               VWord _ w  -> w >>= \w' -> return $ IndexSeqMap (\i -> VBit <$> indexWordValue sym w' i)+               VWord _ w  -> return $ indexSeqMap (\i -> VBit <$> indexWordValue sym w i)                VSeq _ vs  -> return vs                VStream vs -> return vs                _ -> evalPanic "Expected sequence value" ["indexPrim"]-      idx' <- asIndex sym "index" ix =<< idx+      let vs' = case (len, dir) of+                  (_    , IndexForward)  -> vs+                  (Nat n, IndexBackward) -> reverseSeqMap n vs+                  (Inf  , IndexBackward) -> evalPanic "Expected finite sequence" ["!"]+      idx' <- asIndex sym "index" ix <$> idx       assertIndexInBounds sym len idx'       case idx' of-        Left i                    -> int_op  len eltTy vs ix i-        Right (WordVal w')        -> word_op len eltTy vs ix w'-        Right (LargeBitsVal m bs) -> bits_op len eltTy vs ix =<< traverse (fromVBit <$>) (enumerateSeqMap m bs)+        Left i  -> int_op  len eltTy vs' ix i+        Right w -> word_op len eltTy vs' ix (wordValueSize sym w) =<< enumerateIndexSegments sym w  {-# INLINE updatePrim #-} @@ -1546,7 +1423,7 @@   Backend sym =>   sym ->   (Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) ->-  (Nat' -> TValue -> SeqMap sym    -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)) ->+  (Nat' -> TValue -> SeqMap sym (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) ->   Prim sym updatePrim sym updateWord updateSeq =   PNumPoly \len ->@@ -1556,17 +1433,17 @@   PFun     \idx ->   PFun     \val ->   PPrim-   do idx' <- asIndex sym "update" ix =<< idx+   do idx' <- asIndex sym "update" ix <$> idx       assertIndexInBounds sym len idx'-      xs >>= \case-        VWord l w  -> do w' <- sDelay sym w-                         return $ VWord l (w' >>= \w'' -> updateWord len eltTy w'' idx' val)-        VSeq l vs  -> VSeq l  <$> updateSeq len eltTy vs idx' val-        VStream vs -> VStream <$> updateSeq len eltTy vs idx' val-        _ -> evalPanic "Expected sequence value" ["updatePrim"]+      case (len, eltTy) of+        (Nat n, TVBit) -> VWord n <$> delayWordValue sym n+                             (do w <- fromWordVal "updatePrim" <$> xs; updateWord len eltTy w idx' val)+        (Nat n, _    ) -> VSeq n <$> delaySeqMap sym+                             (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val)+        (Inf  , _    ) -> VStream <$> delaySeqMap sym+                             (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val)  {-# INLINE fromToV #-}- -- @[ 0 .. 10 ]@ fromToV :: Backend sym => sym -> Prim sym fromToV sym =@@ -1578,26 +1455,10 @@     case (first, lst) of       (Nat first', Nat lst') ->         let len = 1 + (lst' - first')-        in VSeq len $ IndexSeqMap $ \i -> f (first' + i)+        in VSeq len $ indexSeqMap $ \i -> f (first' + i)       _ -> evalPanic "fromToV" ["invalid arguments"] -{-# INLINE fromToLessThanV #-}---- @[ 0 .. <10 ]@-fromToLessThanV :: Backend sym => sym -> Prim sym-fromToLessThanV sym =-  PFinPoly \first ->-  PNumPoly \bound ->-  PTyPoly  \ty ->-  PVal-    let !f = mkLit sym ty-        ss = IndexSeqMap $ \i -> f (first + i)-    in case bound of-         Inf        -> VStream ss-         Nat bound' -> VSeq (bound' - first) ss- {-# INLINE fromThenToV #-}- -- @[ 0, 1 .. 10 ]@ fromThenToV :: Backend sym => sym -> Prim sym fromThenToV sym =@@ -1611,9 +1472,78 @@     case (first, next, lst, len) of       (Nat first', Nat next', Nat _lst', Nat len') ->         let diff = next' - first'-        in VSeq len' $ IndexSeqMap $ \i -> f (first' + i*diff)+        in VSeq len' $ indexSeqMap $ \i -> f (first' + i*diff)       _ -> evalPanic "fromThenToV" ["invalid arguments"] +{-# INLINE fromToLessThanV #-}+-- @[ 0 .. <10 ]@+fromToLessThanV :: Backend sym => sym -> Prim sym+fromToLessThanV sym =+  PFinPoly \first ->+  PNumPoly \bound ->+  PTyPoly  \ty ->+  PVal+    let !f = mkLit sym ty+        ss = indexSeqMap $ \i -> f (first + i)+    in case bound of+         Inf        -> VStream ss+         Nat bound' -> VSeq (bound' - first) ss++{-# INLINE fromToByV #-}+-- @[ 0 .. 10 by 2 ]@+fromToByV :: Backend sym => sym -> Prim sym+fromToByV sym =+  PFinPoly \first ->+  PFinPoly \lst ->+  PFinPoly \stride ->+  PTyPoly  \ty ->+  PVal+    let !f = mkLit sym ty+        ss = indexSeqMap $ \i -> f (first + i*stride)+     in VSeq (1 + ((lst - first) `div` stride)) ss++{-# INLINE fromToByLessThanV #-}+-- @[ 0 .. <10 by 2 ]@+fromToByLessThanV :: Backend sym => sym -> Prim sym+fromToByLessThanV sym =+  PFinPoly \first ->+  PNumPoly \bound ->+  PFinPoly \stride ->+  PTyPoly  \ty ->+  PVal+    let !f = mkLit sym ty+        ss = indexSeqMap $ \i -> f (first + i*stride)+     in case bound of+          Inf -> VStream ss+          Nat bound' -> VSeq ((bound' - first + stride - 1) `div` stride) ss+++{-# INLINE fromToDownByV #-}+-- @[ 10 .. 0 down by 2 ]@+fromToDownByV :: Backend sym => sym -> Prim sym+fromToDownByV sym =+  PFinPoly \first ->+  PFinPoly \lst ->+  PFinPoly \stride ->+  PTyPoly  \ty ->+  PVal+    let !f = mkLit sym ty+        ss = indexSeqMap $ \i -> f (first - i*stride)+     in VSeq (1 + ((first - lst) `div` stride)) ss++{-# INLINE fromToDownByGreaterThanV #-}+-- @[ 10 .. >0 down by 2 ]@+fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym+fromToDownByGreaterThanV sym =+  PFinPoly \first ->+  PFinPoly \bound ->+  PFinPoly \stride ->+  PTyPoly  \ty ->+  PVal+    let !f = mkLit sym ty+        ss = indexSeqMap $ \i -> f (first - i*stride)+     in VSeq ((first - bound + stride - 1) `div` stride) ss+ {-# INLINE infFromV #-} infFromV :: Backend sym => sym -> Prim sym infFromV sym =@@ -1621,7 +1551,7 @@   PFun    \x ->   PPrim     do mx <- sDelay sym x-       return $ VStream $ IndexSeqMap $ \i ->+       return $ VStream $ indexSeqMap $ \i ->          do x' <- mx             i' <- integerLit sym i             addV sym ty x' =<< intV sym i' ty@@ -1638,37 +1568,14 @@                    y <- next                    d <- subV sym ty y x                    pure (x,d))-       return $ VStream $ IndexSeqMap $ \i -> do+       return $ VStream $ indexSeqMap $ \i -> do          (x,d) <- mxd          i' <- integerLit sym i          addV sym ty x =<< mulV sym ty d =<< intV sym i' ty  -- Shifting --------------------------------------------------- -barrelShifter :: Backend sym =>-  sym ->-  (SeqMap sym -> Integer -> SEval sym (SeqMap sym))-     {- ^ concrete shifting operation -} ->-  SeqMap sym  {- ^ initial value -} ->-  [SBit sym]  {- ^ bits of shift amount, in big-endian order -} ->-  SEval sym (SeqMap sym)-barrelShifter sym shift_op = go-  where-  go x [] = return x -  go x (b:bs)-    | Just True <- bitAsLit sym b-    = do x_shft <- shift_op x (2 ^ length bs)-         go x_shft bs--    | Just False <- bitAsLit sym b-    = do go x bs--    | otherwise-    = do x_shft <- shift_op x (2 ^ length bs)-         x' <- memoMap sym (mergeSeqMap sym b x_shft x)-         go x' bs- {-# INLINE shiftLeftReindex #-} shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer shiftLeftReindex sz i shft =@@ -1695,30 +1602,8 @@      Inf -> evalPanic "cannot rotate infinite sequence" []      Nat n -> Just ((i+n-shft) `mod` n) --- | 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' ->-  TValue ->-  SInteger sym ->-  SEval sym [SBit sym]-enumerateIntBits sym (Nat n) _ idx = enumerateIntBits' sym n idx-enumerateIntBits _sym Inf _ _ = liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer shifting")) --- | 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 [SBit sym]-enumerateIntBits' sym n idx =-  do w <- wordFromInt sym (widthInteger n) idx-     unpackWord sym w-+{-# INLINE logicShift #-} -- | Generic implementation of shifting. --   Uses the provided word-level operation to perform the shift, when --   possible.  Otherwise falls back on a barrel shifter that uses@@ -1749,16 +1634,19 @@   PFun     \y ->   PPrim     do xs' <- xs-       y' <- asIndex sym "shift" ix =<< y+       y' <- asIndex sym "shift" ix <$> y        case y' of          Left int_idx ->            do pneg <- intLessThan sym int_idx =<< integerLit sym 0               iteValue sym pneg-                (intShifter sym nm wopNeg reindexNeg m ix a xs' =<< shrinkRange sym m ix =<< intNegate sym int_idx)-                (intShifter sym nm wopPos reindexPos m ix a xs' =<< shrinkRange sym m ix int_idx)+                (intShifter sym nm wopNeg reindexNeg m a xs' =<< shrinkRange sym m ix =<< intNegate sym int_idx)+                (intShifter sym nm wopPos reindexPos m a xs' =<< shrinkRange sym m ix int_idx)          Right idx ->            wordShifter sym nm wopPos reindexPos m a xs' idx +++{-# INLINE intShifter #-} intShifter :: Backend sym =>    sym ->    String ->@@ -1766,36 +1654,18 @@    (Nat' -> Integer -> Integer -> Maybe Integer) ->    Nat' ->    TValue ->-   TValue ->    GenValue sym ->    SInteger sym ->    SEval sym (GenValue sym)-intShifter sym nm wop reindex m ix a xs idx =-   do let shiftOp vs shft =-              memoMap sym $ IndexSeqMap $ \i ->-                case reindex m i shft of-                  Nothing -> zeroV sym a-                  Just i' -> lookupSeqMap vs i'-      case xs of-        VWord w x ->-           return $ VWord w $ do-             x >>= \case-               WordVal x' -> WordVal <$> (wop x' =<< wordFromInt sym w idx)-               LargeBitsVal n bs0 ->-                 do idx_bits <- enumerateIntBits sym m ix idx-                    LargeBitsVal n <$> barrelShifter sym shiftOp bs0 idx_bits--        VSeq w vs0 ->-           do idx_bits <- enumerateIntBits sym m ix idx-              VSeq w <$> barrelShifter sym shiftOp vs0 idx_bits--        VStream vs0 ->-           do idx_bits <- enumerateIntBits sym m ix idx-              VStream <$> barrelShifter sym shiftOp vs0 idx_bits--        _ -> evalPanic "expected sequence value in shift operation" [nm]+intShifter sym nm wop reindex m a xs idx =+  case xs of+    VWord w x  -> VWord w <$> shiftWordByInteger sym wop (reindex m) x idx+    VSeq w vs  -> VSeq w  <$> shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx+    VStream vs -> VStream <$> shiftSeqByInteger sym (mergeValue sym) (reindex m) (zeroV sym a) m vs idx+    _ -> evalPanic "expected sequence value in shift operation" [nm]  +{-# INLINE wordShifter #-} wordShifter :: Backend sym =>    sym ->    String ->@@ -1807,31 +1677,15 @@    WordValue sym ->    SEval sym (GenValue sym) wordShifter sym nm wop reindex m a xs idx =-  let shiftOp vs shft =-          memoMap sym $ IndexSeqMap $ \i ->-            case reindex m i shft of-              Nothing -> zeroV sym a-              Just i' -> lookupSeqMap vs i'-   in case xs of-        VWord w x ->-           return $ VWord w $ do-             x >>= \case-               WordVal x' -> WordVal <$> (wop x' =<< asWordVal sym idx)-               LargeBitsVal n bs0 ->-                 do idx_bits <- enumerateWordValue sym idx-                    LargeBitsVal n <$> barrelShifter sym shiftOp bs0 idx_bits+  case xs of+    VWord w x  -> VWord w <$> shiftWordByWord sym wop (reindex m) x idx+    VSeq w vs  -> VSeq w  <$> shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) (Nat w) vs idx+    VStream vs -> VStream <$> shiftSeqByWord sym (mergeValue sym) (reindex m) (zeroV sym a) Inf     vs idx+    _ -> evalPanic "expected sequence value in shift operation" [nm] -        VSeq w vs0 ->-           do idx_bits <- enumerateWordValue sym idx-              VSeq w <$> barrelShifter sym shiftOp vs0 idx_bits -        VStream vs0 ->-           do idx_bits <- enumerateWordValue sym idx-              VStream <$> barrelShifter sym shiftOp vs0 idx_bits -        _ -> evalPanic "expected sequence value in shift operation" [nm]--+{-# INLINE shiftShrink #-} shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym) shiftShrink _sym Inf _ x = return x shiftShrink sym (Nat w) _ x =@@ -1839,6 +1693,7 @@      p  <- intLessThan sym w' x      iteInteger sym p w' x +{-# INLINE rotateShrink #-} rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym) rotateShrink _sym Inf _ _ = panic "rotateShrink" ["expected finite sequence in rotate"] rotateShrink sym (Nat 0) _ _ = integerLit sym 0@@ -1846,6 +1701,30 @@   do w' <- integerLit sym w      intMod sym x w' +{-# INLINE sshrV #-}+sshrV :: Backend sym => sym -> Prim sym+sshrV sym =+  PFinPoly \n ->+  PTyPoly  \ix ->+  PWordFun \x ->+  PStrict  \y ->+  PPrim $+    case asIndex sym ">>$" ix y of+       Left i ->+         do pneg <- intLessThan sym i =<< integerLit sym 0+            VWord n <$> mergeWord' sym+              pneg+              (do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i+                  amt <- wordFromInt sym n i'+                  wordVal <$> wordShiftLeft sym x amt)+              (do i' <- shiftShrink sym (Nat n) ix i+                  amt <- wordFromInt sym n i'+                  wordVal <$> wordSignedShiftRight sym x amt)++       Right wv ->+         do amt <- asWordVal sym wv+            VWord n . wordVal <$> wordSignedShiftRight sym x amt+ -- Miscellaneous ---------------------------------------------------------------  {-# SPECIALIZE errorV ::@@ -1860,38 +1739,9 @@   TValue ->   String ->   SEval sym (GenValue sym)-errorV sym ty0 msg =-     do stk <- sGetCallStack sym-        loop stk ty0-  where-  err stk = sWithCallStack sym stk (cryUserError sym msg)--  loop stk = \case-       TVBit -> err stk-       TVInteger -> err stk-       TVIntMod _ -> err stk-       TVRational -> err stk-       TVArray{} -> err stk-       TVFloat {} -> err stk--       -- sequences-       TVSeq w ety-          | isTBit ety -> return $ VWord w $ return $ LargeBitsVal w $ IndexSeqMap $ \_ -> err stk-          | otherwise  -> return $ VSeq w $ IndexSeqMap $ \_ -> loop stk ety--       TVStream ety -> return $ VStream $ IndexSeqMap $ \_ -> loop stk ety--       -- functions-       TVFun _ bty -> lam sym (\ _ -> loop stk bty)--       -- tuples-       TVTuple tys -> return $ VTuple (map (\t -> loop stk t) tys)--       -- records-       TVRec fields -> return $ VRecord $ fmap (\t -> loop stk t) $ fields--       TVAbstract {} -> err stk-       TVNewtype {} -> err stk+errorV sym _ty msg =+  do stk <- sGetCallStack sym+     sWithCallStack sym stk (cryUserError sym msg)  {-# INLINE valueToChar #-} @@ -1900,7 +1750,7 @@ --   Otherwise, return a '?' character valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char valueToChar sym (VWord 8 wval) =-  do w <- asWordVal sym =<< wval+  do w <- asWordVal sym wval      pure $! fromMaybe '?' (wordAsChar sym w) valueToChar _ _ = evalPanic "valueToChar" ["Not an 8-bit bitvector"] @@ -1910,90 +1760,7 @@ valueToString sym (VSeq n vals) = traverse (valueToChar sym =<<) (enumerateSeqMap n vals) valueToString _ _ = evalPanic "valueToString" ["Not a finite sequence"] --- Merge and if/then/else -{-# INLINE iteValue #-}-iteValue :: Backend sym =>-  sym ->-  SBit sym ->-  SEval sym (GenValue sym) ->-  SEval sym (GenValue sym) ->-  SEval sym (GenValue sym)-iteValue sym b x y-  | Just True  <- bitAsLit sym b = x-  | Just False <- bitAsLit sym b = y-  | otherwise = mergeValue' sym b x y--{-# INLINE mergeWord #-}-mergeWord :: Backend sym =>-  sym ->-  SBit sym ->-  WordValue sym ->-  WordValue sym ->-  SEval sym (WordValue sym)-mergeWord sym c (WordVal w1) (WordVal w2) =-  WordVal <$> iteWord sym c w1 w2-mergeWord sym c w1 w2 =-  LargeBitsVal (wordValueSize sym w1) <$> memoMap sym (mergeSeqMap sym c (asBitsMap sym w1) (asBitsMap sym w2))--{-# INLINE mergeWord' #-}-mergeWord' :: Backend sym =>-  sym ->-  SBit sym ->-  SEval sym (WordValue sym) ->-  SEval sym (WordValue sym) ->-  SEval sym (WordValue sym)-mergeWord' sym = mergeEval sym (mergeWord sym)--{-# INLINE mergeValue' #-}-mergeValue' :: Backend sym =>-  sym ->-  SBit sym ->-  SEval sym (GenValue sym) ->-  SEval sym (GenValue sym) ->-  SEval sym (GenValue sym)-mergeValue' sym = mergeEval sym (mergeValue sym)--mergeValue :: Backend sym =>-  sym ->-  SBit sym ->-  GenValue sym ->-  GenValue sym ->-  SEval sym (GenValue sym)-mergeValue sym c v1 v2 =-  case (v1, v2) of-    (VRecord fs1 , VRecord fs2 ) ->-      do let res = zipRecords (\_lbl -> mergeValue' sym c) fs1 fs2-         case res of-           Left f -> panic "Cryptol.Eval.Generic" [ "mergeValue: incompatible record values", show f ]-           Right r -> pure (VRecord r)-    (VTuple vs1  , VTuple vs2  ) | length vs1 == length vs2  ->-                                  pure $ VTuple $ zipWith (mergeValue' sym c) vs1 vs2-    (VBit b1     , VBit b2     ) -> VBit <$> iteBit sym c b1 b2-    (VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2-    (VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2-    (VFloat f1   , VFloat f2)    -> VFloat <$> iteFloat sym c f1 f2-    (VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> pure $ VWord n1 $ mergeWord' sym c w1 w2-    (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (mergeSeqMap sym c vs1 vs2)-    (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym (mergeSeqMap sym c vs1 vs2)-    (f1@VFun{}   , f2@VFun{}   ) -> lam sym $ \x -> mergeValue' sym c (fromVFun sym f1 x) (fromVFun sym f2 x)-    (f1@VPoly{}  , f2@VPoly{}  ) -> tlam sym $ \x -> mergeValue' sym c (fromVPoly sym f1 x) (fromVPoly sym f2 x)-    (_           , _           ) -> panic "Cryptol.Eval.Generic"-                                  [ "mergeValue: incompatible values" ]--{-# INLINE mergeSeqMap #-}-mergeSeqMap :: Backend sym =>-  sym ->-  SBit sym ->-  SeqMap sym ->-  SeqMap sym ->-  SeqMap sym-mergeSeqMap sym c x y =-  IndexSeqMap $ \i ->-    iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)--- foldlV :: Backend sym => sym -> Prim sym foldlV sym =   PNumPoly \_n ->@@ -2005,7 +1772,7 @@   PPrim     case v of       VSeq n m    -> go0 f z (enumerateSeqMap n m)-      VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym =<< wv)+      VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv)       _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"]   where   go0 _f a [] = a@@ -2029,7 +1796,7 @@   PPrim     case v of       VSeq n m    -> go0 f z (enumerateSeqMap n m)-      VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym =<< wv)+      VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym wv)       _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"]   where   go0 _f a [] = a@@ -2081,9 +1848,9 @@        xs' <- xs        case xs' of           VWord n w ->-            do m <- asBitsMap sym <$> w-               m' <- sparkParMap sym f' n m-               pure (VWord n (pure (LargeBitsVal n m')))+            do let m = asBitsMap sym w+               m' <- sparkParMap sym (\x -> f' (VBit <$> x)) n m+               VWord n <$> (bitmapWordVal sym n (fromVBit <$> m'))           VSeq n m ->             VSeq n <$> sparkParMap sym f' n m @@ -2093,12 +1860,12 @@ sparkParMap ::   Backend sym =>   sym ->-  (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) ->+  (SEval sym a -> SEval sym (GenValue sym)) ->   Integer ->-  SeqMap sym ->-  SEval sym (SeqMap sym)+  SeqMap sym a ->+  SEval sym (SeqMap sym (GenValue sym)) sparkParMap sym f n m =-  finiteSeqMap <$> mapM (sSpark sym . g) (enumerateSeqMap n m)+  finiteSeqMap sym <$> mapM (sSpark sym . g) (enumerateSeqMap n m)  where  g x =    do z <- sDelay sym (f x)@@ -2149,9 +1916,8 @@     , "fpPosInf"    ~> fpConst (fpPosInf sym)     , "fpFromBits"  ~> PFinPoly \e -> PFinPoly \p -> PWordFun \w ->                        PPrim (VFloat <$> fpFromBits sym e p w)-    , "fpToBits"    ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PVal-                            $ VWord (e+p)-                            $ WordVal <$> fpToBits sym x+    , "fpToBits"    ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PPrim+                            (VWord (e+p) . wordVal <$> fpToBits sym x)     , "=.="         ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y ->                        PPrim (VBit <$> fpLogicalEq sym x y) @@ -2272,6 +2038,9 @@                     unary (roundToEvenV sym))      -- Bitvector specific operations+  , ("toSignedInteger"+                  , {-# SCC "Prelude::toSignedInteger" #-}+                    toSignedIntegerV sym)   , ("/$"         , {-# SCC "Prelude::(/$)" #-}                     sdivV sym)   , ("%$"         , {-# SCC "Prelude::(%$)" #-}@@ -2308,6 +2077,20 @@                   , {-# SCC "Prelude::fromToLessThan" #-}                     fromToLessThanV sym) +  , ("fromToBy"   , {-# SCC "Prelude::fromToBy" #-}+                    fromToByV sym)++  , ("fromToByLessThan",+                    {-# SCC "Prelude::fromToByLessThan" #-}+                    fromToByLessThanV sym)++  , ("fromToDownBy", {-# SCC "Prelude::fromToDownBy" #-}+                     fromToDownByV sym)++  , ("fromToDownByGreaterThan"+                  , {-# SCC "Prelude::fromToDownByGreaterThan" #-}+                    fromToDownByGreaterThanV sym)+     -- Sequence manipulations   , ("#"          , {-# SCC "Prelude::(#)" #-}                     PFinPoly \front ->@@ -2315,37 +2098,69 @@                     PTyPoly  \elty  ->                     PFun \l ->                     PFun \r ->-                    PPrim (join (ccatV sym (Nat front) back elty <$> l <*> r)))+                    PPrim $ ccatV sym front back elty l r)    , ("join"       , {-# SCC "Prelude::join" #-}                     PNumPoly \parts ->                     PFinPoly \each  ->                     PTyPoly  \a     ->-                    PStrict  \x   ->+                    PFun     \x   ->                     PPrim $ joinV sym parts each a x)    , ("split"      , {-# SCC "Prelude::split" #-}-                    ecSplitV sym)+                    PNumPoly \parts ->+                    PFinPoly \each ->+                    PTyPoly  \a ->+                    PFun     \val ->+                    PPrim $ splitV sym parts each a val) -  , ("splitAt"    , {-# SCC "Prelude::splitAt" #-}+  , ("take"       , {-# SCC "Preldue::take" #-}                     PNumPoly \front ->-                    PNumPoly \back  ->-                    PTyPoly  \a     ->-                    PStrict  \x   ->-                    PPrim $ splitAtV sym front back a x)+                    PNumPoly \back ->+                    PTyPoly  \a ->+                    PFun     \xs ->+                    PPrim $ takeV sym front back a xs) +  , ("drop"       , {-# SCC "Preldue::drop" #-}+                    PFinPoly \front ->+                    PNumPoly \back ->+                    PTyPoly  \a ->+                    PFun     \xs ->+                    PPrim $ dropV sym front back a xs)+   , ("reverse"    , {-# SCC "Prelude::reverse" #-}-                    PFinPoly \_a ->-                    PTyPoly  \_b ->-                    PStrict  \xs ->-                    PPrim $ reverseV sym xs)+                    PFinPoly \a ->+                    PTyPoly  \b ->+                    PFun     \xs ->+                    PPrim $ reverseV sym a b xs)    , ("transpose"  , {-# SCC "Prelude::transpose" #-}                     PNumPoly \a ->                     PNumPoly \b ->                     PTyPoly  \c ->-                    PStrict  \xs ->-                    PPrim $ transposeV sym a b c xs)+                    PFun     \xs ->+                    PPrim $ transposeV sym a b c =<< xs)++    -- Shifts and rotates+  , ("<<"         , {-# SCC "Prelude::(<<)" #-}+                    logicShift sym "<<" shiftShrink+                      (wordShiftLeft sym) (wordShiftRight sym)+                      shiftLeftReindex shiftRightReindex)+  , (">>"         , {-# SCC "Prelude::(>>)" #-}+                    logicShift sym ">>"  shiftShrink+                      (wordShiftRight sym) (wordShiftLeft sym)+                      shiftRightReindex shiftLeftReindex)+  , ("<<<"        , {-# SCC "Prelude::(<<<)" #-}+                    logicShift sym "<<<" rotateShrink+                      (wordRotateLeft sym) (wordRotateRight sym)+                      rotateLeftReindex rotateRightReindex)+  , (">>>"        , {-# SCC "Prelude::(>>>)" #-}+                    logicShift sym ">>>" rotateShrink+                      (wordRotateRight sym) (wordRotateLeft sym)+                      rotateRightReindex rotateLeftReindex)++  , (">>$"        , {-# SCC "Prelude::(>>$)" #-}+                    sshrV sym)      -- Misc 

@@ -251,7 +251,7 @@ > instance Semigroup Env where >   l <> r = Env >     { envVars  = envVars  l <> envVars  r->     , envTypes = envTypes l <> envTypes r +>     , envTypes = envTypes l <> envTypes r >     } > > instance Monoid Env where@@ -523,7 +523,7 @@ that consumes and ignores its type arguments.  > evalNewtypeDecl :: Env -> Newtype -> Env-> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env +> evalNewtypeDecl env nt = bindVar (ntName nt, pure val) env >   where >     val = foldr tabs con (ntParams nt) >     con = VFun (\x -> x)@@ -541,7 +541,7 @@ > evalPrim :: Name -> Value > evalPrim n >   | Just i <- asPrim n, Just v <- Map.lookup i primTable = v->   | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show n]+>   | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show (pp n)]  Cryptol primitives fall into several groups, mostly delineated by corresponding type classes:@@ -560,13 +560,15 @@  * Comparison: `<`, `>`, `<=`, `>=`, `==`, `!=` -* Sequences: `#`, `join`, `split`, `splitAt`, `reverse`, `transpose`+* Sequences: `#`, `join`, `split`, `take`, `drop`, `reverse`, `transpose`  * Shifting: `<<`, `>>`, `<<<`, `>>>`  * Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd` -* Enumerations: `fromTo`, `fromThenTo`, `infFrom`, `infFromThen`+* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `fromToBy`,+                `fromToByLessThan`, `fromToDownBy`, `fromToDownByGreaterThan`,+                `infFrom`, `infFromThen`  * Polynomials: `pmult`, `pdiv`, `pmod` @@ -734,17 +736,21 @@ >                           do vs <- fromVList <$> val >                              indexFront (nMul parts (Nat each)) vs (i * each + j) >->   , "splitAt"    ~> vFinPoly $ \front -> pure $+>   , "take"       ~> VNumPoly $ \front -> pure $+>                     VNumPoly $ \back  -> pure $+>                     VPoly    $ \_a    -> pure $+>                     VFun     $ \v ->+>                       pure $ generateV front $ \i ->+>                                do vs <- fromVList <$> v+>                                   indexFront (nAdd front back) vs i+>+>   , "drop"       ~> vFinPoly $ \front -> pure $ >                     VNumPoly $ \back -> pure $ >                     VPoly $ \_a -> pure $ >                     VFun $ \v ->->                       let xs = pure $ generateV (Nat front) $ \i ->->                                  do vs <- fromVList <$> v->                                     indexFront (nAdd (Nat front) back) vs i->                           ys = pure $ generateV back $ \i ->->                                  do vs <- fromVList <$> v->                                     indexFront (nAdd (Nat front) back) vs (front+i)->                        in pure (VTuple [ xs, ys ])+>                       pure $ generateV back $ \i ->+>                                do vs <- fromVList <$> v+>                                   indexFront (nAdd (Nat front) back) vs (front+i) > >   , "reverse"    ~> vFinPoly $ \n -> pure $ >                     VPoly $ \_a -> pure $@@ -778,18 +784,71 @@ >   -- Enumerations >   , "fromTo"     ~> vFinPoly $ \first -> pure $ >                     vFinPoly $ \lst   -> pure $->                     VPoly    $ \ty  ->->                     let f i = literal i ty->                     in pure (VList (Nat (1 + lst - first)) (map f [first .. lst]))+>                     VPoly    $ \ty    -> pure $+>                     let f i = literal i ty in+>                     VList (Nat (1 + lst - first)) (map f [first .. lst]) >+>   , "fromToLessThan" ~>+>                     vFinPoly $ \first -> pure $+>                     VNumPoly $ \bound -> pure $+>                     VPoly    $ \ty    -> pure $+>                     let f i = literal i ty in+>                     case bound of+>                       Inf -> VList Inf (map f [first ..])+>                       Nat bound' ->+>                         let len = bound' - first in+>                         VList (Nat len) (map f (genericTake len [first ..]))+>+>   , "fromToBy"   ~> vFinPoly $ \first  -> pure $+>                     vFinPoly $ \lst    -> pure $+>                     vFinPoly $ \stride -> pure $+>                     VPoly    $ \ty     -> pure $+>                     let f i = literal i ty in+>                     let vs  = [ f (first + i*stride) | i <- [0..] ] in+>                     let len = 1 + ((lst-first) `div` stride) in+>                     VList (Nat len) (genericTake len vs)+>+>   , "fromToByLessThan" ~>+>                     vFinPoly $ \first  -> pure $+>                     VNumPoly $ \bound  -> pure $+>                     vFinPoly $ \stride -> pure $+>                     VPoly    $ \ty     -> pure $+>                     let f i = literal i ty in+>                     let vs  = [ f (first + i*stride) | i <- [0..] ] in+>                     case bound of+>                       Inf -> VList Inf vs+>                       Nat bound' ->+>                         let len = (bound'-first+stride-1) `div` stride in+>                         VList (Nat len) (genericTake len vs)+>+>   , "fromToDownBy" ~>+>                     vFinPoly $ \first  -> pure $+>                     vFinPoly $ \lst    -> pure $+>                     vFinPoly $ \stride -> pure $+>                     VPoly    $ \ty     -> pure $+>                     let f i = literal i ty in+>                     let vs  = [ f (first - i*stride) | i <- [0..] ] in+>                     let len = 1 + ((first-lst) `div` stride) in+>                     VList (Nat len) (genericTake len vs)+>+>   , "fromToDownByGreaterThan" ~>+>                     vFinPoly $ \first  -> pure $+>                     vFinPoly $ \lst    -> pure $+>                     vFinPoly $ \stride -> pure $+>                     VPoly    $ \ty     -> pure $+>                     let f i = literal i ty in+>                     let vs  = [ f (first - i*stride) | i <- [0..] ] in+>                     let len = (first-lst+stride-1) `div` stride in+>                     VList (Nat len) (genericTake len vs)+> >   , "fromThenTo" ~> vFinPoly $ \first -> pure $ >                     vFinPoly $ \next  -> pure $ >                     vFinPoly $ \_lst  -> pure $ >                     VPoly    $ \ty    -> pure $->                     vFinPoly $ \len   ->->                     let f i = literal i ty->                     in pure (VList (Nat len)->                               (map f (genericTake len [first, next ..])))+>                     vFinPoly $ \len   -> pure $+>                     let f i = literal i ty in+>                     VList (Nat len)+>                           (map f (genericTake len [first, next ..])) > >   , "infFrom"    ~> VPoly $ \ty -> pure $ >                     VFun $ \first ->@@ -1711,11 +1770,10 @@ >           case traverse isBit vs of >             Just bs -> ppBV opts (mkBv n (bitsToInteger bs)) >             Nothing -> ppList (map (ppEValue opts) vs)->       where ppList docs = brackets (fsep (punctuate comma docs))->             isBit v = case v of Value (VBit b) -> Just b+>       where isBit v = case v of Value (VBit b) -> Just b >                                 _      -> Nothing->     VTuple vs  -> parens (sep (punctuate comma (map (ppEValue opts) vs)))->     VRecord fs -> braces (sep (punctuate comma (map ppField fs)))+>     VTuple vs  -> ppTuple (map (ppEValue opts) vs)+>     VRecord fs -> ppRecord (map ppField fs) >       where ppField (f,r) = pp f <+> char '=' <+> ppEValue opts r >     VFun _     -> text "<function>" >     VPoly _    -> text "<polymorphic value>"@@ -1732,7 +1790,7 @@ > evaluate expr minp = return (Right (val, modEnv), []) >   where >     modEnv = M.minpModuleEnv minp->     extDgs = concatMap mDecls (M.loadedModules modEnv)+>     extDgs = concatMap mDecls (M.loadedModules modEnv) ++ M.deDecls (M.meDynEnv modEnv) >     nts    = Map.elems (M.loadedNewtypes modEnv) >     env    = foldl evalDeclGroup (foldl evalNewtypeDecl mempty nts) extDgs >     val    = evalExpr env expr

@@ -23,21 +23,22 @@  import qualified Control.Exception as X import           Control.Monad.IO.Class (MonadIO(..))-import           Data.Bits (bit, shiftL) import qualified Data.Map as Map import qualified Data.Text as T  import Data.SBV.Dynamic as SBV  import Cryptol.Backend-import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )+import Cryptol.Backend.Monad (Unsupported(..), EvalError(..) ) import Cryptol.Backend.SBV+import Cryptol.Backend.SeqMap+import Cryptol.Backend.WordValue  import Cryptol.Eval.Type (TValue(..)) import Cryptol.Eval.Generic import Cryptol.Eval.Prims import Cryptol.Eval.Value-import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)+import Cryptol.TypeCheck.Solver.InfNat (Nat'(..)) import Cryptol.Utils.Ident  -- Values ----------------------------------------------------------------------@@ -52,36 +53,9 @@   Map.union (genericPrimTable sym getEOpts) $   Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v)) -  [ (">>$"         , sshrV sym)--    -- Shifts and rotates-  , ("<<"          , logicShift sym "<<"-                       shiftShrink-                       (\x y -> pure (shl x y))-                       (\x y -> pure (lshr x y))-                       shiftLeftReindex shiftRightReindex)--  , (">>"          , logicShift sym ">>"-                       shiftShrink-                       (\x y -> pure (lshr x y))-                       (\x y -> pure (shl x y))-                       shiftRightReindex shiftLeftReindex)--  , ("<<<"         , logicShift sym "<<<"-                       rotateShrink-                       (\x y -> pure (SBV.svRotateLeft x y))-                       (\x y -> pure (SBV.svRotateRight x y))-                       rotateLeftReindex rotateRightReindex)--  , (">>>"         , logicShift sym ">>>"-                       rotateShrink-                       (\x y -> pure (SBV.svRotateRight x y))-                       (\x y -> pure (SBV.svRotateLeft x y))-                       rotateRightReindex rotateLeftReindex)--    -- Indexing and updates-  , ("@"           , indexPrim sym (indexFront sym) (indexFront_bits sym) (indexFront sym))-  , ("!"           , indexPrim sym (indexBack sym) (indexBack_bits sym) (indexBack sym))+  [ -- Indexing and updates+    ("@"           , indexPrim sym IndexForward  (indexFront sym) (indexFront_segs sym))+  , ("!"           , indexPrim sym IndexBackward (indexFront sym) (indexFront_segs sym))    , ("update"      , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))   , ("updateEnd"   , updatePrim sym (updateBackSym_word sym) (updateBackSym sym))@@ -92,7 +66,7 @@   SBV ->   Nat' ->   TValue ->-  SeqMap SBV ->+  SeqMap SBV (GenValue SBV) ->   TValue ->   SVal ->   SEval SBV Value@@ -102,125 +76,77 @@    | Nat n <- mblen   , TVSeq wlen TVBit <- a-  = do wvs <- traverse (fromWordVal "indexFront" =<<) (enumerateSeqMap n xs)-       case asWordList wvs of+  = do wvs <- traverse (fromWordVal "indexFront" <$>) (enumerateSeqMap n xs)+       asWordList sym wvs >>= \case          Just ws ->            do z <- wordLit sym wlen 0-              return $ VWord wlen $ pure $ WordVal $ SBV.svSelect ws z idx-         Nothing -> folded+              return $ VWord wlen $ wordVal $ SBV.svSelect ws z idx+         Nothing -> folded' -  | otherwise-  = folded+  | otherwise = folded' +  where     k = SBV.kindOf idx-    def = zeroV sym a-    f n y = iteValue sym (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y++    f n (Just y) = Just $ iteValue sym (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y+    f n Nothing  = Just $ lookupSeqMap xs n++    folded' =+      case folded of+        Nothing -> raiseError sym (InvalidIndex Nothing)+        Just m  -> m+     folded =       case k of         KBounded _ w ->           case mblen of-            Nat n | n < 2^w -> foldr f def [0 .. n-1]-            _ -> foldr f def [0 .. 2^w - 1]+            Nat n | n < 2^w -> foldr f Nothing [0 .. n-1]+            _ -> foldr f Nothing [0 .. 2^w - 1]         _ ->           case mblen of-            Nat n -> foldr f def [0 .. n-1]-            Inf -> liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))--indexBack ::-  SBV ->-  Nat' ->-  TValue ->-  SeqMap SBV ->-  TValue ->-  SWord SBV ->-  SEval SBV Value-indexBack sym (Nat n) a xs ix idx = indexFront sym (Nat n) a (reverseSeqMap n xs) ix idx-indexBack _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack"]--indexFront_bits ::-  SBV ->-  Nat' ->-  TValue ->-  SeqMap SBV ->-  TValue ->-  [SBit SBV] ->-  SEval SBV Value-indexFront_bits sym mblen _a xs _ix bits0 = go 0 (length bits0) bits0- where-  go :: Integer -> Int -> [SBit SBV] -> SEval SBV Value-  go i _k []-    -- For indices out of range, fail-    | Nat n <- mblen-    , i >= n-    = raiseError sym (InvalidIndex (Just i))--    | otherwise-    = lookupSeqMap xs i--  go i k (b:bs)-    -- Fail early when all possible indices we could compute from here-    -- are out of bounds-    | Nat n <- mblen-    , (i `shiftL` k) >= n-    = raiseError sym (InvalidIndex Nothing)--    | otherwise-    = iteValue sym b-         (go ((i `shiftL` 1) + 1) (k-1) bs)-         (go  (i `shiftL` 1)      (k-1) bs)-+            Nat n -> foldr f Nothing [0 .. n-1]+            Inf -> Just (liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))) -indexBack_bits ::+indexFront_segs ::   SBV ->   Nat' ->   TValue ->-  SeqMap SBV ->+  SeqMap SBV (GenValue SBV) ->   TValue ->-  [SBit SBV] ->+  Integer ->+  [IndexSegment SBV] ->   SEval SBV Value-indexBack_bits sym (Nat n) a xs ix idx = indexFront_bits sym (Nat n) a (reverseSeqMap n xs) ix idx-indexBack_bits _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"]-+indexFront_segs sym mblen a xs ix _idx_bits [WordIndexSegment w] =+  indexFront sym mblen a xs ix w --- | Compare a symbolic word value with a concrete integer.-wordValueEqualsInteger :: SBV -> WordValue SBV -> Integer -> SEval SBV (SBit SBV)-wordValueEqualsInteger sym wv i-  | wordValueSize sym wv < widthInteger i = return SBV.svFalse-  | otherwise =-    case wv of-      WordVal w -> return $ SBV.svEqual w (literalSWord (SBV.intSizeOf w) i)-      _ -> bitsAre i <$> enumerateWordValueRev sym wv -- little-endian+indexFront_segs sym mblen _a xs _ix idx_bits segs =+  do xs' <- barrelShifter sym (mergeValue sym) shiftOp mblen xs idx_bits segs+     lookupSeqMap xs' 0   where-    bitsAre :: Integer -> [SBit SBV] -> SBit SBV-    bitsAre n [] = SBV.svBool (n == 0)-    bitsAre n (b : bs) = SBV.svAnd (bitIs (odd n) b) (bitsAre (n `div` 2) bs)--    bitIs :: Bool -> SBit SBV -> SBit SBV-    bitIs b x = if b then x else SBV.svNot x+    shiftOp vs amt = pure (indexSeqMap (\i -> lookupSeqMap vs $! amt+i))   updateFrontSym ::   SBV ->   Nat' ->   TValue ->-  SeqMap SBV ->+  SeqMap SBV (GenValue SBV) ->   Either (SInteger SBV) (WordValue SBV) ->   SEval SBV (GenValue SBV) ->-  SEval SBV (SeqMap SBV)+  SEval SBV (SeqMap SBV (GenValue SBV)) updateFrontSym sym _len _eltTy vs (Left idx) val =   case SBV.svAsInteger idx of     Just i -> return $ updateSeqMap vs i val-    Nothing -> return $ IndexSeqMap $ \i ->+    Nothing -> return $ indexSeqMap $ \i ->       do b <- intEq sym idx =<< integerLit sym i          iteValue sym b val (lookupSeqMap vs i)  updateFrontSym sym _len _eltTy vs (Right wv) val =-  case wv of-    WordVal w | Just j <- SBV.svAsInteger w ->-      return $ updateSeqMap vs j val-    _ ->-      return $ IndexSeqMap $ \i ->+  wordValAsLit sym wv >>= \case+   Just j -> return $ updateSeqMap vs j val+   Nothing ->+      return $ indexSeqMap $ \i ->       do b <- wordValueEqualsInteger sym wv i          iteValue sym b val (lookupSeqMap vs i) @@ -234,56 +160,35 @@   SEval SBV (WordValue SBV) updateFrontSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_bits"] -updateFrontSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =-  LargeBitsVal n <$> updateFrontSym sym (Nat n) eltTy bv idx val--updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =+updateFrontSym_word sym (Nat n) _eltTy w (Left idx) val =   do idx' <- wordFromInt sym n idx-     updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val--updateFrontSym_word sym (Nat n) eltTy bv (Right wv) val =-  case wv of-    WordVal idx-      | Just j <- SBV.svAsInteger idx ->-          updateWordValue sym bv j (fromVBit <$> val)--      | WordVal bw <- bv ->-        WordVal <$>-          do b <- fromVBit <$> val-             let sz   = SBV.intSizeOf bw-             let z    = literalSWord sz 0-             let znot = SBV.svNot z-             let q    = SBV.svSymbolicMerge (SBV.kindOf bw) True b znot z-             let msk  = SBV.svShiftRight (literalSWord sz (bit (sz-1))) idx-             let bw'  = SBV.svAnd bw (SBV.svNot msk)-             return $! SBV.svXOr bw' (SBV.svAnd q msk)--    _ -> LargeBitsVal n <$> updateFrontSym sym (Nat n) eltTy (asBitsMap sym bv) (Right wv) val+     updateWordByWord sym IndexForward w (wordVal idx') (fromVBit <$> val)+updateFrontSym_word sym (Nat _n) _eltTy w (Right idx) val =+  updateWordByWord sym IndexForward w idx (fromVBit <$> val)   updateBackSym ::   SBV ->   Nat' ->   TValue ->-  SeqMap SBV ->+  SeqMap SBV (GenValue SBV) ->   Either (SInteger SBV) (WordValue SBV) ->   SEval SBV (GenValue SBV) ->-  SEval SBV (SeqMap SBV)+  SEval SBV (SeqMap SBV (GenValue SBV)) updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]  updateBackSym sym (Nat n) _eltTy vs (Left idx) val =   case SBV.svAsInteger idx of     Just i -> return $ updateSeqMap vs (n - 1 - i) val-    Nothing -> return $ IndexSeqMap $ \i ->+    Nothing -> return $ indexSeqMap $ \i ->       do b <- intEq sym idx =<< integerLit sym (n - 1 - i)          iteValue sym b val (lookupSeqMap vs i)  updateBackSym sym (Nat n) _eltTy vs (Right wv) val =-  case wv of-    WordVal w | Just j <- SBV.svAsInteger w ->-      return $ updateSeqMap vs (n - 1 - j) val-    _ ->-      return $ IndexSeqMap $ \i ->+  wordValAsLit sym wv >>= \case+    Just j -> return $ updateSeqMap vs (n - 1 - j) val+    Nothing ->+      return $ indexSeqMap $ \i ->       do b <- wordValueEqualsInteger sym wv (n - 1 - i)          iteValue sym b val (lookupSeqMap vs i) @@ -297,56 +202,9 @@   SEval SBV (WordValue SBV) updateBackSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym_bits"] -updateBackSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =-  LargeBitsVal n <$> updateBackSym sym (Nat n) eltTy bv idx val--updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =+updateBackSym_word sym (Nat n) _eltTy w (Left idx) val =   do idx' <- wordFromInt sym n idx-     updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val--updateBackSym_word sym (Nat n) eltTy bv (Right wv) val = do-  case wv of-    WordVal idx-      | Just j <- SBV.svAsInteger idx ->-          updateWordValue sym bv (n - 1 - j) (fromVBit <$> val)--      | WordVal bw <- bv ->-        WordVal <$>-          do b <- fromVBit <$> val-             let sz   = SBV.intSizeOf bw-             let z    = literalSWord sz 0-             let znot = SBV.svNot z-             let q    = SBV.svSymbolicMerge (SBV.kindOf bw) True b znot z-             let msk  = SBV.svShiftLeft (literalSWord sz 1) idx-             let bw'  = SBV.svAnd bw (SBV.svNot msk)-             return $! SBV.svXOr bw' (SBV.svAnd q msk)--    _ -> LargeBitsVal n <$> updateBackSym sym (Nat n) eltTy (asBitsMap sym bv) (Right wv) val---asWordList :: [WordValue SBV] -> Maybe [SWord SBV]-asWordList = go id- where go :: ([SWord SBV] -> [SWord SBV]) -> [WordValue SBV] -> Maybe [SWord SBV]-       go f [] = Just (f [])-       go f (WordVal x :vs) = go (f . (x:)) vs-       go _f (LargeBitsVal _ _ : _) = Nothing--sshrV :: SBV -> Prim SBV-sshrV sym =-  PNumPoly \n ->-  PTyPoly  \ix ->-  PWordFun \x ->-  PStrict  \y ->-  PPrim $-   asIndex sym ">>$" ix y >>= \case-     Left idx ->-       do let w = toInteger (SBV.intSizeOf x)-          let pneg = svLessThan idx (svInteger KUnbounded 0)-          zneg <- shl x  . svFromInteger w <$> shiftShrink sym n ix (SBV.svUNeg idx)-          zpos <- ashr x . svFromInteger w <$> shiftShrink sym n ix idx-          let z = svSymbolicMerge (kindOf x) True pneg zneg zpos-          return . VWord w . pure . WordVal $ z+     updateWordByWord sym IndexBackward w (wordVal idx') (fromVBit <$> val)+updateBackSym_word sym (Nat _n) _eltTy w (Right idx) val =+  updateWordByWord sym IndexBackward w idx (fromVBit <$> val) -     Right wv ->-       do z <- ashr x <$> asWordVal sym wv-          return . VWord (toInteger (SBV.intSizeOf x)) . pure . WordVal $ z

@@ -6,6 +6,7 @@ -- Stability   :  provisional -- Portability :  portable +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-}@@ -16,7 +17,6 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternGuards #-}-{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TupleSections #-}@@ -26,7 +26,6 @@ module Cryptol.Eval.Value   ( -- * GenericValue     GenValue(..)-  , forceWordValue   , forceValue   , Backend(..)   , asciiMode@@ -39,9 +38,6 @@   , tlam   , nlam   , ilam-  , toStream-  , toFinSeq-  , toSeq   , mkSeq     -- ** Value eliminators   , fromVBit@@ -64,59 +60,32 @@     -- ** Pretty printing   , defaultPPOpts   , ppValue--    -- * Sequence Maps-  , SeqMap (..)-  , lookupSeqMap-  , finiteSeqMap-  , infiniteSeqMap-  , enumerateSeqMap-  , streamSeqMap-  , reverseSeqMap-  , updateSeqMap-  , dropSeqMap-  , concatSeqMap-  , splitSeqMap-  , memoMap-  , zipSeqMap-  , mapSeqMap-  , largeBitSize-    -- * WordValue-  , WordValue(..)-  , asWordVal-  , asBitsMap-  , enumerateWordValue-  , enumerateWordValueRev-  , wordValueSize-  , indexWordValue-  , updateWordValue+    -- * Merge and if/then/else+  , iteValue+  , mergeValue   ) where -import Control.Monad.IO.Class-import Data.Bits-import Data.IORef-import Data.Map.Strict (Map) import Data.Ratio-import qualified Data.Map.Strict as Map-import MonadLib import Numeric (showIntAtBase)  import Cryptol.Backend+import Cryptol.Backend.SeqMap import qualified Cryptol.Backend.Arch as Arch import Cryptol.Backend.Monad   ( evalPanic, wordTooWide, CallStack, combineCallStacks ) import Cryptol.Backend.FloatHelpers (fpPP)+import Cryptol.Backend.WordValue+ import Cryptol.Eval.Type  import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))+ import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.Logger(Logger) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.PP import Cryptol.Utils.RecordMap -import Data.List(genericIndex)- import GHC.Generics (Generic)  -- | Some options for evalutaion@@ -127,186 +96,6 @@  -- Values ---------------------------------------------------------------------- --- | A sequence map represents a mapping from nonnegative integer indices---   to values.  These are used to represent both finite and infinite sequences.-data SeqMap sym-  = IndexSeqMap  !(Integer -> SEval sym (GenValue sym))-  | UpdateSeqMap !(Map Integer (SEval sym (GenValue sym)))-                 !(Integer -> SEval sym (GenValue sym))--lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)-lookupSeqMap (IndexSeqMap f) i = f i-lookupSeqMap (UpdateSeqMap m f) i =-  case Map.lookup i m of-    Just x  -> x-    Nothing -> f i---- | An arbitrarily-chosen number of elements where we switch from a dense---   sequence representation of bit-level words to 'SeqMap' representation.-largeBitSize :: Integer-largeBitSize = 1 `shiftL` 48---- | Generate a finite sequence map from a list of values-finiteSeqMap :: [SEval sym (GenValue sym)] -> SeqMap sym-finiteSeqMap xs =-   UpdateSeqMap-      (Map.fromList (zip [0..] xs))-      (\i -> panic "finiteSeqMap" ["Out of bounds access of finite seq map", "length: " ++ show (length xs), show i])---- | Generate an infinite sequence map from a stream of values-infiniteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)-infiniteSeqMap sym xs =-   -- TODO: use an int-trie?-   memoMap sym (IndexSeqMap $ \i -> genericIndex xs i)---- | Create a finite list of length @n@ of the values from @[0..n-1]@ in---   the given the sequence emap.-enumerateSeqMap :: (Integral n) => n -> SeqMap sym -> [SEval sym (GenValue sym)]-enumerateSeqMap n m = [ lookupSeqMap m  i | i <- [0 .. (toInteger n)-1] ]---- | Create an infinite stream of all the values in a sequence map-streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]-streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ]---- | Reverse the order of a finite sequence map-reverseSeqMap :: Integer     -- ^ Size of the sequence map-              -> SeqMap sym-              -> SeqMap sym-reverseSeqMap n vals = IndexSeqMap $ \i -> lookupSeqMap vals (n - 1 - i)--updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym-updateSeqMap (UpdateSeqMap m sm) i x = UpdateSeqMap (Map.insert i x m) sm-updateSeqMap (IndexSeqMap f) i x = UpdateSeqMap (Map.singleton i x) f---- | Concatenate the first @n@ values of the first sequence map onto the---   beginning of the second sequence map.-concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym-concatSeqMap n x y =-    IndexSeqMap $ \i ->-       if i < n-         then lookupSeqMap x i-         else lookupSeqMap y (i-n)---- | Given a number @n@ and a sequence map, return two new sequence maps:---   the first containing the values from @[0..n-1]@ and the next containing---   the values from @n@ onward.-splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)-splitSeqMap n xs = (hd,tl)-  where-  hd = xs-  tl = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)---- | Drop the first @n@ elements of the given 'SeqMap'.-dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym-dropSeqMap 0 xs = xs-dropSeqMap n xs = IndexSeqMap $ \i -> lookupSeqMap xs (i+n)---- | Given a sequence map, return a new sequence map that is memoized using---   a finite map memo table.-memoMap :: Backend sym => sym -> SeqMap sym -> SEval sym (SeqMap sym)-memoMap sym x = do-  stk <- sGetCallStack sym-  cache <- liftIO $ newIORef $ Map.empty-  return $ IndexSeqMap (memo cache stk)--  where-  memo cache stk i = do-    mz <- liftIO (Map.lookup i <$> readIORef cache)-    case mz of-      Just z  -> return z-      Nothing -> sWithCallStack sym stk (doEval cache i)--  doEval cache i = do-    v <- lookupSeqMap x i-    liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))-    return v---- | Apply the given evaluation function pointwise to the two given---   sequence maps.-zipSeqMap ::-  Backend sym =>-  sym ->-  (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->-  SeqMap sym ->-  SeqMap sym ->-  SEval sym (SeqMap sym)-zipSeqMap sym f x y =-  memoMap sym (IndexSeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i))---- | Apply the given function to each value in the given sequence map-mapSeqMap ::-  Backend sym =>-  sym ->-  (GenValue sym -> SEval sym (GenValue sym)) ->-  SeqMap sym -> SEval sym (SeqMap sym)-mapSeqMap sym f x =-  memoMap sym (IndexSeqMap $ \i -> f =<< lookupSeqMap x i)---- | For efficiency reasons, we handle finite sequences of bits as special cases---   in the evaluator.  In cases where we know it is safe to do so, we prefer to---   used a "packed word" representation of bit sequences.  This allows us to rely---   directly on Integer types (in the concrete evaluator) and SBV's Word types (in---   the symbolic simulator).------   However, if we cannot be sure all the bits of the sequence---   will eventually be forced, we must instead rely on an explicit sequence of bits---   representation.-data WordValue sym-  = WordVal !(SWord sym)                      -- ^ Packed word representation for bit sequences.-  | LargeBitsVal !Integer !(SeqMap sym)       -- ^ A large bitvector sequence, represented as a-                                            --   'SeqMap' of bits.- deriving (Generic)---- | Force a word value into packed word form-asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)-asWordVal _   (WordVal w)         = return w-asWordVal sym (LargeBitsVal n xs) = packWord sym =<< traverse (fromVBit <$>) (enumerateSeqMap n xs)---- | Force a word value into a sequence of bits-asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym-asBitsMap sym (WordVal w)  = IndexSeqMap $ \i -> VBit <$> (wordBit sym w i)-asBitsMap _   (LargeBitsVal _ xs) = xs---- | Turn a word value into a sequence of bits, forcing each bit.---   The sequence is returned in big-endian order.-enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]-enumerateWordValue sym (WordVal w) = unpackWord sym w-enumerateWordValue _ (LargeBitsVal n xs) = traverse (fromVBit <$>) (enumerateSeqMap n xs)---- | Turn a word value into a sequence of bits, forcing each bit.---   The sequence is returned in reverse of the usual order, which is little-endian order.-enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]-enumerateWordValueRev sym (WordVal w)  = reverse <$> unpackWord sym w-enumerateWordValueRev _   (LargeBitsVal n xs) = traverse (fromVBit <$>) (enumerateSeqMap n (reverseSeqMap n xs))---- | Compute the size of a word value-wordValueSize :: Backend sym => sym -> WordValue sym -> Integer-wordValueSize sym (WordVal w)  = wordLen sym w-wordValueSize _ (LargeBitsVal n _) = n---- | Select an individual bit from a word value-indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)-indexWordValue sym (WordVal w) idx-   | 0 <= idx && idx < wordLen sym w = wordBit sym w idx-   | otherwise = invalidIndex sym idx-indexWordValue sym (LargeBitsVal n xs) idx-   | 0 <= idx && idx < n = fromVBit <$> lookupSeqMap xs idx-   | otherwise = invalidIndex sym idx---- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the---   given bit value.-updateWordValue :: Backend sym =>-  sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)-updateWordValue sym (WordVal w) idx b-   | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx-   | isReady sym b = WordVal <$> (wordUpdate sym w idx =<< b)--updateWordValue sym wv idx b-   | 0 <= idx && idx < wordValueSize sym wv =-        pure $ LargeBitsVal (wordValueSize sym wv) $ updateSeqMap (asBitsMap sym wv) idx (VBit <$> b)-   | otherwise = invalidIndex sym idx-- -- | Generic value type, parameterized by bit and word types. -- --   NOTE: we maintain an important invariant regarding sequence types.@@ -320,21 +109,16 @@   | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @   | VRational !(SRational sym)                 -- ^ @ Rational @   | VFloat !(SFloat sym)-  | VSeq !Integer !(SeqMap sym)                -- ^ @ [n]a   @+  | VSeq !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a   @                                                --   Invariant: VSeq is never a sequence of bits-  | VWord !Integer !(SEval sym (WordValue sym))  -- ^ @ [n]Bit @-  | VStream !(SeqMap sym)                   -- ^ @ [inf]a @+  | VWord !Integer !(WordValue sym)            -- ^ @ [n]Bit @+  | VStream !(SeqMap sym (GenValue sym))       -- ^ @ [inf]a @   | VFun  CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions   | VPoly CallStack (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)   | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)  deriving Generic  --- | Force the evaluation of a word value-forceWordValue :: Backend sym => WordValue sym -> SEval sym ()-forceWordValue (WordVal w)  = seq w (return ())-forceWordValue (LargeBitsVal n xs) = mapM_ (\x -> const () <$> x) (enumerateSeqMap n xs)- -- | Force the evaluation of a value forceValue :: Backend sym => GenValue sym -> SEval sym () forceValue v = case v of@@ -345,7 +129,7 @@   VInteger i  -> seq i (return ())   VRational q -> seq q (return ())   VFloat f    -> seq f (return ())-  VWord _ wv  -> forceWordValue =<< wv+  VWord _ wv  -> forceWordValue wv   VStream _   -> return ()   VFun{}      -> return ()   VPoly{}     -> return ()@@ -353,7 +137,7 @@   -instance Backend sym => Show (GenValue sym) where+instance Show (GenValue sym) where   show v = case v of     VRecord fs -> "record:" ++ show (displayOrder fs)     VTuple xs  -> "tuple:" ++ show (length xs)@@ -368,7 +152,6 @@     VPoly{}    -> "poly"     VNumPoly{} -> "numpoly" - -- Pretty Printing -------------------------------------------------------------  ppValue :: forall sym.@@ -382,30 +165,32 @@   loop :: GenValue sym -> SEval sym Doc   loop val = case val of     VRecord fs         -> do fs' <- traverse (>>= loop) fs-                             return $ braces (sep (punctuate comma (map ppField (displayFields fs'))))+                             return $ ppRecord (map ppField (fields fs'))       where       ppField (f,r) = pp f <+> char '=' <+> r     VTuple vals        -> do vals' <- traverse (>>=loop) vals-                             return $ parens (sep (punctuate comma vals'))+                             return $ ppTuple vals'     VBit b             -> ppSBit x b     VInteger i         -> ppSInteger x i     VRational q        -> ppSRational x q     VFloat i           -> ppSFloat x opts i     VSeq sz vals       -> ppWordSeq sz vals-    VWord _ wv         -> ppWordVal =<< wv+    VWord _ wv         -> ppWordVal wv     VStream vals       -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals-                             return $ brackets $ fsep-                                   $ punctuate comma-                                   ( vals' ++ [text "..."]-                                   )+                             return $ ppList ( vals' ++ [text "..."] )     VFun{}             -> return $ text "<function>"     VPoly{}            -> return $ text "<polymorphic value>"     VNumPoly{}         -> return $ text "<polymorphic value>" +  fields :: RecordMap Ident Doc -> [(Ident, Doc)]+  fields = case useFieldOrder opts of+    DisplayOrder -> displayFields+    CanonicalOrder -> canonicalFields+   ppWordVal :: WordValue sym -> SEval sym Doc   ppWordVal w = ppSWord x opts =<< asWordVal x w -  ppWordSeq :: Integer -> SeqMap sym -> SEval sym Doc+  ppWordSeq :: Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc   ppWordSeq sz vals = do     ws <- sequence (enumerateSeqMap sz vals)     case ws of@@ -416,9 +201,9 @@               case traverse (wordAsChar x) vs of                 Just str -> return $ text (show str)                 _ -> do vs' <- mapM (ppSWord x opts) vs-                        return $ brackets (fsep (punctuate comma vs'))+                        return $ ppList vs'       _ -> do ws' <- traverse loop ws-              return $ brackets (fsep (punctuate comma ws'))+              return $ ppList ws'  ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc ppSBit sym b =@@ -485,7 +270,7 @@   prefix len = case base of     2  -> text "0b" <.> padding 1 len     8  -> text "0o" <.> padding 3 len-    10 -> empty+    10 -> mempty     16 -> text "0x" <.> padding 4 len     _  -> text "0"  <.> char '<' <.> int base <.> char '>' @@ -514,10 +299,10 @@ -- Value Constructors ----------------------------------------------------------  -- | Create a packed word of n bits.-word :: Backend sym => sym -> Integer -> Integer -> GenValue sym+word :: Backend sym => sym -> Integer -> Integer -> SEval sym (GenValue sym) word sym n i   | n >= Arch.maxBigIntWidth = wordTooWide n-  | otherwise                = VWord n (WordVal <$> wordLit sym n i)+  | otherwise                = VWord n . wordVal <$> wordLit sym n i   -- | Construct a function value@@ -544,36 +329,14 @@                      Nat i -> f i                      Inf   -> panic "ilam" [ "Unexpected `inf`" ]) --- | Generate a stream.-toStream :: Backend sym => sym -> [GenValue sym] -> SEval sym (GenValue sym)-toStream sym vs =-   VStream <$> infiniteSeqMap sym (map pure vs)--toFinSeq ::-  Backend sym =>-  sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym-toFinSeq sym len elty vs-   | isTBit elty = VWord len (WordVal <$> packWord sym (map fromVBit vs))-   | otherwise   = VSeq len $ finiteSeqMap (map pure vs)- -- | Construct either a finite sequence, or a stream.  In the finite case, -- record whether or not the elements were bits, to aid pretty-printing.-toSeq ::-  Backend sym =>-  sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym)-toSeq sym len elty vals = case len of-  Nat n -> return $ toFinSeq sym n elty vals-  Inf   -> toStream sym vals----- | Construct either a finite sequence, or a stream.  In the finite case,--- record whether or not the elements were bits, to aid pretty-printing.-mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym-mkSeq len elty vals = case len of+mkSeq :: Backend sym => sym -> Nat' -> TValue -> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym)+mkSeq sym len elty vals = case len of   Nat n-    | isTBit elty -> VWord n $ pure $ LargeBitsVal n vals-    | otherwise   -> VSeq n vals-  Inf             -> VStream vals+    | isTBit elty -> VWord n <$> bitmapWordVal sym n (fromVBit <$> vals)+    | otherwise   -> pure $ VSeq n vals+  Inf             -> pure $ VStream vals   -- Value Destructors -----------------------------------------------------------@@ -582,47 +345,47 @@ fromVBit :: GenValue sym -> SBit sym fromVBit val = case val of   VBit b -> b-  _      -> evalPanic "fromVBit" ["not a Bit"]+  _      -> evalPanic "fromVBit" ["not a Bit", show val]  -- | Extract an integer value. fromVInteger :: GenValue sym -> SInteger sym fromVInteger val = case val of   VInteger i -> i-  _      -> evalPanic "fromVInteger" ["not an Integer"]+  _      -> evalPanic "fromVInteger" ["not an Integer", show val]  -- | Extract a rational value. fromVRational :: GenValue sym -> SRational sym fromVRational val = case val of   VRational q -> q-  _      -> evalPanic "fromVRational" ["not a Rational"]+  _      -> evalPanic "fromVRational" ["not a Rational", show val]  -- | Extract a finite sequence value.-fromVSeq :: GenValue sym -> SeqMap sym+fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym) fromVSeq val = case val of   VSeq _ vs -> vs-  _         -> evalPanic "fromVSeq" ["not a sequence"]+  _         -> evalPanic "fromVSeq" ["not a sequence", show val]  -- | Extract a sequence.-fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym)+fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym)) fromSeq msg val = case val of   VSeq _ vs   -> return vs   VStream vs  -> return vs-  _           -> evalPanic "fromSeq" ["not a sequence", msg]+  _           -> evalPanic "fromSeq" ["not a sequence", msg, show val] -fromWordVal :: Backend sym => String -> GenValue sym -> SEval sym (WordValue sym)+fromWordVal :: Backend sym => String -> GenValue sym -> WordValue sym fromWordVal _msg (VWord _ wval) = wval-fromWordVal msg _ = evalPanic "fromWordVal" ["not a word value", msg]+fromWordVal msg val = evalPanic "fromWordVal" ["not a word value", msg, show val]  asIndex :: Backend sym =>-  sym -> String -> TValue -> GenValue sym -> SEval sym (Either (SInteger sym) (WordValue sym))-asIndex _sym _msg TVInteger (VInteger i) = pure (Left i)-asIndex _sym _msg _ (VWord _ wval) = Right <$> wval-asIndex _sym  msg _ _ = evalPanic "asIndex" ["not an index value", msg]+  sym -> String -> TValue -> GenValue sym -> Either (SInteger sym) (WordValue sym)+asIndex _sym _msg TVInteger (VInteger i) = Left i+asIndex _sym _msg _ (VWord _ wval) = Right wval+asIndex _sym  msg _ val = evalPanic "asIndex" ["not an index value", msg, show val]  -- | Extract a packed word. fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym)-fromVWord sym _msg (VWord _ wval) = wval >>= asWordVal sym-fromVWord _ msg _ = evalPanic "fromVWord" ["not a word", msg]+fromVWord sym _msg (VWord _ wval) = asWordVal sym wval+fromVWord _ msg val = evalPanic "fromVWord" ["not a word", msg, show val]  vWordLen :: Backend sym => GenValue sym -> Maybe Integer vWordLen val = case val of@@ -632,55 +395,119 @@ -- | If the given list of values are all fully-evaluated thunks --   containing bits, return a packed word built from the same bits. --   However, if any value is not a fully-evaluated bit, return 'Nothing'.-tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> Maybe (SEval sym (SWord sym))+tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym)) tryFromBits sym = go id   where-  go f [] = Just (packWord sym =<< sequence (f []))-  go f (v : vs) | isReady sym v = go (f . ((fromVBit <$> v):)) vs-  go _ (_ : _) = Nothing+  go f [] = Just <$> (packWord sym (f []))+  go f (v : vs) =+    isReady sym v >>= \case+      Just v' -> go (f . ((fromVBit v'):)) vs+      Nothing -> pure Nothing  -- | Extract a function from a value. fromVFun :: Backend sym => sym -> GenValue sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) fromVFun sym val = case val of   VFun fnstk f ->     \x -> sModifyCallStack sym (\stk -> combineCallStacks stk fnstk) (f x)-  _ -> evalPanic "fromVFun" ["not a function"]+  _ -> evalPanic "fromVFun" ["not a function", show val]  -- | Extract a polymorphic function from a value. fromVPoly :: Backend sym => sym -> GenValue sym -> (TValue -> SEval sym (GenValue sym)) fromVPoly sym val = case val of   VPoly fnstk f ->     \x -> sModifyCallStack sym (\stk -> combineCallStacks stk fnstk) (f x)-  _ -> evalPanic "fromVPoly" ["not a polymorphic value"]+  _ -> evalPanic "fromVPoly" ["not a polymorphic value", show val]  -- | Extract a polymorphic function from a value. fromVNumPoly :: Backend sym => sym -> GenValue sym -> (Nat' -> SEval sym (GenValue sym)) fromVNumPoly sym val = case val of   VNumPoly fnstk f ->     \x -> sModifyCallStack sym (\stk -> combineCallStacks stk fnstk) (f x)-  _  -> evalPanic "fromVNumPoly" ["not a polymorphic value"]+  _  -> evalPanic "fromVNumPoly" ["not a polymorphic value", show val]  -- | Extract a tuple from a value. fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)] fromVTuple val = case val of   VTuple vs -> vs-  _         -> evalPanic "fromVTuple" ["not a tuple"]+  _         -> evalPanic "fromVTuple" ["not a tuple", show val]  -- | Extract a record from a value. fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym)) fromVRecord val = case val of   VRecord fs -> fs-  _          -> evalPanic "fromVRecord" ["not a record"]+  _          -> evalPanic "fromVRecord" ["not a record", show val]  fromVFloat :: GenValue sym -> SFloat sym fromVFloat val =   case val of     VFloat x -> x-    _        -> evalPanic "fromVFloat" ["not a Float"]+    _        -> evalPanic "fromVFloat" ["not a Float", show val]  -- | Lookup a field in a record. lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym) lookupRecord f val =   case lookupField f (fromVRecord val) of     Just x  -> x-    Nothing -> evalPanic "lookupRecord" ["malformed record"]+    Nothing -> evalPanic "lookupRecord" ["malformed record", show val]+++-- Merge and if/then/else++{-# INLINE iteValue #-}+iteValue :: Backend sym =>+  sym ->+  SBit sym ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym)+iteValue sym b x y+  | Just True  <- bitAsLit sym b = x+  | Just False <- bitAsLit sym b = y+  | otherwise = mergeValue' sym b x y++{-# INLINE mergeValue' #-}+mergeValue' :: Backend sym =>+  sym ->+  SBit sym ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym) ->+  SEval sym (GenValue sym)+mergeValue' sym = mergeEval sym (mergeValue sym)++mergeValue :: Backend sym =>+  sym ->+  SBit sym ->+  GenValue sym ->+  GenValue sym ->+  SEval sym (GenValue sym)+mergeValue sym c v1 v2 =+  case (v1, v2) of+    (VRecord fs1 , VRecord fs2 ) ->+      do let res = zipRecords (\_lbl -> mergeValue' sym c) fs1 fs2+         case res of+           Left f -> panic "Cryptol.Eval.Value" [ "mergeValue: incompatible record values", show f ]+           Right r -> pure (VRecord r)+    (VTuple vs1  , VTuple vs2  ) | length vs1 == length vs2  ->+                                  pure $ VTuple $ zipWith (mergeValue' sym c) vs1 vs2+    (VBit b1     , VBit b2     ) -> VBit <$> iteBit sym c b1 b2+    (VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2+    (VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2+    (VFloat f1   , VFloat f2)    -> VFloat <$> iteFloat sym c f1 f2+    (VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> VWord n1 <$> mergeWord sym c w1 w2+    (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (Nat n1) (mergeSeqMapVal sym c vs1 vs2)+    (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym Inf (mergeSeqMapVal sym c vs1 vs2)+    (f1@VFun{}   , f2@VFun{}   ) -> lam sym $ \x -> mergeValue' sym c (fromVFun sym f1 x) (fromVFun sym f2 x)+    (f1@VPoly{}  , f2@VPoly{}  ) -> tlam sym $ \x -> mergeValue' sym c (fromVPoly sym f1 x) (fromVPoly sym f2 x)+    (_           , _           ) -> panic "Cryptol.Eval.Value"+                                  [ "mergeValue: incompatible values", show v1, show v2 ]++{-# INLINE mergeSeqMapVal #-}+mergeSeqMapVal :: Backend sym =>+  sym ->+  SBit sym ->+  SeqMap sym (GenValue sym)->+  SeqMap sym (GenValue sym)->+  SeqMap sym (GenValue sym)+mergeSeqMapVal sym c x y =+  indexSeqMap $ \i ->+    iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)

@@ -24,7 +24,7 @@ import           Control.Concurrent.MVar import           Control.Monad (foldM) import           Control.Monad.IO.Class-import           Data.Bits+ import qualified Data.Map as Map import qualified Data.Set as Set import           Data.Text (Text)@@ -40,6 +40,8 @@  import Cryptol.Backend import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )+import Cryptol.Backend.SeqMap+import Cryptol.Backend.WordValue import Cryptol.Backend.What4  import Cryptol.Eval.Generic@@ -47,9 +49,10 @@ import Cryptol.Eval.Type (TValue(..)) import Cryptol.Eval.Value + import qualified Cryptol.SHA as SHA -import Cryptol.TypeCheck.Solver.InfNat( Nat'(..), widthInteger )+import Cryptol.TypeCheck.Solver.InfNat( Nat'(..) )  import Cryptol.Utils.Ident import Cryptol.Utils.Panic@@ -60,7 +63,6 @@ -- See also Cryptol.Prims.Eval.primTable primTable :: W4.IsSymExprBuilder sym => What4 sym -> IO EvalOpts -> Map.Map PrimIdent (Prim (What4 sym)) primTable sym getEOpts =-  let w4sym = w4 sym in   Map.union (suiteBPrims sym) $   Map.union (primeECPrims sym) $   Map.union (genericFloatTable sym) $@@ -68,25 +70,9 @@    Map.fromList $ map (\(n, v) -> (prelPrim n, v)) -  [ (">>$"         , sshrV sym)--    -- Shifts and rotates-  , ("<<"          , logicShift sym "<<"  shiftShrink-                        (w4bvShl w4sym) (w4bvLshr w4sym)-                        shiftLeftReindex shiftRightReindex)-  , (">>"          , logicShift sym ">>"  shiftShrink-                        (w4bvLshr w4sym) (w4bvShl w4sym)-                        shiftRightReindex shiftLeftReindex)-  , ("<<<"         , logicShift sym "<<<" rotateShrink-                        (w4bvRol w4sym) (w4bvRor w4sym)-                        rotateLeftReindex rotateRightReindex)-  , (">>>"         , logicShift sym ">>>" rotateShrink-                        (w4bvRor w4sym) (w4bvRol w4sym)-                        rotateRightReindex rotateLeftReindex)--    -- Indexing and updates-  , ("@"           , indexPrim sym (indexFront_int sym) (indexFront_bits sym) (indexFront_word sym))-  , ("!"           , indexPrim sym (indexBack_int sym) (indexBack_bits sym) (indexBack_word sym))+  [ -- Indexing and updates+    ("@"           , indexPrim sym IndexForward  (indexFront_int sym) (indexFront_segs sym))+  , ("!"           , indexPrim sym IndexBackward (indexFront_int sym) (indexFront_segs sym))    , ("update"      , updatePrim sym (updateFrontSym_word sym) (updateFrontSym sym))   , ("updateEnd"   , updatePrim sym (updateBackSym_word sym)  (updateBackSym sym))@@ -235,7 +221,7 @@              fn <- liftIO $ getUninterpFn sym ("AESKeyExpand" <> Text.pack (show k)) args (W4.BaseStructRepr ret)              z  <- liftIO $ W4.applySymFn (w4 sym) fn ws              -- compute a sequence that projects the relevant fields from the outout tuple-             pure $ VSeq (4*(k+7)) $ IndexSeqMap $ \i ->+             pure $ VSeq (4*(k+7)) $ indexSeqMap $ \i ->                case intIndex (fromInteger i) (size ret) of                  Just (Some idx) | Just W4.Refl <- W4.testEquality (ret!idx) (W4.BaseBVRepr (W4.knownNat @32)) ->                    fromWord32 =<< liftIO (W4.structField (w4 sym) z idx)@@ -250,7 +236,7 @@           addUninterpWarning sym "SHA-224"           initSt <- liftIO (mkSHA256InitialState sym SHA.initialSHA224State)           finalSt <- foldM (\st blk -> processSHA256Block sym st =<< blk) initSt blks-          pure $ VSeq 7 $ IndexSeqMap \i ->+          pure $ VSeq 7 $ indexSeqMap \i ->             case intIndex (fromInteger i) (knownSize :: Size SHA256State) of               Just (Some idx) ->                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx@@ -268,7 +254,7 @@           addUninterpWarning sym "SHA-256"           initSt <- liftIO (mkSHA256InitialState sym SHA.initialSHA256State)           finalSt <- foldM (\st blk -> processSHA256Block sym st =<< blk) initSt blks-          pure $ VSeq 8 $ IndexSeqMap \i ->+          pure $ VSeq 8 $ indexSeqMap \i ->             case intIndex (fromInteger i) (knownSize :: Size SHA256State) of               Just (Some idx) ->                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx@@ -286,7 +272,7 @@           addUninterpWarning sym "SHA-384"           initSt <- liftIO (mkSHA512InitialState sym SHA.initialSHA384State)           finalSt <- foldM (\st blk -> processSHA512Block sym st =<< blk) initSt blks-          pure $ VSeq 6 $ IndexSeqMap \i ->+          pure $ VSeq 6 $ indexSeqMap \i ->             case intIndex (fromInteger i) (knownSize :: Size SHA512State) of               Just (Some idx) ->                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx@@ -304,7 +290,7 @@           addUninterpWarning sym "SHA-512"           initSt <- liftIO (mkSHA512InitialState sym SHA.initialSHA512State)           finalSt <- foldM (\st blk -> processSHA512Block sym st =<< blk) initSt blks-          pure $ VSeq 8 $ IndexSeqMap \i ->+          pure $ VSeq 8 $ indexSeqMap \i ->             case intIndex (fromInteger i) (knownSize :: Size SHA512State) of               Just (Some idx) ->                 do z <- liftIO $ W4.structField (w4 sym) finalSt idx@@ -459,7 +445,7 @@                            ]  toWord32 :: W4.IsSymExprBuilder sym =>-  What4 sym -> String -> SeqMap (What4 sym) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)+  What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32) toWord32 sym nm ss i =   do x <- fromVWord sym nm =<< lookupSeqMap ss i      case x of@@ -467,11 +453,10 @@        _ -> panic nm ["Unexpected word size", show (SW.bvWidth x)]  fromWord32 :: W4.IsSymExprBuilder sym => W4.SymBV sym 32 -> SEval (What4 sym) (Value sym)-fromWord32 = pure . VWord 32 . pure . WordVal . SW.DBV-+fromWord32 = pure . VWord 32 . wordVal . SW.DBV  toWord64 :: W4.IsSymExprBuilder sym =>-  What4 sym -> String -> SeqMap (What4 sym) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)+  What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64) toWord64 sym nm ss i =   do x <- fromVWord sym nm =<< lookupSeqMap ss i      case x of@@ -479,7 +464,7 @@        _ -> panic nm ["Unexpected word size", show (SW.bvWidth x)]  fromWord64 :: W4.IsSymExprBuilder sym => W4.SymBV sym 64 -> SEval (What4 sym) (Value sym)-fromWord64 = pure . VWord 64 . pure . WordVal . SW.DBV+fromWord64 = pure . VWord 64 . wordVal . SW.DBV   @@ -496,7 +481,7 @@      w3 <- toWord32 sym nm ss 3      fn <- liftIO $ getUninterpFn sym funNm argCtx (W4.BaseStructRepr argCtx)      z  <- liftIO $ W4.applySymFn (w4 sym) fn (Empty :> w0 :> w1 :> w2 :> w3)-     pure $ VSeq 4 $ IndexSeqMap \i ->+     pure $ VSeq 4 $ indexSeqMap \i ->        if | i == 0 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @0))           | i == 1 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @1))           | i == 2 -> fromWord32 =<< liftIO (W4.structField (w4 sym) z (natIndex @2))@@ -511,34 +496,12 @@    argCtx = W4.knownRepr  -sshrV :: W4.IsSymExprBuilder sym => What4 sym -> Prim (What4 sym)-sshrV sym =-  PFinPoly \n ->-  PTyPoly  \ix ->-  PWordFun \x ->-  PStrict  \y ->-  PPrim $-    asIndex sym ">>$" ix y >>= \case-       Left i ->-         do pneg <- intLessThan sym i =<< integerLit sym 0-            zneg <- do i' <- shiftShrink sym (Nat n) ix =<< intNegate sym i-                       amt <- wordFromInt sym n i'-                       w4bvShl (w4 sym) x amt-            zpos <- do i' <- shiftShrink sym (Nat n) ix i-                       amt <- wordFromInt sym n i'-                       w4bvAshr (w4 sym) x amt-            return (VWord (SW.bvWidth x) (WordVal <$> iteWord sym pneg zneg zpos))--       Right wv ->-         do amt <- asWordVal sym wv-            return (VWord (SW.bvWidth x) (WordVal <$> w4bvAshr (w4 sym) x amt))- indexFront_int ::   W4.IsSymExprBuilder sym =>   What4 sym ->   Nat' ->   TValue ->-  SeqMap (What4 sym) ->+  SeqMap (What4 sym) (GenValue (What4 sym)) ->   TValue ->   SInteger (What4 sym) ->   SEval (What4 sym) (Value sym)@@ -547,7 +510,9 @@   = lookupSeqMap xs i    | (lo, Just hi) <- bounds-  = foldr f def [lo .. hi]+  = case foldr f Nothing [lo .. hi] of+      Nothing -> raiseError sym (InvalidIndex Nothing)+      Just m  -> m    | otherwise   = liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))@@ -555,11 +520,10 @@  where     w4sym = w4 sym -    def = raiseError sym (InvalidIndex Nothing)--    f n y =+    f n (Just y) = Just $        do p <- liftIO (W4.intEq w4sym idx =<< W4.intLit w4sym n)           iteValue sym p (lookupSeqMap xs n) y+    f n Nothing = Just $ lookupSeqMap xs n      bounds =       (case W4.rangeLowBound (W4.integerBounds idx) of@@ -581,44 +545,34 @@         (Nat n, _)           -> Just n         (_    , TVIntMod m)  -> Just m         _                    -> Nothing--indexBack_int ::-  W4.IsSymExprBuilder sym =>-  What4 sym ->-  Nat' ->-  TValue ->-  SeqMap (What4 sym) ->-  TValue ->-  SInteger (What4 sym) ->-  SEval (What4 sym) (Value sym)-indexBack_int sym (Nat n) a xs ix idx = indexFront_int sym (Nat n) a (reverseSeqMap n xs) ix idx-indexBack_int _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_int"]--indexFront_word ::+indexFront_segs ::   W4.IsSymExprBuilder sym =>   What4 sym ->   Nat' ->   TValue ->-  SeqMap (What4 sym) ->+  SeqMap (What4 sym) (GenValue (What4 sym)) ->   TValue ->-  SWord (What4 sym) ->+  Integer ->+  [IndexSegment (What4 sym)] ->   SEval (What4 sym) (Value sym)-indexFront_word sym mblen _a xs _ix idx+indexFront_segs sym mblen _a xs _ix _idx_bits [WordIndexSegment idx]   | Just i <- SW.bvAsUnsignedInteger idx   = lookupSeqMap xs i    | otherwise-  = foldr f def idxs+  = case foldr f Nothing idxs of+      Nothing -> raiseError sym (InvalidIndex Nothing)+      Just m  -> m   where     w4sym = w4 sym      w = SW.bvWidth idx-    def = raiseError sym (InvalidIndex Nothing) -    f n y =+    f n (Just y) = Just $        do p <- liftIO (SW.bvEq w4sym idx =<< SW.bvLit w4sym w n)           iteValue sym p (lookupSeqMap xs n) y+    f n Nothing = Just $ lookupSeqMap xs n      -- maximum possible in-bounds index given the bitwidth     -- of the index value and the length of the sequence@@ -635,112 +589,34 @@         Just (lo, hi) -> [lo .. min hi maxIdx]         _ -> [0 .. maxIdx] -indexBack_word ::-  W4.IsSymExprBuilder sym =>-  What4 sym ->-  Nat' ->-  TValue ->-  SeqMap (What4 sym) ->-  TValue ->-  SWord (What4 sym) ->-  SEval (What4 sym) (Value sym)-indexBack_word sym (Nat n) a xs ix idx = indexFront_word sym (Nat n) a (reverseSeqMap n xs) ix idx-indexBack_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_word"]--indexFront_bits :: forall sym.-  W4.IsSymExprBuilder sym =>-  What4 sym ->-  Nat' ->-  TValue ->-  SeqMap (What4 sym) ->-  TValue ->-  [SBit (What4 sym)] ->-  SEval (What4 sym) (Value sym)-indexFront_bits sym mblen _a xs _ix bits0 = go 0 (length bits0) bits0- where-  go :: Integer -> Int -> [W4.Pred sym] -> W4Eval sym (Value sym)-  go i _k []-    -- For indices out of range, fail-    | Nat n <- mblen-    , i >= n-    = raiseError sym (InvalidIndex (Just i))--    | otherwise-    = lookupSeqMap xs i--  go i k (b:bs)-    -- Fail early when all possible indices we could compute from here-    -- are out of bounds-    | Nat n <- mblen-    , (i `shiftL` k) >= n-    = raiseError sym (InvalidIndex Nothing)--    | otherwise-    = iteValue sym b-         (go ((i `shiftL` 1) + 1) (k-1) bs)-         (go  (i `shiftL` 1)      (k-1) bs)--indexBack_bits ::-  W4.IsSymExprBuilder sym =>-  What4 sym ->-  Nat' ->-  TValue ->-  SeqMap (What4 sym) ->-  TValue ->-  [SBit (What4 sym)] ->-  SEval (What4 sym) (Value sym)-indexBack_bits sym (Nat n) a xs ix idx = indexFront_bits sym (Nat n) a (reverseSeqMap n xs) ix idx-indexBack_bits _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"]----- | Compare a symbolic word value with a concrete integer.-wordValueEqualsInteger :: forall sym.-  W4.IsSymExprBuilder sym =>-  What4 sym ->-  WordValue (What4 sym) ->-  Integer ->-  W4Eval sym (W4.Pred sym)-wordValueEqualsInteger sym wv i-  | wordValueSize sym wv < widthInteger i = return (W4.falsePred w4sym)-  | otherwise =-    case wv of-      WordVal w -> liftIO (SW.bvEq w4sym w =<< SW.bvLit w4sym (SW.bvWidth w) i)-      _ -> liftIO . bitsAre i =<< enumerateWordValueRev sym wv -- little-endian+indexFront_segs sym mblen _a xs _ix idx_bits segs =+  do xs' <- barrelShifter sym (mergeValue sym) shiftOp mblen xs idx_bits segs+     lookupSeqMap xs' 0   where-    w4sym = w4 sym+    shiftOp vs amt = pure (indexSeqMap (\i -> lookupSeqMap vs $! amt+i)) -    bitsAre :: Integer -> [W4.Pred sym] -> IO (W4.Pred sym)-    bitsAre n [] = pure (W4.backendPred w4sym (n == 0))-    bitsAre n (b : bs) =-      do pb  <- bitIs (testBit n 0) b-         pbs <- bitsAre (n `shiftR` 1) bs-         W4.andPred w4sym pb pbs -    bitIs :: Bool -> W4.Pred sym -> IO (W4.Pred sym)-    bitIs b x = if b then pure x else W4.notPred w4sym x- updateFrontSym ::   W4.IsSymExprBuilder sym =>   What4 sym ->   Nat' ->   TValue ->-  SeqMap (What4 sym) ->+  SeqMap (What4 sym) (GenValue (What4 sym)) ->   Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->   SEval (What4 sym) (Value sym) ->-  SEval (What4 sym) (SeqMap (What4 sym))+  SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym))) updateFrontSym sym _len _eltTy vs (Left idx) val =   case W4.asInteger idx of     Just i -> return $ updateSeqMap vs i val-    Nothing -> return $ IndexSeqMap $ \i ->+    Nothing -> return $ indexSeqMap $ \i ->       do b <- intEq sym idx =<< integerLit sym i          iteValue sym b val (lookupSeqMap vs i) -updateFrontSym sym _len _eltTy vs (Right wv) val =-  case wv of-    WordVal w | Just j <- SW.bvAsUnsignedInteger w ->-      return $ updateSeqMap vs j val-    _ ->-      memoMap sym $ IndexSeqMap $ \i ->+updateFrontSym sym len _eltTy vs (Right wv) val =+  wordValAsLit sym wv >>= \case+    Just j -> return $ updateSeqMap vs j val+    Nothing ->+      memoMap sym len $ indexSeqMap $ \i ->       do b <- wordValueEqualsInteger sym wv i          iteValue sym b val (lookupSeqMap vs i) @@ -749,25 +625,25 @@   What4 sym ->   Nat' ->   TValue ->-  SeqMap (What4 sym) ->+  SeqMap (What4 sym) (GenValue (What4 sym)) ->   Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->   SEval (What4 sym) (Value sym) ->-  SEval (What4 sym) (SeqMap (What4 sym))+  SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym))) updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]  updateBackSym sym (Nat n) _eltTy vs (Left idx) val =   case W4.asInteger idx of     Just i -> return $ updateSeqMap vs (n - 1 - i) val-    Nothing -> return $ IndexSeqMap $ \i ->+    Nothing -> return $ indexSeqMap $ \i ->       do b <- intEq sym idx =<< integerLit sym (n - 1 - i)          iteValue sym b val (lookupSeqMap vs i)  updateBackSym sym (Nat n) _eltTy vs (Right wv) val =-  case wv of-    WordVal w | Just j <- SW.bvAsUnsignedInteger w ->+  wordValAsLit sym wv >>= \case+    Just j ->       return $ updateSeqMap vs (n - 1 - j) val-    _ ->-      memoMap sym $ IndexSeqMap $ \i ->+    Nothing ->+      memoMap sym (Nat n) $ indexSeqMap $ \i ->       do b <- wordValueEqualsInteger sym wv (n - 1 - i)          iteValue sym b val (lookupSeqMap vs i) @@ -783,36 +659,11 @@   SEval (What4 sym) (WordValue (What4 sym)) updateFrontSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_word"] -updateFrontSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =-  LargeBitsVal n <$> updateFrontSym sym (Nat n) eltTy bv idx val--updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =+updateFrontSym_word sym (Nat n) _eltTy w (Left idx) val =   do idx' <- wordFromInt sym n idx-     updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val--updateFrontSym_word sym (Nat n) eltTy bv (Right wv) val =-  case wv of-    WordVal idx-      | Just j <- SW.bvAsUnsignedInteger idx ->-          updateWordValue sym bv j (fromVBit <$> val)--      | WordVal bw <- bv ->-        WordVal <$>-          do b <- fromVBit <$> val-             let sz = SW.bvWidth bw-             highbit <- liftIO (SW.bvLit (w4 sym) sz (bit (fromInteger (sz-1))))-             msk <- w4bvLshr (w4 sym) highbit idx-             liftIO $-               case W4.asConstantPred b of-                 Just True  -> SW.bvOr  (w4 sym) bw msk-                 Just False -> SW.bvAnd (w4 sym) bw =<< SW.bvNot (w4 sym) msk-                 Nothing ->-                   do q <- SW.bvFill (w4 sym) sz b-                      bw' <- SW.bvAnd (w4 sym) bw =<< SW.bvNot (w4 sym) msk-                      SW.bvXor (w4 sym) bw' =<< SW.bvAnd (w4 sym) q msk--    _ -> LargeBitsVal (wordValueSize sym wv) <$>-           updateFrontSym sym (Nat n) eltTy (asBitsMap sym bv) (Right wv) val+     updateWordByWord sym IndexForward w (wordVal idx') (fromVBit <$> val)+updateFrontSym_word sym (Nat _n) _eltTy w (Right idx) val =+  updateWordByWord sym IndexForward w idx (fromVBit <$> val)   updateBackSym_word ::@@ -824,35 +675,10 @@   Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->   SEval (What4 sym) (GenValue (What4 sym)) ->   SEval (What4 sym) (WordValue (What4 sym))-updateBackSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym_word"]--updateBackSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =-  LargeBitsVal n <$> updateBackSym sym (Nat n) eltTy bv idx val+updateBackSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_word"] -updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =+updateBackSym_word sym (Nat n) _eltTy w (Left idx) val =   do idx' <- wordFromInt sym n idx-     updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val--updateBackSym_word sym (Nat n) eltTy bv (Right wv) val =-  case wv of-    WordVal idx-      | Just j <- SW.bvAsUnsignedInteger idx ->-          updateWordValue sym bv (n - 1 - j) (fromVBit <$> val)--      | WordVal bw <- bv ->-        WordVal <$>-          do b <- fromVBit <$> val-             let sz = SW.bvWidth bw-             lowbit <- liftIO (SW.bvLit (w4 sym) sz 1)-             msk <- w4bvShl (w4 sym) lowbit idx-             liftIO $-               case W4.asConstantPred b of-                 Just True  -> SW.bvOr  (w4 sym) bw msk-                 Just False -> SW.bvAnd (w4 sym) bw =<< SW.bvNot (w4 sym) msk-                 Nothing ->-                   do q <- SW.bvFill (w4 sym) sz b-                      bw' <- SW.bvAnd (w4 sym) bw =<< SW.bvNot (w4 sym) msk-                      SW.bvXor (w4 sym) bw' =<< SW.bvAnd (w4 sym) q msk--    _ -> LargeBitsVal (wordValueSize sym wv) <$>-           updateBackSym sym (Nat n) eltTy (asBitsMap sym bv) (Right wv) val+     updateWordByWord sym IndexBackward w (wordVal idx') (fromVBit <$> val)+updateBackSym_word sym (Nat _n) _eltTy w (Right idx) val =+  updateWordByWord sym IndexBackward w idx (fromVBit <$> val)

@@ -32,7 +32,7 @@   pmod :: Int -> Integer -> Integer -> Integer-pmod w x m = mask .&. go 0 0 (reduce 1)+pmod w x m = go degree (x .&. mask) (clearBit m degree)   where     degree :: Int     degree = fromInteger (widthInteger m - 1)@@ -43,6 +43,7 @@      mask = bit degree - 1 +    -- invariant: z and p are in the range [0..mask]     go !i !z !p       | i < w     = go (i+1) (if testBit x i then z `xor` p else z) (reduce (p `shiftL` 1))       | otherwise = z

@@ -29,10 +29,12 @@   , renameType      -- * Interfaces-  , Iface(..), IfaceParams(..), IfaceDecls(..), genIface+  , Iface, IfaceG(..), IfaceParams(..), IfaceDecls(..), T.genIface   , IfaceTySyn, IfaceDecl(..)   ) where +import Data.Map (Map)+ import qualified Cryptol.Eval.Concrete as Concrete import           Cryptol.ModuleSystem.Env import           Cryptol.ModuleSystem.Interface@@ -44,6 +46,7 @@ import           Cryptol.Parser.Name (PName) import           Cryptol.Parser.NoPat (RemovePatterns) import qualified Cryptol.TypeCheck.AST     as T+import qualified Cryptol.TypeCheck.Interface as T import qualified Cryptol.Utils.Ident as M  -- Public Interface ------------------------------------------------------------@@ -93,7 +96,7 @@ evalExpr e env = runModuleM env (interactive (Base.evalExpr e))  -- | Typecheck top-level declarations.-checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup])+checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn) checkDecls ds env = runModuleM env                   $ interactive                   $ Base.checkDecls ds@@ -105,10 +108,14 @@ noPat :: RemovePatterns a => a -> ModuleCmd a noPat a env = runModuleM env (interactive (Base.noPat a)) +-- | Rename a *use* of a value name. The distinction between uses and+-- binding is used to keep track of dependencies. renameVar :: R.NamingEnv -> PName -> ModuleCmd Name renameVar names n env = runModuleM env $ interactive $-  Base.rename M.interactiveName names (R.renameVar n)+  Base.rename M.interactiveName names (R.renameVar R.NameUse n) +-- | Rename a *use* of a type name. The distinction between uses and+-- binding is used to keep track of dependencies. renameType :: R.NamingEnv -> PName -> ModuleCmd Name renameType names n env = runModuleM env $ interactive $-  Base.rename M.interactiveName names (R.renameType n)+  Base.rename M.interactiveName names (R.renameType R.NameUse n)

@@ -12,14 +12,38 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE OverloadedStrings #-}  module Cryptol.ModuleSystem.Base where +import qualified Control.Exception as X+import Control.Monad (unless,when)+import Data.Maybe (fromMaybe)+import Data.Monoid ((<>))+import Data.Text.Encoding (decodeUtf8')+import Data.IORef(newIORef,readIORef)+import System.Directory (doesFileExist, canonicalizePath)+import System.FilePath ( addExtension+                       , isAbsolute+                       , joinPath+                       , (</>)+                       , normalise+                       , takeDirectory+                       , takeFileName+                       )+import qualified System.IO.Error as IOE+import qualified Data.Map as Map++import Prelude ()+import Prelude.Compat hiding ( (<>) )+++ import Cryptol.ModuleSystem.Env (DynamicEnv(..)) import Cryptol.ModuleSystem.Fingerprint import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Monad-import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)+import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..)) import Cryptol.ModuleSystem.Env (lookupModule                                 , LoadedModule(..)                                 , meCoreLint, CoreLint(..)@@ -53,33 +77,21 @@                        , suiteBContents, primeECContents, preludeReferenceContents ) import Cryptol.Transform.MonoValues (rewModule) -import qualified Control.Exception as X-import Control.Monad (unless,when)-import Data.Maybe (fromMaybe)-import Data.Monoid ((<>))-import Data.Text.Encoding (decodeUtf8')-import System.Directory (doesFileExist, canonicalizePath)-import System.FilePath ( addExtension-                       , isAbsolute-                       , joinPath-                       , (</>)-                       , normalise-                       , takeDirectory-                       , takeFileName-                       )-import qualified System.IO.Error as IOE-import qualified Data.Map as Map -import Prelude ()-import Prelude.Compat hiding ( (<>) )-- -- Renaming --------------------------------------------------------------------  rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a rename modName env m = do+  ifaces <- getIfaces   (res,ws) <- liftSupply $ \ supply ->-    case R.runRenamer supply modName env m of+    let info = R.RenamerInfo+                 { renSupply  = supply+                 , renContext = TopModule modName+                 , renEnv     = env+                 , renIfaces  = ifaces+                 }+    in+    case R.runRenamer info m of       (Right (a,supply'),ws) -> ((Right a,ws),supply')       (Left errs,ws)         -> ((Left errs,ws),supply) @@ -89,12 +101,8 @@     Left errs -> renamerErrors errs  -- | Rename a module in the context of its imported modules.-renameModule :: P.Module PName-             -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)-renameModule m = do-  (decls,menv) <- importIfaces (map thing (P.mImports m))-  (declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m)-  return (decls,declsEnv,rm)+renameModule :: P.Module PName -> ModuleM R.RenamedModule+renameModule m = rename (thing (mName m)) mempty (R.renameModule m)   -- NoPat -----------------------------------------------------------------------@@ -200,15 +208,18 @@       unless quiet $ withLogger logPutStrLn        ("Loading module " ++ pretty (P.thing (P.mName pm)))-     tcm <- optionalInstantiate =<< checkModule isrc path pm ++     (nameEnv,tcmod) <- checkModule isrc path pm+     tcm <- optionalInstantiate tcmod+      -- extend the eval env, unless a functor.      tbl <- Concrete.primTable <$> getEvalOptsAction      let ?evalPrim = \i -> Right <$> Map.lookup i tbl      callStacks <- getCallStacks      let ?callStacks = callStacks      unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)-     loadedModule path fp tcm+     loadedModule path fp nameEnv tcm       return tcm   where@@ -231,17 +242,6 @@ fullyQualified :: P.Import -> P.Import fullyQualified i = i { iAs = Just (iModule i) } --- | Find the interface referenced by an import, and generate the naming--- environment that it describes.-importIface :: P.Import -> ModuleM (IfaceDecls,R.NamingEnv)-importIface imp =-  do Iface { .. } <- getIface (T.iModule imp)-     return (ifPublic, R.interpImport imp ifPublic)---- | Load a series of interfaces, merging their public interfaces.-importIfaces :: [P.Import] -> ModuleM (IfaceDecls,R.NamingEnv)-importIfaces is = mconcat `fmap` mapM importIface is- moduleFile :: ModName -> String -> FilePath moduleFile n = addExtension (joinPath (modNameChunks n)) @@ -299,13 +299,13 @@ addPrelude m   | preludeName == P.thing (P.mName m) = m   | preludeName `elem` importedMods    = m-  | otherwise                          = m { mImports = importPrelude : mImports m }+  | otherwise                          = m { mDecls = importPrelude : mDecls m }   where   importedMods  = map (P.iModule . P.thing) (P.mImports m)-  importPrelude = P.Located+  importPrelude = P.DImport P.Located     { P.srcRange = emptyRange     , P.thing    = P.Import-      { iModule    = preludeName+      { iModule    = P.ImpTop preludeName       , iAs        = Nothing       , iSpec      = Nothing       }@@ -353,23 +353,20 @@ -- | Typecheck a group of declarations. -- -- INVARIANT: This assumes that NoPat has already been run on the declarations.-checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup])+checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup], Map.Map Name T.TySyn) checkDecls ds = do   fe <- getFocusedEnv   let params = mctxParams fe       decls  = mctxDecls  fe       names  = mctxNames  fe -  -- introduce names for the declarations before renaming them-  declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds))-  rds <- rename interactiveName (declsEnv `R.shadowing` names)-             (traverse R.rename ds)-+  (declsEnv,rds) <- rename interactiveName names+                  $ R.renameTopDecls interactiveName ds   prims <- getPrimMap   let act  = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter                       , tcPrims = prims }-  ds' <- typecheck act rds params decls-  return (declsEnv,ds')+  (ds',tyMap) <- typecheck act rds params decls+  return (declsEnv,ds',tyMap)  -- | Generate the primitive map. If the prelude is currently being loaded, this -- should be generated directly from the naming environment given to the renamer@@ -390,12 +387,23 @@                   [ "Unable to find the prelude" ]  -- | Load a module, be it a normal module or a functor instantiation.-checkModule :: ImportSource -> ModulePath -> P.Module PName -> ModuleM T.Module+checkModule ::+  ImportSource -> ModulePath -> P.Module PName ->+  ModuleM (R.NamingEnv, T.Module) checkModule isrc path m =   case P.mInstance m of     Nothing -> checkSingleModule T.tcModule isrc path m-    Just fmName -> do tf <- getLoaded (thing fmName)-                      checkSingleModule (T.tcModuleInst tf) isrc path m+    Just fmName ->+      do mbtf <- getLoadedMaybe (thing fmName)+         case mbtf of+           Just tf ->+             do renThis <- io $ newIORef (lmNamingEnv tf)+                let how = T.tcModuleInst renThis (lmModule tf)+                (_,m') <- checkSingleModule how isrc path m+                newEnv <- io $ readIORef renThis+                pure (newEnv,m')+           Nothing -> panic "checkModule"+                        [ "Functor of module instantiation not loaded" ]   -- | Typecheck a single module.  If the module is an instantiation@@ -406,7 +414,7 @@   ImportSource                 {- ^ why are we loading this -} ->   ModulePath                   {- path -} ->   P.Module PName               {- ^ module to check -} ->-  ModuleM T.Module+  ModuleM (R.NamingEnv,T.Module) checkSingleModule how isrc path m = do    -- check that the name of the module matches expectations@@ -432,13 +440,13 @@   npm <- noPat nim    -- rename everything-  (tcEnv,declsEnv,scm) <- renameModule npm+  renMod <- renameModule npm    -- when generating the prim map for the typechecker, if we're checking the   -- prelude, we have to generate the map from the renaming environment, as we   -- don't have the interface yet.   prims <- if thing (mName m) == preludeName-              then return (R.toPrimMap declsEnv)+              then return (R.toPrimMap (R.rmDefines renMod))               else getPrimMap    -- typecheck@@ -447,11 +455,12 @@                      , tcPrims  = prims }  -  tcm0 <- typecheck act scm noIfaceParams tcEnv+  tcm0 <- typecheck act (R.rmModule renMod) noIfaceParams (R.rmImported renMod)    let tcm = tcm0 -- fromMaybe tcm0 (addModParams tcm0) -  liftSupply (`rewModule` tcm)+  rewMod <- liftSupply (`rewModule` tcm)+  pure (R.rmInScope renMod,rewMod)  data TCLinter o = TCLinter   { lintCheck ::@@ -473,11 +482,11 @@   , lintModule = Nothing   } -declsLinter :: TCLinter [ T.DeclGroup ]+declsLinter :: TCLinter ([ T.DeclGroup ], a) declsLinter = TCLinter-  { lintCheck = \ds' i -> case TcSanity.tcDecls i ds' of-                            Left err -> Left err-                            Right os -> Right os+  { lintCheck = \(ds',_) i -> case TcSanity.tcDecls i ds' of+                                Left err -> Left err+                                Right os -> Right os    , lintModule = Nothing   }@@ -529,16 +538,17 @@  -- | Generate input for the typechecker. genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput-genInferInput r prims params env = do+genInferInput r prims params env' = do   seeds <- getNameSeeds   monoBinds <- getMonoBinds-  cfg <- getSolverConfig   solver <- getTCSolver   supply <- getSupply   searchPath <- getSearchPath   callStacks <- getCallStacks    -- TODO: include the environment needed by the module+  let env = flatPublicDecls env'+            -- XXX: we should really just pass this directly   return T.InferInput     { T.inpRange     = r     , T.inpVars      = Map.map ifDeclSig (ifDecls env)@@ -548,7 +558,6 @@     , T.inpNameSeeds = seeds     , T.inpMonoBinds = monoBinds     , T.inpCallStacks = callStacks-    , T.inpSolverConfig = cfg     , T.inpSearchPath = searchPath     , T.inpSupply    = supply     , T.inpPrimNames = prims

@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE OverloadedStrings #-} module Cryptol.ModuleSystem.Env where  #ifndef RELOCATABLE@@ -24,6 +25,7 @@ import qualified Cryptol.ModuleSystem.NamingEnv as R import Cryptol.Parser.AST import qualified Cryptol.TypeCheck as T+import qualified Cryptol.TypeCheck.Interface as T import qualified Cryptol.TypeCheck.AST as T import Cryptol.Utils.PP (PP(..),text,parens,NameDisp) @@ -31,6 +33,7 @@ import Control.Monad (guard,mplus) import qualified Control.Exception as X import Data.Function (on)+import Data.Set(Set) import Data.Map (Map) import qualified Data.Map as Map import Data.Semigroup@@ -60,9 +63,6 @@   , meNameSeeds     :: T.NameSeeds     -- ^ A source of new names for the type checker. -  , meSolverConfig  :: T.SolverConfig-    -- ^ Configuration settings for the SMT solver used for type-checking.-   , meEvalEnv       :: EvalEnv     -- ^ The evaluation environment.  Contains the values for all loaded     -- modules, both public and private.@@ -150,12 +150,6 @@     , meSearchPath    = searchPath     , meDynEnv        = mempty     , meMonoBinds     = True-    , meSolverConfig  = T.SolverConfig-                          { T.solverPath = "z3"-                          , T.solverArgs = [ "-smt2", "-in" ]-                          , T.solverVerbose = 0-                          , T.solverPreludePath = searchPath-                          }     , meCoreLint      = NoCoreLint     , meSupply        = emptySupply     }@@ -194,91 +188,79 @@ -- or type check new expressions. data ModContext = ModContext   { mctxParams          :: IfaceParams+  , mctxExported        :: Set Name   , mctxDecls           :: IfaceDecls+    -- ^ Should contain at least names in NamingEnv, but may have more   , mctxNames           :: R.NamingEnv+    -- ^ What's in scope inside the module   , mctxNameDisp        :: NameDisp-  , mctxTypeProvenace   :: Map Name DeclProvenance-  , mctxValueProvenance :: Map Name DeclProvenance   } --- | Specifies how a declared name came to be in scope.-data DeclProvenance =-    NameIsImportedFrom ModName-  | NameIsLocalPublic-  | NameIsLocalPrivate-  | NameIsParameter-  | NameIsDynamicDecl-    deriving (Eq,Ord)+-- This instance is a bit bogus.  It is mostly used to add the dynamic+-- environemnt to an existing module, and it makes sense for that use case.+instance Semigroup ModContext where+  x <> y = ModContext { mctxParams   = jnParams (mctxParams x) (mctxParams y)+                      , mctxExported = mctxExported x <> mctxExported y+                      , mctxDecls    = mctxDecls x  <> mctxDecls  y+                      , mctxNames    = names+                      , mctxNameDisp = R.toNameDisp names+                      } +      where+      names = mctxNames x `R.shadowing` mctxNames y+      jnParams a b+        | isEmptyIfaceParams a = b+        | isEmptyIfaceParams b = a+        | otherwise =+          panic "ModContext" [ "Cannot combined 2 parameterized contexts" ] --- | Given the state of the environment, compute information about what's--- in scope on the REPL.  This includes what's in the focused module, plus any--- additional definitions from the REPL (e.g., let bound names, and @it@).-focusedEnv :: ModuleEnv -> ModContext-focusedEnv me =-  ModContext-    { mctxParams   = parameters-    , mctxDecls    = mconcat (dynDecls : localDecls : importedDecls)-    , mctxNames    = namingEnv-    , mctxNameDisp = R.toNameDisp namingEnv-    , mctxTypeProvenace = fst provenance-    , mctxValueProvenance = snd provenance-    }+instance Monoid ModContext where+  mempty = ModContext { mctxParams   = noIfaceParams+                      , mctxDecls    = mempty+                      , mctxExported = mempty+                      , mctxNames    = mempty+                      , mctxNameDisp = R.toNameDisp mempty+                      } -  where-  (importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports)-  localDecls    = publicDecls `mappend` privateDecls-  localNames    = R.unqualifiedEnv localDecls `mappend`-                                                R.modParamsNamingEnv parameters-  dynDecls      = deIfaceDecls (meDynEnv me)-  dynNames      = deNames (meDynEnv me) -  namingEnv     = dynNames   `R.shadowing`-                   localNames `R.shadowing`-                   mconcat importedNames -  provenance    = shadowProvs-                $ declsProv NameIsDynamicDecl dynDecls-                : declsProv NameIsLocalPublic publicDecls-                : declsProv NameIsLocalPrivate privateDecls-                : paramProv parameters-                : importedProvs+modContextOf :: ModName -> ModuleEnv -> Maybe ModContext+modContextOf mname me =+  do lm <- lookupModule mname me+     let localIface  = lmInterface lm+         localNames  = lmNamingEnv lm+         loadedDecls = map (ifPublic . lmInterface)+                     $ getLoadedModules (meLoadedModules me)+     pure ModContext+       { mctxParams   = ifParams localIface+       , mctxExported = ifaceDeclsNames (ifPublic localIface)+       , mctxDecls    = mconcat (ifPrivate localIface : loadedDecls)+       , mctxNames    = localNames+       , mctxNameDisp = R.toNameDisp localNames+       } -  (imports, parameters, publicDecls, privateDecls) =-    case meFocusedModule me of-      Nothing -> (mempty, noIfaceParams, mempty, mempty)-      Just fm ->-        case lookupModule fm me of-          Just lm ->-            let Iface { .. } = lmInterface lm-            in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate)-          Nothing -> panic "focusedEnv" ["Focused module is not loaded."]+dynModContext :: ModuleEnv -> ModContext+dynModContext me = mempty { mctxNames    = dynNames+                          , mctxNameDisp = R.toNameDisp dynNames+                          , mctxDecls    = deIfaceDecls (meDynEnv me)+                          }+  where dynNames = deNames (meDynEnv me) -  loadImport imp =-    case lookupModule (iModule imp) me of-      Just lm ->-        let decls = ifPublic (lmInterface lm)-        in ( R.interpImport imp decls-           , decls-           , declsProv (NameIsImportedFrom (iModule imp)) decls-           )-      Nothing -> panic "focusedEnv"-                   [ "Missing imported module: " ++ show (pp (iModule imp)) ]  -  -- earlier ones shadow-  shadowProvs ps = let (tss,vss) = unzip ps-                   in (Map.unions tss, Map.unions vss) -  paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns)-    where doMap mp = const NameIsParameter <$> mp--  declsProv prov IfaceDecls { .. } =-    ( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]-    , doMap ifDecls-    )-    where doMap mp = const prov <$> mp-+-- | Given the state of the environment, compute information about what's+-- in scope on the REPL.  This includes what's in the focused module, plus any+-- additional definitions from the REPL (e.g., let bound names, and @it@).+focusedEnv :: ModuleEnv -> ModContext+focusedEnv me =+  case meFocusedModule me of+    Nothing -> dynModContext me+    Just fm -> case modContextOf fm me of+                 Just c -> dynModContext me <> c+                 Nothing -> panic "focusedEnv"+                              [ "Focused modules not loaded: " ++ show (pp fm) ]+    -- Loaded Modules -------------------------------------------------------------- @@ -350,9 +332,11 @@     -- For files we just use the cononical path, for in memory things we     -- use their label. +  , lmNamingEnv         :: !R.NamingEnv+    -- ^ What's in scope in this module+   , lmInterface         :: Iface-    -- ^ The module's interface. This is for convenient.  At the moment-    -- we have the whole module in 'lmModule', so this could be computer.+    -- ^ The module's interface.    , lmModule            :: T.Module     -- ^ The actual type-checked module@@ -378,8 +362,9 @@ -- | Add a freshly loaded module.  If it was previously loaded, then -- the new version is ignored. addLoadedModule ::-  ModulePath -> String -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules-addLoadedModule path ident fp tm lm+  ModulePath -> String -> Fingerprint -> R.NamingEnv -> T.Module ->+  LoadedModules -> LoadedModules+addLoadedModule path ident fp nameEnv tm lm   | isLoaded (T.mName tm) lm  = lm   | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :                                                 lmLoadedParamModules lm }@@ -390,7 +375,8 @@     { lmName            = T.mName tm     , lmFilePath        = path     , lmModuleId        = ident-    , lmInterface       = genIface tm+    , lmNamingEnv       = nameEnv+    , lmInterface       = T.genIface tm     , lmModule          = tm     , lmFingerprint     = fp     }@@ -414,37 +400,43 @@ data DynamicEnv = DEnv   { deNames :: R.NamingEnv   , deDecls :: [T.DeclGroup]+  , deTySyns :: Map Name T.TySyn   , deEnv   :: EvalEnv   } deriving Generic  instance Semigroup DynamicEnv where   de1 <> de2 = DEnv-    { deNames = deNames de1 <> deNames de2-    , deDecls = deDecls de1 <> deDecls de2-    , deEnv   = deEnv   de1 <> deEnv   de2+    { deNames  = deNames de1  <> deNames de2+    , deDecls  = deDecls de1  <> deDecls de2+    , deTySyns = deTySyns de1 <> deTySyns de2+    , deEnv    = deEnv   de1  <> deEnv   de2     }  instance Monoid DynamicEnv where   mempty = DEnv-    { deNames = mempty-    , deDecls = mempty-    , deEnv   = mempty+    { deNames  = mempty+    , deDecls  = mempty+    , deTySyns = mempty+    , deEnv    = mempty     }   mappend de1 de2 = de1 <> de2  -- | Build 'IfaceDecls' that correspond to all of the bindings in the -- dynamic environment. ----- XXX: if we ever add type synonyms or newtypes at the REPL, revisit+-- XXX: if we add newtypes, etc. at the REPL, revisit -- this. deIfaceDecls :: DynamicEnv -> IfaceDecls-deIfaceDecls DEnv { deDecls = dgs } =-  mconcat [ IfaceDecls-            { ifTySyns   = Map.empty-            , ifNewtypes = Map.empty-            , ifAbstractTypes = Map.empty-            , ifDecls    = Map.singleton (ifDeclName ifd) ifd-            }-          | decl <- concatMap T.groupDecls dgs-          , let ifd = mkIfaceDecl decl-          ]+deIfaceDecls DEnv { deDecls = dgs, deTySyns = tySyns } =+    IfaceDecls { ifTySyns = tySyns+               , ifNewtypes = Map.empty+               , ifAbstractTypes = Map.empty+               , ifDecls = decls+               , ifModules = Map.empty+               }+  where+    decls = mconcat+      [ Map.singleton (ifDeclName ifd) ifd+      | decl <- concatMap T.groupDecls dgs+      , let ifd = T.mkIfaceDecl decl+      ]