-- |
-- Module      :  Cryptol.Testing.Concrete
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# 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

-- | A test result is either a pass, a failure due to evaluating to
-- @False@, or a failure due to an exception raised during evaluation
data TestResult
  = Pass
  | FailFalse [Value]
  | FailError EvalError [Value]

isPass :: TestResult -> Bool
isPass :: TestResult -> Bool
isPass Pass = Bool
True
isPass _    = Bool
False

-- | Apply a testable value to some arguments.
-- Note that this function assumes that the values come from a call to
-- `testableType` (i.e., things are type-correct). We run in the IO
-- monad in order to catch any @EvalError@s.
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

{- | Given a (function) type, compute all possible inputs for it.
We also return the types of the arguments and
the total number of test (i.e., the length of the outer list. -}
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

{- | Given a fully-evaluated type, try to compute the number of values in it.
Returns `Nothing` for infinite types, user-defined types, polymorphic types,
and, currently, function spaces.  Of course, we can easily compute the
sizes of function spaces, but we can't easily enumerate their inhabitants. -}
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


{- | Returns all the values in a type.  Returns an empty list of values,
for types where 'typeSize' returned '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       -> []  -- We don't generate function values.
        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 _ _ -> []

--------------------------------------------------------------------------------
-- Driver function

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 -- ^ The property as entered by the user
  , TestSpec m s -> Integer
testTotal :: Integer
  , TestSpec m s -> Maybe Integer
testPossible :: Maybe Integer -- ^ Nothing indicates infinity
  , 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 -- ^ The property as entered by the user
  , 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 -- delProgress -- unnecessary?
          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