{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE LambdaCase #-}
module Test.IOTasks.Testing (
taskCheck, taskCheckWith, taskCheckOutcome, taskCheckWithOutcome,
Args(..), stdArgs,
FeedbackStyle(..), TraceStyle(..), defaultFeedback,
Outcome(..), CoreOutcome(..), OutcomeHints(..),
ExpectedRun, ActualRun,
isSuccess, isFailure,
overflowWarnings,
printOutcomeWith, pPrintOutcomeHints,
taskCheckOn, generateStaticTestSuite,
Inputs,
) where
import Test.IOTasks.IOrep (IOrep, Line, runProgram)
import Test.IOTasks.Specification
import Test.IOTasks.Constraints
import Test.IOTasks.Trace
import Test.IOTasks.Z3
import Test.IOTasks.Overflow
import Test.IOTasks.Internal.Output
import Test.IOTasks.FeedbackStyle
import Control.Concurrent.STM
import Control.Monad (when, forM, replicateM)
import Data.List (sortOn)
import Data.Functor (void)
import Data.Bifunctor (first, Bifunctor (second))
import Text.PrettyPrint hiding ((<>))
import Control.Concurrent.Async
import System.IO
import Test.QuickCheck (generate)
taskCheck :: IOrep () -> Specification -> IO ()
taskCheck :: IOrep () -> Specification -> IO ()
taskCheck = Args -> IOrep () -> Specification -> IO ()
taskCheckWith Args
stdArgs
data Args
= Args
{ Args -> Int
maxIterationUnfold :: Int
, Args -> Integer
valueSize :: Integer
, Args -> Int
solverTimeout :: Int
, Args -> Int
maxTimeouts :: Int
, Args -> Int
testsPerPath :: Int
, Args -> Int
maxNegative :: Int
, Args -> Bool
terminalOutput :: Bool
, Args -> FeedbackStyle
feedbackStyle :: FeedbackStyle
, Args -> Bool
avoidOverflows :: Bool
, Args -> Int
solverMaxSeqLength :: Int
}
stdArgs :: Args
stdArgs :: Args
stdArgs = Args
{ maxIterationUnfold :: Int
maxIterationUnfold = Int
25
, valueSize :: Integer
valueSize = Integer
100
, solverTimeout :: Int
solverTimeout = Int
1000
, maxTimeouts :: Int
maxTimeouts = Int
3
, testsPerPath :: Int
testsPerPath = Int
5
, maxNegative :: Int
maxNegative = Int
5
, terminalOutput :: Bool
terminalOutput = Bool
True
, feedbackStyle :: FeedbackStyle
feedbackStyle = FeedbackStyle
defaultFeedback
, avoidOverflows :: Bool
avoidOverflows = Bool
True
, solverMaxSeqLength :: Int
solverMaxSeqLength = Int
25
}
taskCheckWith :: Args -> IOrep () -> Specification -> IO ()
taskCheckWith :: Args -> IOrep () -> Specification -> IO ()
taskCheckWith Args
args IOrep ()
p Specification
s = IO Outcome -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Outcome -> IO ()) -> IO Outcome -> IO ()
forall a b. (a -> b) -> a -> b
$ Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome Args
args IOrep ()
p Specification
s
taskCheckOutcome :: IOrep () -> Specification -> IO Outcome
taskCheckOutcome :: IOrep () -> Specification -> IO Outcome
taskCheckOutcome = Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome Args
stdArgs
type SatPaths = Int
type NumberOfInputs = Int
type Timeouts = Int
type Overflows = Int
type PartialTimeout = Bool
taskCheckWithOutcome :: Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome :: Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome Args{Bool
Int
Integer
FeedbackStyle
maxIterationUnfold :: Args -> Int
valueSize :: Args -> Integer
solverTimeout :: Args -> Int
maxTimeouts :: Args -> Int
testsPerPath :: Args -> Int
maxNegative :: Args -> Int
terminalOutput :: Args -> Bool
feedbackStyle :: Args -> FeedbackStyle
avoidOverflows :: Args -> Bool
solverMaxSeqLength :: Args -> Int
maxIterationUnfold :: Int
valueSize :: Integer
solverTimeout :: Int
maxTimeouts :: Int
testsPerPath :: Int
maxNegative :: Int
terminalOutput :: Bool
feedbackStyle :: FeedbackStyle
avoidOverflows :: Bool
solverMaxSeqLength :: Int
..} IOrep ()
prog Specification
spec = do
Output
output <- Handle -> IO Output
newOutput Handle
stdout
TQueue (Maybe SimplePath)
q <- STM (TQueue (Maybe SimplePath)) -> IO (TQueue (Maybe SimplePath))
forall a. STM a -> IO a
atomically STM (TQueue (Maybe SimplePath))
forall a. STM (TQueue a)
newTQueue
TVar (Maybe Int)
nVar <- Maybe Int -> IO (TVar (Maybe Int))
forall a. a -> IO (TVar a)
newTVarIO Maybe Int
forall a. Maybe a
Nothing
(()
_,(CoreOutcome
coreOut,Int
satPaths,Int
nInputs,Int
timeouts,Int
overflows)) <- IO ()
-> IO (CoreOutcome, Int, Int, Int, Int)
-> IO ((), (CoreOutcome, Int, Int, Int, Int))
forall a b. IO a -> IO b -> IO (a, b)
concurrently
(TVar (Maybe Int)
-> Int
-> ConstraintTree
-> Int
-> Int
-> Bool
-> TQueue (Maybe SimplePath)
-> IO ()
satPathsQ TVar (Maybe Int)
nVar Int
solverTimeout (Specification -> ConstraintTree
constraintTree Specification
spec) Int
maxIterationUnfold Int
solverMaxSeqLength Bool
avoidOverflows TQueue (Maybe SimplePath)
q)
(Output
-> TVar (Maybe Int)
-> TQueue (Maybe SimplePath)
-> IO (CoreOutcome, Int, Int, Int, Int)
testProcedure Output
output TVar (Maybe Int)
nVar TQueue (Maybe SimplePath)
q)
let out :: Outcome
out = CoreOutcome -> OutcomeHints -> Outcome
Outcome CoreOutcome
coreOut (if Int
overflows Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then OutcomeHints
NoHints else Int -> OutcomeHints
OverflowHint Int
overflows)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Output -> String -> IO ()
putLnP Output
output (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
[String
"generated", Int -> String
forall a. Show a => a -> String
show Int
nInputs,String
"input", Bool -> String -> String -> String
useSingularIf (Int
nInputs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) String
"sequence" String
"sequences", String
"covering", Int -> String
forall a. Show a => a -> String
show Int
satPaths, String
"satisfiable", Bool -> String -> String -> String
useSingularIf (Int
nInputs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) String
"path" String
"paths"]
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
timeouts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
Output -> String -> IO ()
putLnP Output
output (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"---",Int -> String
forall a. Show a => a -> String
show Int
timeouts, Bool -> String -> String -> String
useSingularIf (Int
timeouts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) String
"path" String
"paths", String
"timed out"]
Output -> Doc -> IO ()
forall a. Show a => Output -> a -> IO ()
printP Output
output (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ FeedbackStyle -> Outcome -> Doc
printOutcomeWith FeedbackStyle
feedbackStyle Outcome
out
Outcome -> IO Outcome
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Outcome
out
where
testProcedure :: Output -> TVar (Maybe Int) -> TQueue (Maybe SimplePath) -> IO (CoreOutcome,SatPaths,NumberOfInputs,Timeouts,Overflows)
testProcedure :: Output
-> TVar (Maybe Int)
-> TQueue (Maybe SimplePath)
-> IO (CoreOutcome, Int, Int, Int, Int)
testProcedure Output
output TVar (Maybe Int)
nVar TQueue (Maybe SimplePath)
q = (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
0,Int
0,Int
0,Int
0) Maybe CoreOutcome
forall a. Maybe a
Nothing
where
mainLoop :: (SatPaths,NumberOfInputs,Timeout,Overflows) -> Maybe CoreOutcome -> IO (CoreOutcome,SatPaths,NumberOfInputs,Timeouts,Overflows)
mainLoop :: (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nP,Int
n,Int
t,Int
o) Maybe CoreOutcome
mFailure | Int
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTimeouts =
case Maybe CoreOutcome
mFailure of
(Just CoreOutcome
failure) -> (CoreOutcome, Int, Int, Int, Int)
-> IO (CoreOutcome, Int, Int, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreOutcome
failure,Int
nP,Int
n,Int
t,Int
o)
Maybe CoreOutcome
Nothing -> (CoreOutcome, Int, Int, Int, Int)
-> IO (CoreOutcome, Int, Int, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreOutcome
GaveUp,Int
nP,Int
n,Int
t,Int
o)
mainLoop (Int
nP,Int
n,Int
t,Int
o) Maybe CoreOutcome
mFailure = do
Maybe SimplePath
next <- STM (Maybe SimplePath) -> IO (Maybe SimplePath)
forall a. STM a -> IO a
atomically (STM (Maybe SimplePath) -> IO (Maybe SimplePath))
-> STM (Maybe SimplePath) -> IO (Maybe SimplePath)
forall a b. (a -> b) -> a -> b
$ TQueue (Maybe SimplePath) -> STM (Maybe SimplePath)
forall a. TQueue a -> STM a
readTQueue TQueue (Maybe SimplePath)
q
Maybe Int
currentMaxPathLength <- TVar (Maybe Int) -> IO (Maybe Int)
forall a. TVar a -> IO a
readTVarIO TVar (Maybe Int)
nVar
case Maybe SimplePath
next of
Maybe SimplePath
Nothing -> case Maybe CoreOutcome
mFailure of
Just CoreOutcome
failure -> (CoreOutcome, Int, Int, Int, Int)
-> IO (CoreOutcome, Int, Int, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreOutcome
failure,Int
nP,Int
n,Int
t,Int
o)
Maybe CoreOutcome
Nothing -> (CoreOutcome, Int, Int, Int, Int)
-> IO (CoreOutcome, Int, Int, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> CoreOutcome
Success Int
n,Int
nP,Int
n,Int
t,Int
o)
Just SimplePath
p
| Bool -> (Int -> Bool) -> Maybe Int -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Path -> Int
pathDepth ([Int] -> SimplePath -> Path
completePath [] SimplePath
p) >) Maybe Int
currentMaxPathLength -> (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nP,Int
n,Int
t,Int
o) Maybe CoreOutcome
mFailure
| Bool
otherwise -> do
(PathOutcome
outPlain,Int
n',Int
oPlain) <- Int -> SimplePath -> IO (PathOutcome, Int, Int)
testPlain Int
n SimplePath
p
case PathOutcome
outPlain of
PathFailure{} -> (Int, Int, Int, Int)
-> PathOutcome
-> Maybe CoreOutcome
-> IO (CoreOutcome, Int, Int, Int, Int)
handleFailure (Int
nP,Int
n',Int
t,Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oPlain) PathOutcome
outPlain Maybe CoreOutcome
mFailure
PathOutcome
PathTimeout -> Bool
-> (Int, Int, Int, Int)
-> Maybe CoreOutcome
-> IO (CoreOutcome, Int, Int, Int, Int)
handleTimeout (Int
n' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n) (Int
nP,Int
n',Int
t,Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oPlain) Maybe CoreOutcome
mFailure
PathOutcome
PathSuccess -> do
if SimplePath -> Bool
canBeInjected SimplePath
p
then do
(PathOutcome
outInject,Int
n'',Int
oInject) <- Int -> SimplePath -> IO (PathOutcome, Int, Int)
testInjected Int
n' SimplePath
p
case PathOutcome
outInject of
PathFailure{} -> (Int, Int, Int, Int)
-> PathOutcome
-> Maybe CoreOutcome
-> IO (CoreOutcome, Int, Int, Int, Int)
handleFailure (Int
nP,Int
n'',Int
t,Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oPlainInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oInject) PathOutcome
outInject Maybe CoreOutcome
mFailure
PathOutcome
PathTimeout -> Bool
-> (Int, Int, Int, Int)
-> Maybe CoreOutcome
-> IO (CoreOutcome, Int, Int, Int, Int)
handleTimeout (Int
n'' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n') (Int
nP,Int
n'',Int
t,Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oPlainInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oInject) Maybe CoreOutcome
mFailure
PathOutcome
PathSuccess -> (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nPInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
n'',Int
t,Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oPlainInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oInject) Maybe CoreOutcome
mFailure
else (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nPInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
n',Int
t,Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oPlain) Maybe CoreOutcome
mFailure
handleFailure :: (SatPaths,NumberOfInputs,Timeout,Overflows) -> PathOutcome -> Maybe CoreOutcome -> IO (CoreOutcome,SatPaths,NumberOfInputs,Timeouts,Overflows)
handleFailure :: (Int, Int, Int, Int)
-> PathOutcome
-> Maybe CoreOutcome
-> IO (CoreOutcome, Int, Int, Int, Int)
handleFailure (Int
nP,Int
n,Int
t,Int
o) (PathFailure [String]
i ExpectedRun
et ExpectedRun
at MatchResult
r) Maybe CoreOutcome
mFailure = do
if Bool -> (CoreOutcome -> Bool) -> Maybe CoreOutcome -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (\case {Failure [String]
j ExpectedRun
_ ExpectedRun
_ MatchResult
_ -> [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
j; CoreOutcome
_ -> String -> Bool
forall a. HasCallStack => String -> a
error String
"impossible"}) Maybe CoreOutcome
mFailure
then do
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Int) -> Maybe Int -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar (Maybe Int)
nVar (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
(Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nPInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
n,Int
t,Int
o) (CoreOutcome -> Maybe CoreOutcome
forall a. a -> Maybe a
Just (CoreOutcome -> Maybe CoreOutcome)
-> CoreOutcome -> Maybe CoreOutcome
forall a b. (a -> b) -> a -> b
$ [String]
-> ExpectedRun -> ExpectedRun -> MatchResult -> CoreOutcome
Failure [String]
i ExpectedRun
et ExpectedRun
at MatchResult
r)
else
(Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nPInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
n,Int
t,Int
o) Maybe CoreOutcome
mFailure
handleFailure (Int, Int, Int, Int)
_ PathOutcome
_ Maybe CoreOutcome
_ = String -> IO (CoreOutcome, Int, Int, Int, Int)
forall a. HasCallStack => String -> a
error String
"handleFailure: impossible"
handleTimeout :: PartialTimeout -> (SatPaths,NumberOfInputs,Timeout,Overflows) -> Maybe CoreOutcome -> IO (CoreOutcome,SatPaths,NumberOfInputs,Timeouts,Overflows)
handleTimeout :: Bool
-> (Int, Int, Int, Int)
-> Maybe CoreOutcome
-> IO (CoreOutcome, Int, Int, Int, Int)
handleTimeout Bool
True (Int
nP,Int
n,Int
t,Int
o) = (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nPInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
n,Int
t,Int
o)
handleTimeout Bool
False (Int
nP,Int
n,Int
t,Int
o) = (Int, Int, Int, Int)
-> Maybe CoreOutcome -> IO (CoreOutcome, Int, Int, Int, Int)
mainLoop (Int
nP,Int
n,Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
o)
testPlain :: NumberOfInputs -> SimplePath -> IO (PathOutcome,NumberOfInputs,Overflows)
testPlain :: Int -> SimplePath -> IO (PathOutcome, Int, Int)
testPlain Int
n SimplePath
p = (Int, Int) -> [Path] -> IO (PathOutcome, Int, Int)
pathLoop (Int
n,Int
0) ([Path] -> IO (PathOutcome, Int, Int))
-> [Path] -> IO (PathOutcome, Int, Int)
forall a b. (a -> b) -> a -> b
$ Int -> Path -> [Path]
forall a. Int -> a -> [a]
replicate Int
testsPerPath (Path -> [Path]) -> Path -> [Path]
forall a b. (a -> b) -> a -> b
$ [Int] -> SimplePath -> Path
completePath [] SimplePath
p
testInjected :: NumberOfInputs -> SimplePath -> IO (PathOutcome,NumberOfInputs,Overflows)
testInjected :: Int -> SimplePath -> IO (PathOutcome, Int, Int)
testInjected Int
n SimplePath
p = do
PathInjector
injector <- SimplePath -> Int -> Int -> Bool -> IO PathInjector
mkPathInjector SimplePath
p Int
solverTimeout Int
solverMaxSeqLength Bool
avoidOverflows
[Path]
ps <- Int -> IO Path -> IO [Path]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
testsPerPath (Gen Path -> IO Path
forall a. Gen a -> IO a
generate (Gen Path -> IO Path) -> Gen Path -> IO Path
forall a b. (a -> b) -> a -> b
$ PathInjector -> Int -> Gen Path
injectNegatives PathInjector
injector Int
maxNegative)
(PathOutcome
out,Int
n',Int
o) <- (Int, Int) -> [Path] -> IO (PathOutcome, Int, Int)
pathLoop (Int
n,Int
0) [Path]
ps
case PathOutcome
out of
PathFailure{} -> do
[Path]
smaller <- [IO Path] -> IO [Path]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ Gen Path -> IO Path
forall a. Gen a -> IO a
generate (Gen Path -> IO Path) -> Gen Path -> IO Path
forall a b. (a -> b) -> a -> b
$ PathInjector -> Int -> Gen Path
injectNegatives PathInjector
injector Int
m | Int
m <- [Int
1..Int
maxNegative] ]
(PathOutcome
outShrink,Int
n'',Int
o') <- (Int, Int) -> [Path] -> IO (PathOutcome, Int, Int)
pathLoop (Int
n',Int
o) [Path]
smaller
(PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int))
-> (PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a b. (a -> b) -> a -> b
$ case PathOutcome
outShrink of
PathFailure{} -> (PathOutcome
outShrink,Int
n'',Int
o')
PathOutcome
_ -> (PathOutcome
out,Int
n'',Int
o')
PathOutcome
_ -> (PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PathOutcome
out,Int
n',Int
o)
pathLoop :: (NumberOfInputs,Overflows) -> [Path] -> IO (PathOutcome,NumberOfInputs,Overflows)
pathLoop :: (Int, Int) -> [Path] -> IO (PathOutcome, Int, Int)
pathLoop (Int
n,Int
o) [] = (PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PathOutcome
PathSuccess,Int
n,Int
o)
pathLoop (Int
n,Int
o) (Path
p:[Path]
ps) = do
SatResult [String]
nextInput <- Int -> Path -> Integer -> Int -> Bool -> IO (SatResult [String])
findPathInput Int
solverTimeout Path
p Integer
valueSize Int
solverMaxSeqLength Bool
avoidOverflows
case SatResult [String]
nextInput of
SatResult [String]
NotSAT -> IO ()
reportUnsat IO () -> IO (PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Int, Int) -> [Path] -> IO (PathOutcome, Int, Int)
pathLoop (Int
n,Int
o) [Path]
ps
SatResult [String]
Timeout -> (PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PathOutcome
PathTimeout,Int
n,Int
o)
SAT [String]
input -> do
Int -> IO ()
reportTestExecution Int
n
let
(PathOutcome
out,Bool
overflow) = (OverflowWarning -> Bool)
-> (PathOutcome, OverflowWarning) -> (PathOutcome, Bool)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (OverflowWarning -> OverflowWarning -> Bool
forall a. Eq a => a -> a -> Bool
== OverflowWarning
OverflowOccurred) ((PathOutcome, OverflowWarning) -> (PathOutcome, Bool))
-> (PathOutcome, OverflowWarning) -> (PathOutcome, Bool)
forall a b. (a -> b) -> a -> b
$ [String] -> (PathOutcome, OverflowWarning)
testInput [String]
input
o' :: Int
o' = if Bool
overflow then Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 else Int
o
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
overflow IO ()
reportOverflow
case PathOutcome
out of
PathOutcome
PathSuccess -> (Int, Int) -> [Path] -> IO (PathOutcome, Int, Int)
pathLoop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
o') [Path]
ps
out :: PathOutcome
out@PathFailure{} -> do
Int -> IO ()
reportCounterexample ([String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
input)
(PathOutcome, Int, Int) -> IO (PathOutcome, Int, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PathOutcome
out,Int
n,Int
o')
PathOutcome
PathTimeout -> String -> IO (PathOutcome, Int, Int)
forall a. HasCallStack => String -> a
error String
"does not happen"
testInput :: Inputs -> (PathOutcome,OverflowWarning)
testInput :: [String] -> (PathOutcome, OverflowWarning)
testInput [String]
input =
let
(ExpectedRun
specTrace,OverflowWarning
warn) = (AbstractTrace -> ExpectedRun)
-> (AbstractTrace, OverflowWarning)
-> (ExpectedRun, OverflowWarning)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first AbstractTrace -> ExpectedRun
normalizedTrace ((AbstractTrace, OverflowWarning)
-> (ExpectedRun, OverflowWarning))
-> (AbstractTrace, OverflowWarning)
-> (ExpectedRun, OverflowWarning)
forall a b. (a -> b) -> a -> b
$ Specification -> [String] -> (AbstractTrace, OverflowWarning)
runSpecification Specification
spec [String]
input
progTrace :: ExpectedRun
progTrace = IOrep () -> [String] -> ExpectedRun
runProgram IOrep ()
prog [String]
input
in case ExpectedRun
specTrace ExpectedRun -> ExpectedRun -> MatchResult
`covers` ExpectedRun
progTrace of
MatchResult
result | MatchResult -> Bool
isSuccessfulMatch MatchResult
result -> (PathOutcome
PathSuccess,OverflowWarning
warn)
MatchResult
failure -> ([String]
-> ExpectedRun -> ExpectedRun -> MatchResult -> PathOutcome
PathFailure [String]
input ExpectedRun
specTrace ExpectedRun
progTrace MatchResult
failure, OverflowWarning
warn)
reportTestExecution :: Int -> IO ()
reportTestExecution :: Int -> IO ()
reportTestExecution Int
n = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (Output -> String -> IO ()
putT Output
output ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(",Int -> String
forall a. Show a => a -> String
show Int
n,String
" tests)"]) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Output -> IO ()
oFlush Output
output)
reportCounterexample :: Int -> IO ()
reportCounterexample :: Int -> IO ()
reportCounterexample Int
len = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Output -> String -> IO ()
putLnP Output
output (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"found counterexample of length",Int -> String
forall a. Show a => a -> String
show Int
len]
reportOverflow :: IO ()
reportOverflow :: IO ()
reportOverflow = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Output -> String -> IO ()
putLnP Output
output String
"Overflow of Int range detected."
reportUnsat :: IO ()
reportUnsat :: IO ()
reportUnsat = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Output -> String -> IO ()
putLnP Output
output String
"unexpected unsat result in test case generation, maybe some value set is (conditionally) uninhabited"
type Inputs = [Line]
type ExpectedRun = NTrace
type ActualRun = NTrace
data Outcome = Outcome CoreOutcome OutcomeHints
deriving (Outcome -> Outcome -> Bool
(Outcome -> Outcome -> Bool)
-> (Outcome -> Outcome -> Bool) -> Eq Outcome
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Outcome -> Outcome -> Bool
== :: Outcome -> Outcome -> Bool
$c/= :: Outcome -> Outcome -> Bool
/= :: Outcome -> Outcome -> Bool
Eq, Int -> Outcome -> String -> String
[Outcome] -> String -> String
Outcome -> String
(Int -> Outcome -> String -> String)
-> (Outcome -> String)
-> ([Outcome] -> String -> String)
-> Show Outcome
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Outcome -> String -> String
showsPrec :: Int -> Outcome -> String -> String
$cshow :: Outcome -> String
show :: Outcome -> String
$cshowList :: [Outcome] -> String -> String
showList :: [Outcome] -> String -> String
Show)
data CoreOutcome = Success Int | Failure Inputs ExpectedRun ActualRun MatchResult | GaveUp
deriving (CoreOutcome -> CoreOutcome -> Bool
(CoreOutcome -> CoreOutcome -> Bool)
-> (CoreOutcome -> CoreOutcome -> Bool) -> Eq CoreOutcome
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CoreOutcome -> CoreOutcome -> Bool
== :: CoreOutcome -> CoreOutcome -> Bool
$c/= :: CoreOutcome -> CoreOutcome -> Bool
/= :: CoreOutcome -> CoreOutcome -> Bool
Eq, Int -> CoreOutcome -> String -> String
[CoreOutcome] -> String -> String
CoreOutcome -> String
(Int -> CoreOutcome -> String -> String)
-> (CoreOutcome -> String)
-> ([CoreOutcome] -> String -> String)
-> Show CoreOutcome
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> CoreOutcome -> String -> String
showsPrec :: Int -> CoreOutcome -> String -> String
$cshow :: CoreOutcome -> String
show :: CoreOutcome -> String
$cshowList :: [CoreOutcome] -> String -> String
showList :: [CoreOutcome] -> String -> String
Show)
data OutcomeHints = NoHints | OverflowHint Int
deriving (OutcomeHints -> OutcomeHints -> Bool
(OutcomeHints -> OutcomeHints -> Bool)
-> (OutcomeHints -> OutcomeHints -> Bool) -> Eq OutcomeHints
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OutcomeHints -> OutcomeHints -> Bool
== :: OutcomeHints -> OutcomeHints -> Bool
$c/= :: OutcomeHints -> OutcomeHints -> Bool
/= :: OutcomeHints -> OutcomeHints -> Bool
Eq, Int -> OutcomeHints -> String -> String
[OutcomeHints] -> String -> String
OutcomeHints -> String
(Int -> OutcomeHints -> String -> String)
-> (OutcomeHints -> String)
-> ([OutcomeHints] -> String -> String)
-> Show OutcomeHints
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> OutcomeHints -> String -> String
showsPrec :: Int -> OutcomeHints -> String -> String
$cshow :: OutcomeHints -> String
show :: OutcomeHints -> String
$cshowList :: [OutcomeHints] -> String -> String
showList :: [OutcomeHints] -> String -> String
Show)
instance Semigroup Outcome where
(Outcome f :: CoreOutcome
f@Failure{} OutcomeHints
h) <> :: Outcome -> Outcome -> Outcome
<> Outcome
_ = CoreOutcome -> OutcomeHints -> Outcome
Outcome CoreOutcome
f OutcomeHints
h
(Outcome CoreOutcome
GaveUp OutcomeHints
h) <> Outcome
_ = CoreOutcome -> OutcomeHints -> Outcome
Outcome CoreOutcome
GaveUp OutcomeHints
h
(Outcome CoreOutcome
cx OutcomeHints
hx) <> (Outcome CoreOutcome
cy OutcomeHints
hy) = CoreOutcome -> OutcomeHints -> Outcome
Outcome (CoreOutcome
cx CoreOutcome -> CoreOutcome -> CoreOutcome
forall a. Semigroup a => a -> a -> a
<> CoreOutcome
cy) (OutcomeHints
hx OutcomeHints -> OutcomeHints -> OutcomeHints
forall a. Semigroup a => a -> a -> a
<> OutcomeHints
hy)
instance Monoid Outcome where
mempty :: Outcome
mempty = CoreOutcome -> OutcomeHints -> Outcome
Outcome CoreOutcome
forall a. Monoid a => a
mempty OutcomeHints
forall a. Monoid a => a
mempty
instance Monoid CoreOutcome where
mempty :: CoreOutcome
mempty = Int -> CoreOutcome
Success Int
0
instance Semigroup CoreOutcome where
Success Int
x <> :: CoreOutcome -> CoreOutcome -> CoreOutcome
<> Success Int
y = Int -> CoreOutcome
Success (Int -> CoreOutcome) -> Int -> CoreOutcome
forall a b. (a -> b) -> a -> b
$ Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y
Success Int
_ <> f :: CoreOutcome
f@Failure{} = CoreOutcome
f
Success Int
_ <> CoreOutcome
GaveUp = CoreOutcome
GaveUp
f :: CoreOutcome
f@Failure{} <> CoreOutcome
_ = CoreOutcome
f
CoreOutcome
GaveUp <> CoreOutcome
_ = CoreOutcome
GaveUp
instance Monoid OutcomeHints where
mempty :: OutcomeHints
mempty = OutcomeHints
NoHints
instance Semigroup OutcomeHints where
OutcomeHints
NoHints <> :: OutcomeHints -> OutcomeHints -> OutcomeHints
<> OutcomeHints
y = OutcomeHints
y
OutcomeHints
x <> OutcomeHints
NoHints = OutcomeHints
x
OverflowHint Int
x <> OverflowHint Int
y = Int -> OutcomeHints
OverflowHint (Int -> OutcomeHints) -> Int -> OutcomeHints
forall a b. (a -> b) -> a -> b
$ Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y
isSuccess :: Outcome -> Bool
isSuccess :: Outcome -> Bool
isSuccess (Outcome Success{} OutcomeHints
_) = Bool
True
isSuccess Outcome
_ = Bool
False
isFailure :: Outcome -> Bool
isFailure :: Outcome -> Bool
isFailure (Outcome Failure{} OutcomeHints
_) = Bool
True
isFailure Outcome
_ = Bool
False
overflowWarnings :: Outcome -> Int
overflowWarnings :: Outcome -> Int
overflowWarnings (Outcome CoreOutcome
_ OutcomeHints
NoHints) = Int
0
overflowWarnings (Outcome CoreOutcome
_ (OverflowHint Int
n)) = Int
n
data PathOutcome = PathSuccess | PathTimeout | PathFailure Inputs ExpectedRun ActualRun MatchResult
deriving (PathOutcome -> PathOutcome -> Bool
(PathOutcome -> PathOutcome -> Bool)
-> (PathOutcome -> PathOutcome -> Bool) -> Eq PathOutcome
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PathOutcome -> PathOutcome -> Bool
== :: PathOutcome -> PathOutcome -> Bool
$c/= :: PathOutcome -> PathOutcome -> Bool
/= :: PathOutcome -> PathOutcome -> Bool
Eq,Int -> PathOutcome -> String -> String
[PathOutcome] -> String -> String
PathOutcome -> String
(Int -> PathOutcome -> String -> String)
-> (PathOutcome -> String)
-> ([PathOutcome] -> String -> String)
-> Show PathOutcome
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> PathOutcome -> String -> String
showsPrec :: Int -> PathOutcome -> String -> String
$cshow :: PathOutcome -> String
show :: PathOutcome -> String
$cshowList :: [PathOutcome] -> String -> String
showList :: [PathOutcome] -> String -> String
Show)
printOutcomeWith :: FeedbackStyle -> Outcome -> Doc
printOutcomeWith :: FeedbackStyle -> Outcome -> Doc
printOutcomeWith FeedbackStyle{Bool
TraceStyle
simplifyFeedback :: Bool
traceStyle :: TraceStyle
traceStyle :: FeedbackStyle -> TraceStyle
simplifyFeedback :: FeedbackStyle -> Bool
..}
| Bool
simplifyFeedback = (Doc -> Doc -> Doc) -> Outcome -> Doc
pPrintOutcomeSimple Doc -> Doc -> Doc
layoutHow
| Bool
otherwise = (Doc -> Doc -> Doc) -> Outcome -> Doc
pPrintOutcome Doc -> Doc -> Doc
layoutHow
where
layoutHow :: Doc -> Doc -> Doc
layoutHow = case TraceStyle
traceStyle of
TraceStyle
HorizontalTrace -> Doc -> Doc -> Doc
(<+>)
TraceStyle
VerticalTrace -> Doc -> Doc -> Doc
($+$)
pPrintOutcome :: (Doc -> Doc -> Doc) -> Outcome -> Doc
pPrintOutcome :: (Doc -> Doc -> Doc) -> Outcome -> Doc
pPrintOutcome Doc -> Doc -> Doc
f (Outcome CoreOutcome
core OutcomeHints
hints) = OutcomeHints -> Doc
pPrintOutcomeHints OutcomeHints
hints Doc -> Doc -> Doc
$+$ Bool -> (Doc -> Doc -> Doc) -> CoreOutcome -> Doc
pPrintCoreOutcome Bool
False Doc -> Doc -> Doc
f CoreOutcome
core
pPrintOutcomeSimple :: (Doc -> Doc -> Doc) -> Outcome -> Doc
pPrintOutcomeSimple :: (Doc -> Doc -> Doc) -> Outcome -> Doc
pPrintOutcomeSimple Doc -> Doc -> Doc
f (Outcome CoreOutcome
core OutcomeHints
hints) = OutcomeHints -> Doc
pPrintOutcomeHints OutcomeHints
hints Doc -> Doc -> Doc
$+$ Bool -> (Doc -> Doc -> Doc) -> CoreOutcome -> Doc
pPrintCoreOutcome Bool
True Doc -> Doc -> Doc
f CoreOutcome
core
pPrintCoreOutcome :: Bool -> (Doc -> Doc -> Doc) -> CoreOutcome -> Doc
pPrintCoreOutcome :: Bool -> (Doc -> Doc -> Doc) -> CoreOutcome -> Doc
pPrintCoreOutcome Bool
_ Doc -> Doc -> Doc
_ (Success Int
n) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"+++ OK, passed",Int -> String
forall a. Show a => a -> String
show Int
n,Bool -> String -> String -> String
useSingularIf (Int
nInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
1) String
"test." String
"tests."]
pPrintCoreOutcome Bool
_ Doc -> Doc -> Doc
_ CoreOutcome
GaveUp = String -> Doc
text String
"*** Gave up!"
pPrintCoreOutcome Bool
simple Doc -> Doc -> Doc
f (Failure [String]
is ExpectedRun
et ExpectedRun
at MatchResult
r) = [Doc] -> Doc
vcat
[ String -> Doc
text String
"*** Failure"
, String -> Doc
text (String
"Input sequence: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
showInputs [String]
is)
, String -> Doc
text (String
"Expected run" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String -> String
when Bool
simple String
" (simplified)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":") Doc -> Doc -> Doc
<+> ExpectedRun -> Doc
showTraceHow ExpectedRun
et
, String -> Doc
text String
"Actual run:" Doc -> Doc -> Doc
<+> (Doc -> Doc -> Doc) -> ExpectedRun -> Doc
showTraceNSimple' Doc -> Doc -> Doc
f ExpectedRun
at
, String -> Doc
text String
"Error:"
, Int -> Doc -> Doc
nest Int
2 ((Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintResult Doc -> Doc -> Doc
f MatchResult
r)
]
where
when :: Bool -> String -> String
when Bool
b String
str = if Bool
b then String
str else String
""
((Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintResult, ExpectedRun -> Doc
showTraceHow)
| Bool
simple = ((Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResultSimple,(Doc -> Doc -> Doc) -> ExpectedRun -> Doc
showTraceNSimple' Doc -> Doc -> Doc
f)
| Bool
otherwise = ((Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult,(Doc -> Doc -> Doc) -> ExpectedRun -> Doc
showTraceN' Doc -> Doc -> Doc
f)
showInputs :: Inputs -> String
showInputs :: [String] -> String
showInputs = [String] -> String
unwords ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char
'?':)
pPrintOutcomeHints :: OutcomeHints -> Doc
pPrintOutcomeHints :: OutcomeHints -> Doc
pPrintOutcomeHints OutcomeHints
NoHints = Doc
forall a. Monoid a => a
mempty
pPrintOutcomeHints (OverflowHint Int
n) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [Int -> String
forall a. Show a => a -> String
show Int
n,String
"overflows of Int range were detected during testing"]
taskCheckOn :: [Inputs] -> IOrep () -> Specification -> Outcome
taskCheckOn :: [[String]] -> IOrep () -> Specification -> Outcome
taskCheckOn [[String]]
i IOrep ()
p Specification
s = (CoreOutcome -> OutcomeHints -> Outcome)
-> (CoreOutcome, OutcomeHints) -> Outcome
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry CoreOutcome -> OutcomeHints -> Outcome
Outcome (Int
-> Int
-> [[String]]
-> IOrep ()
-> Specification
-> (CoreOutcome, OutcomeHints)
go Int
0 Int
0 [[String]]
i IOrep ()
p Specification
s) where
go :: Int
-> Int
-> [[String]]
-> IOrep ()
-> Specification
-> (CoreOutcome, OutcomeHints)
go Int
n Int
o [] IOrep ()
_ Specification
_ = (Int -> CoreOutcome
Success Int
n, Int -> OutcomeHints
overflowHint Int
o)
go Int
n Int
o ([String]
i:[[String]]
is) IOrep ()
prog Specification
spec =
let
(ExpectedRun
specTrace,OverflowWarning
warn) = (AbstractTrace -> ExpectedRun)
-> (AbstractTrace, OverflowWarning)
-> (ExpectedRun, OverflowWarning)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first AbstractTrace -> ExpectedRun
normalizedTrace ((AbstractTrace, OverflowWarning)
-> (ExpectedRun, OverflowWarning))
-> (AbstractTrace, OverflowWarning)
-> (ExpectedRun, OverflowWarning)
forall a b. (a -> b) -> a -> b
$ Specification -> [String] -> (AbstractTrace, OverflowWarning)
runSpecification Specification
spec [String]
i
progTrace :: ExpectedRun
progTrace = IOrep () -> [String] -> ExpectedRun
runProgram IOrep ()
prog [String]
i
o' :: Int
o' = if OverflowWarning
warn OverflowWarning -> OverflowWarning -> Bool
forall a. Eq a => a -> a -> Bool
== OverflowWarning
OverflowOccurred then Int
oInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 else Int
o
in case ExpectedRun
specTrace ExpectedRun -> ExpectedRun -> MatchResult
`covers` ExpectedRun
progTrace of
MatchResult
result | MatchResult -> Bool
isSuccessfulMatch MatchResult
result -> Int
-> Int
-> [[String]]
-> IOrep ()
-> Specification
-> (CoreOutcome, OutcomeHints)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
o' [[String]]
is IOrep ()
prog Specification
spec
MatchResult
failure -> ([String]
-> ExpectedRun -> ExpectedRun -> MatchResult -> CoreOutcome
Failure [String]
i ExpectedRun
specTrace ExpectedRun
progTrace MatchResult
failure, Int -> OutcomeHints
overflowHint Int
o')
overflowHint :: Int -> OutcomeHints
overflowHint Int
0 = OutcomeHints
NoHints
overflowHint Int
n = Int -> OutcomeHints
OverflowHint Int
n
generateStaticTestSuite :: Args -> Specification -> IO [Inputs]
generateStaticTestSuite :: Args -> Specification -> IO [[String]]
generateStaticTestSuite Args{Bool
Int
Integer
FeedbackStyle
maxIterationUnfold :: Args -> Int
valueSize :: Args -> Integer
solverTimeout :: Args -> Int
maxTimeouts :: Args -> Int
testsPerPath :: Args -> Int
maxNegative :: Args -> Int
terminalOutput :: Args -> Bool
feedbackStyle :: Args -> FeedbackStyle
avoidOverflows :: Args -> Bool
solverMaxSeqLength :: Args -> Int
maxIterationUnfold :: Int
valueSize :: Integer
solverTimeout :: Int
maxTimeouts :: Int
testsPerPath :: Int
maxNegative :: Int
terminalOutput :: Bool
feedbackStyle :: FeedbackStyle
avoidOverflows :: Bool
solverMaxSeqLength :: Int
..} Specification
spec = do
let simple :: [SimplePath]
simple = Int -> ConstraintTree -> [SimplePath]
simplePaths Int
maxIterationUnfold (ConstraintTree -> [SimplePath]) -> ConstraintTree -> [SimplePath]
forall a b. (a -> b) -> a -> b
$ Specification -> ConstraintTree
constraintTree Specification
spec
[Path]
full <- [[Path]] -> [Path]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Path]] -> [Path]) -> IO [[Path]] -> IO [Path]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SimplePath] -> (SimplePath -> IO [Path]) -> IO [[Path]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [SimplePath]
simple (\SimplePath
p -> do
PathInjector
injector <- SimplePath -> Int -> Int -> Bool -> IO PathInjector
mkPathInjector SimplePath
p Int
solverTimeout Int
solverMaxSeqLength Bool
avoidOverflows
Int -> IO Path -> IO [Path]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
testsPerPath (Gen Path -> IO Path
forall a. Gen a -> IO a
generate (Gen Path -> IO Path) -> Gen Path -> IO Path
forall a b. (a -> b) -> a -> b
$ PathInjector -> Int -> Gen Path
injectNegatives PathInjector
injector Int
maxNegative))
let sortedPaths :: [Path]
sortedPaths = (Path -> Int) -> [Path] -> [Path]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn Path -> Int
pathDepth [Path]
full
[SatResult [String]] -> [[String]]
forall a. [SatResult a] -> [a]
catSATs ([SatResult [String]] -> [[String]])
-> IO [SatResult [String]] -> IO [[String]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Path]
-> (Path -> IO (SatResult [String])) -> IO [SatResult [String]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Path]
sortedPaths (\Path
p -> Int -> Path -> Integer -> Int -> Bool -> IO (SatResult [String])
findPathInput Int
solverTimeout Path
p Integer
valueSize Int
solverMaxSeqLength Bool
avoidOverflows)
catSATs :: [SatResult a] -> [a]
catSATs :: forall a. [SatResult a] -> [a]
catSATs [] = []
catSATs (SAT a
x : [SatResult a]
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [SatResult a] -> [a]
forall a. [SatResult a] -> [a]
catSATs [SatResult a]
xs
catSATs (SatResult a
_:[SatResult a]
xs) = [SatResult a] -> [a]
forall a. [SatResult a] -> [a]
catSATs [SatResult a]
xs
useSingularIf :: Bool -> String -> String -> String
useSingularIf :: Bool -> String -> String -> String
useSingularIf Bool
p String
singular String
plural
| Bool
p = String
singular
| Bool
otherwise = String
plural