mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-11 07:00:49 +03:00
Merge pull request #338 from robdockins/new-eval
New monadic evaluator, now with fewer nontermination bugs!
This commit is contained in:
robdockins
GitHub
commit
93a1628d53
@ -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)
|
||||
|
||||
@ -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
|
||||
where key = 0x3243f6a8885a308d313198a2e0370734
|
||||
|
||||
bench_data : [128 * nblocks]
|
||||
bench_data = //random 0
|
||||
0xcddf97f18ad18da94ae27558e975608f673c896a718cffbc90c746160a003d540e353ea1a32cf650c25298cf353b36849f68360e07ad40a9e6c0e4dd2351dce8c06dd82c27642a5e9ce3804780d531af41768b4697b45383d58dfd98c9f2e6d5788e671229529d239b40fc9a52436c437e716cef3c5503d567eff3c2f35d806ae4431455ec096526b1b584cb4a80efde3174361e912a46bf8b7b8d3ca4cebacea935ccd766976614885f5330441ca4acee37c9728fb53708042d9952d8ef3ca544c870a7ee689f8b6d78764368e849274946d0e8bdc69f4a4004cbbce034f1d0a6f8447a756a5f9c217e377909d0c4bde859732e7263c03013c623cb1f2478b77f7838b3d3581e0aba9da951dd18466a131bca89252fc17b9bbe475530d425ac7a79cbc26a941dcc16ded680dddada735c76fa469ebeadf1c8fc33a2c7dc00b865eaec95f1448583425302a9023d39c3bb794685a5e30f196f7c0bdc2b8790d35f8bb9c4359e17ca53e8450da4db030bb67fb4cab68ef4a5edfbe120f1c9824b4faa0cc767bb7304238a798534f065cc1cc8fe310d76c2b440b64348a8e16873eddb5931313573c2cb43a47c2ff0f9c8ec264a0a6ec6474c1056fc7f376c01e5d3b6fea382b5086c7c80bb4c5505f2d4f18dc01cff4baa71eac658ca78e5acbde546dbe85dd71708fb46c8ec00ef75b9b577f93a3c550781a642d5bc4fa2da325656f737d272875b9185fe86a0e0e3eefaf51294d0f06340db93715c99df443e286c0d1e2ae869a7e0d705d6369362a220617ac4803fd205de679ea6ed82881cc2315d73c9cc8f4512ee61afaf127eac098d1d31b075c16aa902024594337c6b2a290cedcbd44190105d20de7ef16fb310400ccbc9ca6a1f4de0a9b1f82b780ee3eda52af664b883c32dd70c860905c0f9e83ee0ae5fc016b81c4c4ca70c05703035637e4988a827bf6e230ba30dc78b8c5663e14273827fb6c4aa700b95a04f1456ce15d18740ee79b7aeb85feffac9f5bd54c9a9bd494a9fc8fab4280316ac8f6552849a798e2b5d7326bb2208fdf2cf6b372311edcd87bb2b1805afd1b6e085fad1a28bc4578e1abea57227f49c141d7d08893d8083249e32cc9645748684cc5d4d492abbdaf5f8373b5e2e4bd91c15346e1d455415395bc0342185665ebeb94fda5fdf7e601961bf1f1109373e935a077a0088980844ce1c87f347380f3c805b01407cf9154f5818db41a6f5d87994df790421a9dbf7d56c11a5e723ec853f32bcf7dc0eef03bbf164564167c6212c35ddd9d6112eb43e4826d1da8f065b804fd48b5ff863b4f4246ba6ebaef90396843e084168d6826abf5f6b0e82c7a7a96707e650e86f82862c5910e0c4d6a48182656e0e76be4017c739feb2da56bb69db4b0885c772180607ce880b15064b5b9878cd1c3d4ae9657c5fdf5ca5d7755807d74e2a57aed4e9fe90c49ed4f01ae3cb812ada6b15c7009d98930d8a41cf23e8f5a962e93c8cecef6044cfcc8843d1f6b5dfb868de036fa5d992c861f056f504f54e8d077028143a2807676c02faf35435ee43cb1ece1a82c7f142be774c824b7e8e3fcad737f58f4818994842ab40a211f9569ad476beef0f2f97be0fb515cf0754641748b2af38d58937c3428a147647911734d54bf06be7f3fcab19b874ff52893af6a45c44adf11c17bf177fc0e90539327373e6594e249aca3a386272d1405455e7e8b463029c0460a31b59b9dc1a15d18cdf1997df250721735651c5e7de7059cb755aa4a0c99962e6485b2ccb02ffecb022fc867e36a63ef77ee8740af2e6f25b0d497d3bcc213a939a47a64057caf107e79661d15f469f8e32b2175bed98af21776a9a2cde4e4982ecd695b4dcef8822806cf74ac73aa5b9d8e6dc0a6d2b97b75d11553a9478296631b7a3c340113247f32bf7a7c42e85b9e517b4f9a09ab453de795f156f09d2704bfa56f5ade38e0eae826796bd54165967332985ecdd4991b8e2bb4016e0d2da173690feace03245c2ef868b44ea7892c0ce15d818a32e5bf57d53a1d86cbb3074221083cfa570c17104da26c063b3a349ce35facd3b7bf267383235a5620217d58201c74105302f3445e024313338fe93dd6f617088b41c836083ceae512782e458c4f5c74bd1987ccb098d1d89fe63a5e5881e56b0c5aba87ef2c5e8d6333d91e9dcbdc45a3c16d67b32c4e51e95231aa7e0b9342c599ebdc6ebb6e4dce1fcd98add42d6ab08707a6f5a38154ad5a3674e8a05105c5ecec180f9661122da31a94e9ad7d337ff5ab4a28a5c5cba9a393f484ed5e5f37bbb4b7caecbf9cbb432cae0b2f6bd5ce6068104f012d6428a9b172847e18f12708de6248cdf0401c865292645fb30114f4f4b53d4473b6ffc53ae0870e85c24f631f52c04d227ea9bc0a59828b6f9eafd95cac13ccfb1cdbae3550b0cd99e1812346d5d01b5a782d1d50fbedf858a4a044fd9384e3a6c10cb4227e276c7399b897b9dcbd2a5cb4e14d8341dd32029938f444fa3dcf2d23198f6bf042439cf96a534f3041774a6c3d5b6bb5bfcd8d7af57402431c7dd758da93ccef39495977cece58087ecc80b278d3e9966b7bd8b183f0379f28aa3c9a885065b8a090f3af15a15acb553b36a73d25a581e7f54f5e1f6f49c4f638ce40ba67629e910a04444d5f6b66c4548b611f851feb08d64fa4d99b83ad218d182d0e86e7f87d4923599a547effed6b9c86e853aef9e60767bff33de916bd799eaf3922ae80abadcc91c95f47e702e2fbd2631d0b77ef85f092204141250c4162b0369be64c1d6bdc2d58c02981cc1de13ae3efba34fbfb3dd0ef3ac4c502a1b87c6ee6bc1a9131b098a85d31560c60c599398d0bd80b37bf4d20df81522b2acc749178fb785
|
||||
|
||||
|
||||
bench_result : [128 * nblocks]
|
||||
bench_result =
|
||||
0x9b00ae426bcc2cd6150a0af62b8be77fbb389c5b061a893588d1918f50f1f31ea1183bd81fd7faae77b4f6321a17130f46e21a2653b1f7dc520bf13305c5e7141cee9d8809d58b9b8ec2aa225120ea6ecec21fba09678bbbeda0b483ad299a8adb7b306599531cf717fd67a1c25e2adeeb48521619991e122b053c3a842936b14b6eea74734a6fc2abea6c1fc4780b2df8059ce9715299eeff7b6577409ebae71285929379cd065df0c249f9696e1b28da476ae52d55d0b1f676c619271d37d4211906d402e4eaf4df3031be5bc00962b7747e7b880bf55bee2882e5008e1c1fed70beb7e54be0545100a2e122b94536b888aaea25dde9e0715dfc892dee2b4fb8e94c6b15a2e77adad1f98e50ffef837309998fcdfd9bcb3d16dcd2a162a3b66c2533474981ba72321aaa9a611c670015fa6cbf9f7d7f26b3da415eccf01872cc3a686f659c0cc0d1d08a1d41470b0ceab527bd6499433a2f2df865982b3f616c246fe49f3a15b676983f7f853f6355bc2f4cdc39e5a29347f7031ab7d2659d0ddfb259fbdfe37eaee2e4dcbdfe0ac584038c5a98d85182ca2424f0e75b7f84d512828ed20bbd05065ed4ba0b850b51c31ecb231f2c879993038d7c9487e0fa46a84a02d4f5408faabd9f41edbbef5d6183dd880ea5b7272a2c46900e02357550c036f4b84168a3e891cd8fe33c2d521ce060a2863bb735e97614d0f5bf40068bfacb02297351db4a5bd80d8140a7e0734550967b2445d4236411e04f83e7f15f5148c9d758994cb8427238cea307ddde786dd74e5565b1dd905d085ebb5a7c725d72164adeeafd7387636c31eee2e729bd0fdf95686f957befdb190101cc23cc9b8e39c652e937bd1e21adad99b86d3b2ed0e4ed4ea4bd9d9ed2ad2b99adf40577fba6b25364cd6d96f79cb0f24ae551021904b57c1d469cfac780ea8469c530ab9d2fe6e98c270c5e1babed259878f48ab5824ebf327d8d18fd2e460334cc0ca9f3b0208c0b322a074185830c460cf58c45cef2234aa5ceb6ac294325bd4d4f9e569531165b9e731c84ffc92f453ce92464658592396f83555284a5f69288e3263d7bd083fa3257b0a11a9d8e4702ed06ebd172eacb7f559527637e0259573b1723c079465d593d5e89163e187ae7ac629ed75e398274daf9c420cac2d3b8f0de82dc9d50cd85d93460213416e3e5c0960c563d26fdb56e1e0dc79b251e95364389f6acbd78edd2664be1edc789b2c7a45b2101c69b3cdb8f9f6a2d7316d2cdca02fb5119d76c9bc93f7bc4e075eee1d453fa4668f368919d14035a7ba293d9787744f44e734443e9abc79a8d7aea71918f0a925026809cf43ae2fd1f6ea00fae2f87d4e7d83e4e86c81695d77e48d5f7080d61d878bde080cec46f4ed19d78f2b0c14db0bb6c871e6506064aa1c7b23c7d2baa9b5db5be3fc94923e09fddc13cd8322d05d990b3a9c5ce418c542eb80b1839a23ed7bc0b588ec957db3df1e1389ff0d541ec2f5331ab92fa7f85efa5ae9ec1c513365df179bb29d4f1914940c68468bd12e9fce04c8d08b6d3f1a4e2d632303ca99656bb248efbb6becad7ac6535678d6534aec746fbca6ec3dec85e4db505872e88bde65214b92eba09b91aff63c5db7e440a1f0ef0bca38759f9aaa35c0b8c565ec4307cc07a3226c992163aaa968ab9b9e507fa4b1910d1c24442615ffea299a8d7fcaf7aa2db3fac83d9f3b8a90bd9ae9100167944e01a07c011d0115870f5079d991d3dccd71fdd23b383b69409a1ba519c22194de6d1048e1195a4c716e0b27055aef816218d94972177732b0abd9df432d8f09293d8b22cc83e05522f7fa46742cd29b63357096601137130dc772717f8f4d02b5651fae2d74f72b25e9266090b95bf3ecb6ddda78edfa47346cf336e79548f9ea09eebe95da8903c86af35cb0abdaa4b78f05b2ef66342072b229a7f030e5b2f8e2ead7a8f5ea2a512cf0f02a4b0fc23e5aef4518f1c40674f5552a040cddf2daf47eec38103e6703720bdf40d68f8de4a9c9a39b1a21a2ea15337772526128abb3234bdce85dd7187a827f7aed625b862887f4ef41f656cc76c5311e34e654e0babe2230d3c1f7554106bab1dcdf18361e5579cf794af967421a1f06f80cfc254a9fa0a5b2a7bebd6dc8bbbf178f9647e356a4fd61e41301386784ba90dfaf5823a0007e50e61a0c3720b9b54edb800ba805e3817cddc7015febed997de87030f3341fad7249ce4530d55f5e0b3aac5a9de0d72c6c5672bc29440354d3a7d88873abdd090f41fa1db8740736583f74c7bfe526b283274f4bc08dea4884ccd75d34df9d8410f7e488b541f467331c5e7da352faa1019c394535472aa0f1ed1512928591e0b4335271df7a7d2d9d7fa1f7f4522be394b39bf15a7bc7a97ad21e171a638eb27d44efd57921938ed70335e3f3a8922553392db8a07e02cd4dc1184edbfbadaf09f97c50268d25dd5e7064968fde486d68b1051cef118d80c7a2c911a8cad22b26fd94f559cc12972b655ce014914cd3c20542815a0ff98ee166611eb2edc147bf2989d4fa1d72d88f7d211d05fe8e312b441edb3627982da6606d0cfa1c696979af5ff371e293c0a749f172343ab5f87ccd8a9d1c364f032e763a939f0696989a5316b48df43763d42170f598326579acba84e16508b5d4ffac1723c9bb98f7736e961c67caf3243b07760b3be602be9995a1a6b8c5360357e9fefab445229ccddd6214476a2c3af0eeadcd067db77ecaf7c84d605b99c89ab583edac68c3c8d951cce207c2df274709fe2d25477f14a8e50bc05f82b2cf49d9b56d97182b90a9395d90f23b9ee734d70d9312c9f6278f0ecd5f90c82f67693a589a94a6555f3abd8eac5408259879603acdc67b6fb
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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.}
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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 ["<<loop>> 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
|
||||
|
||||
@ -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)
|
||||
|
||||
|
||||
@ -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)
|
||||
|
||||
209
src/Cryptol/Eval/Monad.hs
Normal file
209
src/Cryptol/Eval/Monad.hs
Normal file
@ -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 "<<loop>>" <+> 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))
|
||||
@ -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
|
||||
|
||||
@ -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 "<function>"
|
||||
VPoly _ -> text "<polymorphic value>"
|
||||
VNumPoly _ -> text "<polymorphic value>"
|
||||
VFun _ -> return $ text "<function>"
|
||||
VPoly _ -> return $ text "<polymorphic value>"
|
||||
|
||||
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
|
||||
]
|
||||
|
||||
@ -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'
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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)
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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 _ _ -> []
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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"
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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 =
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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 ]
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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 <interactive>:1:1--1:36:
|
||||
Defaulting type parameter 'bits'
|
||||
of finite enumeration
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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))
|
||||
|
||||
@ -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,
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user