diff --git a/bench/Main.hs b/bench/Main.hs index a9823366..08040752 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -7,11 +7,16 @@ -- Portability : portable {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} module Main where import qualified Data.Text.Lazy as T import qualified Data.Text.Lazy.IO as T +import qualified Cryptol.Eval as E +import qualified Cryptol.Eval.Monad as E +import qualified Cryptol.Eval.Value as E + import qualified Cryptol.ModuleSystem.Base as M import qualified Cryptol.ModuleSystem.Env as M import qualified Cryptol.ModuleSystem.Monad as M @@ -22,12 +27,15 @@ import qualified Cryptol.Parser.AST as P import qualified Cryptol.Parser.NoInclude as P import qualified Cryptol.Symbolic as S +import qualified Cryptol.Symbolic.Value as S import qualified Cryptol.TypeCheck as T import qualified Cryptol.TypeCheck.AST as T import qualified Cryptol.Utils.Ident as I +import qualified Data.SBV.Dynamic as SBV + import Criterion.Main main :: IO () @@ -47,13 +55,13 @@ main = defaultMain [ , tc "SHA512" "bench/data/SHA512.cry" ] , bgroup "conc_eval" [ - ceval "AES" "bench/data/AES.cry" "bench bench_data" + ceval "AES" "bench/data/AES.cry" "bench_correct" + , ceval "ZUC" "bench/data/ZUC.cry" "ZUC_TestVectors" , ceval "SHA512" "bench/data/SHA512.cry" "testVector1 ()" ] , bgroup "sym_eval" [ - seval "AES" "bench/data/AES.cry" "aesEncrypt (zero, zero)" - , seval "ZUC" "bench/data/ZUC.cry" - "ZUC_isResistantToCollisionAttack" + seval "AES" "bench/data/AES.cry" "bench_correct" + , seval "ZUC" "bench/data/ZUC.cry" "ZUC_TestVectors" , seval "SHA512" "bench/data/SHA512.cry" "testVector1 ()" ] ] @@ -116,7 +124,11 @@ ceval name path expr = return texpr return (texpr, menv') in env setup $ \ ~(texpr, menv) -> - bench name $ nfIO $ M.runModuleM menv $ M.evalExpr texpr + bench name $ nfIO $ E.runEval $ do + env <- E.evalDecls (S.allDeclGroups menv) mempty + (e :: E.Value) <- E.evalExpr env texpr + E.forceValue e + seval :: String -> FilePath -> T.Text -> Benchmark seval name path expr = @@ -130,6 +142,8 @@ seval name path expr = return texpr return (texpr, menv') in env setup $ \ ~(texpr, menv) -> - bench name $ flip nf texpr $ \texpr' -> - let senv = S.evalDecls mempty (S.allDeclGroups menv) - in S.evalExpr senv texpr' + bench name $ nfIO $ E.runEval $ do + env <- E.evalDecls (S.allDeclGroups menv) mempty + (e :: S.Value) <- E.evalExpr env texpr + E.io $ SBV.compileToSMTLib SBV.SMTLib2 False $ + return (S.fromVBit e) diff --git a/bench/data/AES.cry b/bench/data/AES.cry index 3b95fc87..d98ec1e1 100644 --- a/bench/data/AES.cry +++ b/bench/data/AES.cry @@ -242,9 +242,17 @@ property AESCorrect msg key = aesDecrypt (aesEncrypt (msg, key), key) == msg type nblocks = 128 -bench_data : [128 * nblocks] -bench_data = random 0 +property bench_correct = bench bench_data == bench_result bench : [128 * nblocks] -> [128 * nblocks] bench data = join [ aesEncrypt (block, key) | block <- split data ] - where key = 0x3243f6a8885a308d313198a2e0370734 \ No newline at end of file + where key = 0x3243f6a8885a308d313198a2e0370734 + +bench_data : [128 * nblocks] +bench_data = //random 0 + 0xcddf97f18ad18da94ae27558e975608f673c896a718cffbc90c746160a003d540e353ea1a32cf650c25298cf353b36849f68360e07ad40a9e6c0e4dd2351dce8c06dd82c27642a5e9ce3804780d531af41768b4697b45383d58dfd98c9f2e6d5788e671229529d239b40fc9a52436c437e716cef3c5503d567eff3c2f35d806ae4431455ec096526b1b584cb4a80efde3174361e912a46bf8b7b8d3ca4cebacea935ccd766976614885f5330441ca4acee37c9728fb53708042d9952d8ef3ca544c870a7ee689f8b6d78764368e849274946d0e8bdc69f4a4004cbbce034f1d0a6f8447a756a5f9c217e377909d0c4bde859732e7263c03013c623cb1f2478b77f7838b3d3581e0aba9da951dd18466a131bca89252fc17b9bbe475530d425ac7a79cbc26a941dcc16ded680dddada735c76fa469ebeadf1c8fc33a2c7dc00b865eaec95f1448583425302a9023d39c3bb794685a5e30f196f7c0bdc2b8790d35f8bb9c4359e17ca53e8450da4db030bb67fb4cab68ef4a5edfbe120f1c9824b4faa0cc767bb7304238a798534f065cc1cc8fe310d76c2b440b64348a8e16873eddb5931313573c2cb43a47c2ff0f9c8ec264a0a6ec6474c1056fc7f376c01e5d3b6fea382b5086c7c80bb4c5505f2d4f18dc01cff4baa71eac658ca78e5acbde546dbe85dd71708fb46c8ec00ef75b9b577f93a3c550781a642d5bc4fa2da325656f737d272875b9185fe86a0e0e3eefaf51294d0f06340db93715c99df443e286c0d1e2ae869a7e0d705d6369362a220617ac4803fd205de679ea6ed82881cc2315d73c9cc8f4512ee61afaf127eac098d1d31b075c16aa902024594337c6b2a290cedcbd44190105d20de7ef16fb310400ccbc9ca6a1f4de0a9b1f82b780ee3eda52af664b883c32dd70c860905c0f9e83ee0ae5fc016b81c4c4ca70c05703035637e4988a827bf6e230ba30dc78b8c5663e14273827fb6c4aa700b95a04f1456ce15d18740ee79b7aeb85feffac9f5bd54c9a9bd494a9fc8fab4280316ac8f6552849a798e2b5d7326bb2208fdf2cf6b372311edcd87bb2b1805afd1b6e085fad1a28bc4578e1abea57227f49c141d7d08893d8083249e32cc9645748684cc5d4d492abbdaf5f8373b5e2e4bd91c15346e1d455415395bc0342185665ebeb94fda5fdf7e601961bf1f1109373e935a077a0088980844ce1c87f347380f3c805b01407cf9154f5818db41a6f5d87994df790421a9dbf7d56c11a5e723ec853f32bcf7dc0eef03bbf164564167c6212c35ddd9d6112eb43e4826d1da8f065b804fd48b5ff863b4f4246ba6ebaef90396843e084168d6826abf5f6b0e82c7a7a96707e650e86f82862c5910e0c4d6a48182656e0e76be4017c739feb2da56bb69db4b0885c772180607ce880b15064b5b9878cd1c3d4ae9657c5fdf5ca5d7755807d74e2a57aed4e9fe90c49ed4f01ae3cb812ada6b15c7009d98930d8a41cf23e8f5a962e93c8cecef6044cfcc8843d1f6b5dfb868de036fa5d992c861f056f504f54e8d077028143a2807676c02faf35435ee43cb1ece1a82c7f142be774c824b7e8e3fcad737f58f4818994842ab40a211f9569ad476beef0f2f97be0fb515cf0754641748b2af38d58937c3428a147647911734d54bf06be7f3fcab19b874ff52893af6a45c44adf11c17bf177fc0e90539327373e6594e249aca3a386272d1405455e7e8b463029c0460a31b59b9dc1a15d18cdf1997df250721735651c5e7de7059cb755aa4a0c99962e6485b2ccb02ffecb022fc867e36a63ef77ee8740af2e6f25b0d497d3bcc213a939a47a64057caf107e79661d15f469f8e32b2175bed98af21776a9a2cde4e4982ecd695b4dcef8822806cf74ac73aa5b9d8e6dc0a6d2b97b75d11553a9478296631b7a3c340113247f32bf7a7c42e85b9e517b4f9a09ab453de795f156f09d2704bfa56f5ade38e0eae826796bd54165967332985ecdd4991b8e2bb4016e0d2da173690feace03245c2ef868b44ea7892c0ce15d818a32e5bf57d53a1d86cbb3074221083cfa570c17104da26c063b3a349ce35facd3b7bf267383235a5620217d58201c74105302f3445e024313338fe93dd6f617088b41c836083ceae512782e458c4f5c74bd1987ccb098d1d89fe63a5e5881e56b0c5aba87ef2c5e8d6333d91e9dcbdc45a3c16d67b32c4e51e95231aa7e0b9342c599ebdc6ebb6e4dce1fcd98add42d6ab08707a6f5a38154ad5a3674e8a05105c5ecec180f9661122da31a94e9ad7d337ff5ab4a28a5c5cba9a393f484ed5e5f37bbb4b7caecbf9cbb432cae0b2f6bd5ce6068104f012d6428a9b172847e18f12708de6248cdf0401c865292645fb30114f4f4b53d4473b6ffc53ae0870e85c24f631f52c04d227ea9bc0a59828b6f9eafd95cac13ccfb1cdbae3550b0cd99e1812346d5d01b5a782d1d50fbedf858a4a044fd9384e3a6c10cb4227e276c7399b897b9dcbd2a5cb4e14d8341dd32029938f444fa3dcf2d23198f6bf042439cf96a534f3041774a6c3d5b6bb5bfcd8d7af57402431c7dd758da93ccef39495977cece58087ecc80b278d3e9966b7bd8b183f0379f28aa3c9a885065b8a090f3af15a15acb553b36a73d25a581e7f54f5e1f6f49c4f638ce40ba67629e910a04444d5f6b66c4548b611f851feb08d64fa4d99b83ad218d182d0e86e7f87d4923599a547effed6b9c86e853aef9e60767bff33de916bd799eaf3922ae80abadcc91c95f47e702e2fbd2631d0b77ef85f092204141250c4162b0369be64c1d6bdc2d58c02981cc1de13ae3efba34fbfb3dd0ef3ac4c502a1b87c6ee6bc1a9131b098a85d31560c60c599398d0bd80b37bf4d20df81522b2acc749178fb785 + + +bench_result : [128 * nblocks] +bench_result = + 0x9b00ae426bcc2cd6150a0af62b8be77fbb389c5b061a893588d1918f50f1f31ea1183bd81fd7faae77b4f6321a17130f46e21a2653b1f7dc520bf13305c5e7141cee9d8809d58b9b8ec2aa225120ea6ecec21fba09678bbbeda0b483ad299a8adb7b306599531cf717fd67a1c25e2adeeb48521619991e122b053c3a842936b14b6eea74734a6fc2abea6c1fc4780b2df8059ce9715299eeff7b6577409ebae71285929379cd065df0c249f9696e1b28da476ae52d55d0b1f676c619271d37d4211906d402e4eaf4df3031be5bc00962b7747e7b880bf55bee2882e5008e1c1fed70beb7e54be0545100a2e122b94536b888aaea25dde9e0715dfc892dee2b4fb8e94c6b15a2e77adad1f98e50ffef837309998fcdfd9bcb3d16dcd2a162a3b66c2533474981ba72321aaa9a611c670015fa6cbf9f7d7f26b3da415eccf01872cc3a686f659c0cc0d1d08a1d41470b0ceab527bd6499433a2f2df865982b3f616c246fe49f3a15b676983f7f853f6355bc2f4cdc39e5a29347f7031ab7d2659d0ddfb259fbdfe37eaee2e4dcbdfe0ac584038c5a98d85182ca2424f0e75b7f84d512828ed20bbd05065ed4ba0b850b51c31ecb231f2c879993038d7c9487e0fa46a84a02d4f5408faabd9f41edbbef5d6183dd880ea5b7272a2c46900e02357550c036f4b84168a3e891cd8fe33c2d521ce060a2863bb735e97614d0f5bf40068bfacb02297351db4a5bd80d8140a7e0734550967b2445d4236411e04f83e7f15f5148c9d758994cb8427238cea307ddde786dd74e5565b1dd905d085ebb5a7c725d72164adeeafd7387636c31eee2e729bd0fdf95686f957befdb190101cc23cc9b8e39c652e937bd1e21adad99b86d3b2ed0e4ed4ea4bd9d9ed2ad2b99adf40577fba6b25364cd6d96f79cb0f24ae551021904b57c1d469cfac780ea8469c530ab9d2fe6e98c270c5e1babed259878f48ab5824ebf327d8d18fd2e460334cc0ca9f3b0208c0b322a074185830c460cf58c45cef2234aa5ceb6ac294325bd4d4f9e569531165b9e731c84ffc92f453ce92464658592396f83555284a5f69288e3263d7bd083fa3257b0a11a9d8e4702ed06ebd172eacb7f559527637e0259573b1723c079465d593d5e89163e187ae7ac629ed75e398274daf9c420cac2d3b8f0de82dc9d50cd85d93460213416e3e5c0960c563d26fdb56e1e0dc79b251e95364389f6acbd78edd2664be1edc789b2c7a45b2101c69b3cdb8f9f6a2d7316d2cdca02fb5119d76c9bc93f7bc4e075eee1d453fa4668f368919d14035a7ba293d9787744f44e734443e9abc79a8d7aea71918f0a925026809cf43ae2fd1f6ea00fae2f87d4e7d83e4e86c81695d77e48d5f7080d61d878bde080cec46f4ed19d78f2b0c14db0bb6c871e6506064aa1c7b23c7d2baa9b5db5be3fc94923e09fddc13cd8322d05d990b3a9c5ce418c542eb80b1839a23ed7bc0b588ec957db3df1e1389ff0d541ec2f5331ab92fa7f85efa5ae9ec1c513365df179bb29d4f1914940c68468bd12e9fce04c8d08b6d3f1a4e2d632303ca99656bb248efbb6becad7ac6535678d6534aec746fbca6ec3dec85e4db505872e88bde65214b92eba09b91aff63c5db7e440a1f0ef0bca38759f9aaa35c0b8c565ec4307cc07a3226c992163aaa968ab9b9e507fa4b1910d1c24442615ffea299a8d7fcaf7aa2db3fac83d9f3b8a90bd9ae9100167944e01a07c011d0115870f5079d991d3dccd71fdd23b383b69409a1ba519c22194de6d1048e1195a4c716e0b27055aef816218d94972177732b0abd9df432d8f09293d8b22cc83e05522f7fa46742cd29b63357096601137130dc772717f8f4d02b5651fae2d74f72b25e9266090b95bf3ecb6ddda78edfa47346cf336e79548f9ea09eebe95da8903c86af35cb0abdaa4b78f05b2ef66342072b229a7f030e5b2f8e2ead7a8f5ea2a512cf0f02a4b0fc23e5aef4518f1c40674f5552a040cddf2daf47eec38103e6703720bdf40d68f8de4a9c9a39b1a21a2ea15337772526128abb3234bdce85dd7187a827f7aed625b862887f4ef41f656cc76c5311e34e654e0babe2230d3c1f7554106bab1dcdf18361e5579cf794af967421a1f06f80cfc254a9fa0a5b2a7bebd6dc8bbbf178f9647e356a4fd61e41301386784ba90dfaf5823a0007e50e61a0c3720b9b54edb800ba805e3817cddc7015febed997de87030f3341fad7249ce4530d55f5e0b3aac5a9de0d72c6c5672bc29440354d3a7d88873abdd090f41fa1db8740736583f74c7bfe526b283274f4bc08dea4884ccd75d34df9d8410f7e488b541f467331c5e7da352faa1019c394535472aa0f1ed1512928591e0b4335271df7a7d2d9d7fa1f7f4522be394b39bf15a7bc7a97ad21e171a638eb27d44efd57921938ed70335e3f3a8922553392db8a07e02cd4dc1184edbfbadaf09f97c50268d25dd5e7064968fde486d68b1051cef118d80c7a2c911a8cad22b26fd94f559cc12972b655ce014914cd3c20542815a0ff98ee166611eb2edc147bf2989d4fa1d72d88f7d211d05fe8e312b441edb3627982da6606d0cfa1c696979af5ff371e293c0a749f172343ab5f87ccd8a9d1c364f032e763a939f0696989a5316b48df43763d42170f598326579acba84e16508b5d4ffac1723c9bb98f7736e961c67caf3243b07760b3be602be9995a1a6b8c5360357e9fefab445229ccddd6214476a2c3af0eeadcd067db77ecaf7c84d605b99c89ab583edac68c3c8d951cce207c2df274709fe2d25477f14a8e50bc05f82b2cf49d9b56d97182b90a9395d90f23b9ee734d70d9312c9f6278f0ecd5f90c82f67693a589a94a6555f3abd8eac5408259879603acdc67b6fb \ No newline at end of file diff --git a/cryptol.cabal b/cryptol.cabal index f75ed6d7..9b3c6d01 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -53,6 +53,7 @@ library gitrev >= 1.0, GraphSCC >= 1.0.4, heredoc >= 0.2, + lrucache >= 1.2, monad-control >= 1.0, monadLib >= 3.7.2, old-time >= 1.1, @@ -145,7 +146,7 @@ library Cryptol.Eval, Cryptol.Eval.Arch, Cryptol.Eval.Env, - Cryptol.Eval.Error, + Cryptol.Eval.Monad, Cryptol.Eval.Type, Cryptol.Eval.Value, @@ -253,4 +254,5 @@ benchmark cryptol-bench , criterion , cryptol , deepseq + , sbv , text diff --git a/docs/CryptolPrims.md b/docs/CryptolPrims.md index 16066227..e7a72164 100644 --- a/docs/CryptolPrims.md +++ b/docs/CryptolPrims.md @@ -106,3 +106,5 @@ Debugging undefined : {a} a error : {n a} [n][8] -> a + trace : {n, a, b} [n][8] -> a -> b -> b + traceVal : {n, a} [n][8] -> a -> a diff --git a/docs/ProgrammingCryptol/prims/Primitives.tex b/docs/ProgrammingCryptol/prims/Primitives.tex index 3b26c216..f5e23624 100644 --- a/docs/ProgrammingCryptol/prims/Primitives.tex +++ b/docs/ProgrammingCryptol/prims/Primitives.tex @@ -66,6 +66,8 @@ primsPlaceHolder=1; \begin{Verbatim} error : {a, b} [a][8] -> b undefined : {a} a + trace : {n, a, b} [n][8] -> a -> b -> b + traceVal : {n, a} [n][8] -> a -> a \end{Verbatim} \todo[inline]{\texttt{error} and \texttt{undefined} are not covered in the book at the moment.} diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 561617e2..f3d3e837 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -212,7 +212,6 @@ primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a */ primitive splitAt : {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) - /** * Joins sequences. */ @@ -329,3 +328,30 @@ groupBy = split`{parts=parts} * Define the base 2 logarithm function in terms of width */ type lg2 n = width (max n 1 - 1) + +/** + * Debugging function for tracing. The first argument is a string, + * which is prepended to the printed value of the second argument. + * This combined string is then printed when the trace function is + * evaluated. The return value is equal to the third argument. + * + * The exact timing and number of times the trace message is printed + * depend on the internal details of the Cryptol evaluation order, + * which are unspecified. Thus, the output produced by this + * operation may be difficult to predict. + */ +primitive trace : {n, a, b} [n][8] -> a -> b -> b + +/** + * Debugging function for tracing values. The first argument is a string, + * which is prepended to the printed value of the second argument. + * This combined string is then printed when the trace function is + * evaluated. The return value is equal to the second argument. + * + * The exact timing and number of times the trace message is printed + * depend on the internal details of the Cryptol evaluation order, + * which are unspecified. Thus, the output produced by this + * operation may be difficult to predict. + */ +traceVal : {n, a} [n][8] -> a -> a +traceVal msg x = trace msg x x diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index a1f49562..37c84ce2 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -6,81 +6,145 @@ -- Stability : provisional -- Portability : portable +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ParallelListComp #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Safe #-} {-# LANGUAGE PatternGuards #-} module Cryptol.Eval ( moduleEnv - , EvalEnv() + , runEval + , Eval + , EvalEnv , emptyEnv , evalExpr , evalDecls , EvalError(..) - , WithBase(..) + , forceValue ) where -import Cryptol.Eval.Error import Cryptol.Eval.Env +import Cryptol.Eval.Monad import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name import Cryptol.TypeCheck.AST -import Cryptol.TypeCheck.Solver.InfNat (Nat') +import Cryptol.TypeCheck.Solver.InfNat(Nat'(..)) +import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP -import Cryptol.Prims.Eval -import qualified Data.Map as Map +import Control.Monad +import Control.Monad.Fix +import qualified Data.Sequence as Seq +import Data.IORef +import Data.List +import Data.Maybe +import qualified Data.Map.Strict as Map import Prelude () import Prelude.Compat +type EvalEnv = GenEvalEnv Bool BV +type ReadEnv = EvalEnv + -- Expression Evaluation ------------------------------------------------------- -moduleEnv :: Module -> EvalEnv -> EvalEnv -moduleEnv m env = evalDecls (mDecls m) (evalNewtypes (mNewtypes m) env) +-- | Extend the given evaluation environment with all the declarations +-- contained in the given module. +moduleEnv :: EvalPrims b w + => Module -- ^ Module containing declarations to evaluate + -> GenEvalEnv b w -- ^ Environment to extend + -> Eval (GenEvalEnv b w) +moduleEnv m env = evalDecls (mDecls m) =<< evalNewtypes (mNewtypes m) env -evalExpr :: EvalEnv -> Expr -> Value +-- | Evaluate a Cryptol expression to a value. This evaluator is parameterized +-- by the `EvalPrims` class, which defines the behavior of bits and words, in +-- addition to providing implementations for all the primitives. +evalExpr :: EvalPrims b w + => GenEvalEnv b w -- ^ Evaluation environment + -> Expr -- ^ Expression to evaluate + -> Eval (GenValue b w) evalExpr env expr = case expr of - EList es ty -> VSeq (isTBit (evalValType env ty)) (map (evalExpr env) es) + -- Try to detect when the user has directly written a finite sequence of + -- literal bit values and pack these into a word. + EList es ty + -- 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 $ return $ + case tryFromBits vs of + Just w -> WordVal w + Nothing -> BitsVal $ Seq.fromList $ map (fromVBit <$>) vs + | otherwise -> {-# SCC "evalExpr->EList" #-} + VSeq len <$> finiteSeqMap vs + where + tyv = evalValType (envTypes env) ty + vs = map (evalExpr env) es + len = genericLength es - ETuple es -> VTuple (map eval es) + ETuple es -> {-# SCC "evalExpr->ETuple" #-} do + let xs = map eval es + return $ VTuple xs - ERec fields -> VRecord [ (f,eval e) | (f,e) <- fields ] + ERec fields -> {-# SCC "evalExpr->ERec" #-} do + let xs = [ (f, eval e) + | (f,e) <- fields + ] + return $ VRecord xs - ESel e sel -> evalSel env e sel + ESel e sel -> {-# SCC "evalExpr->ESel" #-} do + x <- eval e + evalSel x sel - EIf c t f | fromVBit (eval c) -> eval t - | otherwise -> eval f + EIf c t f -> {-# SCC "evalExpr->EIf" #-} do + b <- fromVBit <$> eval c + iteValue b (eval t) (eval f) - EComp l h gs -> evalComp env (evalValType env l) h gs + EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do + let len = evalNumType (envTypes env) n + let elty = evalValType (envTypes env) t + evalComp env len elty h gs - EVar n -> case lookupVar n env of - Just val -> val - Nothing -> panic "[Eval] evalExpr" + EVar n -> {-# SCC "evalExpr->EVar" #-} do + case lookupVar n env of + Just val -> val + Nothing -> do + envdoc <- ppEnv defaultPPOpts env + panic "[Eval] evalExpr" ["var `" ++ show (pp n) ++ "` is not defined" - , pretty (WithBase defaultPPOpts env) + , show envdoc ] - ETAbs tv b -> case tpKind tv of - KType -> VPoly $ \ty -> evalExpr (bindType (tpVar tv) (Right ty) env) b - KNum -> VNumPoly $ \n -> evalExpr (bindType (tpVar tv) (Left n) env) b - k -> panic "[Eval] evalExpr" ["invalid kind on type abstraction", show k] + ETAbs tv b -> {-# SCC "evalExpr->ETAbs" #-} + case tpKind tv of + KType -> return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) (Right ty) env) b + KNum -> return $ VNumPoly $ \n -> evalExpr (bindType (tpVar tv) (Left n) env) b + k -> panic "[Eval] evalExpr" ["invalid kind on type abstraction", show k] - ETApp e ty -> case eval e of - VPoly f -> f (evalValType env ty) - VNumPoly f -> f (evalNumType env ty) - val -> panic "[Eval] evalExpr" - ["expected a polymorphic value" - , show (ppV val), show e, show ty - ] + ETApp e ty -> {-# SCC "evalExpr->ETApp" #-} do + eval e >>= \case + VPoly f -> f $! (evalValType (envTypes env) ty) + VNumPoly f -> f $! (evalNumType (envTypes env) ty) + val -> do vdoc <- ppV val + panic "[Eval] evalExpr" + ["expected a polymorphic value" + , show vdoc, show e, show ty + ] - EApp f x -> case eval f of - VFun f' -> f' (eval x) - it -> panic "[Eval] evalExpr" ["not a function", show (ppV it) ] + EApp f x -> {-# SCC "evalExpr->EApp" #-} do + eval f >>= \case + VFun f' -> f' (eval x) + it -> do itdoc <- ppV it + panic "[Eval] evalExpr" ["not a function", show itdoc ] - EAbs n _ty b -> VFun (\ val -> evalExpr (bindVar n val env) b ) + EAbs n _ty b -> {-# SCC "evalExpr->EAbs" #-} + return $ VFun (\v -> do env' <- bindVar n v env + evalExpr env' b) -- XXX these will likely change once there is an evidence value EProofAbs _ e -> evalExpr env e @@ -88,23 +152,31 @@ evalExpr env expr = case expr of ECast e _ty -> evalExpr env e - EWhere e ds -> evalExpr (evalDecls ds env) e + EWhere e ds -> {-# SCC "evalExpr->EWhere" #-} do + env' <- evalDecls ds env + evalExpr env' e where + {-# INLINE eval #-} eval = evalExpr env - ppV = ppValue defaultPPOpts -- Newtypes -------------------------------------------------------------------- -evalNewtypes :: Map.Map Name Newtype -> EvalEnv -> EvalEnv -evalNewtypes nts env = Map.foldl (flip evalNewtype) env nts +evalNewtypes :: EvalPrims b w + => Map.Map Name Newtype + -> GenEvalEnv b w + -> Eval (GenEvalEnv b w) +evalNewtypes nts env = foldM (flip evalNewtype) env $ Map.elems nts -- | Introduce the constructor function for a newtype. -evalNewtype :: Newtype -> EvalEnv -> EvalEnv -evalNewtype nt = bindVar (ntName nt) (foldr tabs con (ntParams nt)) +evalNewtype :: EvalPrims b w + => Newtype + -> GenEvalEnv b w + -> Eval (GenEvalEnv b w) +evalNewtype nt = bindVar (ntName nt) (return (foldr tabs con (ntParams nt))) where tabs _tp body = tlam (\ _ -> body) con = VFun id @@ -112,58 +184,258 @@ evalNewtype nt = bindVar (ntName nt) (foldr tabs con (ntParams nt)) -- Declarations ---------------------------------------------------------------- -evalDecls :: [DeclGroup] -> EvalEnv -> EvalEnv -evalDecls dgs env = foldl (flip evalDeclGroup) env dgs +-- | Extend the given evaluation environment with the result of evaluating the +-- given collection of declaration groups. +evalDecls :: EvalPrims b w + => [DeclGroup] -- ^ Declaration groups to evaluate + -> GenEvalEnv b w -- ^ Environment to extend + -> Eval (GenEvalEnv b w) +evalDecls dgs env = foldM evalDeclGroup env dgs -evalDeclGroup :: DeclGroup -> EvalEnv -> EvalEnv -evalDeclGroup dg env = env' - where - -- the final environment is passed in for each declaration, to permit - -- recursive values. - env' = case dg of - Recursive ds -> foldr (evalDecl env') env ds - NonRecursive d -> evalDecl env d env +evalDeclGroup :: EvalPrims b w + => GenEvalEnv b w + -> DeclGroup + -> Eval (GenEvalEnv b w) +evalDeclGroup env dg = do + case dg of + Recursive ds -> do + -- declare a "hole" for each declaration + -- and extend the evaluation environment + holes <- mapM declHole ds + let holeEnv = Map.fromList $ [ (nm,h) | (nm,_,h,_) <- holes ] + let env' = env `mappend` emptyEnv{ envVars = holeEnv } -evalDecl :: ReadEnv -> Decl -> EvalEnv -> EvalEnv -evalDecl renv d = - bindVar (dName d) $ - case dDefinition d of - DPrim -> evalPrim d - DExpr e -> evalExpr renv e + -- evaluate the declaration bodies, building a new evaluation environment + env'' <- foldM (evalDecl env') env ds + + -- now backfill the holes we declared earlier using the definitions + -- calculcated in the previous step + mapM_ (fillHole env'') holes + + -- return the map containing the holes + return env' + + NonRecursive d -> do + evalDecl env env d + + +-- | This operation is used to complete the process of setting up recursive declaration +-- groups. It 'backfills' previously-allocated thunk values with the actual evaluation +-- procedure for the body of recursive definitions. +-- +-- In order to faithfully evaluate the nonstrict semantics of Cryptol, we have to take some +-- care in this process. In particular, we need to ensure that every recursive definition +-- binding is indistinguishable from it's eta-expanded form. The straightforward solution +-- to this is to force an eta-expansion procedure on all recursive definitions. +-- However, for the so-called 'Value' types we can instead optimisticly use the 'delayFill' +-- operation and only fall back on full eta expansion if the thunk is double-forced. +fillHole :: BitWord b w + => GenEvalEnv b w + -> (Name, Schema, Eval (GenValue b w), Eval (GenValue b w) -> Eval ()) + -> Eval () +fillHole env (nm, sch, _, fill) = do + case lookupVar nm env of + Nothing -> evalPanic "fillHole" ["Recursive definition not completed", show (ppLocName nm)] + Just x + | isValueType env sch -> fill =<< delayFill x (etaDelay (show (ppLocName nm)) env sch x) + | otherwise -> fill (etaDelay (show (ppLocName nm)) env sch x) + + +-- | 'Value' types are non-polymorphic types recursive constructed from +-- bits, finite sequences, tuples and records. Types of this form can +-- be implemented rather more efficently 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 b w -> 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 (map (go . snd) xs) + go _ = False + +isValueType _ _ = False + + +-- | Eta-expand a word value. This forces an unpacked word representation. +etaWord :: BitWord b w + => Integer + -> Eval (GenValue b w) + -> Eval (WordValue b w) +etaWord n x = do + w <- delay Nothing (fromWordVal "during eta-expansion" =<< x) + return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i -> + do w' <- w; indexWordValue w' (toInteger i) + + +-- | Given a simulator value and it's 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 :: BitWord b w + => String + -> GenEvalEnv b w + -> Schema + -> Eval (GenValue b w) + -> Eval (GenValue b w) +etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs + where + goTpVars env [] x = go (evalValType (envTypes env) tp0) x + goTpVars env (v:vs) x = + case tpKind v of + KType -> return $ VPoly $ \t -> + goTpVars (bindType (tpVar v) (Right t) env) vs ( ($t) . fromVPoly =<< x ) + KNum -> return $ VNumPoly $ \n -> + goTpVars (bindType (tpVar v) (Left n) env) vs ( ($n) . fromVNumPoly =<< x ) + k -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k] + + go tp (Ready x) = + case x of + VBit _ -> return x + VWord _ _ -> return x + VSeq n xs + | TVSeq nt el <- tp + -> return $ VSeq n $ SeqMap $ \i -> go el (lookupSeqMap xs i) + + VStream xs + | TVSeq nt el <- tp + -> return $ VStream $ SeqMap $ \i -> go el (lookupSeqMap xs i) + + VTuple xs + | TVTuple ts <- tp + -> return $ VTuple (zipWith go ts xs) + + VRecord fs + | TVRec fts <- tp + -> return $ VRecord $ + let err f = evalPanic "expected record value with field" [show f] in + [ (f, go (fromMaybe (err f) (lookup f fts)) x) + | (f,x) <- fs + ] + + VFun f + | TVFun _t1 t2 <- tp + -> return $ VFun $ \a -> go t2 (f a) + + _ -> evalPanic "type mismatch during eta-expansion" [] + + go tp x = case tp of + TVBit -> x + + TVSeq n TVBit -> + do w <- delayFill (fromWordVal "during eta-expansion" =<< x) (etaWord n x) + return $ VWord n w + + TVSeq n el -> + do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x) + return $ VSeq n $ SeqMap $ \i -> do + go el (flip lookupSeqMap i =<< x') + + TVStream el -> + do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x) + return $ VStream $ SeqMap $ \i -> + go el (flip lookupSeqMap i =<< x') + + TVFun _t1 t2 -> + do x' <- delay (Just msg) (fromVFun <$> x) + return $ VFun $ \a -> go t2 ( ($a) =<< x' ) + + TVTuple ts -> + do let n = length ts + x' <- delay (Just msg) (fromVTuple <$> x) + return $ VTuple $ + [ go t =<< (flip genericIndex i <$> x') + | i <- [0..(n-1)] + | t <- ts + ] + + TVRec fs -> + do x' <- delay (Just msg) (fromVRecord <$> x) + let err f = evalPanic "expected record value with field" [show f] + return $ VRecord $ + [ (f, go t =<< (fromMaybe (err f) . lookup f <$> x')) + | (f,t) <- fs + ] + + +declHole :: Decl + -> Eval (Name, Schema, Eval (GenValue b w), Eval (GenValue b w) -> Eval ()) +declHole d = + case dDefinition d of + DPrim -> evalPanic "Unexpected primitive declaration in recursive group" + [show (ppLocName nm)] + DExpr e -> do + (hole, fill) <- blackhole msg + return (nm, sch, hole, fill) + where + nm = dName d + sch = dSignature d + msg = unwords ["<> while evaluating", show (pp nm)] + + +-- | Evaluate a declaration, extending the evaluation environment. +-- Two input environments are given: the first is an environment +-- to use when evaluating the body of the declaration; the second +-- is the environment to extend. There are two environments to +-- handle the subtle name-binding issues that arise from recurisve +-- definitions. The 'read only' environment is used to bring recursive +-- names into scope while we are still defining them. +evalDecl :: EvalPrims b w + => GenEvalEnv b w -- ^ A 'read only' environment for use in declaration bodies + -> GenEvalEnv b w -- ^ An evalaution environment to extend with the given declaration + -> Decl -- ^ The declaration to evaluate + -> Eval (GenEvalEnv b w) +evalDecl renv env d = + case dDefinition d of + DPrim -> bindVarDirect (dName d) (evalPrim d) env + DExpr e -> bindVar (dName d) (evalExpr renv e) env -- Selectors ------------------------------------------------------------------- -evalSel :: ReadEnv -> Expr -> Selector -> Value -evalSel env e sel = case sel of +-- | 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). +evalSel :: forall b w + . EvalPrims b w + => GenValue b w + -> Selector + -> Eval (GenValue b w) +evalSel val sel = case sel of TupleSel n _ -> tupleSel n val RecordSel n _ -> recordSel n val - ListSel ix _ -> fromSeq val !! ix - + ListSel ix _ -> case val of + VSeq _ xs' -> lookupSeqMap xs' (toInteger ix) + VStream xs' -> lookupSeqMap xs' (toInteger ix) + VWord _ wv -> VBit <$> (flip indexWordValue (toInteger ix) =<< wv) where - val = evalExpr env e - tupleSel n v = case v of - VTuple vs -> vs !! n - VSeq False vs -> VSeq False [ tupleSel n v1 | v1 <- vs ] - VStream vs -> VStream [ tupleSel n v1 | v1 <- vs ] - VFun f -> VFun (\x -> tupleSel n (f x)) - _ -> evalPanic "Cryptol.Eval.evalSel" - [ "Unexpected value in tuple selection" - , show (ppValue defaultPPOpts v) ] + VTuple vs -> vs !! n + VSeq w vs -> VSeq w <$> mapSeqMap (tupleSel n) vs + VStream vs -> VStream <$> mapSeqMap (tupleSel n) vs + VFun f -> return $ VFun (\x -> tupleSel n =<< f x) + _ -> do vdoc <- ppValue defaultPPOpts v + evalPanic "Cryptol.Eval.evalSel" + [ "Unexpected value in tuple selection" + , show vdoc ] recordSel n v = case v of - VRecord {} -> lookupRecord n v - VSeq False vs -> VSeq False [ recordSel n v1 | v1 <- vs ] - VStream vs -> VStream [recordSel n v1 | v1 <- vs ] - VFun f -> VFun (\x -> recordSel n (f x)) - _ -> evalPanic "Cryptol.Eval.evalSel" - [ "Unexpected value in record selection" - , show (ppValue defaultPPOpts v) ] + VRecord {} -> lookupRecord n v + VSeq w vs -> VSeq w <$> mapSeqMap (recordSel n) vs + VStream vs -> VStream <$> mapSeqMap (recordSel n) vs + VFun f -> return $ VFun (\x -> recordSel n =<< f x) + _ -> do vdoc <- ppValue defaultPPOpts v + evalPanic "Cryptol.Eval.evalSel" + [ "Unexpected value in record selection" + , show vdoc ] @@ -171,110 +443,128 @@ evalSel env e sel = case sel of -- List Comprehension Environments --------------------------------------------- --- | A variation of the ZipList type from Control.Applicative, with a --- separate constructor for pure values. This datatype is used to --- represent the list of values that each variable takes on within a --- list comprehension. The @Zip@ constructor is for bindings that take --- different values at different positions in the list, while the --- @Pure@ constructor is for bindings originating outside the list --- comprehension, which have the same value for all list positions. -data ZList a = Pure a | Zip [a] - -getZList :: ZList a -> [a] -getZList (Pure x) = repeat x -getZList (Zip xs) = xs - -instance Functor ZList where - fmap f (Pure x) = Pure (f x) - fmap f (Zip xs) = Zip (map f xs) - -instance Applicative ZList where - pure x = Pure x - Pure f <*> Pure x = Pure (f x) - Pure f <*> Zip xs = Zip (map f xs) - Zip fs <*> Pure x = Zip (map ($ x) fs) - Zip fs <*> Zip xs = Zip (zipWith ($) fs xs) - -- | Evaluation environments for list comprehensions: Each variable -- name is bound to a list of values, one for each element in the list -- comprehension. -data ListEnv = ListEnv - { leVars :: Map.Map Name (ZList Value) - , leTypes :: Map.Map TVar (Either Nat' TValue) +data ListEnv b w = ListEnv + { leVars :: !(Map.Map Name (Integer -> Eval (GenValue b w))) + -- ^ Bindings whose values vary by position + , leStatic :: !(Map.Map Name (Eval (GenValue b w))) + -- ^ Bindings whose values are constant + , leTypes :: !TypeEnv } -instance Monoid ListEnv where +instance Monoid (ListEnv b w) where mempty = ListEnv - { leVars = Map.empty - , leTypes = Map.empty + { leVars = Map.empty + , leStatic = Map.empty + , leTypes = Map.empty } mappend l r = ListEnv - { leVars = Map.union (leVars l) (leVars r) - , leTypes = Map.union (leTypes l) (leTypes r) + { leVars = Map.union (leVars l) (leVars r) + , leStatic = Map.union (leStatic l) (leStatic r) + , leTypes = Map.union (leTypes l) (leTypes r) } -toListEnv :: EvalEnv -> ListEnv +toListEnv :: GenEvalEnv b w -> ListEnv b w toListEnv e = ListEnv - { leVars = fmap Pure (envVars e) - , leTypes = envTypes e + { leVars = mempty + , leStatic = envVars e + , leTypes = envTypes e } --- | Take parallel slices of the list environment. If some names are --- bound to longer lists of values (e.g. if they come from a different --- parallel branch of a comprehension) then the last elements will be --- dropped as the lists are zipped together. -zipListEnv :: ListEnv -> [EvalEnv] -zipListEnv (ListEnv vm tm) = - [ EvalEnv { envVars = v, envTypes = tm } - | v <- getZList (sequenceA vm) ] - -bindVarList :: Name -> [Value] -> ListEnv -> ListEnv -bindVarList n vs lenv = lenv { leVars = Map.insert n (Zip vs) (leVars lenv) } +-- | Evaluate a list environment at a position. +-- This choses a particular value for the varying +-- locations. +evalListEnv :: ListEnv b w -> Integer -> GenEvalEnv b w +evalListEnv (ListEnv vm st tm) i = + let v = fmap ($i) vm + in EvalEnv{ envVars = Map.union v st + , envTypes = tm + } +bindVarList :: Name + -> (Integer -> Eval (GenValue b w)) + -> ListEnv b w + -> ListEnv b w +bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) } -- List Comprehensions --------------------------------------------------------- -- | Evaluate a comprehension. -evalComp :: ReadEnv -> TValue -> Expr -> [[Match]] -> Value -evalComp env seqty body ms = - case isTSeq seqty of - Just (len, el) -> toSeq len el [ evalExpr e body | e <- envs ] - _ -> evalPanic "Cryptol.Eval" ["evalComp given a non sequence", show seqty] - - -- XXX we could potentially print this as a number if the type was available. - where - -- generate a new environment for each iteration of each parallel branch - benvs :: [ListEnv] - benvs = map (branchEnvs (toListEnv env)) ms - - -- join environments to produce environments at each step through the process. - envs :: [EvalEnv] - envs = zipListEnv (mconcat benvs) +evalComp :: EvalPrims b w + => GenEvalEnv b w -- ^ Starting evaluation environment + -> Nat' -- ^ Length of the comprehension + -> TValue -- ^ Type of the comprehension elements + -> Expr -- ^ Head expression of the comprehension + -> [[Match]] -- ^ List of parallel comprehension branches + -> Eval (GenValue b w) +evalComp env len elty body ms = + do lenv <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms + mkSeq len elty <$> memoMap (SeqMap $ \i -> do + evalExpr (evalListEnv lenv i) body) -- | Turn a list of matches into the final environments for each iteration of -- the branch. -branchEnvs :: ListEnv -> [Match] -> ListEnv -branchEnvs env matches = foldl evalMatch env matches +branchEnvs :: EvalPrims b w + => ListEnv b w + -> [Match] + -> Eval (ListEnv b w) +branchEnvs env matches = foldM evalMatch env matches -- | Turn a match into the list of environments it represents. -evalMatch :: ListEnv -> Match -> ListEnv +evalMatch :: EvalPrims b w + => ListEnv b w + -> Match + -> Eval (ListEnv b w) evalMatch lenv m = case m of -- many envs - From n _ty expr -> bindVarList n (concat vss) lenv' + From n l ty expr -> + case len of + -- Select from a sequence of finite length. This causes us to 'stutter' + -- through our previous choices `nLen` times. + Nat nLen -> do + vss <- memoMap $ SeqMap $ \i -> evalExpr (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 r =<< w) + VSeq _ xs' -> lookupSeqMap xs' r + VStream xs' -> lookupSeqMap xs' r + return $ 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 + -- `leVars` elements of the comprehension environment into `leStatic` elements + -- by selecting out the 0th element. + Inf -> do + let allvars = Map.union (fmap ($0) (leVars lenv)) (leStatic lenv) + let lenv' = lenv { leVars = Map.empty + , leStatic = allvars + } + let env = EvalEnv allvars (leTypes lenv) + xs <- evalExpr env expr + let vs i = case xs of + VWord _ w -> VBit <$> (flip indexWordValue i =<< w) + VSeq _ xs' -> lookupSeqMap xs' i + VStream xs' -> lookupSeqMap xs' i + return $ bindVarList n vs lenv' + where - vss = [ fromSeq (evalExpr env expr) | env <- zipListEnv lenv ] - stutter (Pure x) = Pure x - stutter (Zip xs) = Zip [ x | (x, vs) <- zip xs vss, _ <- vs ] - lenv' = lenv { leVars = fmap stutter (leVars lenv) } + len = evalNumType (leTypes lenv) l -- 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 -> bindVarList (dName d) (map f (zipListEnv lenv)) lenv - where f env = - case dDefinition d of - DPrim -> evalPrim d - DExpr e -> evalExpr env e + Let d -> return $ bindVarList (dName d) (\i -> f (evalListEnv lenv i)) lenv + where + f env = + case dDefinition d of + -- Primitives here should never happen, I think... + -- perhaps this should be converted to an error. + DPrim -> return $ evalPrim d + DExpr e -> evalExpr env e diff --git a/src/Cryptol/Eval/Env.hs b/src/Cryptol/Eval/Env.hs index b32a7aa5..cb81685c 100644 --- a/src/Cryptol/Eval/Env.hs +++ b/src/Cryptol/Eval/Env.hs @@ -14,13 +14,16 @@ {-# LANGUAGE DeriveGeneric #-} module Cryptol.Eval.Env where +import Cryptol.Eval.Monad( Eval, delay, ready ) +import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.ModuleSystem.Name import Cryptol.TypeCheck.AST -import Cryptol.TypeCheck.Solver.InfNat (Nat'(..)) +import Cryptol.TypeCheck.Solver.InfNat import Cryptol.Utils.PP -import qualified Data.Map as Map + +import qualified Data.Map.Strict as Map import GHC.Generics (Generic) import Control.DeepSeq @@ -30,14 +33,12 @@ import Prelude.Compat -- Evaluation Environment ------------------------------------------------------ -type ReadEnv = EvalEnv - -data EvalEnv = EvalEnv - { envVars :: Map.Map Name Value - , envTypes :: Map.Map TVar (Either Nat' TValue) +data GenEvalEnv b w = EvalEnv + { envVars :: !(Map.Map Name (Eval (GenValue b w))) + , envTypes :: !TypeEnv } deriving (Generic, NFData) -instance Monoid EvalEnv where +instance Monoid (GenEvalEnv b w) where mempty = EvalEnv { envVars = Map.empty , envTypes = Map.empty @@ -48,26 +49,47 @@ instance Monoid EvalEnv where , envTypes = Map.union (envTypes l) (envTypes r) } -instance PP (WithBase EvalEnv) where - ppPrec _ (WithBase opts env) = brackets (fsep (map bind (Map.toList (envVars env)))) - where - bind (k,v) = pp k <+> text "->" <+> ppValue opts v +ppEnv :: BitWord b w => PPOpts -> GenEvalEnv b w -> Eval Doc +ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env)) + where + bind (k,v) = do vdoc <- ppValue opts =<< v + return (pp k <+> text "->" <+> vdoc) -emptyEnv :: EvalEnv +-- | Evaluation environment with no bindings +emptyEnv :: GenEvalEnv b w emptyEnv = mempty -- | Bind a variable in the evaluation environment. -bindVar :: Name -> Value -> EvalEnv -> EvalEnv -bindVar n val env = env { envVars = Map.insert n val (envVars env) } +bindVar :: Name + -> Eval (GenValue b w) + -> GenEvalEnv b w + -> Eval (GenEvalEnv b w) +bindVar n val env = do + let nm = show $ ppLocName n + val' <- delay (Just nm) val + return $ env{ envVars = Map.insert n val' (envVars env) } + +-- | Bind a variable to a value in the evaluation environment, without +-- creating a thunk. +bindVarDirect :: Name + -> GenValue b w + -> GenEvalEnv b w + -> Eval (GenEvalEnv b w) +bindVarDirect n val env = do + return $ env{ envVars = Map.insert n (ready val) (envVars env) } -- | Lookup a variable in the environment. -lookupVar :: Name -> EvalEnv -> Maybe Value +{-# INLINE lookupVar #-} +lookupVar :: Name -> GenEvalEnv b w -> Maybe (Eval (GenValue b w)) lookupVar n env = Map.lookup n (envVars env) --- | Bind a type variable of kind # or *. -bindType :: TVar -> Either Nat' TValue -> EvalEnv -> EvalEnv +-- | Bind a type variable of kind *. +{-# INLINE bindType #-} +bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w -> GenEvalEnv b w bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) } -- | Lookup a type variable. -lookupType :: TVar -> EvalEnv -> Maybe (Either Nat' TValue) +{-# INLINE lookupType #-} +lookupType :: TVar -> GenEvalEnv b w -> Maybe (Either Nat' TValue) lookupType p env = Map.lookup p (envTypes env) + diff --git a/src/Cryptol/Eval/Error.hs b/src/Cryptol/Eval/Error.hs deleted file mode 100644 index 75ff7b1a..00000000 --- a/src/Cryptol/Eval/Error.hs +++ /dev/null @@ -1,69 +0,0 @@ --- | --- Module : $Header$ --- Copyright : (c) 2013-2016 Galois, Inc. --- License : BSD3 --- Maintainer : cryptol@galois.com --- Stability : provisional --- Portability : portable - -{-# LANGUAGE Safe #-} -{-# LANGUAGE DeriveDataTypeable #-} - -module Cryptol.Eval.Error where - -import Cryptol.Utils.Panic -import Cryptol.Utils.PP -import Cryptol.TypeCheck.AST(Type) - -import Data.Typeable (Typeable) -import qualified Control.Exception as X - - --- Errors ---------------------------------------------------------------------- - --- | Panic from an Eval context. -evalPanic :: String -> [String] -> a -evalPanic cxt = panic ("[Eval] " ++ cxt) - - -data EvalError - = InvalidIndex Integer - | TypeCannotBeDemoted Type - | DivideByZero - | WordTooWide Integer - | UserError String - deriving (Typeable,Show) - -instance PP EvalError where - ppPrec _ e = case e of - InvalidIndex i -> text "invalid sequence index:" <+> integer i - TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t - DivideByZero -> text "division by 0" - WordTooWide w -> - text "word too wide for memory:" <+> integer w <+> text "bits" - UserError x -> text "Run-time error:" <+> text x - -instance X.Exception EvalError - --- | A sequencing operation has gotten an invalid index. -invalidIndex :: Integer -> a -invalidIndex i = X.throw (InvalidIndex i) - --- | For things like `(inf) or `(0-1) -typeCannotBeDemoted :: Type -> a -typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t) - --- | For division by 0. -divideByZero :: a -divideByZero = X.throw DivideByZero - --- | For when we know that a word is too wide and will exceed gmp's --- limits (though words approaching this size will probably cause the --- system to crash anyway due to lack of memory) -wordTooWide :: Integer -> a -wordTooWide w = X.throw (WordTooWide w) - --- | For `error` -cryUserError :: String -> a -cryUserError msg = X.throw (UserError msg) - diff --git a/src/Cryptol/Eval/Monad.hs b/src/Cryptol/Eval/Monad.hs new file mode 100644 index 00000000..d7540bde --- /dev/null +++ b/src/Cryptol/Eval/Monad.hs @@ -0,0 +1,209 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + +{-# LANGUAGE Safe #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor #-} + +module Cryptol.Eval.Monad +( -- * Evaluation monad + Eval(..) +, runEval +, io +, delay +, delayFill +, ready +, blackhole + -- * Error repoprting +, EvalError(..) +, evalPanic +, typeCannotBeDemoted +, divideByZero +, wordTooWide +, cryUserError +, cryLoopError +, invalidIndex +) where + +import Control.DeepSeq +import Control.Monad +import Control.Monad.Fix +import Control.Monad.IO.Class +import Data.IORef +import Data.Typeable (Typeable) +import qualified Control.Exception as X + + +import Cryptol.Utils.Panic +import Cryptol.Utils.PP +import Cryptol.TypeCheck.AST(Type) + + +ready :: a -> Eval a +ready a = Ready a + +-- | The monad for Cryptol evaluation. +data Eval a + = Ready !a + | Thunk !(IO a) + +data ThunkState a + = Unforced -- ^ This thunk has not yet been forced + | BlackHole -- ^ This thunk is currently being evaluated + | Forced !a -- ^ This thunk has previously been forced, and has the given value + +{-# INLINE delay #-} +-- | Delay the given evaluation computation, returning a thunk +-- which will run the computation when forced. Raise a loop +-- error if the resulting thunk is forced during it's own evaluation. +delay :: Maybe String -- ^ Optional name to print if a loop is detected + -> Eval a -- ^ Computation to delay + -> Eval (Eval a) +delay _ (Ready a) = Ready (Ready a) +delay msg (Thunk x) = Thunk $ do + let msg' = maybe "" ("while evaluating "++) msg + let retry = cryLoopError msg' + r <- newIORef Unforced + return $ unDelay retry r x + +{-# INLINE delayFill #-} + +-- | Delay the given evaluation computation, returning a thunk +-- which will run the computation when forced. Run the 'retry' +-- computation instead if the resulting thunk is forced during +-- it's own evaluation. +delayFill :: Eval a -- ^ Computation to delay + -> Eval a -- ^ Backup computation to run if a tight loop is detected + -> Eval (Eval a) +delayFill (Ready x) _ = Ready (Ready x) +delayFill (Thunk x) retry = Thunk $ do + r <- newIORef Unforced + return $ unDelay retry r x + +-- | Produce a thunk value which can be filled with its associcated computation +-- after the fact. A preallocated thunk is returned, along with an operation to +-- fill the thunk with the associated computation. +-- This is used to implement recursive declaration groups. +blackhole :: String -- ^ A name to associated with this thunk. + -> Eval (Eval a, Eval a -> Eval ()) +blackhole msg = do + r <- io $ newIORef (fail msg) + let get = join (io $ readIORef r) + let set = io . writeIORef r + return (get, set) + +unDelay :: Eval a -> IORef (ThunkState a) -> IO a -> Eval a +unDelay retry r x = do + rval <- io $ readIORef r + case rval of + Forced val -> return val + BlackHole -> + retry + Unforced -> io $ do + writeIORef r BlackHole + val <- x + writeIORef r (Forced val) + return val + +-- | Execute the given evaluation action. +runEval :: Eval a -> IO a +runEval (Ready a) = return a +runEval (Thunk x) = x + +{-# INLINE evalBind #-} +evalBind :: Eval a -> (a -> Eval b) -> Eval b +evalBind (Ready a) f = f a +evalBind (Thunk x) f = Thunk (x >>= runEval . f) + +instance Functor Eval where + fmap f (Ready x) = Ready (f x) + fmap f (Thunk m) = Thunk (f <$> m) + {-# INLINE fmap #-} + +instance Applicative Eval where + pure = return + (<*>) = ap + {-# INLINE pure #-} + {-# INLINE (<*>) #-} + +instance Monad Eval where + return = Ready + fail = Thunk . fail + (>>=) = evalBind + {-# INLINE return #-} + {-# INLINE (>>=) #-} + +instance MonadIO Eval where + liftIO = io + +instance NFData a => NFData (Eval a) where + rnf (Ready a) = rnf a + rnf (Thunk _) = () + +instance MonadFix Eval where + mfix f = Thunk $ mfix (\x -> runEval (f x)) + +io :: IO a -> Eval a +io = Thunk +{-# INLINE io #-} + + +-- Errors ---------------------------------------------------------------------- + +-- | Panic from an Eval context. +evalPanic :: String -> [String] -> a +evalPanic cxt = panic ("[Eval] " ++ cxt) + + +-- | Data type describing errors that can occur during evaluation +data EvalError + = InvalidIndex Integer -- ^ Out-of-bounds index + | TypeCannotBeDemoted Type -- ^ Non-numeric type passed to demote function + | DivideByZero -- ^ Division or modulus by 0 + | WordTooWide Integer -- ^ Bitvector too large + | UserError String -- ^ Call to the Cryptol 'error' primitive + | LoopError String -- ^ Detectable nontermination + deriving (Typeable,Show) + +instance PP EvalError where + ppPrec _ e = case e of + InvalidIndex i -> text "invalid sequence index:" <+> integer i + TypeCannotBeDemoted t -> text "type cannot be demoted:" <+> pp t + DivideByZero -> text "division by 0" + WordTooWide w -> + text "word too wide for memory:" <+> integer w <+> text "bits" + UserError x -> text "Run-time error:" <+> text x + LoopError x -> text "<>" <+> text x + +instance X.Exception EvalError + +-- | For things like `(inf) or `(0-1) +typeCannotBeDemoted :: Type -> a +typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t) + +-- | For division by 0. +divideByZero :: a +divideByZero = X.throw DivideByZero + +-- | For when we know that a word is too wide and will exceed gmp's +-- limits (though words approaching this size will probably cause the +-- system to crash anyway due to lack of memory) +wordTooWide :: Integer -> a +wordTooWide w = X.throw (WordTooWide w) + +-- | For `error` +cryUserError :: String -> Eval a +cryUserError msg = Thunk (X.throwIO (UserError msg)) + +-- | For cases where we can detect tight loops +cryLoopError :: String -> Eval a +cryLoopError msg = Thunk (X.throwIO (LoopError msg)) + +-- | A sequencing operation has gotten an invalid index. +invalidIndex :: Integer -> Eval a +invalidIndex i = Thunk (X.throwIO (InvalidIndex i)) diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index eb8d7558..6bd407c8 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -7,26 +7,79 @@ -- Portability : portable {-# LANGUAGE Safe, PatternGuards #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +module Cryptol.Eval.Type where -module Cryptol.Eval.Type (evalType, evalValType, evalNumType, evalTF) where - -import Cryptol.Eval.Env -import Cryptol.Eval.Error -import Cryptol.Eval.Value (TValue(..), tvSeq) +import Cryptol.Eval.Monad import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat +import Cryptol.Utils.Panic (panic) +import Cryptol.Utils.Ident (Ident) import Data.Maybe(fromMaybe) +import qualified Data.Map.Strict as Map +import GHC.Generics (Generic) +import Control.DeepSeq + +-- | An evaluated type of kind *. +-- These types do not contain type variables, type synonyms, or type functions. +data TValue + = TVBit -- ^ @ Bit @ + | TVSeq Integer TValue -- ^ @ [n]a @ + | TVStream TValue -- ^ @ [inf]t @ + | TVTuple [TValue] -- ^ @ (a, b, c )@ + | TVRec [(Ident, TValue)] -- ^ @ { x : a, y : b, z : c } @ + | TVFun TValue TValue -- ^ @ a -> b @ + deriving (Generic, NFData) + +-- | Convert a type value back into a regular type +tValTy :: TValue -> Type +tValTy tv = + case tv of + TVBit -> tBit + TVSeq n t -> tSeq (tNum n) (tValTy t) + TVStream t -> tSeq tInf (tValTy t) + TVTuple ts -> tTuple (map tValTy ts) + TVRec fs -> tRec [ (f, tValTy t) | (f, t) <- fs ] + TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2) + +instance Show TValue where + showsPrec p v = showsPrec p (tValTy v) + + +-- Utilities ------------------------------------------------------------------- + +-- | True if the evaluated value is @Bit@ +isTBit :: TValue -> Bool +isTBit TVBit = True +isTBit _ = False + +-- | Produce a sequence type value +tvSeq :: Nat' -> TValue -> TValue +tvSeq (Nat n) t = TVSeq n t +tvSeq Inf t = TVStream t + +-- | Coerce an extended natural into an integer, +-- for values known to be finite +finNat' :: Nat' -> Integer +finNat' n' = + case n' of + Nat x -> x + Inf -> panic "Cryptol.Eval.Value.finNat'" [ "Unexpected `inf`" ] -- Type Evaluation ------------------------------------------------------------- +type TypeEnv = Map.Map TVar (Either Nat' TValue) + + -- | Evaluation for types (kind * or #). -evalType :: EvalEnv -> Type -> Either Nat' TValue +evalType :: TypeEnv -> Type -> Either Nat' TValue evalType env ty = case ty of TVar tv -> - case lookupType tv env of + case Map.lookup tv env of Just v -> v Nothing -> evalPanic "evalType" ["type variable not bound", show tv] @@ -49,18 +102,20 @@ evalType env ty = num = evalNumType env -- | Evaluation for value types (kind *). -evalValType :: EvalEnv -> Type -> TValue +evalValType :: TypeEnv -> Type -> TValue evalValType env ty = case evalType env ty of Left _ -> evalPanic "evalValType" ["expected value type, found numeric type"] Right t -> t -evalNumType :: EvalEnv -> Type -> Nat' +-- | Evaluation for number types (kind #). +evalNumType :: TypeEnv -> Type -> Nat' evalNumType env ty = case evalType env ty of Left n -> n Right _ -> evalPanic "evalValType" ["expected numeric type, found value type"] + -- | Reduce type functions, raising an exception for undefined values. evalTF :: TFun -> [Nat'] -> Nat' evalTF f vs diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs index 8fd8e531..dcc0305b 100644 --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -11,112 +11,234 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + module Cryptol.Eval.Value where +import Data.Bits +import qualified Data.Sequence as Seq +import qualified Data.Foldable as Fold + +import MonadLib + import qualified Cryptol.Eval.Arch as Arch -import Cryptol.Eval.Error +import Cryptol.Eval.Monad +import Cryptol.Eval.Type + import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat(Nat'(..)) import Cryptol.Utils.Ident (Ident,mkIdent) import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) -import Control.Monad (guard, zipWithM) -import Data.List(genericTake) -import Data.Bits (setBit,testBit,(.&.),shiftL) +import Data.List(genericLength, genericIndex) import qualified Data.Text as T import Numeric (showIntAtBase) import GHC.Generics (Generic) import Control.DeepSeq --- Utilities ------------------------------------------------------------------- +import qualified Data.Cache.LRU.IO as LRU -isTBit :: TValue -> Bool -isTBit TVBit = True -isTBit _ = False - -isTSeq :: TValue -> Maybe (Nat', TValue) -isTSeq (TVSeq n t) = Just (Nat n, t) -isTSeq (TVStream t) = Just (Inf, t) -isTSeq _ = Nothing - -isTFun :: TValue -> Maybe (TValue, TValue) -isTFun (TVFun t1 t2) = Just (t1, t2) -isTFun _ = Nothing - -isTTuple :: TValue -> Maybe (Int,[TValue]) -isTTuple (TVTuple ts) = Just (length ts, ts) -isTTuple _ = Nothing - -isTRec :: TValue -> Maybe [(Ident, TValue)] -isTRec (TVRec fs) = Just fs -isTRec _ = Nothing - -tvSeq :: Nat' -> TValue -> TValue -tvSeq (Nat n) t = TVSeq n t -tvSeq Inf t = TVStream t - -finNat' :: Nat' -> Integer -finNat' n' = - case n' of - Nat x -> x - Inf -> panic "Cryptol.Eval.Value.finNat'" [ "Unexpected `inf`" ] -- Values ---------------------------------------------------------------------- --- | width, value +-- | Concrete bitvector values: width, value -- Invariant: The value must be within the range 0 .. 2^width-1 data BV = BV !Integer !Integer deriving (Generic, NFData) +instance Show BV where + show = show . bvVal + +-- | Apply an integer function to the values of bitvectors. +-- This function assumes both bitvectors are the same width. +binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV +binBV f (BV w x) (BV _ y) = mkBv w (f x y) + +-- | Apply an integer function to the values of a bitvector. +-- This function assumes the function will not require masking. +unaryBV :: (Integer -> Integer) -> BV -> BV +unaryBV f (BV w x) = mkBv w $ f x + +bvVal :: BV -> Integer +bvVal (BV _w x) = x + -- | Smart constructor for 'BV's that checks for the width limit mkBv :: Integer -> Integer -> BV mkBv w i = BV w (mask w i) +-- | A sequence map represents a mapping from nonnegative integer indices +-- to values. These are used to represent both finite and infinite sequences. +newtype SeqMap b w = SeqMap { lookupSeqMap :: Integer -> Eval (GenValue b w) } +type SeqValMap = SeqMap Bool BV + +instance NFData (SeqMap b w) where + rnf x = seq x () + +-- | Generate a finite sequence map from a list of values +finiteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w) +finiteSeqMap xs = do + memoMap (SeqMap $ \i -> genericIndex xs i) + +-- | Generate an infinite sequence map from a stream of values +infiniteSeqMap :: [Eval (GenValue b w)] -> Eval (SeqMap b w) +infiniteSeqMap xs = + memoMap (SeqMap $ \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 b w -> [Eval (GenValue b w)] +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 b w -> [Eval (GenValue b w)] +streamSeqMap m = [ lookupSeqMap m i | i <- [0..] ] + +-- | Reverse the order of a finite sequence map +reverseSeqMap :: Integer -- ^ Size of the sequence map + -> SeqMap b w + -> SeqMap b w +reverseSeqMap n vals = SeqMap $ \i -> lookupSeqMap vals (n - 1 - i) + +-- | 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 b w -> (SeqMap b w, SeqMap b w) +splitSeqMap n xs = (hd,tl) + where + hd = xs + tl = SeqMap $ \i -> lookupSeqMap xs (i+n) + +-- | Given a sequence map, return a new sequence map that is memoized using +-- fixed sized memo table. The memo table is managed using a Least-Recently-Used +-- (LRU) cache eviction policy. +-- +-- Currently, the cache size is fixed at 64 elements. +-- This seems to provide a good compromize between memory useage and effective +-- memoization. +memoMap :: SeqMap b w -> Eval (SeqMap b w) +memoMap x = do + -- TODO: make the size of the LRU cache a tuneable parameter... + let lruSize = 64 + lru <- io $ LRU.newAtomicLRU (Just lruSize) + return $ SeqMap $ memo lru + + where + memo lru i = do + mz <- io $ LRU.lookup i lru + case mz of + Just z -> return z + Nothing -> doEval lru i + + doEval lru i = do + v <- lookupSeqMap x i + io $ LRU.insert i v lru + return v + +-- | Apply the given evaluation function pointwise to the two given +-- sequence maps. +zipSeqMap :: (GenValue b w -> GenValue b w -> Eval (GenValue b w)) + -> SeqMap b w + -> SeqMap b w + -> Eval (SeqMap b w) +zipSeqMap f x y = + memoMap (SeqMap $ \i -> join (f <$> lookupSeqMap x i <*> lookupSeqMap y i)) + +-- | Apply the given function to each value in the given sequence map +mapSeqMap :: (GenValue b w -> Eval (GenValue b w)) + -> SeqMap b w -> Eval (SeqMap b w) +mapSeqMap f x = + memoMap (SeqMap $ \i -> f =<< lookupSeqMap x i) + +-- | For efficency 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 evalautor) 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 b w + = WordVal !w -- ^ Packed word representation for bit sequences. + | BitsVal !(Seq.Seq (Eval b)) -- ^ Sequence of thunks representing bits. + deriving (Generic, NFData) + +-- | Force a word value into packed word form +asWordVal :: BitWord b w => WordValue b w -> Eval w +asWordVal (WordVal w) = return w +asWordVal (BitsVal bs) = packWord <$> sequence (Fold.toList bs) + +-- | Force a word value into a sequence of bits +asBitsVal :: BitWord b w => WordValue b w -> Seq.Seq (Eval b) +asBitsVal (WordVal w) = Seq.fromList $ map ready $ unpackWord w +asBitsVal (BitsVal bs) = bs + +-- | Select an individual bit from a word value +indexWordValue :: BitWord b w => WordValue b w -> Integer -> Eval b +indexWordValue (WordVal w) idx = return $ genericIndex (unpackWord w) idx +indexWordValue (BitsVal bs) idx = Seq.index bs (fromInteger idx) + + -- | Generic value type, parameterized by bit and word types. +-- +-- NOTE: we maintain an important invariant regarding sequence types. +-- `VSeq` must never be used for finite sequences of bits. +-- Always use the `VWord` constructor instead! Infinite sequences of bits +-- are handled by the `VStream` constructor, just as for other types. data GenValue b w - = VRecord [(Ident, GenValue b w)] -- @ { .. } @ - | VTuple [GenValue b w] -- @ ( .. ) @ - | VBit b -- @ Bit @ - | VSeq Bool [GenValue b w] -- @ [n]a @ - -- The boolean parameter indicates whether or not - -- this is a sequence of bits. - | VWord w -- @ [n]Bit @ - | VStream [GenValue b w] -- @ [inf]a @ - | VFun (GenValue b w -> GenValue b w) -- functions - | VPoly (TValue -> GenValue b w) -- polymorphic values (kind *) - | VNumPoly (Nat' -> GenValue b w) -- polymorphic values (kind #) - deriving (Generic, NFData) + = VRecord ![(Ident, Eval (GenValue b w))] -- ^ @ { .. } @ + | VTuple ![Eval (GenValue b w)] -- ^ @ ( .. ) @ + | VBit !b -- ^ @ Bit @ + | VSeq !Integer !(SeqMap b w) -- ^ @ [n]a @ + -- Invariant: VSeq is never a sequence of bits + | VWord !Integer !(Eval (WordValue b w)) -- ^ @ [n]Bit @ + | VStream !(SeqMap b w) -- ^ @ [inf]a @ + | VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- ^ functions + | VPoly (TValue -> Eval (GenValue b w)) -- ^ polymorphic values (kind *) + | VNumPoly (Nat' -> Eval (GenValue b w)) -- ^ polymorphic values (kind #) + deriving (Generic, NFData) + + +-- | Force the evaluation of a word value +forceWordValue :: WordValue b w -> Eval () +forceWordValue (WordVal _w) = return () +forceWordValue (BitsVal bs) = mapM_ (\b -> const () <$> b) bs + +-- | Force the evaluation of a value +forceValue :: GenValue b w -> Eval () +forceValue v = case v of + VRecord fs -> mapM_ (\x -> forceValue =<< snd x) fs + VTuple xs -> mapM_ (forceValue =<<) xs + VSeq n xs -> mapM_ (forceValue =<<) (enumerateSeqMap n xs) + VBit _b -> return () + VWord _ wv -> forceWordValue =<< wv + VStream _ -> return () + VFun _ -> return () + VPoly _ -> return () + + +instance (Show b, Show w) => Show (GenValue b w) where + show v = case v of + VRecord fs -> "record:" ++ show (map fst fs) + VTuple xs -> "tuple:" ++ show (length xs) + VBit b -> show b + VSeq n _ -> "seq:" ++ show n + VWord n _ -> "word:" ++ show n + VStream _ -> "stream" + VFun _ -> "fun" + VPoly _ -> "poly" type Value = GenValue Bool BV --- | An evaluated type of kind *. --- These types do not contain type variables, type synonyms, or type functions. -data TValue - = TVBit - | TVSeq Integer TValue - | TVStream TValue -- ^ [inf]t - | TVTuple [TValue] - | TVRec [(Ident, TValue)] - | TVFun TValue TValue - deriving (Generic, NFData) - -tValTy :: TValue -> Type -tValTy tv = - case tv of - TVBit -> tBit - TVSeq n t -> tSeq (tNum n) (tValTy t) - TVStream t -> tSeq tInf (tValTy t) - TVTuple ts -> tTuple (map tValTy ts) - TVRec fs -> tRec [ (f, tValTy t) | (f, t) <- fs ] - TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2) - -instance Show TValue where - showsPrec p v = showsPrec p (tValTy v) - -- Pretty Printing ------------------------------------------------------------- @@ -129,36 +251,54 @@ data PPOpts = PPOpts defaultPPOpts :: PPOpts defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5 } -ppValue :: PPOpts -> Value -> Doc +atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c) +atFst f (x,y) = fmap (,y) $ f x + +atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b) +atSnd f (x,y) = fmap (x,) $ f y + +ppValue :: forall b w + . BitWord b w + => PPOpts + -> GenValue b w + -> Eval Doc ppValue opts = loop where + loop :: GenValue b w -> Eval Doc loop val = case val of - VRecord fs -> braces (sep (punctuate comma (map ppField fs))) + VRecord fs -> do fs' <- traverse (atSnd (>>=loop)) $ fs + return $ braces (sep (punctuate comma (map ppField fs'))) where - ppField (f,r) = pp f <+> char '=' <+> loop r - VTuple vals -> parens (sep (punctuate comma (map loop vals))) - VBit b | b -> text "True" - | otherwise -> text "False" - VSeq isWord vals - | isWord -> ppWord opts (fromVWord val) - | otherwise -> ppWordSeq vals - VWord (BV w i) -> ppWord opts (BV w i) - VStream vals -> brackets $ fsep + ppField (f,r) = pp f <+> char '=' <+> r + VTuple vals -> do vals' <- traverse (>>=loop) vals + return $ parens (sep (punctuate comma vals')) + VBit b -> return $ ppBit b + VSeq sz vals -> ppWordSeq sz vals + VWord _ wv -> ppWordVal =<< wv + VStream vals -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals + return $ brackets $ fsep $ punctuate comma - ( take (useInfLength opts) (map loop vals) - ++ [text "..."] + ( vals' ++ [text "..."] ) - VFun _ -> text "" - VPoly _ -> text "" - VNumPoly _ -> text "" + VFun _ -> return $ text "" + VPoly _ -> return $ text "" - ppWordSeq ws = + ppWordVal :: WordValue b w -> Eval Doc + ppWordVal w = ppWord opts <$> asWordVal w + + ppWordSeq :: Integer -> SeqMap b w -> Eval Doc + ppWordSeq sz vals = do + ws <- sequence (enumerateSeqMap sz vals) case ws of w : _ - | Just l <- vWordLen w, asciiMode opts l -> - text $ show $ map (integerToChar . fromWord) ws - _ -> brackets (fsep (punctuate comma (map loop ws))) - + | Just l <- vWordLen w + , asciiMode opts l + -> do vs <- traverse (fromVWord "ppWordSeq") ws + case traverse wordAsChar vs of + Just str -> return $ text str + _ -> return $ brackets (fsep (punctuate comma $ map (ppWord opts) vs)) + _ -> do ws' <- traverse loop ws + return $ brackets (fsep (punctuate comma ws')) asciiMode :: PPOpts -> Integer -> Bool asciiMode opts width = useAscii opts && (width == 7 || width == 8) @@ -166,14 +306,9 @@ asciiMode opts width = useAscii opts && (width == 7 || width == 8) integerToChar :: Integer -> Char integerToChar = toEnum . fromInteger -data WithBase a = WithBase PPOpts a - deriving (Functor) -instance PP (WithBase Value) where - ppPrec _ (WithBase opts v) = ppValue opts v - -ppWord :: PPOpts -> BV -> Doc -ppWord opts (BV width i) +ppBV :: PPOpts -> BV -> Doc +ppBV opts (BV width i) | base > 36 = integer i -- not sure how to rule this out | asciiMode opts width = text (show (toEnum (fromInteger i) :: Char)) | otherwise = prefix <> text value @@ -199,18 +334,97 @@ ppWord opts (BV width i) digits = "0123456789abcdefghijklmnopqrstuvwxyz" --- Big-endian Words ------------------------------------------------------------ +-- | This type class defines a collection of operations on bits and words that +-- are necessary to define generic evaluator primitives that operate on both concrete +-- and symbolic values uniformly. +class BitWord b w | b -> w, w -> b where + -- | Pretty-print an individual bit + ppBit :: b -> Doc -class BitWord b w where + -- | Pretty-print a word value + ppWord :: PPOpts -> w -> Doc - -- | NOTE this assumes that the sequence of bits is big-endian and finite, so the - -- first element of the list will be the most significant bit. + -- | Attempt to render a word value as an ASCII character. Return `Nothing` + -- if the character value is unknown (e.g., for symbolic values). + wordAsChar :: w -> Maybe Char + + -- | The number of bits in a word value. + wordLen :: w -> Integer + + -- | Construct a literal bit value from a boolean. + bitLit :: Bool -> b + + -- | Construct a literal word value given a bit width and a value. + wordLit :: Integer -- ^ Width + -> Integer -- ^ Value + -> w + + -- | Construct a word value from a finite sequence of bits. + -- NOTE: this assumes that the sequence of bits is big-endian and finite, so the + -- first element of the list will be the most significant bit. packWord :: [b] -> w - -- | NOTE this produces a list of bits that represent a big-endian word, so the - -- most significant bit is the first element of the list. + -- | Deconstruct a packed word value in to a finite sequence of bits. + -- NOTE: this produces a list of bits that represent a big-endian word, so + -- the most significant bit is the first element of the list. unpackWord :: w -> [b] + -- | Concatenate the two given word values. + -- NOTE: the first argument represents the more-significant bits + joinWord :: w -> w -> w + + -- | Take the most-significant bits, and return + -- those bits and the remainder. The first element + -- of the pair is the most significant bits. + -- The two integer sizes must sum to the length of the given word value. + splitWord :: Integer -- ^ left width + -> Integer -- ^ right width + -> w + -> (w, w) + + -- | Extract a subsequence of bits from a packed word value. + -- 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 `extractWord n i w` is equivelant to + -- first shifting `w` right by `i` bits, and then truncating to + -- `n` bits. + extractWord :: Integer -- ^ Number of bits to take + -> Integer -- ^ starting bit + -> w + -> w + + -- | 2's complement addition of packed words. The arguments must have + -- equal bit width, and the result is of the same width. Overflow is silently + -- discarded. + wordPlus :: w -> w -> w + + -- | 2's complement subtraction of packed words. The arguments must have + -- equal bit width, and the result is of the same width. Overflow is silently + -- discarded. + wordMinus :: w -> w -> w + + -- | 2's complement multiplication of packed words. The arguments must have + -- equal bit width, and the result is of the same width. The high bits of the + -- multiplication are silently discarded. + wordMult :: w -> w -> w + + +-- | This class defines additional operations necessary to define generic evaluation +-- functions. +class BitWord b w => EvalPrims b w where + -- | Eval prim binds primitive declarations to the primitive values that implement them. + evalPrim :: Decl -> GenValue b w + + -- | if/then/else operation. Choose either the 'then' value or the 'else' value depending + -- on the value of the test bit. + iteValue :: b -- ^ Test bit + -> Eval (GenValue b w) -- ^ 'then' value + -> Eval (GenValue b w) -- ^ 'else' value + -> Eval (GenValue b w) + + +-- Concrete Big-endian Words ------------------------------------------------------------ mask :: Integer -- ^ Bit-width -> Integer -- ^ Value @@ -218,74 +432,106 @@ mask :: Integer -- ^ Bit-width mask w i | w >= Arch.maxBigIntWidth = wordTooWide w | otherwise = i .&. ((1 `shiftL` fromInteger w) - 1) - instance BitWord Bool BV where + wordLen (BV w _) = w + wordAsChar (BV _ x) = Just $ integerToChar x + + ppBit b | b = text "True" + | otherwise = text "False" + + ppWord = ppBV + + bitLit b = b + wordLit = mkBv packWord bits = BV (toInteger w) a where w = case length bits of len | toInteger len >= Arch.maxBigIntWidth -> wordTooWide (toInteger len) | otherwise -> len - a = foldl set 0 (zip [w - 1, w - 2 .. 0] bits) - set acc (n,b) | b = setBit acc n - | otherwise = acc + a = foldl setb 0 (zip [w - 1, w - 2 .. 0] bits) + setb acc (n,b) | b = setBit acc n + | otherwise = acc unpackWord (BV w a) = [ testBit a n | n <- [w' - 1, w' - 2 .. 0] ] where w' = fromInteger w + joinWord (BV i x) (BV j y) = + BV (i + j) (shiftL x (fromInteger j) + y) + + splitWord leftW rightW (BV _ x) = + ( BV leftW (x `shiftR` (fromInteger rightW)), mkBv rightW x ) + + extractWord n i (BV _ x) = mkBv n (x `shiftR` (fromInteger i)) + + wordPlus (BV i x) (BV j y) + | i == j = mkBv i (x+y) + | otherwise = panic "Attempt to add words of different sizes: wordPlus" [] + + wordMinus (BV i x) (BV j y) + | i == j = mkBv i (x-y) + | otherwise = panic "Attempt to subtract words of different sizes: wordMinus" [] + + wordMult (BV i x) (BV j y) + | i == j = mkBv i (x*y) + | otherwise = panic "Attempt to multiply words of different sizes: wordMult" [] + -- Value Constructors ---------------------------------------------------------- -- | Create a packed word of n bits. -word :: Integer -> Integer -> Value -word n i = VWord (mkBv n i) +word :: BitWord b w => Integer -> Integer -> GenValue b w +word n i = VWord n $ ready $ WordVal $ wordLit n i -lam :: (GenValue b w -> GenValue b w) -> GenValue b w +lam :: (Eval (GenValue b w) -> Eval (GenValue b w)) -> GenValue b w lam = VFun --- | A type lambda that expects a @Type@ of kind *. +-- | Functions that assume word inputs +wlam :: BitWord b w => (w -> Eval (GenValue b w)) -> GenValue b w +wlam f = VFun (\x -> x >>= fromVWord "wlam" >>= f) + +-- | A type lambda that expects a @Type@. tlam :: (TValue -> GenValue b w) -> GenValue b w -tlam = VPoly +tlam f = VPoly (return . f) -- | A type lambda that expects a @Type@ of kind #. nlam :: (Nat' -> GenValue b w) -> GenValue b w -nlam = VNumPoly +nlam f = VNumPoly (return . f) -- | Generate a stream. -toStream :: [GenValue b w] -> GenValue b w -toStream = VStream +toStream :: [GenValue b w] -> Eval (GenValue b w) +toStream vs = + VStream <$> infiniteSeqMap (map ready vs) -toFinSeq :: TValue -> [GenValue b w] -> GenValue b w -toFinSeq elty = VSeq (isTBit elty) +toFinSeq :: BitWord b w + => Integer -> TValue -> [GenValue b w] -> Eval (GenValue b w) +toFinSeq len elty vs + | isTBit elty = return $ VWord len $ ready $ WordVal $ packWord $ map fromVBit vs + | otherwise = VSeq len <$> finiteSeqMap (map ready vs) -- | This is strict! boolToWord :: [Bool] -> Value -boolToWord = VWord . packWord +boolToWord bs = VWord (genericLength bs) $ ready $ WordVal $ packWord bs -- | 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 :: Nat' -> TValue -> [GenValue b w] -> GenValue b w +toSeq :: BitWord b w + => Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w) toSeq len elty vals = case len of - Nat n -> toFinSeq elty (genericTake n vals) + Nat n -> toFinSeq n elty vals Inf -> toStream vals --- | Construct one of: --- * a word, when the sequence is finite and the elements are bits --- * a sequence, when the sequence is finite but the elements aren't bits --- * a stream, when the sequence is not finite --- --- NOTE: do not use this constructor in the case where the thing may be a --- finite, but recursive, sequence. -toPackedSeq :: Nat' -> TValue -> [Value] -> Value -toPackedSeq len elty vals = case len of - -- finite sequence, pack a word if the elements are bits. - Nat _ | isTBit elty -> boolToWord (map fromVBit vals) - | otherwise -> VSeq False vals - - -- infinite sequence, construct a stream - Inf -> VStream 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 :: Nat' -> TValue -> SeqMap b w -> GenValue b w +mkSeq len elty vals = case len of + Nat n + | isTBit elty -> VWord n $ return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i -> + fromVBit <$> lookupSeqMap vals (toInteger i) + | otherwise -> VSeq n vals + Inf -> VStream vals -- Value Destructors ----------------------------------------------------------- @@ -296,68 +542,85 @@ fromVBit val = case val of VBit b -> b _ -> evalPanic "fromVBit" ["not a Bit"] --- | Extract a sequence. -fromSeq :: BitWord b w => GenValue b w -> [GenValue b w] -fromSeq val = case val of - VSeq _ vs -> vs - VWord bv -> map VBit (unpackWord bv) - VStream vs -> vs - _ -> evalPanic "fromSeq" ["not a sequence"] +bitsSeq :: BitWord b w => WordValue b w -> Integer -> Eval b +bitsSeq (WordVal w) = + let bs = unpackWord w + in \i -> return $ genericIndex bs i +bitsSeq (BitsVal bs) = \i -> Seq.index bs (fromInteger i) -fromStr :: Value -> String -fromStr = map (toEnum . fromInteger . fromWord) . fromSeq +-- | Extract a sequence. +fromSeq :: forall b w. BitWord b w => String -> GenValue b w -> Eval (SeqMap b w) +fromSeq msg val = case val of + VSeq _ vs -> return vs + VStream vs -> return vs + _ -> evalPanic "fromSeq" ["not a sequence", msg] + +fromStr :: Value -> Eval String +fromStr (VSeq n vals) = + traverse (\x -> toEnum . fromInteger <$> (fromWord "fromStr" =<< x)) (enumerateSeqMap n vals) +fromStr _ = evalPanic "fromStr" ["Not a finite sequence"] + +fromWordVal :: String -> GenValue b w -> Eval (WordValue b w) +fromWordVal _msg (VWord _ wval) = wval +fromWordVal msg _ = evalPanic "fromWordVal" ["not a word value", msg] -- | Extract a packed word. -fromVWord :: BitWord b w => GenValue b w -> w -fromVWord val = case val of - VWord bv -> bv -- this should always mask - VSeq isWord bs | isWord -> packWord (map fromVBit bs) - _ -> evalPanic "fromVWord" ["not a word"] +fromVWord :: BitWord b w => String -> GenValue b w -> Eval w +fromVWord _msg (VWord _ wval) = wval >>= asWordVal +fromVWord msg _ = evalPanic "fromVWord" ["not a word", msg] -vWordLen :: Value -> Maybe Integer +vWordLen :: BitWord b w => GenValue b w -> Maybe Integer vWordLen val = case val of - VWord (BV w _) -> Just w - VSeq isWord bs | isWord -> Just (toInteger (length bs)) - _ -> Nothing + VWord n _wv -> Just n + _ -> Nothing + +-- | 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 :: BitWord b w => [Eval (GenValue b w)] -> Maybe w +tryFromBits = go id + where + go f [] = Just (packWord (f [])) + go f (Ready (VBit b):vs) = go ((b:) . f) vs + go f (v:vs) = Nothing -- | Turn a value into an integer represented by w bits. -fromWord :: Value -> Integer -fromWord val = a - where BV _ a = fromVWord val +fromWord :: String -> Value -> Eval Integer +fromWord msg val = bvVal <$> fromVWord msg val -- | Extract a function from a value. -fromVFun :: GenValue b w -> (GenValue b w -> GenValue b w) +fromVFun :: GenValue b w -> (Eval (GenValue b w) -> Eval (GenValue b w)) fromVFun val = case val of VFun f -> f _ -> evalPanic "fromVFun" ["not a function"] -- | Extract a polymorphic function from a value. -fromVPoly :: GenValue b w -> (TValue -> GenValue b w) +fromVPoly :: GenValue b w -> (TValue -> Eval (GenValue b w)) fromVPoly val = case val of VPoly f -> f _ -> evalPanic "fromVPoly" ["not a polymorphic value"] -- | Extract a polymorphic function from a value. -fromVNumPoly :: GenValue b w -> (Nat' -> GenValue b w) +fromVNumPoly :: GenValue b w -> (Nat' -> Eval (GenValue b w)) fromVNumPoly val = case val of VNumPoly f -> f _ -> evalPanic "fromVNumPoly" ["not a polymorphic value"] -- | Extract a tuple from a value. -fromVTuple :: GenValue b w -> [GenValue b w] +fromVTuple :: GenValue b w -> [Eval (GenValue b w)] fromVTuple val = case val of VTuple vs -> vs _ -> evalPanic "fromVTuple" ["not a tuple"] -- | Extract a record from a value. -fromVRecord :: GenValue b w -> [(Ident, GenValue b w)] +fromVRecord :: GenValue b w -> [(Ident, Eval (GenValue b w))] fromVRecord val = case val of VRecord fs -> fs _ -> evalPanic "fromVRecord" ["not a record"] -- | Lookup a field in a record. -lookupRecord :: Ident -> GenValue b w -> GenValue b w +lookupRecord :: Ident -> GenValue b w -> Eval (GenValue b w) lookupRecord f rec = case lookup f (fromVRecord rec) of Just val -> val Nothing -> evalPanic "lookupRecord" ["malformed record"] @@ -368,38 +631,41 @@ lookupRecord f rec = case lookup f (fromVRecord rec) of -- this value, if we can determine it. -- -- XXX: View patterns would probably clean up this definition a lot. -toExpr :: PrimMap -> Type -> Value -> Maybe Expr -toExpr prims = go +toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr) +toExpr prims t0 v0 = findOne (go t0 v0) where prim n = ePrim prims (mkIdent (T.pack n)) + go :: Type -> Value -> ChoiceT Eval Expr go ty val = case (ty, val) of (TRec tfs, VRecord vfs) -> do let fns = map fst vfs guard (map fst tfs == fns) - fes <- zipWithM go (map snd tfs) (map snd vfs) + fes <- zipWithM go (map snd tfs) =<< lift (traverse snd vfs) return $ ERec (zip fns fes) (TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do guard (tl == (length tvs)) - ETuple `fmap` zipWithM go ts tvs + ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs)) (TCon (TC TCBit) [], VBit True ) -> return (prim "True") (TCon (TC TCBit) [], VBit False) -> return (prim "False") - (TCon (TC TCSeq) [a,b], VSeq _ []) -> do + (TCon (TC TCSeq) [a,b], VSeq 0 _) -> do guard (a == tZero) return $ EList [] b - (TCon (TC TCSeq) [a,b], VSeq _ svs) -> do - guard (a == tNum (length svs)) - ses <- mapM (go b) svs + (TCon (TC TCSeq) [a,b], VSeq n svs) -> do + guard (a == tNum n) + ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs)) return $ EList ses b - (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord (BV w v)) -> do + (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do + BV w v <- lift (asWordVal =<< wval) guard (a == tNum w) return $ ETApp (ETApp (prim "demote") (tNum v)) (tNum w) (_, VStream _) -> fail "cannot construct infinite expressions" (_, VFun _) -> fail "cannot convert function values to expressions" (_, VPoly _) -> fail "cannot convert polymorphic values to expressions" - _ -> panic "Cryptol.Eval.Value.toExpr" - ["type mismatch:" - , pretty ty - , render (ppValue defaultPPOpts val) - ] + _ -> do doc <- lift (ppValue defaultPPOpts val) + panic "Cryptol.Eval.Value.toExpr" + ["type mismatch:" + , pretty ty + , render doc + ] diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 91eb95e5..4fc8ecbe 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -18,7 +18,9 @@ import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap) import Cryptol.ModuleSystem.Env (lookupModule, LoadedModule(..) , meCoreLint, CoreLint(..)) import qualified Cryptol.Eval as E +import qualified Cryptol.Eval.Monad as E import qualified Cryptol.Eval.Value as E +import Cryptol.Prims.Eval () import qualified Cryptol.ModuleSystem.NamingEnv as R import qualified Cryptol.ModuleSystem.Renamer as R import qualified Cryptol.Parser as P @@ -454,14 +456,15 @@ evalExpr :: T.Expr -> ModuleM E.Value evalExpr e = do env <- getEvalEnv denv <- getDynEnv - return (E.evalExpr (env <> deEnv denv) e) + io $ E.runEval $ (E.evalExpr (env <> deEnv denv) e) evalDecls :: [T.DeclGroup] -> ModuleM () evalDecls dgs = do env <- getEvalEnv denv <- getDynEnv let env' = env <> deEnv denv - denv' = denv { deDecls = deDecls denv ++ dgs - , deEnv = E.evalDecls dgs env' + deEnv' <- io $ E.runEval $ E.evalDecls dgs env' + let denv' = denv { deDecls = deDecls denv ++ dgs + , deEnv = deEnv' } setDynEnv denv' diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index fc4219ab..a35ae493 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -18,6 +18,7 @@ import Paths_cryptol (getDataDir) #endif import Cryptol.Eval (EvalEnv) +import Cryptol.Eval.Value (BV) import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Name (Supply,emptySupply) import qualified Cryptol.ModuleSystem.NamingEnv as R diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 789efe78..25fb42d1 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -11,7 +11,10 @@ {-# LANGUAGE DeriveGeneric #-} module Cryptol.ModuleSystem.Monad where -import Cryptol.Eval.Env (EvalEnv) +import Cryptol.Eval (EvalEnv) +import Cryptol.Eval.Value (BV) + +import qualified Cryptol.Eval.Monad as E import Cryptol.ModuleSystem.Env import Cryptol.ModuleSystem.Interface import Cryptol.ModuleSystem.Name (FreshM(..),Supply) @@ -29,6 +32,7 @@ import Cryptol.Parser.Position (Range) import Cryptol.Utils.Ident (interactiveName) import Cryptol.Utils.PP +import Control.Monad.IO.Class import Control.Exception (IOException) import Data.Function (on) import Data.Maybe (isJust) @@ -273,6 +277,9 @@ instance Monad m => FreshM (ModuleT m) where set $! me { meSupply = s' } return a +instance MonadIO m => MonadIO (ModuleT m) where + liftIO m = lift $ liftIO m + runModuleT :: Monad m => ModuleEnv -> ModuleT m a @@ -385,10 +392,12 @@ loadedModule path m = ModuleT $ do env <- get set $! env { meLoadedModules = addLoadedModule path m (meLoadedModules env) } -modifyEvalEnv :: (EvalEnv -> EvalEnv) -> ModuleM () +modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM () modifyEvalEnv f = ModuleT $ do env <- get - set $! env { meEvalEnv = f (meEvalEnv env) } + let evalEnv = meEvalEnv env + evalEnv' <- inBase $ E.runEval (f evalEnv) + set $! env { meEvalEnv = evalEnv' } getEvalEnv :: ModuleM EvalEnv getEvalEnv = ModuleT (meEvalEnv `fmap` get) diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index a5c79bdb..8d30e431 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -6,28 +6,38 @@ -- Stability : provisional -- Portability : portable +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE BangPatterns #-} module Cryptol.Prims.Eval where +import Control.Monad (join, when) + import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),fromNat,genLog, nMul) import qualified Cryptol.Eval.Arch as Arch -import Cryptol.Eval.Error -import Cryptol.Eval.Type(evalTF) +import Cryptol.Eval.Env +import Cryptol.Eval.Monad +import Cryptol.Eval.Type import Cryptol.Eval.Value import Cryptol.Testing.Random (randomValue) import Cryptol.Utils.Panic (panic) import Cryptol.ModuleSystem.Name (asPrim) import Cryptol.Utils.Ident (Ident,mkIdent) +import Cryptol.Utils.PP +import qualified Data.Foldable as Fold import Data.List (sortBy, transpose, genericTake, genericDrop, - genericReplicate, genericSplitAt, genericIndex) + genericReplicate, genericSplitAt, genericIndex, + foldl') +import qualified Data.Sequence as Seq import Data.Ord (comparing) import Data.Bits (Bits(..)) @@ -36,131 +46,185 @@ import qualified Data.Text as T import System.Random.TF.Gen (seedTFGen) +import Debug.Trace(trace) + -- Primitives ------------------------------------------------------------------ -evalPrim :: Decl -> Value -evalPrim Decl { dName = n, .. } - | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val +instance EvalPrims Bool BV where + evalPrim Decl { dName = n, .. } + | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val + + evalPrim Decl { .. } = + panic "Eval" [ "Unimplemented primitive", show dName ] + + iteValue b t f = if b then t else f -evalPrim Decl { .. } = - panic "Eval" [ "Unimplemented primitive", show dName ] primTable :: Map.Map Ident Value primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v)) - [ ("+" , binary (arithBinary (liftBinArith (+)))) - , ("-" , binary (arithBinary (liftBinArith (-)))) - , ("*" , binary (arithBinary (liftBinArith (*)))) - , ("/" , binary (arithBinary (liftBinArith divWrap))) - , ("%" , binary (arithBinary (liftBinArith modWrap))) - , ("^^" , binary (arithBinary modExp)) - , ("lg2" , unary (arithUnary lg2)) - , ("negate" , unary (arithUnary negate)) - , ("<" , binary (cmpOrder (\o -> o == LT ))) - , (">" , binary (cmpOrder (\o -> o == GT ))) - , ("<=" , binary (cmpOrder (\o -> o == LT || o == EQ))) - , (">=" , binary (cmpOrder (\o -> o == GT || o == EQ))) - , ("==" , binary (cmpOrder (\o -> o == EQ))) - , ("!=" , binary (cmpOrder (\o -> o /= EQ))) - , ("&&" , binary (logicBinary (.&.))) - , ("||" , binary (logicBinary (.|.))) - , ("^" , binary (logicBinary xor)) - , ("complement" , unary (logicUnary complement)) - , ("<<" , logicShift shiftLW shiftLS) - , (">>" , logicShift shiftRW shiftRS) - , ("<<<" , logicShift rotateLW rotateLS) - , (">>>" , logicShift rotateRW rotateRS) + [ ("+" , {-# SCC "Prelude::(+)" #-} + binary (arithBinary (liftBinArith (+)))) + , ("-" , {-# SCC "Prelude::(-)" #-} + binary (arithBinary (liftBinArith (-)))) + , ("*" , {-# SCC "Prelude::(*)" #-} + binary (arithBinary (liftBinArith (*)))) + , ("/" , {-# SCC "Prelude::(/)" #-} + binary (arithBinary (liftBinArith divWrap))) + , ("%" , {-# SCC "Prelude::(%)" #-} + binary (arithBinary (liftBinArith modWrap))) + , ("^^" , {-# SCC "Prelude::(^^)" #-} + binary (arithBinary modExp)) + , ("lg2" , {-# SCC "Prelude::lg2" #-} + unary (arithUnary (liftUnaryArith lg2))) + , ("negate" , {-# SCC "Prelude::negate" #-} + unary (arithUnary (liftUnaryArith negate))) + , ("<" , {-# SCC "Prelude::(<)" #-} + binary (cmpOrder "<" (\o -> o == LT ))) + , (">" , {-# SCC "Prelude::(>)" #-} + binary (cmpOrder ">" (\o -> o == GT ))) + , ("<=" , {-# SCC "Prelude::(<=)" #-} + binary (cmpOrder "<=" (\o -> o == LT || o == EQ))) + , (">=" , {-# SCC "Prelude::(>=)" #-} + binary (cmpOrder ">=" (\o -> o == GT || o == EQ))) + , ("==" , {-# SCC "Prelude::(==)" #-} + binary (cmpOrder "==" (\o -> o == EQ))) + , ("!=" , {-# SCC "Prelude::(!=)" #-} + binary (cmpOrder "!=" (\o -> o /= EQ))) + , ("&&" , {-# SCC "Prelude::(&&)" #-} + binary (logicBinary (.&.) (binBV (.&.)))) + , ("||" , {-# SCC "Prelude::(||)" #-} + binary (logicBinary (.|.) (binBV (.|.)))) + , ("^" , {-# SCC "Prelude::(^)" #-} + binary (logicBinary xor (binBV xor))) + , ("complement" , {-# SCC "Prelude::complement" #-} + unary (logicUnary complement (unaryBV complement))) + , ("<<" , {-# SCC "Prelude::(<<)" #-} + logicShift shiftLW shiftLB shiftLS) + , (">>" , {-# SCC "Prelude::(>>)" #-} + logicShift shiftRW shiftLB shiftRS) + , ("<<<" , {-# SCC "Prelude::(<<<)" #-} + logicShift rotateLW rotateLB rotateLS) + , (">>>" , {-# SCC "Prelude::(>>>)" #-} + logicShift rotateRW rotateRB rotateRS) , ("True" , VBit True) , ("False" , VBit False) - , ("demote" , ecDemoteV) + , ("demote" , {-# SCC "Prelude::demote" #-} + ecDemoteV) - , ("#" , nlam $ \ front -> + , ("#" , {-# SCC "Prelude::(#)" #-} + nlam $ \ front -> nlam $ \ back -> tlam $ \ elty -> - lam $ \ l -> - lam $ \ r -> ccatV front back elty l r) + lam $ \ l -> return $ + lam $ \ r -> join (ccatV front back elty <$> l <*> r)) - , ("@" , indexPrimOne indexFront) - , ("@@" , indexPrimMany indexFrontRange) - , ("!" , indexPrimOne indexBack) - , ("!!" , indexPrimMany indexBackRange) + , ("@" , {-# SCC "Prelude::(@)" #-} + indexPrimOne indexFront_bits indexFront) + , ("@@" , {-# SCC "Prelude::(@@)" #-} + indexPrimMany indexFront_bits indexFront) + , ("!" , {-# SCC "Prelude::(!)" #-} + indexPrimOne indexBack_bits indexBack) + , ("!!" , {-# SCC "Prelude::(!!)" #-} + indexPrimMany indexBack_bits indexBack) - , ("zero" , tlam zeroV) + , ("zero" , {-# SCC "Prelude::zero" #-} + tlam zeroV) - , ("join" , nlam $ \ parts -> - nlam $ \ each -> - tlam $ \ a -> lam (joinV parts each a)) + , ("join" , {-# SCC "Prelude::join" #-} + nlam $ \ parts -> + nlam $ \ (finNat' -> each) -> + tlam $ \ a -> + lam $ \ x -> + joinV parts each a =<< x) - , ("split" , ecSplitV) + , ("split" , {-# SCC "Prelude::split" #-} + ecSplitV) - , ("splitAt" , nlam $ \ front -> + , ("splitAt" , {-# SCC "Prelude::splitAt" #-} + nlam $ \ front -> nlam $ \ back -> - tlam $ \ a -> lam (splitAtV front back a)) + tlam $ \ a -> + lam $ \ x -> + splitAtV front back a =<< x) - , ("fromThen" , fromThenV) - , ("fromTo" , fromToV) - , ("fromThenTo" , fromThenToV) + , ("fromThen" , {-# SCC "Prelude::fromThen" #-} + fromThenV) + , ("fromTo" , {-# SCC "Prelude::fromTo" #-} + fromToV) + , ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-} + fromThenToV) + , ("infFrom" , {-# SCC "Prelude::infFrom" #-} + infFromV) + , ("infFromThen", {-# SCC "Prelude::infFromThen" #-} + infFromThenV) - , ("infFrom" , nlam $ \(finNat' -> bits) -> - lam $ \(fromWord -> first) -> - toStream (map (word bits) [ first .. ])) + , ("error" , {-# SCC "Prelude::error" #-} + tlam $ \a -> + nlam $ \_ -> + lam $ \s -> errorV a =<< (fromStr =<< s)) - , ("infFromThen", nlam $ \(finNat' -> bits) -> - lam $ \(fromWord -> first) -> - lam $ \(fromWord -> next) -> - toStream [ word bits n | n <- [ first, next .. ] ]) - - , ("error" , tlam $ \_ -> - tlam $ \_ -> - lam $ \(fromStr -> s) -> cryUserError s) - - , ("reverse" , nlam $ \a -> + , ("reverse" , {-# SCC "Prelude::reverse" #-} + nlam $ \a -> tlam $ \b -> - lam $ \(fromSeq -> xs) -> toSeq a b (reverse xs)) + lam $ \xs -> reverseV =<< xs) - , ("transpose" , nlam $ \a -> + , ("transpose" , {-# SCC "Prelude::transpose" #-} + nlam $ \a -> nlam $ \b -> tlam $ \c -> - lam $ \((map fromSeq . fromSeq) -> xs) -> - case a of - Nat 0 -> - let val = toSeq a c [] - in case b of - Nat n -> toSeq b (tvSeq a c) $ genericReplicate n val - Inf -> VStream $ repeat val - _ -> toSeq b (tvSeq a c) $ map (toSeq a c) $ transpose xs) + lam $ \xs -> transposeV a b c =<< xs) - , ("pmult" , + , ("pmult" , {-# SCC "Prelude::pmult" #-} let mul !res !_ !_ 0 = res mul res bs as n = mul (if even as then res else xor res bs) (bs `shiftL` 1) (as `shiftR` 1) (n-1) - in nlam $ \(finNat' -> a) -> - nlam $ \(finNat' -> b) -> - lam $ \(fromWord -> x) -> - lam $ \(fromWord -> y) -> word (max 1 (a + b) - 1) (mul 0 x y b)) + in nlam $ \(finNat' -> a) -> + nlam $ \(finNat' -> b) -> + wlam $ \(bvVal -> x) -> return $ + wlam $ \(bvVal -> y) -> return $ word (max 1 (a + b) - 1) (mul 0 x y b)) - , ("pdiv" , nlam $ \(fromInteger . finNat' -> a) -> + , ("pdiv" , {-# SCC "Prelude::pdiv" #-} + nlam $ \(fromInteger . finNat' -> a) -> nlam $ \(fromInteger . finNat' -> b) -> - lam $ \(fromWord -> x) -> - lam $ \(fromWord -> y) -> word (toInteger a) - (fst (divModPoly x a y b))) + wlam $ \(bvVal -> x) -> return $ + wlam $ \(bvVal -> y) -> return $ word (toInteger a) + (fst (divModPoly x a y b))) - , ("pmod" , nlam $ \(fromInteger . finNat' -> a) -> + , ("pmod" , {-# SCC "Prelude::pmod" #-} + nlam $ \(fromInteger . finNat' -> a) -> nlam $ \(fromInteger . finNat' -> b) -> - lam $ \(fromWord -> x) -> - lam $ \(fromWord -> y) -> word (toInteger b) - (snd (divModPoly x a y (b+1)))) - , ("random" , tlam $ \a -> - lam $ \(fromWord -> x) -> randomV a x) + wlam $ \(bvVal -> x) -> return $ + wlam $ \(bvVal -> y) -> return $ word (toInteger b) + (snd (divModPoly x a y (b+1)))) + , ("random" , {-# SCC "Prelude::random" #-} + tlam $ \a -> + wlam $ \(bvVal -> x) -> return $ randomV a x) + , ("trace" , {-# SCC "Prelude::trace" #-} + nlam $ \_n -> + tlam $ \_a -> + tlam $ \_b -> + lam $ \s -> return $ + lam $ \x -> return $ + lam $ \y -> do + msg <- fromStr =<< s + -- FIXME? get PPOPts from elsewhere? + doc <- ppValue defaultPPOpts =<< x + yv <- y + io $ putStrLn $ show $ if null msg then + doc + else + text msg <+> doc + return yv) ] -- | Make a numeric constant. -ecDemoteV :: Value +ecDemoteV :: BitWord b w => GenValue b w ecDemoteV = nlam $ \valT -> nlam $ \bitT -> case (valT, bitT) of - (Nat v, Nat bs) -> VWord (mkBv bs v) + (Nat v, Nat bs) -> word bs v _ -> evalPanic "Cryptol.Eval.Prim.evalConst" ["Unexpected Inf in constant." , show valT @@ -194,21 +258,22 @@ divModPoly xs xsLen ys ysLen -- | Create a packed word modExp :: Integer -- ^ bit size of the resulting word - -> Integer -- ^ base - -> Integer -- ^ exponent - -> Integer -modExp bits base e - | bits == 0 = 0 + -> BV -- ^ base + -> BV -- ^ exponent + -> BV +modExp bits (BV _ base) (BV _ e) + | bits == 0 = BV bits 0 | base < 0 || bits < 0 = evalPanic "modExp" [ "bad args: " , " base = " ++ show base , " e = " ++ show e , " bits = " ++ show modulus ] - | otherwise = doubleAndAdd base e modulus + | otherwise = mkBv bits $ doubleAndAdd base e modulus where modulus = 0 `setBit` fromInteger bits + doubleAndAdd :: Integer -- ^ base -> Integer -- ^ exponent mask -> Integer -- ^ modulus @@ -230,87 +295,120 @@ doubleAndAdd base0 expMask modulus = go 1 base0 expMask -- Operation Lifting ----------------------------------------------------------- -type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w -type Binary = GenBinary Bool BV +type Binary b w = TValue -> GenValue b w -> GenValue b w -> Eval (GenValue b w) -binary :: GenBinary b w -> GenValue b w +binary :: Binary b w -> GenValue b w binary f = tlam $ \ ty -> - lam $ \ a -> - lam $ \ b -> f ty a b + lam $ \ a -> return $ + lam $ \ b -> do + --io $ putStrLn "Entering a binary function" + join (f ty <$> a <*> b) -type GenUnary b w = TValue -> GenValue b w -> GenValue b w -type Unary = GenUnary Bool BV +type Unary b w = TValue -> GenValue b w -> Eval (GenValue b w) -unary :: GenUnary b w -> GenValue b w +unary :: Unary b w -> GenValue b w unary f = tlam $ \ ty -> - lam $ \ a -> f ty a + lam $ \ a -> f ty =<< a -- Arith ----------------------------------------------------------------------- -- | Turn a normal binop on Integers into one that can also deal with a bitsize. -liftBinArith :: (Integer -> Integer -> Integer) -> BinArith -liftBinArith op _ = op +liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV +liftBinArith op w (BV _ x) (BV _ y) = mkBv w $ op x y -type BinArith = Integer -> Integer -> Integer -> Integer +type BinArith w = Integer -> w -> w -> w -arithBinary :: BinArith -> Binary +arithBinary :: forall b w + . BitWord b w + => BinArith w + -> Binary b w arithBinary op = loop where + loop' :: TValue + -> Eval (GenValue b w) + -> Eval (GenValue b w) + -> Eval (GenValue b w) + loop' ty l r = join (loop ty <$> l <*> r) + + loop :: TValue + -> GenValue b w + -> GenValue b w + -> Eval (GenValue b w) loop ty l r = case ty of - - -- words and finite sequences TVSeq w a - | isTBit a -> VWord (mkBv w (op w (fromWord l) (fromWord r))) - | otherwise -> VSeq False (zipWith (loop a) (fromSeq l) (fromSeq r)) + -- words and finite sequences + | isTBit a -> do + lw <- fromVWord "arithLeft" l + rw <- fromVWord "arithRight" r + return $ VWord w $ ready $ WordVal $ op w lw rw + | otherwise -> VSeq w <$> (join (zipSeqMap (loop a) <$> + (fromSeq "arithBinary left" l) <*> + (fromSeq "arithBinary right" r))) - -- streams - TVStream a -> toStream (zipWith (loop a) (fromSeq l) (fromSeq r)) + TVStream a -> + -- streams + VStream <$> (join (zipSeqMap (loop a) <$> + (fromSeq "arithBinary left" l) <*> + (fromSeq "arithBinary right" r))) -- functions TVFun _ ety -> - lam $ \ x -> loop ety (fromVFun l x) (fromVFun r x) + return $ lam $ \ x -> loop' ety (fromVFun l x) (fromVFun r x) -- tuples TVTuple tys -> let ls = fromVTuple l rs = fromVTuple r - in VTuple (zipWith3 loop tys ls rs) + in return $ VTuple (zipWith3 loop' tys ls rs) -- records TVRec fs -> - VRecord [ (f, loop fty (lookupRecord f l) (lookupRecord f r)) - | (f,fty) <- fs ] + return $ VRecord [ (f, loop' fty (lookupRecord f l) (lookupRecord f r)) + | (f,fty) <- fs ] - _ -> evalPanic "arithBinop" ["Invalid arguments"] +type UnaryArith w = Integer -> w -> w -arithUnary :: (Integer -> Integer) -> Unary +liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV +liftUnaryArith op w (BV _ x) = mkBv w $ op x + +arithUnary :: forall b w + . BitWord b w + => UnaryArith w + -> Unary b w arithUnary op = loop where + loop' :: TValue -> Eval (GenValue b w) -> Eval (GenValue b w) + loop' ty x = loop ty =<< x + + loop :: TValue -> GenValue b w -> Eval (GenValue b w) loop ty x = case ty of - -- words and finite sequences TVSeq w a - | isTBit a -> VWord (mkBv w (op (fromWord x))) - | otherwise -> VSeq False (map (loop a) (fromSeq x)) + -- words and finite sequences + | isTBit a -> do + wx <- fromVWord "arithUnary" x + return $ VWord w $ ready $ WordVal $ op w wx + | otherwise -> VSeq w <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x) - -- infinite sequences - TVStream a -> toStream (map (loop a) (fromSeq x)) + TVStream a -> + VStream <$> (mapSeqMap (loop a) =<< fromSeq "arithUnary" x) -- functions TVFun _ ety -> - lam $ \ y -> loop ety (fromVFun x y) + return $ lam $ \ y -> loop' ety (fromVFun x y) -- tuples TVTuple tys -> let as = fromVTuple x - in VTuple (zipWith loop tys as) + in return $ VTuple (zipWith loop' tys as) -- records TVRec fs -> - VRecord [ (f, loop fty (lookupRecord f x)) | (f,fty) <- fs ] + return $ VRecord [ (f, loop' fty (lookupRecord f x)) | (f,fty) <- fs ] + +-- | otherwise = evalPanic "arithUnary" ["Invalid arguments"] - _ -> evalPanic "arithUnary" ["Invalid arguments"] lg2 :: Integer -> Integer lg2 i = case genLog i 2 of @@ -329,36 +427,53 @@ modWrap x y = x `mod` y -- Cmp ------------------------------------------------------------------------- -- | Lexicographic ordering on two values. -lexCompare :: TValue -> Value -> Value -> Ordering -lexCompare ty l r = - case ty of - TVBit -> compare (fromVBit l) (fromVBit r) - TVSeq _ TVBit -> compare (fromWord l) (fromWord r) - TVSeq _ e -> zipLexCompare (repeat e) (fromSeq l) (fromSeq r) - TVTuple etys -> zipLexCompare etys (fromVTuple l) (fromVTuple r) - TVRec fields -> - let tys = map snd (sortBy (comparing fst) fields) - ls = map snd (sortBy (comparing fst) (fromVRecord l)) - rs = map snd (sortBy (comparing fst) (fromVRecord r)) - in zipLexCompare tys ls rs - _ -> evalPanic "lexCompare" ["invalid type"] +lexCompare :: String -> TValue -> Value -> Value -> Eval Ordering +lexCompare nm ty l r = case ty of + + TVBit -> + return $ compare (fromVBit l) (fromVBit r) + + TVSeq _ TVBit -> + compare <$> (fromWord "compareLeft" l) <*> (fromWord "compareRight" r) + + TVSeq w e -> + join (zipLexCompare nm (repeat e) <$> + (enumerateSeqMap w <$> fromSeq "lexCompare left" l) <*> + (enumerateSeqMap w <$> fromSeq "lexCompare right" r)) + + -- tuples + TVTuple etys -> + zipLexCompare nm etys (fromVTuple l) (fromVTuple r) + + -- records + TVRec fields -> + let tys = map snd (sortBy (comparing fst) fields) + ls = map snd (sortBy (comparing fst) (fromVRecord l)) + rs = map snd (sortBy (comparing fst) (fromVRecord r)) + in zipLexCompare nm tys ls rs + + _ -> evalPanic "lexCompare" ["invalid type"] -- XXX the lists are expected to be of the same length, as this should only be -- used with values that come from type-correct expressions. -zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering -zipLexCompare tys ls rs = foldr choose EQ (zipWith3 lexCompare tys ls rs) +zipLexCompare :: String -> [TValue] -> [Eval Value] -> [Eval Value] -> Eval Ordering +zipLexCompare nm tys ls rs = foldr choose (return EQ) (zipWith3 lexCompare' tys ls rs) where - choose c acc = case c of + lexCompare' t l r = join (lexCompare nm t <$> l <*> r) + + choose c acc = c >>= \c' -> case c' of EQ -> acc - _ -> c + _ -> return c' -- | Process two elements based on their lexicographic ordering. -cmpOrder :: (Ordering -> Bool) -> Binary -cmpOrder op ty l r = VBit (op (lexCompare ty l r)) +cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV +cmpOrder nm op ty l r = VBit . op <$> lexCompare nm ty l r -withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary -withOrder choose ty l r = choose (lexCompare ty l r) ty l r +withOrder :: String -> (Ordering -> TValue -> Value -> Value -> Value) -> Binary Bool BV +withOrder nm choose ty l r = + do ord <- lexCompare nm ty l r + return $ choose ord ty l r maxV :: Ordering -> TValue -> Value -> Value -> Value maxV o _ l r = case o of @@ -375,63 +490,165 @@ funCmp :: (Ordering -> Bool) -> Value funCmp op = tlam $ \ _a -> tlam $ \ b -> - lam $ \ l -> - lam $ \ r -> - lam $ \ x -> cmpOrder op b (fromVFun l x) (fromVFun r x) + lam $ \ l -> return $ + lam $ \ r -> return $ + lam $ \ x -> do + l' <- l + r' <- r + x' <- x + fl <- fromVFun l' (ready x') + fr <- fromVFun r' (ready x') + cmpOrder "funCmp" op b fl fr -- Logic ----------------------------------------------------------------------- -zeroV :: TValue -> Value +zeroV :: forall b w + . BitWord b w + => TValue + -> GenValue b w zeroV ty = case ty of -- bits TVBit -> - VBit False + VBit (bitLit False) - -- finite sequences + -- sequences TVSeq w ety - | isTBit ety -> word w 0 - | otherwise -> toFinSeq ety (replicate (fromInteger w) (zeroV ety)) + | isTBit ety -> word w 0 + | otherwise -> VSeq w (SeqMap $ \_ -> ready $ zeroV ety) - -- infinite sequences - TVStream ety -> toStream (repeat (zeroV ety)) + TVStream ety -> + VStream (SeqMap $ \_ -> ready $ zeroV ety) -- functions TVFun _ bty -> - lam (\ _ -> zeroV bty) + lam (\ _ -> ready (zeroV bty)) -- tuples TVTuple tys -> - VTuple (map zeroV tys) + VTuple (map (ready . zeroV) tys) -- records TVRec fields -> - VRecord [ (f,zeroV fty) | (f,fty) <- fields ] + VRecord [ (f,ready $ zeroV fty) | (f,fty) <- fields ] +-- | otherwise = evalPanic "zeroV" ["invalid type for zero"] + + +joinWordVal :: BitWord b w => + WordValue b w -> WordValue b w -> WordValue b w +joinWordVal (WordVal w1) (WordVal w2) = WordVal $ joinWord w1 w2 +joinWordVal w1 w2 = BitsVal $ (asBitsVal w1) Seq.>< (asBitsVal w2) + +joinWords :: forall b w + . BitWord b w + => Integer + -> Integer + -> SeqMap b w + -> Eval (GenValue b w) +joinWords nParts nEach xs = + loop (ready $ WordVal (wordLit 0 0)) (enumerateSeqMap nParts xs) + + where + loop :: Eval (WordValue b w) -> [Eval (GenValue b w)] -> Eval (GenValue b w) + loop !wv [] = return $ VWord (nParts * nEach) wv + loop !wv (w : ws) = do + w >>= \case + VWord _ w' -> loop (joinWordVal <$> wv <*> w') ws + _ -> evalPanic "joinWords: expected word value" [] + +-- loop !bv (Ready (VWord w) : ws) = loop (joinWord bv w) ws + -- loop !bv (w:ws) = do + -- w' <- fromVWord "joinWords" =<< w + -- loop (joinWord bv w') ws + + +joinSeq :: BitWord b w + => Nat' + -> Integer + -> TValue + -> SeqMap b w + -> Eval (GenValue b w) +joinSeq parts each a xs + = return $ mkSeq $ (SeqMap $ \i -> do + let (q,r) = divMod i each + ys <- fromSeq "join seq" =<< lookupSeqMap xs q + lookupSeqMap ys r) + + where + len = parts `nMul` (Nat each) + mkSeq = case len of + Inf -> VStream + Nat n -> VSeq n -- | Join a sequence of sequences into a single sequence. -joinV :: Nat' -> Nat' -> TValue -> Value -> Value -joinV parts each a val = - let len = parts `nMul` each - in toSeq len a (concatMap fromSeq (fromSeq val)) +joinV :: BitWord b w + => Nat' + -> Integer + -> TValue + -> (GenValue b w) + -> Eval (GenValue b w) +joinV parts each a val + -- Try to join a sequence of words, if we can determine that + -- each element is actually a word. Fall back on sequence + -- join otherwise. + | Nat nParts <- parts + , isTBit a + = do xs <- fromSeq "joinV" val + joinWords nParts each xs -splitAtV :: Nat' -> Nat' -> TValue -> Value -> Value +joinV parts each a val = + joinSeq parts each a =<< fromSeq "joinV" val + + +splitWordVal :: BitWord b w + => Integer + -> Integer + -> WordValue b w + -> (WordValue b w, WordValue b w) +splitWordVal leftWidth rightWidth (WordVal w) = + let (lw, rw) = splitWord leftWidth rightWidth w + in (WordVal lw, WordVal rw) +splitWordVal leftWidth rightWidth (BitsVal bs) = + let (lbs, rbs) = Seq.splitAt (fromInteger leftWidth) bs + in (BitsVal lbs, BitsVal rbs) + +splitAtV :: BitWord b w + => Nat' + -> Nat' + -> TValue + -> (GenValue b w) + -> Eval (GenValue b w) splitAtV front back a val = case back of - -- Remember that words are big-endian in cryptol, so the first component - -- needs to be shifted, and the second component just needs to be masked. - Nat rightWidth | aBit, VWord (BV _ i) <- val -> - VTuple [ VWord (BV leftWidth (i `shiftR` fromInteger rightWidth)) - , VWord (mkBv rightWidth i) ] + Nat rightWidth | aBit, VWord _ w <- val -> do + ws <- delay Nothing (splitWordVal leftWidth rightWidth <$> w) + return $ VTuple + [ VWord leftWidth . ready . fst <$> ws + , VWord rightWidth . ready . snd <$> ws + ] - _ -> - let (ls,rs) = genericSplitAt leftWidth (fromSeq val) - in VTuple [VSeq aBit ls, toSeq back a rs] + Inf | aBit, VStream seq <- val -> do + seq <- delay Nothing (fromSeq "splitAtV" val) + ls <- delay Nothing (do m <- fst . splitSeqMap leftWidth <$> seq + let ms = map (fromVBit <$>) (enumerateSeqMap leftWidth m) + return $ Seq.fromList $ ms) + rs <- delay Nothing (snd . splitSeqMap leftWidth <$> seq) + return $ VTuple [ return $ VWord leftWidth (BitsVal <$> ls) + , mkSeq back a <$> rs + ] + + _ -> do + seq <- delay Nothing (fromSeq "splitAtV" val) + ls <- delay Nothing (fst . splitSeqMap leftWidth <$> seq) + rs <- delay Nothing (snd . splitSeqMap leftWidth <$> seq) + return $ VTuple [ VSeq leftWidth <$> ls + , mkSeq back a <$> rs + ] where - aBit = isTBit a leftWidth = case front of @@ -439,109 +656,267 @@ splitAtV front back a val = _ -> evalPanic "splitAtV" ["invalid `front` len"] +extractWordVal :: BitWord b w + => Integer + -> Integer + -> WordValue b w + -> WordValue b w +extractWordVal len start (WordVal w) = + WordVal $ extractWord len start w +extractWordVal len start (BitsVal bs) = + BitsVal $ Seq.take (fromInteger len) $ + Seq.drop (Seq.length bs - fromInteger start - fromInteger len - 1) bs + + -- | Split implementation. -ecSplitV :: Value +ecSplitV :: BitWord b w + => GenValue b w ecSplitV = nlam $ \ parts -> nlam $ \ each -> tlam $ \ a -> lam $ \ val -> - let mkChunks f = map (toFinSeq a) $ f $ fromSeq val - in case (parts, each) of - (Nat p, Nat e) -> VSeq False $ mkChunks (finChunksOf p e) - (Inf , Nat e) -> toStream $ mkChunks (infChunksOf e) + case (parts, each) of + (Nat p, Nat e) | isTBit a -> do + VWord _ val' <- val + return $ VSeq p $ SeqMap $ \i -> do + return $ VWord e (extractWordVal e ((p-i-1)*e) <$> val') + (Nat p, Nat e) -> do + val' <- delay Nothing (fromSeq "ecSplitV" =<< val) + return $ VSeq p $ SeqMap $ \i -> + return $ VSeq e $ SeqMap $ \j -> do + xs <- val' + lookupSeqMap xs (e * i + j) + (Inf , Nat e) -> do + val' <- delay Nothing (fromSeq "ecSplitV" =<< val) + return $ VStream $ SeqMap $ \i -> + return $ VSeq e $ SeqMap $ \j -> do + xs <- val' + lookupSeqMap xs (e * i + j) _ -> evalPanic "splitV" ["invalid type arguments to split"] --- | Split into infinitely many chunks -infChunksOf :: Integer -> [a] -> [[a]] -infChunksOf each xs = let (as,bs) = genericSplitAt each xs - in as : infChunksOf each bs --- | Split into finitely many chunks -finChunksOf :: Integer -> Integer -> [a] -> [[a]] -finChunksOf 0 _ _ = [] -finChunksOf parts each xs = let (as,bs) = genericSplitAt each xs - in as : finChunksOf (parts - 1) each bs +reverseV :: forall b w + . BitWord b w + => GenValue b w + -> Eval (GenValue b w) +reverseV (VSeq n xs) = + return $ VSeq n $ reverseSeqMap n xs +reverseV (VWord n wv) = return (VWord n (revword <$> wv)) + where + revword (WordVal w) = BitsVal $ Seq.reverse $ Seq.fromList $ map ready $ unpackWord w + revword (BitsVal bs) = BitsVal $ Seq.reverse bs +reverseV _ = + evalPanic "reverseV" ["Not a finite sequence"] -ccatV :: Nat' -> Nat' -> TValue -> Value -> Value -> Value -ccatV _front _back (isTBit -> True) (VWord (BV i x)) (VWord (BV j y)) = - VWord (BV (i + j) (shiftL x (fromInteger j) + y)) -ccatV front back elty l r = - toSeq (evalTF TCAdd [front,back]) elty (fromSeq l ++ fromSeq r) +transposeV :: BitWord b w + => Nat' + -> Nat' + -> TValue + -> GenValue b w + -> Eval (GenValue b w) +transposeV a b c xs + | isTBit c, Nat na <- a = + return $ bseq $ SeqMap $ \bi -> + return $ VWord na $ return $ BitsVal $ + Seq.fromFunction (fromInteger na) $ \ai -> do + ys <- flip lookupSeqMap (toInteger ai) =<< fromSeq "transposeV" xs + case ys of + VStream ys' -> fromVBit <$> lookupSeqMap ys' bi + VWord _ wv -> flip bitsSeq bi =<< wv + _ -> evalPanic "transpose" ["expected sequence of bits"] + + | otherwise = do + return $ bseq $ SeqMap $ \bi -> + return $ aseq $ SeqMap $ \ai -> do + ys <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs + z <- flip lookupSeqMap bi =<< fromSeq "transposeV 2" ys + return z + + where + bseq = + case b of + Nat nb -> VSeq nb + Inf -> VStream + aseq = + case a of + Nat na -> VSeq na + Inf -> VStream + + + + +ccatV :: (Show b, Show w, BitWord b w) + => Nat' + -> Nat' + -> TValue + -> (GenValue b w) + -> (GenValue b w) + -> Eval (GenValue b w) + +ccatV front back elty (VWord m l) (VWord n r) = + return $ VWord (m+n) (joinWordVal <$> l <*> r) + +ccatV front back elty (VWord m l) (VStream r) = + return $ VStream $ SeqMap $ \i -> + if i < m then + VBit <$> (flip indexWordValue i =<< l) + else + lookupSeqMap r (i-m) + +ccatV front back elty l r = do + l'' <- delay Nothing (fromSeq "ccatV left" l) + r'' <- delay Nothing (fromSeq "ccatV right" r) + let Nat n = front + mkSeq (evalTF TCAdd [front,back]) elty <$> return (SeqMap $ \i -> + if i < n then do + ls <- l'' + lookupSeqMap ls i + else do + rs <- r'' + lookupSeqMap rs (i-n)) + +wordValLogicOp :: BitWord b w + => (b -> b -> b) + -> (w -> w -> w) + -> WordValue b w + -> WordValue b w + -> WordValue b w +wordValLogicOp _ wop (WordVal w1) (WordVal w2) = WordVal (wop w1 w2) +wordValLogicOp bop _ w1 w2 = + BitsVal $ Seq.zipWith (\x y -> bop <$> x <*> y) (asBitsVal w1) (asBitsVal w2) -- | Merge two values given a binop. This is used for and, or and xor. -logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary -logicBinary op = loop +logicBinary :: forall b w + . BitWord b w + => (b -> b -> b) + -> (w -> w -> w) + -> Binary b w +logicBinary opb opw = loop where + loop' :: TValue + -> Eval (GenValue b w) + -> Eval (GenValue b w) + -> Eval (GenValue b w) + loop' ty l r = join (loop ty <$> l <*> r) + + loop :: TValue + -> GenValue b w + -> GenValue b w + -> Eval (GenValue b w) + loop ty l r = case ty of - TVBit -> VBit (op (fromVBit l) (fromVBit r)) - -- words or finite sequences + TVBit -> return $ VBit (opb (fromVBit l) (fromVBit r)) TVSeq w aty - | isTBit aty -> VWord (BV w (op (fromWord l) (fromWord r))) - -- We assume that bitwise ops do not need re-masking - | otherwise -> VSeq False (zipWith (loop aty) (fromSeq l) - (fromSeq r)) + -- words or finite sequences + | isTBit aty, VWord _ lw <- l, VWord _ rw <- r + -> return $ VWord w (wordValLogicOp opb opw <$> lw <*> rw) + -- We assume that bitwise ops do not need re-masking - -- streams - TVStream aty -> toStream (zipWith (loop aty) (fromSeq l) (fromSeq r)) + -- Nat w | isTBit aty -> do + -- BV _ lw <- fromVWord "logicLeft" l + -- BV _ rw <- fromVWord "logicRight" r + -- return $ VWord $ mkBv w (op lw rw) - TVTuple etys -> - let ls = fromVTuple l - rs = fromVTuple r - in VTuple (zipWith3 loop etys ls rs) + | otherwise -> VSeq w <$> + (join (zipSeqMap (loop aty) <$> + (fromSeq "logicBinary left" l) + <*> (fromSeq "logicBinary right" r))) + + TVStream aty -> + VStream <$> (join (zipSeqMap (loop aty) <$> + (fromSeq "logicBinary left" l) <*> + (fromSeq "logicBinary right" r))) + + TVTuple etys -> do + let ls = fromVTuple l + let rs = fromVTuple r + return $ VTuple $ (zipWith3 loop' etys ls rs) TVFun _ bty -> - lam $ \ a -> loop bty (fromVFun l a) (fromVFun r a) + return $ lam $ \ a -> loop' bty (fromVFun l a) (fromVFun r a) TVRec fields -> - VRecord [ (f,loop fty a b) | (f,fty) <- fields - , let a = lookupRecord f l - b = lookupRecord f r - ] + return $ VRecord [ (f,loop' fty a b) + | (f,fty) <- fields + , let a = lookupRecord f l + b = lookupRecord f r + ] -logicUnary :: (forall a. Bits a => a -> a) -> Unary -logicUnary op = loop +-- | otherwise = evalPanic "logicBinary" ["invalid logic type"] + + +wordValUnaryOp :: BitWord b w + => (b -> b) + -> (w -> w) + -> WordValue b w + -> WordValue b w +wordValUnaryOp _ wop (WordVal w) = WordVal (wop w) +wordValUnaryOp bop _ (BitsVal bs) = BitsVal (fmap (bop <$>) bs) + +logicUnary :: forall b w + . BitWord b w + => (b -> b) + -> (w -> w) + -> Unary b w +logicUnary opb opw = loop where + loop' :: TValue -> Eval (GenValue b w) -> Eval (GenValue b w) + loop' ty val = loop ty =<< val + + loop :: TValue -> GenValue b w -> Eval (GenValue b w) loop ty val = case ty of - TVBit -> VBit (op (fromVBit val)) + TVBit -> return . VBit . opb $ fromVBit val - -- words or finite sequences TVSeq w ety - | isTBit ety -> VWord (mkBv w (op (fromWord val))) - | otherwise -> VSeq False (map (loop ety) (fromSeq val)) + -- words or finite sequences + | isTBit ety, VWord _ wv <- val + -> return $ VWord w (wordValUnaryOp opb opw <$> wv) - -- streams - TVStream ety -> toStream (map (loop ety) (fromSeq val)) + -- Nat w | isTBit ety + -- -> do v <- fromWord "logicUnary" val + -- return $ VWord (mkBv w $ op v) + + | otherwise + -> VSeq w <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val) + + -- streams + TVStream ety -> + VStream <$> (mapSeqMap (loop ety) =<< fromSeq "logicUnary" val) TVTuple etys -> let as = fromVTuple val - in VTuple (zipWith loop etys as) + in return $ VTuple (zipWith loop' etys as) TVFun _ bty -> - lam $ \ a -> loop bty (fromVFun val a) + return $ lam $ \ a -> loop' bty (fromVFun val a) TVRec fields -> - VRecord [ (f,loop fty a) | (f,fty) <- fields, let a = lookupRecord f val ] + return $ VRecord [ (f,loop' fty a) | (f,fty) <- fields, let a = lookupRecord f val ] + +-- | otherwise = evalPanic "logicUnary" ["invalid logic type"] logicShift :: (Integer -> Integer -> Integer -> Integer) -- ^ The function may assume its arguments are masked. -- It is responsible for masking its result if needed. - -> (Nat' -> TValue -> [Value] -> Integer -> [Value]) + -> (Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool)) + -> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap) -> Value -logicShift opW opS +logicShift opW obB opS = nlam $ \ a -> - tlam $ \ _ -> + nlam $ \ _ -> tlam $ \ c -> - lam $ \ l -> - lam $ \ r -> - if isTBit c - then -- words - let BV w i = fromVWord l - in VWord (BV w (opW w i (fromWord r))) + lam $ \ l -> return $ + lam $ \ r -> do + BV _ i <- fromVWord "logicShift amount" =<< r + l >>= \case + VWord w wv -> return $ VWord w $ wv >>= \case + BitsVal bs -> return $ BitsVal (obB w bs i) + WordVal (BV _ x) -> return $ WordVal (BV w (opW w x i)) - else toSeq a c (opS a c (fromSeq l) (fromWord r)) + l' -> mkSeq a c <$> (opS a c <$> (fromSeq "logicShift" =<< l) <*> return i) -- Left shift for words. shiftLW :: Integer -> Integer -> Integer -> Integer @@ -549,26 +924,43 @@ shiftLW w ival by | by >= w = 0 | otherwise = mask w (shiftL ival (fromInteger by)) -shiftLS :: Nat' -> TValue -> [Value] -> Integer -> [Value] -shiftLS w ety vs by = +shiftLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool) +shiftLB w bs by = + Seq.drop (fromInteger (min w by)) bs + Seq.>< + Seq.replicate (fromInteger (min w by)) (ready False) + +shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap +shiftLS w ety vs by = SeqMap $ \i -> case w of Nat len - | by < len -> genericTake len (genericDrop by vs ++ repeat (zeroV ety)) - | otherwise -> genericReplicate len (zeroV ety) - Inf -> genericDrop by vs + | i+by < len -> lookupSeqMap vs (i+by) + | i < len -> return $ zeroV ety + | otherwise -> evalPanic "shiftLS" ["Index out of bounds"] + Inf -> lookupSeqMap vs (i+by) shiftRW :: Integer -> Integer -> Integer -> Integer shiftRW w i by | by >= w = 0 | otherwise = shiftR i (fromInteger by) -shiftRS :: Nat' -> TValue -> [Value] -> Integer -> [Value] -shiftRS w ety vs by = +shiftRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool) +shiftRB w bs by = + Seq.replicate (fromInteger (min w by)) (ready False) + Seq.>< + Seq.take (fromInteger (w - min w by)) bs + +shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap +shiftRS w ety vs by = SeqMap $ \i -> case w of Nat len - | by < len -> genericTake len (genericReplicate by (zeroV ety) ++ vs) - | otherwise -> genericReplicate len (zeroV ety) - Inf -> genericReplicate by (zeroV ety) ++ vs + | i >= by -> lookupSeqMap vs (i-by) + | i < len -> return $ zeroV ety + | otherwise -> evalPanic "shiftLS" ["Index out of bounds"] + Inf + | i >= by -> lookupSeqMap vs (i-by) + | otherwise -> return $ zeroV ety + -- XXX integer doesn't implement rotateL, as there's no bit bound rotateLW :: Integer -> Integer -> Integer -> Integer @@ -576,12 +968,15 @@ 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 -> [Value] -> Integer -> [Value] -rotateLS w _ vs at = +rotateLB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool) +rotateLB w bs by = + let (hd,tl) = Seq.splitAt (fromInteger (by `mod` w)) bs + in tl Seq.>< hd + +rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap +rotateLS w _ vs by = SeqMap $ \i -> case w of - Nat len -> let at' = at `mod` len - (ls,rs) = genericSplitAt at' vs - in rs ++ ls + 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 @@ -590,64 +985,90 @@ 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 -> [Value] -> Integer -> [Value] -rotateRS w _ vs at = +rotateRB :: Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool) +rotateRB w bs by = + let (hd,tl) = Seq.splitAt (fromInteger (w - (by `mod` w))) bs + in tl Seq.>< hd + +rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap +rotateRS w _ vs by = SeqMap $ \i -> case w of - Nat len -> let at' = at `mod` len - (ls,rs) = genericSplitAt (len - at') vs - in rs ++ ls + Nat len -> lookupSeqMap vs ((len - by + i) `mod` len) _ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ] -- Sequence Primitives --------------------------------------------------------- -- | Indexing operations that return one element. -indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value -indexPrimOne op = +indexPrimOne :: BitWord b w + => (Maybe Integer -> TValue -> SeqMap b w -> Seq.Seq b -> Eval (GenValue b w)) + -> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w)) + -> GenValue b w +indexPrimOne bits_op word_op = nlam $ \ n -> - tlam $ \ _a -> + tlam $ \ a -> nlam $ \ _i -> - lam $ \ l -> - lam $ \ r -> - let vs = fromSeq l - ix = fromWord r - in op (fromNat n) vs ix + lam $ \ l -> return $ + lam $ \ r -> do + vs <- l >>= \case + VWord _ w -> w >>= \w' -> return $ SeqMap (\i -> VBit <$> indexWordValue w' i) + VSeq _ vs -> return vs + VStream vs -> return vs + _ -> evalPanic "Expected sequence value" ["indexPrimOne"] + r >>= \case + VWord _ w -> w >>= \case + WordVal w' -> word_op (fromNat n) a vs w' + BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs + _ -> evalPanic "Expected word value" ["indexPrimOne"] -indexFront :: Maybe Integer -> [Value] -> Integer -> Value -indexFront mblen vs ix = +indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value +indexFront mblen _a vs (bvVal -> ix) = case mblen of Just len | len <= ix -> invalidIndex ix - _ -> genericIndex vs ix + _ -> lookupSeqMap vs ix -indexBack :: Maybe Integer -> [Value] -> Integer -> Value -indexBack mblen vs ix = +indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value +indexFront_bits mblen a vs = indexFront mblen a vs . packWord . Fold.toList + +indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value +indexBack mblen _a vs (bvVal -> ix) = case mblen of - Just len | len > ix -> genericIndex vs (len - ix - 1) + Just len | len > ix -> lookupSeqMap vs (len - ix - 1) | otherwise -> invalidIndex ix Nothing -> evalPanic "indexBack" ["unexpected infinite sequence"] +indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq.Seq Bool -> Eval Value +indexBack_bits mblen a vs = indexBack mblen a vs . packWord . Fold.toList + -- | Indexing operations that return many elements. -indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value -indexPrimMany op = +indexPrimMany :: BitWord b w + => (Maybe Integer -> TValue -> SeqMap b w -> Seq.Seq b -> Eval (GenValue b w)) + -> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w)) + -> GenValue b w +indexPrimMany bits_op word_op = nlam $ \ n -> tlam $ \ a -> nlam $ \ m -> - tlam $ \ _i -> - lam $ \ l -> - lam $ \ r -> - let vs = fromSeq l - ixs = map fromWord (fromSeq r) - in toSeq m a (op (fromNat (n)) vs ixs) - -indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value] -indexFrontRange mblen vs = map (indexFront mblen vs) - -indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value] -indexBackRange mblen vs = map (indexBack mblen vs) + nlam $ \ _i -> + lam $ \ l -> return $ + lam $ \ r -> do + vs <- l >>= \case + VWord _ w -> w >>= \w' -> return $ SeqMap (\i -> VBit <$> indexWordValue w' i) + VSeq _ vs -> return vs + VStream vs -> return vs + _ -> evalPanic "Expected sequence value" ["indexPrimMany"] + ixs <- fromSeq "indexPrimMany idx" =<< r + mkSeq m a <$> memoMap (SeqMap $ \i -> do + lookupSeqMap ixs i >>= \case + VWord _ w -> w >>= \case + WordVal w' -> word_op (fromNat n) a vs w' + BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs + _ -> evalPanic "Expected word value" ["indexPrimMany"]) -- @[ 0, 1 .. ]@ -fromThenV :: Value +fromThenV :: BitWord b w + => GenValue b w fromThenV = nlam $ \ first -> nlam $ \ next -> @@ -657,12 +1078,15 @@ fromThenV = (_ , _ , _ , Nat bits') | bits' >= Arch.maxBigIntWidth -> wordTooWide bits' (Nat first', Nat next', Nat len', Nat bits') -> - let nums = enumFromThen first' next' - in VSeq False (genericTake len' (map (VWord . BV bits') nums)) + let diff = next' - first' + in VSeq len' $ SeqMap $ \i -> + ready $ VWord bits' $ return $ + WordVal $ wordLit bits' (first' + i*diff) _ -> evalPanic "fromThenV" ["invalid arguments"] -- @[ 0 .. 10 ]@ -fromToV :: Value +fromToV :: BitWord b w + => GenValue b w fromToV = nlam $ \ first -> nlam $ \ lst -> @@ -671,14 +1095,15 @@ fromToV = (_ , _ , Nat bits') | bits' >= Arch.maxBigIntWidth -> wordTooWide bits' (Nat first', Nat lst', Nat bits') -> - let nums = enumFromThenTo first' (first' + 1) lst' - len = 1 + (lst' - first') - in VSeq False (genericTake len (map (VWord . BV bits') nums)) - - _ -> evalPanic "fromThenV" ["invalid arguments"] + let len = 1 + (lst' - first') + in VSeq len $ SeqMap $ \i -> + ready $ VWord bits' $ return $ + WordVal $ wordLit bits' (first' + i) + _ -> evalPanic "fromToV" ["invalid arguments"] -- @[ 0, 1 .. 10 ]@ -fromThenToV :: Value +fromThenToV :: BitWord b w + => GenValue b w fromThenToV = nlam $ \ first -> nlam $ \ next -> @@ -689,10 +1114,32 @@ fromThenToV = (_ , _ , _ , _ , Nat bits') | bits' >= Arch.maxBigIntWidth -> wordTooWide bits' (Nat first', Nat next', Nat lst', Nat len', Nat bits') -> - let nums = enumFromThenTo first' next' lst' - in VSeq False (genericTake len' (map (VWord . BV bits') nums)) + let diff = next' - first' + in VSeq len' $ SeqMap $ \i -> + ready $ VWord bits' $ return $ + WordVal $ wordLit bits' (first' + i*diff) + _ -> evalPanic "fromThenToV" ["invalid arguments"] - _ -> evalPanic "fromThenV" ["invalid arguments"] + +infFromV :: BitWord b w + => GenValue b w +infFromV = + nlam $ \(finNat' -> bits) -> + wlam $ \first -> + return $ VStream $ SeqMap $ \i -> + ready $ VWord bits $ return $ + WordVal $ wordPlus first (wordLit bits i) + +infFromThenV :: BitWord b w + => GenValue b w +infFromThenV = + nlam $ \(finNat' -> bits) -> + wlam $ \first -> return $ + wlam $ \next -> do + let diff = wordMinus next first + return $ VStream $ SeqMap $ \i -> + ready $ VWord bits $ return $ + WordVal $ wordPlus first (wordMult diff (wordLit bits i)) -- Random Values --------------------------------------------------------------- @@ -709,3 +1156,37 @@ randomV ty seed = unpack s = fromIntegral (s .&. mask64) : unpack (s `shiftR` 64) [a, b, c, d] = take 4 (unpack seed) in fst $ gen 100 $ seedTFGen (a, b, c, d) + +-- Miscellaneous --------------------------------------------------------------- + +errorV :: forall b w + . BitWord b w + => TValue + -> String + -> Eval (GenValue b w) +errorV ty msg = case ty of + -- bits + TVBit -> cryUserError msg + + -- sequences + TVSeq w ety + | isTBit ety -> return $ VWord w $ return $ BitsVal $ + Seq.replicate (fromInteger w) (cryUserError msg) + | otherwise -> return $ VSeq w (SeqMap $ \_ -> errorV ety msg) + + TVStream ety -> + return $ VStream (SeqMap $ \_ -> errorV ety msg) + + -- functions + TVFun _ bty -> + return $ lam (\ _ -> errorV bty msg) + + -- tuples + TVTuple tys -> + return $ VTuple (map (flip errorV msg) tys) + + -- records + TVRec fields -> + return $ VRecord [ (f,errorV fty msg) | (f,fty) <- fields ] + +-- | otherwise = evalPanic "errorV" ["invalid type for error"] diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 7f9220e2..2fa39806 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -56,6 +56,7 @@ import qualified Cryptol.ModuleSystem.NamingEnv as M import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed)) import qualified Cryptol.Utils.Ident as M +import qualified Cryptol.Eval.Monad as E import qualified Cryptol.Eval.Value as E import Cryptol.Testing.Concrete import qualified Cryptol.Testing.Random as TestR @@ -245,13 +246,16 @@ evalCmd str = do P.ExprInput expr -> do (val,_ty) <- replEvalExpr expr ppOpts <- getPPValOpts + valDoc <- io $ rethrowEvalError $ E.runEval $ E.ppValue ppOpts val + -- This is the point where the value gets forced. We deepseq the -- pretty-printed representation of it, rather than the value -- itself, leaving it up to the pretty-printer to determine how -- much of the value to force - out <- io $ rethrowEvalError - $ return $!! show $ pp $ E.WithBase ppOpts val - rPutStrLn out + --out <- io $ rethrowEvalError + -- $ return $!! show $ pp $ E.WithBase ppOpts val + + rPutStrLn (show valDoc) P.LetInput decl -> do -- explicitly make this a top-level declaration, so that it will -- be generalized if mono-binds is enabled @@ -367,13 +371,13 @@ qcCmd qcMode str = prtLn "FAILED" FailFalse vs -> do prtLn "FAILED for the following inputs:" - mapM_ (rPrint . pp . E.WithBase opts) vs + mapM_ (\v -> rPrint =<< (io $ E.runEval $ E.ppValue opts v)) vs FailError err [] -> do prtLn "ERROR" rPrint (pp err) FailError err vs -> do prtLn "ERROR for the following inputs:" - mapM_ (rPrint . pp . E.WithBase opts) vs + mapM_ (\v -> rPrint =<< (io $ E.runEval $ E.ppValue opts v)) vs rPrint (pp err) Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"] @@ -436,8 +440,8 @@ cmdProveSat isSat str = do vss = map (map $ \(_,_,v) -> v) tevss ppvs vs = do parseExpr <- replParseExpr str - let docs = map (pp . E.WithBase ppOpts) vs - -- function application has precedence 3 + docs <- mapM (io . E.runEval . E.ppValue ppOpts) vs + let -- function application has precedence 3 doc = ppPrec 3 parseExpr rPrint $ hang doc 2 (sep docs) <+> text (if isSat then "= True" else "= False") @@ -581,8 +585,9 @@ writeFileCmd file str = do tIsByte x = maybe False (\(n,b) -> T.tIsBit b && T.tIsNum n == Just 8) (T.tIsSeq x) - serializeValue (E.VSeq _ vs) = - return $ BS.pack $ map (serializeByte . E.fromVWord) vs + serializeValue (E.VSeq n vs) = do + ws <- io $ E.runEval (mapM (>>=E.fromVWord "serializeValue") $ E.enumerateSeqMap n vs) + return $ BS.pack $ map serializeByte ws serializeValue _ = panic "Cryptol.REPL.Command.writeFileCmd" ["Impossible: Non-VSeq value of type [n][8]."] @@ -902,8 +907,7 @@ replEvalExpr expr = let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ] return (def1, T.apSubst su (T.sType sig)) - val <- liftModuleCmd (M.evalExpr def1) - _ <- io $ rethrowEvalError $ X.evaluate val + val <- liftModuleCmd (rethrowEvalError . M.evalExpr def1) whenDebug (rPutStrLn (dump def1)) -- add "it" to the namespace bindItVariable ty def1 diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index f064c85d..f5aeffdc 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -16,9 +16,11 @@ module Cryptol.Symbolic where -import Control.Monad (replicateM, when, zipWithM) -import Data.List (transpose, intercalate) +import Control.Monad.IO.Class +import Control.Monad (replicateM, when, zipWithM, foldM) +import Data.List (transpose, intercalate, genericLength, genericIndex) import qualified Data.Map as Map +import qualified Data.Sequence as Seq import qualified Control.Exception as X import qualified Data.SBV.Dynamic as SBV @@ -31,9 +33,11 @@ import qualified Cryptol.ModuleSystem.Monad as M import Cryptol.Symbolic.Prims import Cryptol.Symbolic.Value +import qualified Cryptol.Eval as Eval +import qualified Cryptol.Eval.Monad as Eval +import qualified Cryptol.Eval.Type as Eval import qualified Cryptol.Eval.Value as Eval -import qualified Cryptol.Eval.Type (evalValType, evalNumType) -import qualified Cryptol.Eval.Env (EvalEnv(..)) +import Cryptol.Eval.Env (GenEvalEnv(..)) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat (Nat'(..)) import Cryptol.Utils.Ident (Ident) @@ -43,6 +47,9 @@ import Cryptol.Utils.Panic(panic) import Prelude () import Prelude.Compat +type EvalEnv = GenEvalEnv SBool SWord + + -- External interface ---------------------------------------------------------- proverConfigs :: [(String, SBV.SMTConfig)] @@ -113,6 +120,7 @@ thmSMTResults (SBV.ThmResult r) = [r] proverError :: String -> M.ModuleCmd ProverResult proverError msg modEnv = return (Right (ProverError msg, modEnv), []) + satProve :: ProverCommand -> M.ModuleCmd ProverResult satProve ProverCommand {..} = protectStack proverError $ \modEnv -> M.runModuleM modEnv $ do @@ -158,12 +166,14 @@ satProve ProverCommand {..} = protectStack proverError $ \modEnv -> case predArgTypes pcSchema of Left msg -> return (ProverError msg) Right ts -> do when pcVerbose $ M.io $ putStrLn "Simulating..." - let env = evalDecls mempty extDgs - let v = evalExpr env pcExpr + v <- M.io $ Eval.runEval $ do + env <- Eval.evalDecls extDgs mempty + Eval.evalExpr env pcExpr prims <- M.getPrimMap results' <- runFn $ do args <- mapM tyFn ts - b <- return $! fromVBit (foldl fromVFun v args) + b <- liftIO $ Eval.runEval + (fromVBit <$> foldM fromVFun v (map Eval.ready args)) return b let results = maybe results' (\n -> take n results') mSatNum esatexprs <- case results of @@ -173,12 +183,13 @@ satProve ProverCommand {..} = protectStack proverError $ \modEnv -> tevss <- mapM mkTevs results return $ AllSatResult tevss where - mkTevs result = + mkTevs result = do let Right (_, cws) = SBV.getModel result (vs, _) = parseValues ts cws sattys = unFinType <$> ts - satexprs = zipWithM (Eval.toExpr prims) sattys vs - in case zip3 sattys <$> satexprs <*> pure vs of + satexprs <- liftIO $ Eval.runEval + (zipWithM (Eval.toExpr prims) sattys vs) + case zip3 sattys <$> (sequence satexprs) <*> pure vs of Nothing -> panic "Cryptol.Symbolic.sat" [ "unable to make assignment into expression" ] @@ -208,12 +219,13 @@ satProveOffline ProverCommand {..} = Left msg -> return (Right (Left msg, modEnv), []) Right ts -> do when pcVerbose $ putStrLn "Simulating..." - let env = evalDecls mempty extDgs - let v = evalExpr env pcExpr + v <- liftIO $ Eval.runEval $ + do env <- Eval.evalDecls extDgs mempty + Eval.evalExpr env pcExpr smtlib <- SBV.compileToSMTLib SBV.SMTLib2 isSat $ do args <- mapM tyFn ts - b <- return $! fromVBit (foldl fromVFun v args) - return b + liftIO $ Eval.runEval + (fromVBit <$> foldM fromVFun v (map Eval.ready args)) return (Right (Right smtlib, modEnv), []) protectStack :: (String -> M.ModuleCmd a) @@ -235,17 +247,22 @@ parseValues (t : ts) cws = (v : vs, cws'') parseValue :: FinType -> [SBV.CW] -> (Eval.Value, [SBV.CW]) parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ] parseValue FTBit (cw : cws) = (Eval.VBit (SBV.cwToBool cw), cws) -parseValue (FTSeq 0 FTBit) cws = (Eval.VWord (Eval.BV 0 0), cws) +parseValue (FTSeq 0 FTBit) cws = (Eval.word 0 0, cws) parseValue (FTSeq n FTBit) cws = case SBV.genParse (SBV.KBounded False n) cws of - Just (x, cws') -> (Eval.VWord (Eval.BV (toInteger n) x), cws') - Nothing -> (Eval.VSeq True vs, cws') + Just (x, cws') -> (Eval.word (toInteger n) x, cws') + Nothing -> (VWord (genericLength vs) $ return $ Eval.WordVal $ + Eval.packWord (map fromVBit vs), cws') where (vs, cws') = parseValues (replicate n FTBit) cws -parseValue (FTSeq n t) cws = (Eval.VSeq False vs, cws') +parseValue (FTSeq n t) cws = + (Eval.VSeq (toInteger n) $ Eval.SeqMap $ \i -> + return $ genericIndex vs i + , cws' + ) where (vs, cws') = parseValues (replicate n t) cws -parseValue (FTTuple ts) cws = (Eval.VTuple vs, cws') +parseValue (FTTuple ts) cws = (Eval.VTuple (map Eval.ready vs), cws') where (vs, cws') = parseValues ts cws -parseValue (FTRecord fs) cws = (Eval.VRecord (zip ns vs), cws') +parseValue (FTRecord fs) cws = (Eval.VRecord (zip ns (map Eval.ready vs)), cws') where (ns, ts) = unzip fs (vs, cws') = parseValues ts cws @@ -266,11 +283,11 @@ numType n finType :: TValue -> Maybe FinType finType ty = case ty of - TVBit -> Just FTBit - TVSeq n t -> FTSeq <$> numType n <*> finType t - TVTuple ts -> FTTuple <$> traverse finType ts - TVRec fields -> FTRecord <$> traverse (traverseSnd finType) fields - _ -> Nothing + Eval.TVBit -> Just FTBit + Eval.TVSeq n t -> FTSeq <$> numType n <*> finType t + Eval.TVTuple ts -> FTTuple <$> traverse finType ts + Eval.TVRec fields -> FTRecord <$> traverse (traverseSnd finType) fields + _ -> Nothing unFinType :: FinType -> Type unFinType fty = @@ -286,218 +303,36 @@ unFinType fty = predArgTypes :: Schema -> Either String [FinType] predArgTypes schema@(Forall ts ps ty) | null ts && null ps = - case go (Cryptol.Eval.Type.evalValType mempty ty) of - Just fts -> Right fts - Nothing -> Left $ "Not a valid predicate type:\n" ++ show (pp schema) + case go <$> (Eval.evalType mempty ty) of + Right (Just fts) -> Right fts + _ -> Left $ "Not a valid predicate type:\n" ++ show (pp schema) | otherwise = Left $ "Not a monomorphic type:\n" ++ show (pp schema) where go :: TValue -> Maybe [FinType] - go TVBit = Just [] - go (TVFun ty1 ty2) = (:) <$> finType ty1 <*> go ty2 - go _ = Nothing + go Eval.TVBit = Just [] + go (Eval.TVFun ty1 ty2) = (:) <$> finType ty1 <*> go ty2 + go _ = Nothing forallFinType :: FinType -> SBV.Symbolic Value forallFinType ty = case ty of FTBit -> VBit <$> forallSBool_ - FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0) - FTSeq n FTBit -> VWord <$> (forallBV_ n) - FTSeq n t -> VSeq False <$> replicateM n (forallFinType t) - FTTuple ts -> VTuple <$> mapM forallFinType ts - FTRecord fs -> VRecord <$> mapM (traverseSnd forallFinType) fs + FTSeq 0 FTBit -> return $ Eval.word 0 0 + FTSeq n FTBit -> VWord (toInteger n) . return . Eval.WordVal <$> (forallBV_ n) + FTSeq n t -> do vs <- replicateM n (forallFinType t) + return $ VSeq (toInteger n) $ Eval.SeqMap $ \i -> + return $ genericIndex vs i + FTTuple ts -> VTuple <$> mapM (fmap Eval.ready . forallFinType) ts + FTRecord fs -> VRecord <$> mapM (traverseSnd (fmap Eval.ready . forallFinType)) fs existsFinType :: FinType -> SBV.Symbolic Value existsFinType ty = case ty of FTBit -> VBit <$> existsSBool_ - FTSeq 0 FTBit -> return $ VWord (literalSWord 0 0) - FTSeq n FTBit -> VWord <$> existsBV_ n - FTSeq n t -> VSeq False <$> replicateM n (existsFinType t) - FTTuple ts -> VTuple <$> mapM existsFinType ts - FTRecord fs -> VRecord <$> mapM (traverseSnd existsFinType) fs - --- Simulation environment ------------------------------------------------------ - -data Env = Env - { envVars :: Map.Map Name Value - , envTypes :: Map.Map TVar (Either Nat' TValue) - } - -instance Monoid Env where - mempty = Env - { envVars = Map.empty - , envTypes = Map.empty - } - - mappend l r = Env - { envVars = Map.union (envVars l) (envVars r) - , envTypes = Map.union (envTypes l) (envTypes r) - } - --- | Bind a variable in the evaluation environment. -bindVar :: (Name, Value) -> Env -> Env -bindVar (n, thunk) env = env { envVars = Map.insert n thunk (envVars env) } - --- | Lookup a variable in the environment. -lookupVar :: Name -> Env -> Maybe Value -lookupVar n env = Map.lookup n (envVars env) - --- | Bind a type variable of kind *. -bindType :: TVar -> (Either Nat' TValue) -> Env -> Env -bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) } - --- | Lookup a type variable. -lookupType :: TVar -> Env -> Maybe (Either Nat' TValue) -lookupType p env = Map.lookup p (envTypes env) - --- Expressions ----------------------------------------------------------------- - -evalExpr :: Env -> Expr -> Value -evalExpr env expr = - case expr of - EList es ty -> VSeq (tIsBit ty) (map eval es) - ETuple es -> VTuple (map eval es) - ERec fields -> VRecord [ (f, eval e) | (f, e) <- fields ] - ESel e sel -> evalSel sel (eval e) - EIf b e1 e2 -> iteValue (fromVBit (eval b)) (eval e1) (eval e2) - EComp ty e mss -> evalComp env (evalValType env ty) e mss - EVar n -> case lookupVar n env of - Just x -> x - _ -> panic "Cryptol.Symbolic.evalExpr" [ "Variable " ++ show n ++ " not found" ] - -- TODO: how to deal with uninterpreted functions? - ETAbs tv e -> case tpKind tv of - KType -> VPoly $ \ty -> evalExpr (bindType (tpVar tv) (Right ty) env) e - KNum -> VNumPoly $ \n -> evalExpr (bindType (tpVar tv) (Left n) env) e - k -> panic "[Symbolic] evalExpr" ["invalid kind on type abstraction", show k] - ETApp e ty -> case eval e of - VPoly f -> f (evalValType env ty) - VNumPoly f -> f (evalNumType env ty) - _ -> panic "[Symbolic] evalExpr" - [ "expected a polymorphic value" - , show e, show ty - ] - EApp e1 e2 -> fromVFun (eval e1) (eval e2) - EAbs n _ty e -> VFun $ \x -> evalExpr (bindVar (n, x) env) e - EProofAbs _prop e -> eval e - EProofApp e -> eval e - ECast e _ty -> eval e - EWhere e ds -> evalExpr (evalDecls env ds) e - where - eval e = evalExpr env e - -evalValType :: Env -> Type -> TValue -evalValType env ty = Cryptol.Eval.Type.evalValType env' ty - where env' = Cryptol.Eval.Env.EvalEnv Map.empty (envTypes env) - -evalNumType :: Env -> Type -> Nat' -evalNumType env ty = Cryptol.Eval.Type.evalNumType env' ty - where env' = Cryptol.Eval.Env.EvalEnv Map.empty (envTypes env) - -evalSel :: Selector -> Value -> Value -evalSel sel v = - case sel of - TupleSel n _ -> - case v of - VTuple xs -> xs !! n -- 0-based indexing - VSeq b xs -> VSeq b (map (evalSel sel) xs) - VStream xs -> VStream (map (evalSel sel) xs) - VFun f -> VFun (\x -> evalSel sel (f x)) - _ -> panic "Cryptol.Symbolic.evalSel" [ "Tuple selector applied to incompatible type" ] - - RecordSel n _ -> - case v of - VRecord bs -> case lookup n bs of - Just x -> x - _ -> panic "Cryptol.Symbolic.evalSel" [ "Selector " ++ show n ++ " not found" ] - VSeq b xs -> VSeq b (map (evalSel sel) xs) - VStream xs -> VStream (map (evalSel sel) xs) - VFun f -> VFun (\x -> evalSel sel (f x)) - _ -> panic "Cryptol.Symbolic.evalSel" [ "Record selector applied to non-record" ] - - ListSel n _ -> case v of - VWord s -> VBit (SBV.svTestBit s i) - where i = SBV.intSizeOf s - 1 - n - _ -> fromSeq v !! n -- 0-based indexing - --- Declarations ---------------------------------------------------------------- - -evalDecls :: Env -> [DeclGroup] -> Env -evalDecls = foldl evalDeclGroup - -evalDeclGroup :: Env -> DeclGroup -> Env -evalDeclGroup env dg = - case dg of - NonRecursive d -> bindVar (evalDecl env d) env - Recursive ds -> let env' = foldr bindVar env lazyBindings - bindings = map (evalDecl env') ds - lazyBindings = [ (qname, copyBySchema env (dSignature d) v) - | (d, (qname, v)) <- zip ds bindings ] - in env' - -evalDecl :: Env -> Decl -> (Name, Value) -evalDecl env d = (dName d, body) - where - body = case dDefinition d of - DExpr e -> evalExpr env e - DPrim -> evalPrim d - --- | Make a copy of the given value, building the spine based only on --- the type without forcing the value argument. This lets us avoid --- strictness problems when evaluating recursive definitions. -copyBySchema :: Env -> Schema -> Value -> Value -copyBySchema env0 (Forall params _props ty) = go params env0 - where - go [] env v = copyByType env (evalValType env ty) v - go (p : ps) env v = - case tpKind p of - KType -> VPoly (\t -> go ps (bindType (tpVar p) (Right t) env) (fromVPoly v t)) - KNum -> VNumPoly (\t -> go ps (bindType (tpVar p) (Left t) env) (fromVNumPoly v t)) - k -> panic "[Eval] copyBySchema" ["invalid kind on type abstraction", show k] - -copyByType :: Env -> TValue -> Value -> Value -copyByType env ty v = - case ty of - TVBit -> VBit (fromVBit v) - TVSeq _ ety -> VSeq (isTBit ety) (fromSeq v) - TVStream _ -> VStream (fromSeq v) - TVFun _ bty -> VFun (\x -> copyByType env bty (fromVFun v x)) - TVTuple tys -> VTuple (zipWith (copyByType env) tys (fromVTuple v)) - TVRec fs -> VRecord [ (f, copyByType env t (lookupRecord f v)) | (f, t) <- fs ] --- copyByType env ty v = logicUnary id id (evalValType env ty) v - --- List Comprehensions --------------------------------------------------------- - --- | Evaluate a comprehension. -evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value -evalComp env seqty body ms = - case Eval.isTSeq seqty of - Just (len, el) -> toSeq len el [ evalExpr e body | e <- envs ] - Nothing -> evalPanic "Cryptol.Eval" ["evalComp given a non sequence", show seqty] - - -- XXX we could potentially print this as a number if the type was available. - where - -- generate a new environment for each iteration of each parallel branch - benvs = map (branchEnvs env) ms - - -- take parallel slices of each environment. when the length of the list - -- drops below the number of branches, one branch has terminated. - allBranches es = length es == length ms - slices = takeWhile allBranches (transpose benvs) - - -- join environments to produce environments at each step through the process. - envs = map mconcat slices - --- | Turn a list of matches into the final environments for each iteration of --- the branch. -branchEnvs :: Env -> [Match] -> [Env] -branchEnvs env matches = - case matches of - [] -> [env] - m : ms -> do env' <- evalMatch env m - branchEnvs env' ms - --- | Turn a match into the list of environments it represents. -evalMatch :: Env -> Match -> [Env] -evalMatch env m = case m of - From n _ty expr -> [ bindVar (n, v) env | v <- fromSeq (evalExpr env expr) ] - Let d -> [ bindVar (evalDecl env d) env ] + FTSeq 0 FTBit -> return $ Eval.word 0 0 + FTSeq n FTBit -> VWord (toInteger n) . return . Eval.WordVal <$> (existsBV_ n) + FTSeq n t -> do vs <- replicateM n (existsFinType t) + return $ VSeq (toInteger n) $ Eval.SeqMap $ \i -> + return $ genericIndex vs i + FTTuple ts -> VTuple <$> mapM (fmap Eval.ready . existsFinType) ts + FTRecord fs -> VRecord <$> mapM (traverseSnd (fmap Eval.ready . existsFinType)) fs diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index 213d8a66..7b3920cc 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -8,15 +8,34 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeSynonymInstances #-} + module Cryptol.Symbolic.Prims where +import Data.Bits import Data.List (genericDrop, genericReplicate, genericSplitAt, genericTake, sortBy, transpose) import Data.Ord (comparing) +import qualified Data.Sequence as Seq +import qualified Data.Foldable as Fold -import Cryptol.Eval.Value (BitWord(..)) -import Cryptol.Prims.Eval (binary, unary) +import Cryptol.Eval.Monad (Eval(..), ready) +import Cryptol.Eval.Type (finNat', TValue(..)) +import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..), + finiteSeqMap, reverseSeqMap, wlam, nlam, WordValue(..), + asWordVal, asBitsVal, fromWordVal ) +import Cryptol.Prims.Eval (binary, unary, arithUnary, + arithBinary, Binary, BinArith, + logicBinary, logicUnary, zeroV, + ccatV, splitAtV, joinV, ecSplitV, + reverseV, infFromV, infFromThenV, + fromThenV, fromToV, fromThenToV, + transposeV, indexPrimOne, indexPrimMany, + ecDemoteV) import Cryptol.Symbolic.Value import Cryptol.TypeCheck.AST (Decl(..)) import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul) @@ -31,18 +50,23 @@ import qualified Data.Text as T import Prelude () import Prelude.Compat +import Control.Monad (join) traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) traverseSnd f (x, y) = (,) x <$> f y -- Primitives ------------------------------------------------------------------ -evalPrim :: Decl -> Value -evalPrim Decl { dName = n, .. } - | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val +instance EvalPrims SBool SWord where + evalPrim Decl { dName = n, .. } + | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val -evalPrim Decl { .. } = - panic "Eval" [ "Unimplemented primitive", show dName ] + evalPrim Decl { .. } = + panic "Eval" [ "Unimplemented primitive", show dName ] + + iteValue b x y + | Just b' <- SBV.svAsBool b = if b' then x else y + | otherwise = iteSValue b <$> x <*> y -- See also Cryptol.Prims.Eval.primTable primTable :: Map.Map Ident Value @@ -51,422 +75,325 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v)) , ("False" , VBit SBV.svFalse) , ("demote" , ecDemoteV) -- Converts a numeric type into its corresponding value. -- { val, bits } (fin val, fin bits, bits >= width val) => [bits] - , ("+" , binary (arithBinary SBV.svPlus)) -- {a} (Arith a) => a -> a -> a - , ("-" , binary (arithBinary SBV.svMinus)) -- {a} (Arith a) => a -> a -> a - , ("*" , binary (arithBinary SBV.svTimes)) -- {a} (Arith a) => a -> a -> a - , ("/" , binary (arithBinary SBV.svQuot)) -- {a} (Arith a) => a -> a -> a - , ("%" , binary (arithBinary SBV.svRem)) -- {a} (Arith a) => a -> a -> a + , ("+" , binary (arithBinary (liftBinArith SBV.svPlus))) -- {a} (Arith a) => a -> a -> a + , ("-" , binary (arithBinary (liftBinArith SBV.svMinus))) -- {a} (Arith a) => a -> a -> a + , ("*" , binary (arithBinary (liftBinArith SBV.svTimes))) -- {a} (Arith a) => a -> a -> a + , ("/" , binary (arithBinary (liftBinArith SBV.svQuot))) -- {a} (Arith a) => a -> a -> a + , ("%" , binary (arithBinary (liftBinArith SBV.svRem))) -- {a} (Arith a) => a -> a -> a , ("^^" , binary (arithBinary sExp)) -- {a} (Arith a) => a -> a -> a , ("lg2" , unary (arithUnary sLg2)) -- {a} (Arith a) => a -> a - , ("negate" , unary (arithUnary SBV.svUNeg)) - + , ("negate" , unary (arithUnary (\_ -> SBV.svUNeg))) , ("<" , binary (cmpBinary cmpLt cmpLt SBV.svFalse)) , (">" , binary (cmpBinary cmpGt cmpGt SBV.svFalse)) , ("<=" , binary (cmpBinary cmpLtEq cmpLtEq SBV.svTrue)) , (">=" , binary (cmpBinary cmpGtEq cmpGtEq SBV.svTrue)) , ("==" , binary (cmpBinary cmpEq cmpEq SBV.svTrue)) , ("!=" , binary (cmpBinary cmpNotEq cmpNotEq SBV.svFalse)) - , ("&&" , binary (logicBinary SBV.svAnd SBV.svAnd)) , ("||" , binary (logicBinary SBV.svOr SBV.svOr)) , ("^" , binary (logicBinary SBV.svXOr SBV.svXOr)) , ("complement" , unary (logicUnary SBV.svNot SBV.svNot)) - , ("zero" , VPoly zeroV) + , ("zero" , tlam zeroV) + , ("<<" , logicShift "<<" + SBV.svShiftLeft + (\sz i shft -> + case sz of + Inf -> Just (i+shft) + Nat n + | i+shft >= n -> Nothing + | otherwise -> Just (i+shft))) + , (">>" , logicShift ">>" + SBV.svShiftRight + (\_sz i shft -> + if i-shft < 0 then Nothing else Just (i-shft))) + , ("<<<" , logicShift "<<<" + SBV.svRotateLeft + (\sz i shft -> + case sz of + Inf -> evalPanic "cannot rotate infinite sequence" [] + Nat n -> Just ((i+shft) `mod` n))) + , (">>>" , logicShift ">>>" + SBV.svRotateRight + (\sz i shft -> + case sz of + Inf -> evalPanic "cannot rotate infinite sequence" [] + Nat n -> Just ((i+n-shft) `mod` n))) - , ("<<" , -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a - nlam $ \m -> - tlam $ \_ -> - tlam $ \a -> - VFun $ \xs -> - VFun $ \y -> - case xs of - VWord x -> VWord (SBV.svShiftLeft x (fromVWord y)) - _ -> - let shl :: Integer -> Value - shl i = - case m of - Inf -> dropV i xs - Nat j | i >= j -> replicateV j a (zeroV a) - | otherwise -> catV (dropV i xs) (replicateV i a (zeroV a)) + , ("#" , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d + nlam $ \ front -> + nlam $ \ back -> + tlam $ \ elty -> + lam $ \ l -> return $ + lam $ \ r -> join (ccatV front back elty <$> l <*> r)) - in selectV shl y) + , ("splitAt" , + nlam $ \ front -> + nlam $ \ back -> + tlam $ \ a -> + lam $ \ x -> + splitAtV front back a =<< x) - , (">>" , -- {m,n,a} (fin n) => [m] a -> [n] -> [m] a - nlam $ \m -> - tlam $ \_ -> - tlam $ \a -> - VFun $ \xs -> - VFun $ \y -> - case xs of - VWord x -> VWord (SBV.svShiftRight x (fromVWord y)) - _ -> - let shr :: Integer -> Value - shr i = - case m of - Inf -> catV (replicateV i a (zeroV a)) xs - Nat j | i >= j -> replicateV j a (zeroV a) - | otherwise -> catV (replicateV i a (zeroV a)) (takeV (j - i) xs) - in selectV shr y) - - , ("<<<" , -- {m,n,a} (fin m, fin n) => [m] a -> [n] -> [m] a - nlam $ \m -> - tlam $ \_ -> - tlam $ \_ -> - VFun $ \xs -> - VFun $ \y -> - case xs of - VWord x -> VWord (SBV.svRotateLeft x (fromVWord y)) - _ -> let rol :: Integer -> Value - rol i = catV (dropV k xs) (takeV k xs) - where k = i `mod` finNat' m - in selectV rol y) - - , (">>>" , -- {m,n,a} (fin m, fin n) => [m] a -> [n] -> [m] a - nlam $ \m -> - tlam $ \_ -> - tlam $ \_ -> - VFun $ \xs -> - VFun $ \y -> - case xs of - VWord x -> VWord (SBV.svRotateRight x (fromVWord y)) - _ -> - let ror :: Integer -> Value - ror i = catV (dropV k xs) (takeV k xs) - where k = (- i) `mod` finNat' m - in selectV ror y) - - , ("#" , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d - tlam $ \_ -> - tlam $ \_ -> - tlam $ \_ -> - VFun $ \v1 -> - VFun $ \v2 -> catV v1 v2) - - , ("splitAt" , -- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c) - nlam $ \(finNat' -> a) -> - nlam $ \_ -> - tlam $ \_ -> - VFun $ \v -> VTuple [takeV a v, dropV a v]) - - , ("join" , nlam $ \ parts -> - nlam $ \ each -> - tlam $ \ a -> lam (joinV parts each a)) + , ("join" , + nlam $ \ parts -> + nlam $ \ (finNat' -> each) -> + tlam $ \ a -> + lam $ \ x -> + joinV parts each a =<< x) , ("split" , ecSplitV) - , ("reverse" , - nlam $ \a -> - tlam $ \b -> - lam $ \(fromSeq -> xs) -> toSeq a b (reverse xs)) + , ("reverse" , nlam $ \a -> + tlam $ \b -> + lam $ \xs -> reverseV =<< xs) - , ("transpose" , - nlam $ \a -> - nlam $ \b -> - tlam $ \c -> - lam $ \((map fromSeq . fromSeq) -> xs) -> - case a of - Nat 0 -> - let v = toSeq a c [] - in case b of - Nat n -> toSeq b (tvSeq a c) $ genericReplicate n v - Inf -> VStream $ repeat v - _ -> toSeq b (tvSeq a c) $ map (toSeq a c) $ transpose xs) - - , ("@" , -- {n,a,i} (fin i) => [n]a -> [i] -> a - tlam $ \_ -> - tlam $ \a -> - tlam $ \_ -> - VFun $ \xs -> - VFun $ \y -> - let isInf = case xs of VStream _ -> True; _ -> False - err = zeroV a -- default for out-of-bounds accesses - in atV isInf err (fromSeq xs) y) - - , ("@@" , -- {n,a,m,i} (fin i) => [n]a -> [m][i] -> [m]a - tlam $ \_ -> - tlam $ \a -> - tlam $ \_ -> - tlam $ \_ -> - VFun $ \xs -> - VFun $ \ys -> - let isInf = case xs of VStream _ -> True; _ -> False - err = zeroV a -- default for out-of-bounds accesses - in atV_list (isTBit a) isInf err (fromSeq xs) ys) - - , ("!" , -- {n,a,i} (fin n, fin i) => [n]a -> [i] -> a - tlam $ \_ -> - tlam $ \a -> - tlam $ \_ -> - VFun $ \xs -> - VFun $ \y -> - let err = zeroV a -- default for out-of-bounds accesses - isInf = False -- type of (!) guarantess finite sequences - in atV isInf err (reverse $ fromSeq xs) y) - - , ("!!" , -- {n,a,m,i} (fin n, fin i) => [n]a -> [m][i] -> [m]a - tlam $ \_ -> - tlam $ \a -> - tlam $ \_ -> - tlam $ \_ -> - VFun $ \xs -> - VFun $ \ys -> - let err = zeroV a -- default for out-of-bounds accesses - isInf = False -- type of (!!) guarantess finite sequences - in atV_list (isTBit a) isInf err (reverse $ fromSeq xs) ys) + , ("transpose" , nlam $ \a -> + nlam $ \b -> + tlam $ \c -> + lam $ \xs -> transposeV a b c =<< xs) , ("fromThen" , fromThenV) , ("fromTo" , fromToV) , ("fromThenTo" , fromThenToV) + , ("infFrom" , infFromV) + , ("infFromThen" , infFromThenV) - , ("infFrom" , - nlam $ \(finNat' -> bits) -> - lam $ \(fromVWord -> first) -> - toStream [ VWord (SBV.svPlus first (literalSWord (fromInteger bits) i)) | i <- [0 ..] ]) + , ("@" , indexPrimOne indexFront_bits indexFront) + , ("@@" , indexPrimMany indexFront_bits indexFront) + , ("!" , indexPrimOne indexBack_bits indexBack) + , ("!!" , indexPrimMany indexBack_bits indexBack) - , ("infFromThen" , -- {a} (fin a) => [a] -> [a] -> [inf][a] - tlam $ \_ -> - lam $ \(fromVWord -> first) -> - lam $ \(fromVWord -> next) -> - toStream (map VWord (iterate (SBV.svPlus (SBV.svMinus next first)) first))) + , ("pmult" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1] + nlam $ \(finNat' -> i) -> + nlam $ \(finNat' -> j) -> + VFun $ \v1 -> return $ + VFun $ \v2 -> do + let k = max 1 (i + j) - 1 + mul _ [] ps = ps + mul as (b:bs) ps = mul (SBV.svFalse : as) bs (ites b (as `addPoly` ps) ps) + xs <- sequence . Fold.toList . asBitsVal =<< fromWordVal "pmult 1" =<< v1 + ys <- sequence . Fold.toList . asBitsVal =<< fromWordVal "pmult 2" =<< v2 + let zs = genericTake k (mul xs ys [] ++ repeat SBV.svFalse) + return $ VWord k $ return $ BitsVal $ Seq.fromList $ map ready zs) + + , ("pdiv" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [a] + nlam $ \(finNat' -> i) -> + nlam $ \(finNat' -> j) -> + VFun $ \v1 -> return $ + VFun $ \v2 -> do + xs <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pdiv 1" =<< v1 + ys <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pdiv 2" =<< v2 + let zs = genericTake i (fst (mdp xs ys) ++ repeat SBV.svFalse) + return $ VWord i $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs) + + , ("pmod" , -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b] + nlam $ \(finNat' -> i) -> + nlam $ \(finNat' -> j) -> + VFun $ \v1 -> return $ + VFun $ \v2 -> do + xs <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pmod 1" =<< v1 + ys <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pmod 2" =<< v2 + let zs = genericTake j (snd (mdp xs ys) ++ repeat SBV.svFalse) + return $ VWord j $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs) -- {at,len} (fin len) => [len][8] -> at , ("error" , tlam $ \at -> nlam $ \(finNat' -> _len) -> - VFun $ \_msg -> zeroV at) -- error/undefined, is arbitrarily translated to 0 + VFun $ \_msg -> + return $ zeroV at) -- error/undefined, is arbitrarily translated to 0 - , ("pmult" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1] - nlam $ \(finNat' -> i) -> - nlam $ \(finNat' -> j) -> - VFun $ \v1 -> - VFun $ \v2 -> - let k = max 1 (i + j) - 1 - mul _ [] ps = ps - mul as (b:bs) ps = mul (SBV.svFalse : as) bs (ites b (as `addPoly` ps) ps) - xs = map fromVBit (fromSeq v1) - ys = map fromVBit (fromSeq v2) - zs = take (fromInteger k) (mul xs ys [] ++ repeat SBV.svFalse) - in VSeq True (map VBit zs)) + , ("random" , + tlam $ \_a -> + wlam $ \_x -> + Thunk $ return $ panic + "Cryptol.Symbolic.Prims.evalECon" + [ "can't symbolically evaluate ECRandom" ]) - , ("pdiv" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [a] - nlam $ \(finNat' -> i) -> - tlam $ \_ -> - VFun $ \v1 -> - VFun $ \v2 -> - let xs = map fromVBit (fromSeq v1) - ys = map fromVBit (fromSeq v2) - zs = take (fromInteger i) (fst (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse) - in VSeq True (map VBit (reverse zs))) - - , ("pmod" , -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b] - nlam $ \_ -> - nlam $ \(finNat' -> j) -> - VFun $ \v1 -> - VFun $ \v2 -> - let xs = map fromVBit (fromSeq v1) - ys = map fromVBit (fromSeq v2) - zs = take (fromInteger j) (snd (mdp (reverse xs) (reverse ys)) ++ repeat SBV.svFalse) - in VSeq True (map VBit (reverse zs))) - - , ("random" , panic "Cryptol.Symbolic.Prims.evalECon" - [ "can't symbolically evaluae ECRandom" ]) + -- The trace function simply forces its first two + -- values before returing the third in the symbolic + -- evaluator. + , ("trace", + nlam $ \_n -> + tlam $ \_a -> + tlam $ \_b -> + lam $ \s -> return $ + lam $ \x -> return $ + lam $ \y -> do + _ <- s + _ <- x + y) ] -selectV :: (Integer -> Value) -> Value -> Value -selectV f v = sel 0 bits - where - bits = map fromVBit (fromSeq v) -- index bits in big-endian order +iteWord :: SBool + -> Eval (WordValue SBool SWord) + -> Eval (WordValue SBool SWord) + -> Eval (WordValue SBool SWord) +iteWord c x y = mergeWord True c <$> x <*> y - sel :: Integer -> [SBool] -> Value - sel offset [] = f offset - sel offset (b : bs) = iteValue b m1 m2 +logicShift :: String + -> (SWord -> SWord -> SWord) + -> (Nat' -> Integer -> Integer -> Maybe Integer) + -> Value +logicShift nm wop reindex = + nlam $ \m -> + nlam $ \n -> + tlam $ \a -> + VFun $ \xs -> return $ + VFun $ \y -> do + let Nat len = n + idx <- fromWordVal "<<" =<< y + + xs >>= \case + VWord w x -> return $ VWord w $ do + x >>= \case + WordVal x' -> WordVal . wop x' <$> asWordVal idx + BitsVal bs -> selectV len iteWord idx $ \shft -> + BitsVal $ Seq.fromFunction (Seq.length bs) $ \i -> + case reindex (Nat w) (toInteger i) shft of + Nothing -> return $ bitLit False + Just i' -> Seq.index bs i + + VSeq w xs -> selectV len iteValue idx $ \shft -> + VSeq w $ SeqMap $ \i -> + case reindex (Nat w) i shft of + Nothing -> return $ zeroV a + Just i' -> lookupSeqMap xs i' + + VStream xs -> selectV len iteValue idx $ \shft -> + VStream $ SeqMap $ \i -> + case reindex Inf i shft of + Nothing -> return $ zeroV a + Just i' -> lookupSeqMap xs i' + + _ -> evalPanic "expected sequence value in shift operation" [nm] + + +selectV :: forall a + . Integer + -> (SBool -> Eval a -> Eval a -> Eval a) + -> WordValue SBool SWord + -> (Integer -> a) + -> Eval a +selectV len mux val f = + case val of + WordVal x | Just idx <- SBV.svAsInteger x -> return $ f idx + | otherwise -> sel 0 (unpackWord x) + BitsVal bs -> sel 0 =<< sequence (Fold.toList bs) + + where + -- index bits in big-endian order + bits = sequence $ asBitsVal val + + sel offset [] = return $ f offset + sel offset (b : bs) = mux b m1 m2 where m1 = sel (offset + 2 ^ length bs) bs m2 = sel offset bs -asWordList :: [Value] -> Maybe [SWord] -asWordList = go id - where go :: ([SWord] -> [SWord]) -> [Value] -> Maybe [SWord] + +indexFront :: Maybe Integer + -> TValue + -> SeqMap SBool SWord + -> SWord + -> Eval Value +indexFront mblen a xs idx + | Just i <- SBV.svAsInteger idx + = lookupSeqMap xs i + + | Just n <- mblen + , TVSeq wlen TVBit <- a + = do wvs <- traverse (fromWordVal "indexFront" =<<) (enumerateSeqMap n xs) + case asWordList wvs of + Just ws -> + return $ VWord n $ ready $ WordVal $ SBV.svSelect ws (wordLit wlen 0) idx + Nothing -> foldr f def [0 .. 2^w - 1] + + | otherwise + = foldr f def [0 .. 2^w - 1] + + where + k = SBV.kindOf idx + w = SBV.intSizeOf idx + def = ready $ VWord (toInteger w) $ ready $ WordVal $ SBV.svInteger k 0 + f n y = iteValue (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y + + +indexBack :: Maybe Integer + -> TValue + -> SeqMap SBool SWord + -> SWord + -> Eval Value +indexBack (Just n) a xs idx = indexFront (Just n) a (reverseSeqMap n xs) idx +indexBack Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack"] + +indexFront_bits :: Maybe Integer + -> TValue + -> SeqMap SBool SWord + -> Seq.Seq SBool + -> Eval Value +indexFront_bits mblen a xs bits0 = go 0 (length bits0) (Fold.toList bits0) + where + go :: Integer -> Int -> [SBool] -> Eval Value + go i _k [] + -- For indices out of range, return 0 arbitrarily + | Just n <- mblen + , i >= n + = return $ zeroV a + + | otherwise + = lookupSeqMap xs i + + go i k (b:bs) + | Just n <- mblen + , (i `shiftL` k) >= n + = return $ zeroV a + + | otherwise + = iteValue b (go ((i `shiftL` 1) + 1) (k-1) bs) + (go (i `shiftL` 1) (k-1) bs) + +indexBack_bits :: Maybe Integer + -> TValue + -> SeqMap SBool SWord + -> Seq.Seq SBool + -> Eval Value +indexBack_bits (Just n) a xs idx = indexFront_bits (Just n) a (reverseSeqMap n xs) idx +indexBack_bits Nothing _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"] + + +asBitList :: [Eval SBool] -> Maybe [SBool] +asBitList = go id + where go :: ([SBool] -> [SBool]) -> [Eval SBool] -> Maybe [SBool] go f [] = Just (f []) - go f (VWord x:vs) = go (f . (x:)) vs - go f (VSeq True bs:vs) = go (f . (x:)) vs - where x = packWord $ map fromVBit bs + go f (Ready b:vs) = go (f . (b:)) vs go _ _ = Nothing -atV_list :: Bool -- Are the elements of the resulting sequence bits? - -> Bool -- Is this an infinite sequence? - -> Value -- default value - -> [Value] -- values to select - -> Value -- index - -> Value --- Use SBV selection primitives if possible --- NB: only examine the list if it is finite -atV_list isBit False def (asWordList -> Just ws) v = - case v of - VSeq _ ys -> - VSeq isBit $ map (VWord . SBV.svSelect ws (fromVWord def) . fromVWord) ys - VStream ys -> - VStream $ map (VWord . SBV.svSelect ws (fromVWord def) . fromVWord) ys - _ -> panic "Cryptol.Symbolic.Prims.atV_list" [ "non-mappable value" ] - -atV_list isBit _ def xs v = - case v of - VSeq _ ys -> - VSeq isBit $ map (iteAtV def xs) ys - VStream ys -> - VStream $ map (iteAtV def xs) ys - _ -> panic "Cryptol.Symbolic.Prims.atV_list" [ "non-mappable value" ] - - -atV :: Bool -- Is this an infinite sequence? - -> Value -- default value - -> [Value] -- values to select - -> Value -- index - -> Value - --- When applicable, use the SBV selection operation --- NB: only examine the list if it is finite -atV False def (asWordList -> Just ws) i = - VWord $ SBV.svSelect ws (fromVWord def) (fromVWord i) - --- Otherwise, decompose into a sequence of if/then/else operations -atV _ def vs i = iteAtV def vs i - --- Select a value at an index by building a sequence of if/then/else operations -iteAtV :: Value -> [Value] -> Value -> Value -iteAtV def vs i = - case i of - VSeq True (map fromVBit -> bits) -> -- index bits in big-endian order - case foldr weave vs bits of - [] -> def - y : _ -> y - VWord x -> foldr f def (zip [0 .. 2 ^ SBV.intSizeOf x - 1] vs) - where - k = SBV.kindOf x - f (n, v) y = iteValue (SBV.svEqual x (SBV.svInteger k n)) v y - _ -> evalPanic "Cryptol.Symbolic.Prims.selectV" ["Invalid index argument"] - where - weave :: SBool -> [Value] -> [Value] - weave _ [] = [] - weave b [x1] = [iteValue b def x1] - weave b (x1 : x2 : xs) = iteValue b x2 x1 : weave b xs +asWordList :: [WordValue SBool SWord] -> Maybe [SWord] +asWordList = go id + where go :: ([SWord] -> [SWord]) -> [WordValue SBool SWord] -> Maybe [SWord] + go f [] = Just (f []) + go f (WordVal x :vs) = go (f . (x:)) vs + go f (BitsVal bs:vs) = + case asBitList (Fold.toList bs) of + Just xs -> go (f . (packWord xs:)) vs + Nothing -> Nothing -replicateV :: Integer -- ^ number of elements - -> TValue -- ^ type of element - -> Value -- ^ element - -> Value -replicateV n TVBit x = VSeq True (genericReplicate n x) -replicateV n _ x = VSeq False (genericReplicate n x) +liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord +liftBinArith op _ = op -nth :: a -> [a] -> Int -> a -nth def [] _ = def -nth def (x : xs) n - | n == 0 = x - | otherwise = nth def xs (n - 1) - -nthV :: Value -> Value -> Integer -> Value -nthV err v n = - case v of - VStream xs -> nth err xs (fromInteger n) - VSeq _ xs -> nth err xs (fromInteger n) - VWord x -> let i = SBV.intSizeOf x - 1 - fromInteger n - in if i < 0 then err else - VBit (SBV.svTestBit x i) - _ -> err - -mapV :: Bool -> (Value -> Value) -> Value -> Value -mapV isBit f v = - case v of - VSeq _ xs -> VSeq isBit (map f xs) - VStream xs -> VStream (map f xs) - _ -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ] - -catV :: Value -> Value -> Value -catV xs (VStream ys) = VStream (fromSeq xs ++ ys) -catV (VWord x) ys = VWord (SBV.svJoin x (fromVWord ys)) -catV xs (VWord y) = VWord (SBV.svJoin (fromVWord xs) y) -catV (VSeq b xs) (VSeq _ ys) = VSeq b (xs ++ ys) -catV _ _ = panic "Cryptol.Symbolic.Prims.catV" [ "non-concatenable value" ] - -dropV :: Integer -> Value -> Value -dropV 0 xs = xs -dropV n xs = - case xs of - VSeq b xs' -> VSeq b (genericDrop n xs') - VStream xs' -> VStream (genericDrop n xs') - VWord w -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1 - fromInteger n) 0 w - _ -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ] - -takeV :: Integer -> Value -> Value -takeV n xs = - case xs of - VWord w -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1) (SBV.intSizeOf w - fromInteger n) w - VSeq b xs' -> VSeq b (genericTake n xs') - VStream xs' -> VSeq b (genericTake n xs') - where b = case xs' of VBit _ : _ -> True - _ -> False - _ -> panic "Cryptol.Symbolic.Prims.takeV" [ "non-takeable value" ] - --- | Make a numeric constant. --- { val, bits } (fin val, fin bits, bits >= width val) => [bits] -ecDemoteV :: Value -ecDemoteV = nlam $ \valT -> - nlam $ \bitT -> - case (valT, bitT) of - (Nat v, Nat bs) -> VWord (literalSWord (fromInteger bs) v) - _ -> evalPanic "Cryptol.Prove.evalECon" - ["Unexpected Inf in constant." - , show valT - , show bitT - ] - - --- Arith ----------------------------------------------------------------------- - -type Binary = TValue -> Value -> Value -> Value -type Unary = TValue -> Value -> Value - --- | Models functions of type `{a} (Arith a) => a -> a -> a` -arithBinary :: (SWord -> SWord -> SWord) -> Binary -arithBinary op = loop - where - loop ty l r = - case ty of - TVBit -> evalPanic "arithBinop" ["Invalid arguments"] - TVSeq _ TVBit -> VWord (op (fromVWord l) (fromVWord r)) - TVSeq _ t -> VSeq False (zipWith (loop t) (fromSeq l) (fromSeq r)) - TVStream t -> VStream (zipWith (loop t) (fromSeq l) (fromSeq r)) - TVTuple ts -> VTuple (zipWith3 loop ts (fromVTuple l) (fromVTuple r)) - TVRec fs -> VRecord [ (f, loop t (lookupRecord f l) (lookupRecord f r)) | (f, t) <- fs ] - TVFun _ t -> VFun (\x -> loop t (fromVFun l x) (fromVFun r x)) - --- | Models functions of type `{a} (Arith a) => a -> a` -arithUnary :: (SWord -> SWord) -> Unary -arithUnary op = loop - where - loop ty v = - case ty of - TVBit -> evalPanic "arithUnary" ["Invalid arguments"] - TVSeq _ TVBit -> VWord (op (fromVWord v)) - TVSeq _ t -> VSeq False (map (loop t) (fromSeq v)) - TVStream t -> VStream (map (loop t) (fromSeq v)) - TVTuple ts -> VTuple (zipWith loop ts (fromVTuple v)) - TVRec fs -> VRecord [ (f, loop t (lookupRecord f v)) | (f, t) <- fs ] - TVFun _ t -> VFun (\x -> loop t (fromVFun v x)) - -sExp :: SWord -> SWord -> SWord -sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order +sExp :: Integer -> SWord -> SWord -> SWord +sExp _w x y = go (reverse (unpackWord y)) -- bits in little-endian order where go [] = literalSWord (SBV.intSizeOf x) 1 go (b : bs) = SBV.svIte b (SBV.svTimes x s) s where a = go bs s = SBV.svTimes a a -- | Ceiling (log_2 x) -sLg2 :: SWord -> SWord -sLg2 x = go 0 +sLg2 :: Integer -> SWord -> SWord +sLg2 _w x = go 0 where lit n = literalSWord (SBV.intSizeOf x) n go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1)) @@ -474,9 +401,9 @@ sLg2 x = go 0 -- Cmp ------------------------------------------------------------------------- -cmpValue :: (SBool -> SBool -> a -> a) - -> (SWord -> SWord -> a -> a) - -> (Value -> Value -> a -> a) +cmpValue :: (SBool -> SBool -> Eval a -> Eval a) + -> (SWord -> SWord -> Eval a -> Eval a) + -> (Value -> Value -> Eval a -> Eval a) cmpValue fb fw = cmp where cmp v1 v2 k = @@ -485,172 +412,44 @@ cmpValue fb fw = cmp in cmpValues (vals fs1) (vals fs2) k (VTuple vs1 , VTuple vs2 ) -> cmpValues vs1 vs2 k (VBit b1 , VBit b2 ) -> fb b1 b2 k - (VWord w1 , VWord w2 ) -> fw w1 w2 k - (VSeq _ vs1 , VSeq _ vs2 ) -> cmpValues vs1 vs2 k + (VWord _ w1 , VWord _ w2 ) -> join (fw <$> (asWordVal =<< w1) + <*> (asWordVal =<< w2) + <*> return k) + (VSeq n vs1 , VSeq _ vs2 ) -> cmpValues (enumerateSeqMap n vs1) + (enumerateSeqMap n vs2) k (VStream {} , VStream {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue" [ "Infinite streams are not comparable" ] (VFun {} , VFun {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue" [ "Functions are not comparable" ] (VPoly {} , VPoly {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue" [ "Polymorphic values are not comparable" ] - (VWord w1 , _ ) -> fw w1 (fromVWord v2) k - (_ , VWord w2 ) -> fw (fromVWord v1) w2 k (_ , _ ) -> panic "Cryptol.Symbolic.Prims.cmpValue" [ "type mismatch" ] - cmpValues (x1 : xs1) (x2 : xs2) k = cmp x1 x2 (cmpValues xs1 xs2 k) + cmpValues (x1 : xs1) (x2 : xs2) k = do + x1' <- x1 + x2' <- x2 + cmp x1' x2' (cmpValues xs1 xs2 k) cmpValues _ _ k = k -cmpEq :: SWord -> SWord -> SBool -> SBool -cmpEq x y k = SBV.svAnd (SBV.svEqual x y) k +cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool +cmpEq x y k = SBV.svAnd (SBV.svEqual x y) <$> k -cmpNotEq :: SWord -> SWord -> SBool -> SBool -cmpNotEq x y k = SBV.svOr (SBV.svNotEqual x y) k +cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool +cmpNotEq x y k = SBV.svOr (SBV.svNotEqual x y) <$> k -cmpLt, cmpGt :: SWord -> SWord -> SBool -> SBool -cmpLt x y k = SBV.svOr (SBV.svLessThan x y) (cmpEq x y k) -cmpGt x y k = SBV.svOr (SBV.svGreaterThan x y) (cmpEq x y k) +cmpLt, cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool +cmpLt x y k = SBV.svOr (SBV.svLessThan x y) <$> (cmpEq x y k) +cmpGt x y k = SBV.svOr (SBV.svGreaterThan x y) <$> (cmpEq x y k) -cmpLtEq, cmpGtEq :: SWord -> SWord -> SBool -> SBool -cmpLtEq x y k = SBV.svAnd (SBV.svLessEq x y) (cmpNotEq x y k) -cmpGtEq x y k = SBV.svAnd (SBV.svGreaterEq x y) (cmpNotEq x y k) +cmpLtEq, cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool +cmpLtEq x y k = SBV.svAnd (SBV.svLessEq x y) <$> (cmpNotEq x y k) +cmpGtEq x y k = SBV.svAnd (SBV.svGreaterEq x y) <$> (cmpNotEq x y k) -cmpBinary :: (SBool -> SBool -> SBool -> SBool) - -> (SWord -> SWord -> SBool -> SBool) - -> SBool -> Binary -cmpBinary fb fw b _ty v1 v2 = VBit (cmpValue fb fw v1 v2 b) - - --- Logic ----------------------------------------------------------------------- - -errorV :: String -> TValue -> Value -errorV msg = go - where - go ty = - case ty of - TVBit -> VBit (error msg) - TVSeq n t -> VSeq False (replicate (fromInteger n) (go t)) - TVStream t -> VStream (repeat (go t)) - TVTuple ts -> VTuple [ go t | t <- ts ] - TVRec fs -> VRecord [ (n, go t) | (n, t) <- fs ] - TVFun _ t -> VFun (const (go t)) - -zeroV :: TValue -> Value -zeroV = go - where - go ty = - case ty of - TVBit -> VBit SBV.svFalse - TVSeq n TVBit -> VWord (literalSWord (fromInteger n) 0) - TVSeq n t -> VSeq False (replicate (fromInteger n) (go t)) - TVStream t -> VStream (repeat (go t)) - TVTuple ts -> VTuple [ go t | t <- ts ] - TVRec fs -> VRecord [ (n, go t) | (n, t) <- fs ] - TVFun _ t -> VFun (const (go t)) - --- | Join a sequence of sequences into a single sequence. -joinV :: Nat' -> Nat' -> TValue -> Value -> Value -joinV parts each a v = - let len = parts `nMul` each - in toSeq len a (concatMap fromSeq (fromSeq v)) - --- | Split implementation. -ecSplitV :: Value -ecSplitV = - nlam $ \ parts -> - nlam $ \ each -> - tlam $ \ a -> - lam $ \ v -> - let mkChunks f = map (toFinSeq a) $ f $ fromSeq v - in case (parts, each) of - (Nat p, Nat e) -> VSeq False $ mkChunks (finChunksOf p e) - (Inf , Nat e) -> toStream $ mkChunks (infChunksOf e) - _ -> evalPanic "splitV" ["invalid type arguments to split"] - --- | Split into infinitely many chunks -infChunksOf :: Integer -> [a] -> [[a]] -infChunksOf each xs = let (as,bs) = genericSplitAt each xs - in as : infChunksOf each bs - --- | Split into finitely many chunks -finChunksOf :: Integer -> Integer -> [a] -> [[a]] -finChunksOf 0 _ _ = [] -finChunksOf parts each xs = let (as,bs) = genericSplitAt each xs - in as : finChunksOf (parts - 1) each bs - --- | Merge two values given a binop. This is used for and, or and xor. -logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary -logicBinary bop op = loop - where - loop ty l r = - case ty of - TVBit -> VBit (bop (fromVBit l) (fromVBit r)) - TVSeq _ TVBit -> VWord (op (fromVWord l) (fromVWord r)) - TVSeq _ t -> VSeq False (zipWith (loop t) (fromSeq l) (fromSeq r)) - TVStream t -> VStream (zipWith (loop t) (fromSeq l) (fromSeq r)) - TVTuple ts -> VTuple (zipWith3 loop ts (fromVTuple l) (fromVTuple r)) - TVRec fs -> VRecord [ (f, loop t (lookupRecord f l) (lookupRecord f r)) | (f, t) <- fs ] - TVFun _ t -> VFun (\x -> loop t (fromVFun l x) (fromVFun r x)) - -logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary -logicUnary bop op = loop - where - loop ty v = - case ty of - TVBit -> VBit (bop (fromVBit v)) - TVSeq _ TVBit -> VWord (op (fromVWord v)) - TVSeq _ t -> VSeq False (map (loop t) (fromSeq v)) - TVStream t -> VStream (map (loop t) (fromSeq v)) - TVTuple ts -> VTuple (zipWith loop ts (fromVTuple v)) - TVRec fs -> VRecord [ (f, loop t (lookupRecord f v)) | (f, t) <- fs ] - TVFun _ t -> VFun (\x -> loop t (fromVFun v x)) - --- @[ 0, 1 .. ]@ -fromThenV :: Value -fromThenV = - nlam $ \ first -> - nlam $ \ next -> - nlam $ \ bits -> - nlam $ \ len -> - case (first, next, len, bits) of - (Nat first', Nat next', Nat len', Nat bits') -> - let nums = enumFromThen first' next' - lit i = VWord (literalSWord (fromInteger bits') i) - in VSeq False (genericTake len' (map lit nums)) - _ -> evalPanic "fromThenV" ["invalid arguments"] - --- @[ 0 .. 10 ]@ -fromToV :: Value -fromToV = - nlam $ \ first -> - nlam $ \ lst -> - nlam $ \ bits -> - case (first, lst, bits) of - - (Nat first', Nat lst', Nat bits') -> - let nums = enumFromThenTo first' (first' + 1) lst' - len = 1 + (lst' - first') - lit i = VWord (literalSWord (fromInteger bits') i) - in VSeq False (genericTake len (map lit nums)) - - _ -> evalPanic "fromThenV" ["invalid arguments"] - --- @[ 0, 1 .. 10 ]@ -fromThenToV :: Value -fromThenToV = - nlam $ \ first -> - nlam $ \ next -> - nlam $ \ lst -> - nlam $ \ bits -> - nlam $ \ len -> - case (first, next, lst, len, bits) of - - (Nat first', Nat next', Nat lst', Nat len', Nat bits') -> - let nums = enumFromThenTo first' next' lst' - lit i = VWord (literalSWord (fromInteger bits') i) - in VSeq False (genericTake len' (map lit nums)) - - _ -> evalPanic "fromThenV" ["invalid arguments"] +cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool) + -> (SWord -> SWord -> Eval SBool -> Eval SBool) + -> SBool -> Binary SBool SWord +cmpBinary fb fw b _ty v1 v2 = VBit <$> cmpValue fb fw v1 v2 (return b) -- Polynomials ----------------------------------------------------------------- @@ -696,6 +495,7 @@ mdp xs ys = go (length ys - 1) (reverse ys) ys' = replicate degQuot SBV.svFalse ++ ys (qs, rs) = divx (degQuot+1) degTop xs ys' + -- return the element at index i; if not enough elements, return false -- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient idx :: [SBool] -> Int -> SBool diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs index 4beb2576..fecde8d6 100644 --- a/src/Cryptol/Symbolic/Value.hs +++ b/src/Cryptol/Symbolic/Value.hs @@ -9,6 +9,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternGuards #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Cryptol.Symbolic.Value @@ -18,25 +19,29 @@ module Cryptol.Symbolic.Value , forallBV_, existsBV_ , forallSBool_, existsSBool_ , Value - , TValue(..), isTBit, tvSeq - , GenValue(..), lam, tlam, nlam, toStream, toFinSeq, toSeq, finNat' - , fromVBit, fromVFun, fromVPoly, fromVNumPoly, fromVTuple, fromVRecord - , lookupRecord + , TValue, isTBit, tvSeq + , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq + , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord , fromSeq, fromVWord , evalPanic - , iteValue, mergeValue + , iteSValue, mergeValue, mergeWord ) where import Data.List (foldl') +import qualified Data.Sequence as Seq import Data.SBV.Dynamic -import Cryptol.Eval.Value (TValue(..), isTBit, tvSeq, finNat', GenValue(..), - BitWord(..), lam, tlam, nlam, toStream, toFinSeq, toSeq, +--import Cryptol.Eval.Monad +import Cryptol.Eval.Type (TValue(..), isTBit, tvSeq) +import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream, + toFinSeq, toSeq, WordValue(..), asWordVal, asBitsVal, fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly, - fromVNumPoly, fromVTuple, fromVRecord, lookupRecord) + fromVTuple, fromVRecord, lookupRecord, SeqMap(..), + ppBV,BV(..),integerToChar) import Cryptol.Utils.Panic (panic) +import Cryptol.Utils.PP -- SBool and SWord ------------------------------------------------------------- @@ -68,44 +73,85 @@ type Value = GenValue SBool SWord -- Symbolic Conditionals ------------------------------------------------------- -iteValue :: SBool -> Value -> Value -> Value -iteValue c x y = +iteSValue :: SBool -> Value -> Value -> Value +iteSValue c x y = case svAsBool c of Just True -> x Just False -> y Nothing -> mergeValue True c x y +mergeBit :: Bool + -> SBool + -> SBool + -> SBool + -> SBool +mergeBit f c b1 b2 = svSymbolicMerge KBool f c b1 b2 + +mergeWord :: Bool + -> SBool + -> WordValue SBool SWord + -> WordValue SBool SWord + -> WordValue SBool SWord +mergeWord f c (WordVal w1) (WordVal w2) = + WordVal $ svSymbolicMerge (kindOf w1) f c w1 w2 +mergeWord f c w1 w2 = + BitsVal $ Seq.zipWith mergeBit' (asBitsVal w1) (asBitsVal w2) + where mergeBit' b1 b2 = mergeBit f c <$> b1 <*> b2 + mergeValue :: Bool -> SBool -> Value -> Value -> Value mergeValue f c v1 v2 = case (v1, v2) of (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2 - (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (mergeValue f c) vs1 vs2 - (VBit b1 , VBit b2 ) -> VBit $ mergeBit b1 b2 - (VWord w1 , VWord w2 ) -> VWord $ mergeWord w1 w2 - (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ zipWith (mergeValue f c) vs1 vs2 - (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2 - (VFun f1 , VFun f2 ) -> VFun $ \x -> mergeValue f c (f1 x) (f2 x) - (VPoly f1 , VPoly f2 ) -> VPoly $ \x -> mergeValue f c (f1 x) (f2 x) - (VWord w1 , _ ) -> VWord $ mergeWord w1 (fromVWord v2) - (_ , VWord w2 ) -> VWord $ mergeWord (fromVWord v1) w2 + (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (\x y -> mergeValue f c <$> x <*> y) vs1 vs2 + (VBit b1 , VBit b2 ) -> VBit $ mergeBit f c b1 b2 + (VWord n1 w1, VWord n2 w2 ) | n1 == n2 -> VWord n1 (mergeWord f c <$> w1 <*> w2) + (VSeq n1 vs1, VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 $ mergeSeqMap vs1 vs2 + (VStream vs1, VStream vs2) -> VStream $ mergeSeqMap vs1 vs2 + (VFun f1 , VFun f2 ) -> VFun $ \x -> mergeValue f c <$> (f1 x) <*> (f2 x) + (VPoly f1 , VPoly f2 ) -> VPoly $ \x -> mergeValue f c <$> (f1 x) <*> (f2 x) (_ , _ ) -> panic "Cryptol.Symbolic.Value" [ "mergeValue: incompatible values" ] where - mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2 - mergeWord w1 w2 = svSymbolicMerge (kindOf w1) f c w1 w2 mergeField (n1, x1) (n2, x2) - | n1 == n2 = (n1, mergeValue f c x1 x2) + | n1 == n2 = (n1, mergeValue f c <$> x1 <*> x2) | otherwise = panic "Cryptol.Symbolic.Value" [ "mergeValue.mergeField: incompatible values" ] - mergeStream xs ys = - mergeValue f c (head xs) (head ys) : mergeStream (tail xs) (tail ys) + mergeSeqMap x y = + SeqMap $ \i -> mergeValue f c <$> lookupSeqMap x i <*> lookupSeqMap y i --- Big-endian Words ------------------------------------------------------------ +-- Symbolic Big-endian Words ------------------------------------------------------- instance BitWord SBool SWord where + wordLen v = toInteger (intSizeOf v) + wordAsChar v = integerToChar <$> svAsInteger v + + ppBit v + | Just b <- svAsBool v = text $! if b then "True" else "False" + | otherwise = text "?" + ppWord opts v + | Just x <- svAsInteger v = ppBV opts (BV (wordLen v) x) + | otherwise = text "[?]" + + bitLit b = svBool b + wordLit n x = svInteger (KBounded False (fromInteger n)) x + packWord bs = fromBitsLE (reverse bs) unpackWord x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ] + joinWord x y = svJoin x y + + splitWord _leftW rightW w = + ( svExtract (intSizeOf w - 1) (fromInteger rightW) w + , svExtract (fromInteger rightW - 1) 0 w + ) + + extractWord len start w = + svExtract (fromInteger start + fromInteger len - 1) (fromInteger start) w + + wordPlus = svPlus + wordMinus = svMinus + wordMult = svTimes + -- Errors ---------------------------------------------------------------------- evalPanic :: String -> [String] -> a diff --git a/src/Cryptol/Testing/Concrete.hs b/src/Cryptol/Testing/Concrete.hs index 81bdc8e0..12fb4193 100644 --- a/src/Cryptol/Testing/Concrete.hs +++ b/src/Cryptol/Testing/Concrete.hs @@ -9,7 +9,9 @@ {-# LANGUAGE RecordWildCards #-} module Cryptol.Testing.Concrete where -import Cryptol.Eval.Error +import Control.Monad (join) + +import Cryptol.Eval.Monad import Cryptol.Eval.Value import Cryptol.TypeCheck.AST import Cryptol.Utils.Panic (panic) @@ -19,6 +21,7 @@ import Data.List(genericReplicate) import Prelude () import Prelude.Compat +import Data.List (genericIndex) -- | A test result is either a pass, a failure due to evaluating to -- @False@, or a failure due to an exception raised during evaluation @@ -39,22 +42,24 @@ runOneTest :: Value -> [Value] -> IO TestResult runOneTest v0 vs0 = run `X.catch` handle where run = do - result <- X.evaluate (go v0 vs0) + result <- runEval (go v0 vs0) if result then return Pass else return (FailFalse vs0) handle e = return (FailError e vs0) - go :: Value -> [Value] -> Bool - go (VFun f) (v : vs) = go (f v) vs + go :: Value -> [Value] -> Eval Bool + go (VFun f) (v : vs) = join (go <$> (f (ready v)) <*> return vs) go (VFun _) [] = panic "Not enough arguments while applying function" [] - go (VBit b) [] = b - go v vs = panic "Type error while running test" $ - [ "Function:" - , show $ ppValue defaultPPOpts v - , "Arguments:" - ] ++ map (show . ppValue defaultPPOpts) vs + go (VBit b) [] = return b + go v vs = do vdoc <- ppValue defaultPPOpts v + vsdocs <- mapM (ppValue defaultPPOpts) vs + panic "Type error while running test" $ + [ "Function:" + , show vdoc + , "Arguments:" + ] ++ map show vsdocs {- | Given a (function) type, compute all possible inputs for it. We also return the total number of test (i.e., the length of the outer list. -} @@ -102,7 +107,7 @@ typeValues ty = TVar _ -> [] TUser _ _ t -> typeValues t TRec fs -> [ VRecord xs - | xs <- sequence [ [ (f,v) | v <- typeValues t ] + | xs <- sequence [ [ (f,ready v) | v <- typeValues t ] | (f,t) <- fs ] ] TCon (TC tc) ts -> @@ -113,16 +118,19 @@ typeValues ty = (TCSeq, ts1) -> case map tNoUser ts1 of [ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] -> - [ VWord (BV n x) | x <- [ 0 .. 2^n - 1 ] ] + [ VWord n (ready (WordVal (BV n x))) | x <- [ 0 .. 2^n - 1 ] ] [ TCon (TC (TCNum n)) _, t ] -> - [ VSeq False xs | xs <- sequence $ genericReplicate n - $ typeValues t ] + [ VSeq n (SeqMap $ \i -> return $ genericIndex xs i) + | xs <- sequence $ genericReplicate n + $ typeValues t ] _ -> [] (TCFun, _) -> [] -- We don't generate function values. - (TCTuple _, els) -> [ VTuple xs | xs <- sequence (map typeValues els)] + (TCTuple _, els) -> [ VTuple (map ready xs) + | xs <- sequence (map typeValues els) + ] (TCNewtype _, _) -> [] TCon _ _ -> [] diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index c8b4790b..c3a9c37e 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -11,7 +11,8 @@ {-# LANGUAGE BangPatterns #-} module Cryptol.Testing.Random where -import Cryptol.Eval.Value (BV(..),Value,GenValue(..)) +import Cryptol.Eval.Monad (ready) +import Cryptol.Eval.Value (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..)) import qualified Cryptol.Testing.Concrete as Conc import Cryptol.TypeCheck.AST (Type(..),TCon(..),TC(..),tNoUser) import Cryptol.TypeCheck.Solve(simpType) @@ -19,8 +20,9 @@ import Cryptol.TypeCheck.Solve(simpType) import Cryptol.Utils.Ident (Ident) import Control.Monad (forM) -import Data.List (unfoldr, genericTake) +import Data.List (unfoldr, genericTake, genericIndex) import System.Random (RandomGen, split, random, randomR) +import qualified Data.Sequence as Seq type Gen g = Integer -> g -> (Value, g) @@ -102,21 +104,24 @@ randomBit _ g = randomWord :: RandomGen g => Integer -> Gen g randomWord w _sz g = let (val, g1) = randomR (0,2^w-1) g - in (VWord (BV w val), g1) + in (VWord w (ready (WordVal (BV w val))), g1) -- | Generate a random infinite stream value. randomStream :: RandomGen g => Gen g -> Gen g randomStream mkElem sz g = let (g1,g2) = split g - in (VStream (unfoldr (Just . mkElem sz) g1), g2) + in (VStream $ SeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2) {- | Generate a random sequence. Generally, this should be used for sequences other than bits. For sequences of bits use "randomWord". The difference is mostly about how the results will be displayed. -} randomSequence :: RandomGen g => Integer -> Gen g -> Gen g -randomSequence w mkElem sz g = +randomSequence w mkElem sz g = do let (g1,g2) = split g - in (VSeq False $ genericTake w $ unfoldr (Just . mkElem sz) g1 , g2) + let f g = let (x,g') = mkElem sz g + in seq x (Just (ready x, g')) + let xs = Seq.fromList $ genericTake w $ unfoldr f g1 + seq xs (VSeq w $ SeqMap $ (Seq.index xs . fromInteger), g2) -- | Generate a random tuple value. randomTuple :: RandomGen g => [Gen g] -> Gen g @@ -125,7 +130,7 @@ randomTuple gens sz = go [] gens go els [] g = (VTuple (reverse els), g) go els (mkElem : more) g = let (v, g1) = mkElem sz g - in go (v : els) more g1 + in seq v (go (ready v : els) more g1) -- | Generate a random record value. randomRecord :: RandomGen g => [(Ident, Gen g)] -> Gen g @@ -134,7 +139,7 @@ randomRecord gens sz = go [] gens go els [] g = (VRecord (reverse els), g) go els ((l,mkElem) : more) g = let (v, g1) = mkElem sz g - in go ((l,v) : els) more g1 + in seq v (go ((l,ready v) : els) more g1) {- test = do diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index 35be0d67..d25d07d5 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -185,7 +185,7 @@ rewE rews = go ESel e s -> ESel <$> go e <*> return s EIf e1 e2 e3 -> EIf <$> go e1 <*> go e2 <*> go e3 - EComp t e mss -> EComp t <$> go e <*> mapM (mapM (rewM rews)) mss + EComp len t e mss -> EComp len t <$> go e <*> mapM (mapM (rewM rews)) mss EVar _ -> return expr ETAbs x e -> ETAbs x <$> go e @@ -203,7 +203,7 @@ rewE rews = go rewM :: RewMap -> Match -> M Match rewM rews ma = case ma of - From x t e -> From x t <$> rewE rews e + From x len t e -> From x len t <$> rewE rews e -- These are not recursive. Let d -> Let <$> rewD rews d diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs index 0cadac08..2a44d51e 100644 --- a/src/Cryptol/Transform/Specialize.hs +++ b/src/Cryptol/Transform/Specialize.hs @@ -78,7 +78,7 @@ specializeExpr expr = ERec fs -> ERec <$> traverse (traverseSnd specializeExpr) fs ESel e s -> ESel <$> specializeExpr e <*> pure s EIf e1 e2 e3 -> EIf <$> specializeExpr e1 <*> specializeExpr e2 <*> specializeExpr e3 - EComp t e mss -> EComp t <$> specializeExpr e <*> traverse (traverse specializeMatch) mss + EComp len t e mss -> EComp len t <$> specializeExpr e <*> traverse (traverse specializeMatch) mss -- Bindings within list comprehensions always have monomorphic types. EVar {} -> specializeConst expr ETAbs t e -> do @@ -104,7 +104,7 @@ specializeExpr expr = EWhere e dgs -> specializeEWhere e dgs specializeMatch :: Match -> SpecM Match -specializeMatch (From qn t e) = From qn t <$> specializeExpr e +specializeMatch (From qn l t e) = From qn l t <$> specializeExpr e specializeMatch (Let decl) | null (sVars (dSignature decl)) = return (Let decl) | otherwise = fail "unimplemented: specializeMatch Let unimplemented" diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 0955542d..59c6789b 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -192,9 +192,10 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements) | ESel Expr Selector -- ^ Elimination for tuple/record/list | EIf Expr Expr Expr -- ^ If-then-else - | EComp Type Expr [[Match]] -- ^ List comprehensions - -- The type caches the type of the - -- expr. + | EComp Type Type Expr [[Match]] + -- ^ List comprehensions + -- The types caches the length of the + -- sequence and type of the expr. | EVar Name -- ^ Use of a bound variable @@ -244,8 +245,9 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements) deriving (Show, Generic, NFData) -data Match = From Name Type Expr -- ^ do we need this type? it seems like it - -- can be computed from the expr +data Match = From Name Type Type Expr + -- ^ Type arguments are the length and element + -- type of the sequence expression | Let Decl deriving (Show, Generic, NFData) @@ -792,8 +794,8 @@ instance PP (WithNames Expr) where , text "then" <+> ppW e2 , text "else" <+> ppW e3 ] - EComp _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms) - in brackets $ ppW e <+> vcat (map arm mss) + EComp _ _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms) + in brackets $ ppW e <+> vcat (map arm mss) EVar x -> ppPrefixName x @@ -882,7 +884,7 @@ instance PP Expr where instance PP (WithNames Match) where ppPrec _ (WithNames mat nm) = case mat of - From x _ e -> pp x <+> text "<-" <+> ppWithNames nm e + From x _ _ e -> pp x <+> text "<-" <+> ppWithNames nm e Let d -> text "let" <+> ppWithNames nm d instance PP Match where diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index f7d6c593..350d6557 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -272,7 +272,7 @@ checkE expr tGoal = ds <- combineMaps dss e' <- withMonoTypes ds (checkE e a) - return (EComp tGoal e' mss') + return (EComp len a e' mss') P.EAppT e fs -> do ts <- mapM inferTyParam fs @@ -520,7 +520,7 @@ inferMatch (P.Match p e) = do (x,t) <- inferP (text "XXX:MATCH") p n <- newType (text "sequence length of comprehension match") KNum e' <- checkE e (tSeq n (thing t)) - return (From x (thing t) e', x, t, n) + return (From x n (thing t) e', x, t, n) inferMatch (P.MatchLet b) | P.bMono b = diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index 07cf36d6..5f656e0c 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -313,26 +313,26 @@ instance TVars DelayedCt where | Set.null captured = DelayedCt { dctSource = dctSource g , dctForall = dctForall g - , dctAsmps = apSubst su1 (dctAsmps g) - , dctGoals = apSubst su1 (dctGoals g) + , dctAsmps = apSubst su (dctAsmps g) + , dctGoals = apSubst su (dctGoals g) } + | otherwise = panic "Cryptol.TypeCheck.Subst.apSubst (DelayedCt)" [ "Captured quantified variables:" - , "Substitution: " ++ show m1 + , "Substitution: " ++ show su , "Variables: " ++ show captured , "Constraint: " ++ show g ] where - used = fvs (dctAsmps g, map goal (dctGoals g)) `Set.difference` - Set.fromList (map tpVar (dctForall g)) - m1 = Map.filterWithKey (\k _ -> k `Set.member` used) (suMap su) - su1 = S { suMap = m1, suDefaulting = suDefaulting su } - - captured = Set.fromList (map tpVar (dctForall g)) `Set.intersection` - fvs (Map.elems m1) - - + captured = Set.fromList (map tpVar (dctForall g)) + `Set.intersection` + subVars + subVars = Set.unions + $ map (fvs . applySubstToVar su) + $ Set.toList used + used = fvs (dctAsmps g, map goal (dctGoals g)) `Set.difference` + Set.fromList (map tpVar (dctForall g)) -- | For use in error messages cppKind :: Kind -> Doc diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index 3e0993e7..0a0671cb 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -229,8 +229,9 @@ exprSchema expr = return $ tMono t1 - EComp t e mss -> - do checkTypeIs KType t + EComp len t e mss -> + do checkTypeIs KNum len + checkTypeIs KType t (xs,ls) <- unzip `fmap` mapM checkArm mss -- XXX: check no duplicates @@ -238,7 +239,7 @@ exprSchema expr = case ls of [] -> return () - _ -> convertible t (tSeq (foldr1 tMin ls) elT) + _ -> convertible (tSeq len t) (tSeq (foldr1 tMin ls) elT) return (tMono t) @@ -390,8 +391,10 @@ checkDeclGroup dg = checkMatch :: Match -> TcM ((Name, Schema), Type) checkMatch ma = case ma of - From x t e -> - do checkTypeIs KType t + From x len elt e -> + do checkTypeIs KNum len + checkTypeIs KType elt + let t = tSeq len elt t1 <- exprType e case tNoUser t1 of TCon (TC TCSeq) [ l, el ] diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index 0a6efe16..ee4cb413 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -24,9 +24,9 @@ import Cryptol.TypeCheck.PP(pp) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Subst - (apSubst,fvs,singleSubst,substToList, isEmptySubst, + (apSubst,fvs,singleSubst, isEmptySubst, emptySubst,Subst,listSubst, (@@), Subst, - apSubstMaybe) + apSubstMaybe, substBinds) import Cryptol.TypeCheck.Solver.Class import Cryptol.TypeCheck.Solver.Selector(tryHasGoal) import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num @@ -452,7 +452,7 @@ improveByDefaultingWith s as ps = ] newSu = su1 @@ su -- XXX: is that right? - names = Set.fromList $ map fst $ fromMaybe [] $ substToList newSu + names = substBinds newSu in return ( [ a | a <- as, not (a `Set.member` names) ] , gs1 diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs index d65950ae..c22db367 100644 --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -11,9 +11,26 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Safe #-} -module Cryptol.TypeCheck.Subst where +module Cryptol.TypeCheck.Subst + ( Subst + , emptySubst + , singleSubst + , (@@) + , defaultingSubst + , listSubst + , isEmptySubst + , FVS(..) + , apSubstMaybe + , TVars(..) + , apSubstTypeMapKeys + , substVars + , substBinds + , applySubstToVar + ) where +import Data.Maybe import Data.Either (partitionEithers) +import qualified Data.Foldable as Fold import qualified Data.Map.Strict as Map import qualified Data.IntMap as IntMap import Data.Set (Set) @@ -42,11 +59,13 @@ s2 @@ s1 | Map.null (suMap s2) = s1 else s1{ suDefaulting = True } - -s2 @@ s1 = S { suMap = Map.map (apSubst s2) (suMap s1) `Map.union` suMap s2 +s2 @@ s1 = S { suMap = Map.map (apSubst s2) (suMap s1) `Map.union` (suMap s2) , suDefaulting = suDefaulting s1 || suDefaulting s2 } +substVars :: Subst -> Set TVar +substVars su = fvs . Map.elems $ suMap su + defaultingSubst :: Subst -> Subst defaultingSubst s = s { suDefaulting = True } @@ -54,16 +73,18 @@ defaultingSubst s = s { suDefaulting = True } -- WARNING: We do not validate the list in any way, so the caller should -- ensure that we end up with a valid (e.g., idempotent) substitution. listSubst :: [(TVar,Type)] -> Subst -listSubst xs = S { suMap = Map.fromList xs, suDefaulting = False } +listSubst xs + | null xs = emptySubst + | otherwise = S { suMap = Map.fromList xs, suDefaulting = False } isEmptySubst :: Subst -> Bool -isEmptySubst su = Map.null (suMap su) - --- Returns `Nothing` if this is a deaulting substitution -substToList :: Subst -> Maybe [ (TVar, Type) ] -substToList su | suDefaulting su = Nothing - | otherwise = Just $ Map.toList $ suMap su +isEmptySubst su = Map.null $ suMap su +-- Returns the empty set if this is a deaulting substitution +substBinds :: Subst -> Set TVar +substBinds su + | suDefaulting su = Set.empty + | otherwise = Map.keysSet $ suMap su instance PP (WithNames Subst) where ppPrec _ (WithNames s mp) @@ -91,6 +112,10 @@ instance FVS Type where TUser _ _ t -> go t TRec fs -> Set.unions (map (go . snd) fs) +instance FVS a => FVS (Maybe a) where + fvs Nothing = Set.empty + fvs (Just x) = fvs x + instance FVS a => FVS [a] where fvs xs = Set.unions (map fvs xs) @@ -113,18 +138,16 @@ apSubstMaybe su ty = TRec fs -> TRec `fmap` anyJust fld fs where fld (x,t) = do t1 <- apSubstMaybe su t return (x,t1) - TVar x -> - case Map.lookup x (suMap su) of - Just t -> Just $ if suDefaulting su - then apSubst (defaultingSubst emptySubst) t - else t - Nothing -> if suDefaulting su - then Just (defaultFreeVar x) - else Nothing - - + TVar x -> applySubstToVar su x +applySubstToVar :: Subst -> TVar -> Maybe Type +applySubstToVar su x = + case Map.lookup x (suMap su) of + Just t -> Just t + Nothing + | suDefaulting su -> Just $! defaultFreeVar x + | otherwise -> Nothing class TVars t where apSubst :: Subst -> t -> t -- ^ replaces free vars @@ -144,13 +167,7 @@ instance TVars Type where TCon t ts -> TCon t (apSubst su ts) TUser f ts t -> TUser f (apSubst su ts) (apSubst su t) TRec fs -> TRec [ (x,apSubst su s) | (x,s) <- fs ] - TVar x - | Just t <- Map.lookup x (suMap su) -> - if suDefaulting su - then apSubst (defaultingSubst emptySubst) t - else t - | suDefaulting su -> defaultFreeVar x - | otherwise -> ty + TVar x -> fromMaybe ty $ applySubstToVar su x -- | Pick types for unconstrained unification variables. defaultFreeVar :: TVar -> Type @@ -188,7 +205,7 @@ apSubstTypeMapKeys su = go (\_ x -> x) id -- partition out variables that have been replaced with more specific types (vars,tys) = partitionEithers - [ case Map.lookup v (suMap su) of + [ case applySubstToVar su v of Just ty -> Right (ty,a') Nothing -> Left (v, a') @@ -212,21 +229,23 @@ capture did occur. -} instance TVars Schema where apSubst su sch@(Forall xs ps t) - | Set.null captured = Forall xs (apSubst su1 ps) (apSubst su1 t) + | Set.null captured = Forall xs (apSubst su ps) (apSubst su t) | otherwise = panic "Cryptol.TypeCheck.Subst.apSubst (Schema)" [ "Captured quantified variables:" - , "Substitution: " ++ show (brackets (commaSep (map ppBinding $ Map.toList m1))) + , "Substitution: " ++ show (brackets (commaSep (map ppBinding su_binds))) , "Schema: " ++ show (pp sch) , "Variables: " ++ show (commaSep (map pp (Set.toList captured))) ] where ppBinding (v,x) = pp v <+> text ":=" <+> pp x + captured = Set.fromList (map tpVar xs) + `Set.intersection` + subVars + su_binds = Map.toList $ suMap su used = fvs sch - m1 = Map.filterWithKey (\k _ -> k `Set.member` used) (suMap su) - su1 = S { suMap = m1, suDefaulting = suDefaulting su } - - captured = Set.fromList (map tpVar xs) `Set.intersection` - fvs (Map.elems m1) + subVars = Set.unions + $ map (fvs . applySubstToVar su) + $ Set.toList used instance TVars Expr where @@ -248,13 +267,13 @@ instance TVars Expr where ERec fs -> ERec [ (f, go e) | (f,e) <- fs ] EList es t -> EList (map go es) (apSubst su t) ESel e s -> ESel (go e) s - EComp t e mss -> EComp (apSubst su t) (go e) (apSubst su mss) + EComp len t e mss -> EComp (apSubst su len) (apSubst su t) (go e) (apSubst su mss) EIf e1 e2 e3 -> EIf (go e1) (go e2) (go e3) EWhere e ds -> EWhere (go e) (apSubst su ds) instance TVars Match where - apSubst su (From x t e) = From x (apSubst su t) (apSubst su e) + apSubst su (From x len t e) = From x (apSubst su len) (apSubst su t) (apSubst su e) apSubst su (Let b) = Let (apSubst su b) instance TVars DeclGroup where diff --git a/src/Cryptol/TypeCheck/TypeOf.hs b/src/Cryptol/TypeCheck/TypeOf.hs index 8862b37d..45e4faae 100644 --- a/src/Cryptol/TypeCheck/TypeOf.hs +++ b/src/Cryptol/TypeCheck/TypeOf.hs @@ -34,7 +34,7 @@ fastTypeOf tyenv expr = ERec fields -> tRec [ (name, fastTypeOf tyenv e) | (name, e) <- fields ] ESel e sel -> typeSelect (fastTypeOf tyenv e) sel EIf _ e _ -> fastTypeOf tyenv e - EComp t _ _ -> t + EComp len t _ _ -> tSeq len t EAbs x t e -> tFun t (fastTypeOf (Map.insert x (Forall [] [] t) tyenv) e) EApp e _ -> case tIsFun (fastTypeOf tyenv e) of Just (_, t) -> t diff --git a/tests/issues/issue148.icry.stdout b/tests/issues/issue148.icry.stdout index 07b44e74..36ceed49 100644 --- a/tests/issues/issue148.icry.stdout +++ b/tests/issues/issue148.icry.stdout @@ -5,12 +5,12 @@ Loading module Main Defaulting type parameter 'bits' of literal or demoted expression at ./issue148.cry:4:34--4:35 - to max 2 (width a`190) + to max 2 (width a`203) [warning] at ./issue148.cry:2:1--9:10: Defaulting 2nd type parameter of expression take at ./issue148.cry:6:10--6:14 - to 16 * a`190 + to 16 * a`203 [warning] at :1:1--1:36: Defaulting type parameter 'bits' of finite enumeration diff --git a/tests/issues/issue198.icry.stdout b/tests/issues/issue198.icry.stdout index 3c34588f..55ca23ed 100644 --- a/tests/issues/issue198.icry.stdout +++ b/tests/issues/issue198.icry.stdout @@ -5,15 +5,15 @@ Loading module Main Defaulting type parameter 'bits' of literal or demoted expression at ./simon.cry2:87:34--87:35 - to max 3 (width a`566) + to max 3 (width a`579) [warning] at ./simon.cry2:83:1--92:15: Defaulting type parameter 'bits' of literal or demoted expression at ./simon.cry2:90:29--90:31 - to width a`568 + to width a`581 [warning] at ./simon.cry2:83:1--92:15: Defaulting type parameter 'bits' of literal or demoted expression at ./simon.cry2:89:36--89:38 - to max 6 (max (width a`566) (width (a`567 - 1))) + to max 6 (max (width a`579) (width (a`580 - 1))) True diff --git a/tests/issues/issue214.icry.stdout b/tests/issues/issue214.icry.stdout index a706b39e..38314555 100644 --- a/tests/issues/issue214.icry.stdout +++ b/tests/issues/issue214.icry.stdout @@ -5,9 +5,9 @@ Loading module Main Defaulting type parameter 'bits' of finite enumeration at ./issue214.cry:2:14--2:26 - to max 2 (width (2 * a`190 - 2)) + to max 2 (width (2 * a`203 - 2)) [warning] at ./issue214.cry:2:1--2:49: Defaulting type parameter 'bits' of finite enumeration at ./issue214.cry:2:36--2:48 - to max 2 (width (2 * a`190 - 1)) + to max 2 (width (2 * a`203 - 1)) diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index e5921b1c..4edc9041 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -79,6 +79,8 @@ Symbols tail : {a, b} [1 + a]b -> [a]b take : {front, back, elem} (fin front) => [front + back]elem -> [front]elem + trace : {n, a, b} [n][8] -> a -> b -> b + traceVal : {n, a} [n][8] -> a -> a transpose : {a, b, c} [a][b]c -> [b][a]c undefined : {a} a width : {bits, len, elem} (fin len, fin bits, diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 7635eddf..f33f24b1 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,7 +4,7 @@ Loading module Main [error] at ./issue290v2.cry:2:1--2:19: Unsolved constraint: - a`190 == 1 + a`203 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at ./issue290v2.cry:2:8--2:11