{-# LANGUAGE RecordWildCards #-}
module Cryptol.Testing.Concrete where
import Control.Monad (join, liftM2)
import Cryptol.Eval.Monad
import Cryptol.Eval.Value
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Panic (panic)
import qualified Control.Exception as X
import Data.List(genericReplicate)
import Prelude ()
import Prelude.Compat
data TestResult
= Pass
| FailFalse [Value]
| FailError EvalError [Value]
isPass :: TestResult -> Bool
isPass :: TestResult -> Bool
isPass Pass = Bool
True
isPass _ = Bool
False
runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult
runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult
runOneTest evOpts :: EvalOpts
evOpts v0 :: Value
v0 vs0 :: [Value]
vs0 = IO TestResult
run IO TestResult -> (EvalError -> IO TestResult) -> IO TestResult
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` EvalError -> IO TestResult
forall (m :: * -> *). Monad m => EvalError -> m TestResult
handle
where
run :: IO TestResult
run = do
Bool
result <- EvalOpts -> Eval Bool -> IO Bool
forall a. EvalOpts -> Eval a -> IO a
runEval EvalOpts
evOpts (Value -> [Value] -> Eval Bool
go Value
v0 [Value]
vs0)
if Bool
result
then TestResult -> IO TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return TestResult
Pass
else TestResult -> IO TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([Value] -> TestResult
FailFalse [Value]
vs0)
handle :: EvalError -> m TestResult
handle e :: EvalError
e = TestResult -> m TestResult
forall (m :: * -> *) a. Monad m => a -> m a
return (EvalError -> [Value] -> TestResult
FailError EvalError
e [Value]
vs0)
go :: Value -> [Value] -> Eval Bool
go :: Value -> [Value] -> Eval Bool
go (VFun f :: Eval Value -> Eval Value
f) (v :: Value
v : vs :: [Value]
vs) = Eval (Eval Bool) -> Eval Bool
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Value -> [Value] -> Eval Bool
go (Value -> [Value] -> Eval Bool)
-> Eval Value -> Eval ([Value] -> Eval Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Eval Value -> Eval Value
f (Value -> Eval Value
forall a. a -> Eval a
ready Value
v)) Eval ([Value] -> Eval Bool) -> Eval [Value] -> Eval (Eval Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Value] -> Eval [Value]
forall (m :: * -> *) a. Monad m => a -> m a
return [Value]
vs)
go (VFun _) [] = String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic "Not enough arguments while applying function"
[]
go (VBit b :: Bool
b) [] = Bool -> Eval Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
go v :: Value
v vs :: [Value]
vs = do Doc
vdoc <- PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts Value
v
[Doc]
vsdocs <- (Value -> Eval Doc) -> [Value] -> Eval [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PPOpts -> Value -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
defaultPPOpts) [Value]
vs
String -> [String] -> Eval Bool
forall a. HasCallStack => String -> [String] -> a
panic "Type error while running test" ([String] -> Eval Bool) -> [String] -> Eval Bool
forall a b. (a -> b) -> a -> b
$
[ "Function:"
, Doc -> String
forall a. Show a => a -> String
show Doc
vdoc
, "Arguments:"
] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
forall a. Show a => a -> String
show [Doc]
vsdocs
testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])
testableType :: Type -> Maybe (Maybe Integer, [Type], [[Value]])
testableType ty :: Type
ty =
case Type -> Type
tNoUser Type
ty of
TCon (TC TCFun) [t1 :: Type
t1,t2 :: Type
t2] ->
do let sz :: Maybe Integer
sz = Type -> Maybe Integer
typeSize Type
t1
(tot :: Maybe Integer
tot,ts :: [Type]
ts,vss :: [[Value]]
vss) <- Type -> Maybe (Maybe Integer, [Type], [[Value]])
testableType Type
t2
(Maybe Integer, [Type], [[Value]])
-> Maybe (Maybe Integer, [Type], [[Value]])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) Maybe Integer
sz Maybe Integer
tot, Type
t1Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts, [ Value
v Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
vs | Value
v <- Type -> [Value]
typeValues Type
t1, [Value]
vs <- [[Value]]
vss ])
TCon (TC TCBit) [] -> (Maybe Integer, [Type], [[Value]])
-> Maybe (Maybe Integer, [Type], [[Value]])
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer
forall a. a -> Maybe a
Just 1, [], [[]])
_ -> Maybe (Maybe Integer, [Type], [[Value]])
forall a. Maybe a
Nothing
typeSize :: Type -> Maybe Integer
typeSize :: Type -> Maybe Integer
typeSize ty :: Type
ty =
case Type
ty of
TVar _ -> Maybe Integer
forall a. Maybe a
Nothing
TUser _ _ t :: Type
t -> Type -> Maybe Integer
typeSize Type
t
TRec fs :: [(Ident, Type)]
fs -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ident, Type) -> Maybe Integer)
-> [(Ident, Type)] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> Maybe Integer
typeSize (Type -> Maybe Integer)
-> ((Ident, Type) -> Type) -> (Ident, Type) -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident, Type) -> Type
forall a b. (a, b) -> b
snd) [(Ident, Type)]
fs
TCon (TC tc :: TC
tc) ts :: [Type]
ts ->
case (TC
tc, [Type]
ts) of
(TCNum _, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCInf, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCBit, _) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just 2
(TCInteger, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCIntMod, [sz :: Type
sz]) -> case Type -> Type
tNoUser Type
sz of
TCon (TC (TCNum n :: Integer
n)) _ -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
_ -> Maybe Integer
forall a. Maybe a
Nothing
(TCIntMod, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCSeq, [sz :: Type
sz,el :: Type
el]) -> case Type -> Type
tNoUser Type
sz of
TCon (TC (TCNum n :: Integer
n)) _ -> (Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
n) (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Integer
typeSize Type
el
_ -> Maybe Integer
forall a. Maybe a
Nothing
(TCSeq, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCFun, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCTuple _, els :: [Type]
els) -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Maybe Integer) -> [Type] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Maybe Integer
typeSize [Type]
els
(TCAbstract _, _) -> Maybe Integer
forall a. Maybe a
Nothing
(TCNewtype _, _) -> Maybe Integer
forall a. Maybe a
Nothing
TCon _ _ -> Maybe Integer
forall a. Maybe a
Nothing
typeValues :: Type -> [Value]
typeValues :: Type -> [Value]
typeValues ty :: Type
ty =
case Type
ty of
TVar _ -> []
TUser _ _ t :: Type
t -> Type -> [Value]
typeValues Type
t
TRec fs :: [(Ident, Type)]
fs -> [ [(Ident, Eval Value)] -> Value
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord [(Ident, Eval Value)]
xs
| [(Ident, Eval Value)]
xs <- [[(Ident, Eval Value)]] -> [[(Ident, Eval Value)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ [ (Ident
f,Value -> Eval Value
forall a. a -> Eval a
ready Value
v) | Value
v <- Type -> [Value]
typeValues Type
t ]
| (f :: Ident
f,t :: Type
t) <- [(Ident, Type)]
fs ]
]
TCon (TC tc :: TC
tc) ts :: [Type]
ts ->
case TC
tc of
TCNum _ -> []
TCInf -> []
TCBit -> [ Bool -> Value
forall b w i. b -> GenValue b w i
VBit Bool
False, Bool -> Value
forall b w i. b -> GenValue b w i
VBit Bool
True ]
TCInteger -> []
TCIntMod ->
case (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
tNoUser [Type]
ts of
[ TCon (TC (TCNum n :: Integer
n)) _ ] | 0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n ->
[ Integer -> Value
forall b w i. i -> GenValue b w i
VInteger Integer
x | Integer
x <- [ 0 .. Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 ] ]
_ -> []
TCSeq ->
case (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
tNoUser [Type]
ts of
[ TCon (TC (TCNum n :: Integer
n)) _, TCon (TC TCBit) [] ] ->
[ Integer -> Eval (WordValue Bool BV Integer) -> Value
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
n (WordValue Bool BV Integer -> Eval (WordValue Bool BV Integer)
forall a. a -> Eval a
ready (BV -> WordValue Bool BV Integer
forall b w i. w -> WordValue b w i
WordVal (Integer -> Integer -> BV
BV Integer
n Integer
x))) | Integer
x <- [ 0 .. 2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1 ] ]
[ TCon (TC (TCNum n :: Integer
n)) _, t :: Type
t ] ->
[ Integer -> SeqMap Bool BV Integer -> Value
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
n ([Eval Value] -> SeqMap Bool BV Integer
forall b w i. [Eval (GenValue b w i)] -> SeqMap b w i
finiteSeqMap ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
ready [Value]
xs))
| [Value]
xs <- [[Value]] -> [[Value]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([[Value]] -> [[Value]]) -> [[Value]] -> [[Value]]
forall a b. (a -> b) -> a -> b
$ Integer -> [Value] -> [[Value]]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n
([Value] -> [[Value]]) -> [Value] -> [[Value]]
forall a b. (a -> b) -> a -> b
$ Type -> [Value]
typeValues Type
t ]
_ -> []
TCFun -> []
TCTuple _ -> [ [Eval Value] -> Value
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ((Value -> Eval Value) -> [Value] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Eval Value
forall a. a -> Eval a
ready [Value]
xs)
| [Value]
xs <- [[Value]] -> [[Value]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Type -> [Value]) -> [Type] -> [[Value]]
forall a b. (a -> b) -> [a] -> [b]
map Type -> [Value]
typeValues [Type]
ts)
]
TCAbstract _ -> []
TCNewtype _ -> []
TCon _ _ -> []
data TestSpec m s = TestSpec {
TestSpec m s -> Integer -> s -> m (TestResult, s)
testFn :: Integer -> s -> m (TestResult, s)
, TestSpec m s -> String
testProp :: String
, TestSpec m s -> Integer
testTotal :: Integer
, TestSpec m s -> Maybe Integer
testPossible :: Maybe Integer
, TestSpec m s -> Integer -> Integer -> m ()
testRptProgress :: Integer -> Integer -> m ()
, TestSpec m s -> m ()
testClrProgress :: m ()
, TestSpec m s -> TestResult -> m ()
testRptFailure :: TestResult -> m ()
, TestSpec m s -> m ()
testRptSuccess :: m ()
}
data TestReport = TestReport {
TestReport -> TestResult
reportResult :: TestResult
, TestReport -> String
reportProp :: String
, TestReport -> Integer
reportTestsRun :: Integer
, TestReport -> Maybe Integer
reportTestsPossible :: Maybe Integer
}
runTests :: Monad m => TestSpec m s -> s -> m TestReport
runTests :: TestSpec m s -> s -> m TestReport
runTests TestSpec {..} st0 :: s
st0 = Integer -> s -> m TestReport
go 0 s
st0
where
go :: Integer -> s -> m TestReport
go testNum :: Integer
testNum _ | Integer
testNum Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
testTotal = do
m ()
testRptSuccess
TestReport -> m TestReport
forall (m :: * -> *) a. Monad m => a -> m a
return (TestReport -> m TestReport) -> TestReport -> m TestReport
forall a b. (a -> b) -> a -> b
$ TestResult -> String -> Integer -> Maybe Integer -> TestReport
TestReport TestResult
Pass String
testProp Integer
testNum Maybe Integer
testPossible
go testNum :: Integer
testNum st :: s
st =
do Integer -> Integer -> m ()
testRptProgress Integer
testNum Integer
testTotal
(TestResult, s)
res <- Integer -> s -> m (TestResult, s)
testFn (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (100 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
testNum)) Integer
testTotal) s
st
m ()
testClrProgress
case (TestResult, s)
res of
(Pass, st' :: s
st') -> do
Integer -> s -> m TestReport
go (Integer
testNum Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) s
st'
(failure :: TestResult
failure, _st' :: s
_st') -> do
TestResult -> m ()
testRptFailure TestResult
failure
TestReport -> m TestReport
forall (m :: * -> *) a. Monad m => a -> m a
return (TestReport -> m TestReport) -> TestReport -> m TestReport
forall a b. (a -> b) -> a -> b
$ TestResult -> String -> Integer -> Maybe Integer -> TestReport
TestReport TestResult
failure String
testProp Integer
testNum Maybe Integer
testPossible