{-# 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,
  -- | = pre-computed test suites
  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
    -- | maximum number of iteration unfoldings when searching for satisfiable paths.
    --   (indirectly controls maximum path length)
  { Args -> Int
maxIterationUnfold :: Int
    -- | size of randomly generated input candidates (the solver might find bigger solutions)
  , Args -> Integer
valueSize :: Integer
    -- | solver timeout in milliseconds
  , Args -> Int
solverTimeout :: Int
    -- | maximum number of solver timeouts before giving up
  , Args -> Int
maxTimeouts :: Int
    -- | minimum number of tests generated per path
    --   (when using 'InputMode' 'UntilValid' more test will be performed)
  , Args -> Int
testsPerPath :: Int
    -- | maximum number of negative inputs per path (for 'InputMode' 'UntilValid')
  , Args -> Int
maxNegative :: Int
    -- | print extra information
  , Args -> Bool
terminalOutput :: Bool
    -- | feedback formating
  , Args -> FeedbackStyle
feedbackStyle :: FeedbackStyle
    -- | check that intermediate results do not cause Int overflows,
    --   including parts of 'OutputTerms' when possible (best-effort, no guarantees on completeness)
  , Args -> Bool
avoidOverflows :: Bool
    -- | maximum length of string values in the backend solver.
    --   Smaller values may speed up test case generation, at the risk of not finding some satisfiable paths
  , 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 -- 1 sec
  , 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 -- skip this path
              | 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 -- there might be paths in the queue that are longer than a found counterexample
            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"]

-- static test suite generation
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