Skip to content

Commit

Permalink
Add option to save all traces
Browse files Browse the repository at this point in the history
  • Loading branch information
marnovandermaas committed Jun 7, 2024
1 parent e06758e commit ce2c644
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 12 deletions.
11 changes: 8 additions & 3 deletions src/QuickCheckVEngine/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@ data Options = Options
, optShrink :: Bool
, optStrict :: Bool
, optSave :: Bool
, optSaveAll :: Bool
, optContinueOnFail:: Bool
, optIgnoreAsserts :: Bool
, csrIncludeRegex :: Maybe String
Expand Down Expand Up @@ -127,6 +128,7 @@ defaultOptions = Options
, optShrink = True
, optStrict = False
, optSave = True
, optSaveAll = False
, optContinueOnFail= False
, optIgnoreAsserts = False
, optSingleImp = False
Expand Down Expand Up @@ -193,6 +195,9 @@ options =
, Option [] ["no-save"]
(NoArg (\ opts -> opts { optSave = False }))
"Don't offer to save failed counter-examples"
, Option [] ["save-all"]
(NoArg (\ opts -> opts { optSaveAll = True }))
"Save all traces not just failures"
, Option [] ["continue-on-fail"]
(NoArg (\ opts -> opts { optContinueOnFail = True }))
"Keep running tests after failure to find multiple failures"
Expand Down Expand Up @@ -293,7 +298,7 @@ main = withSocketsDo $ do
let checkSingle :: Test TestResult -> Int -> Bool -> Int -> (Test TestResult -> IO ()) -> IO Result
checkSingle test verbosity doShrink len onFail = do
quickCheckWithResult (Args Nothing 1 1 len (verbosity > 0) (if doShrink then 1000 else 0))
(prop implA m_implB alive onFail archDesc (timeoutDelay flags) verbosity (optIgnoreAsserts flags) (optStrict flags) (return test))
(prop implA m_implB alive onFail archDesc (timeoutDelay flags) verbosity Nothing (optIgnoreAsserts flags) (optStrict flags) (return test))
let check_mcause_on_trap :: Test TestResult -> Test TestResult
check_mcause_on_trap (trace :: Test TestResult) = if or (hasTrap <$> trace) then filterTest p trace <> wrapTest testSuffix else trace
where hasTrap (_, a, b) = maybe False rvfiIsTrap a || maybe False rvfiIsTrap b
Expand Down Expand Up @@ -327,15 +332,15 @@ main = withSocketsDo $ do
Nothing -> "# Automatically generated failing test case\n"
writeFile (dir ++ "/failure-" ++ tstamp ++ ".S") (prelude ++ contents)
let saveOnFail :: Maybe FilePath -> Test TestResult -> (Test TestResult -> Test TestResult) -> IO ()
saveOnFail sourceFile test testTrans = runImpls implA m_implB alive (timeoutDelay flags) 0 test onTrace onDeath onDeath
saveOnFail sourceFile test testTrans = runImpls implA m_implB alive (timeoutDelay flags) 0 Nothing test onTrace onDeath onDeath
where onDeath test = do putStrLn "Failure rerunning test"
askAndSave sourceFile (show test) Nothing testTrans
onTrace trace = askAndSave sourceFile (showAnnotatedTrace (isNothing m_implB) archDesc trace) (Just trace) testTrans
let checkTrapAndSave sourceFile test = saveOnFail sourceFile test (check_mcause_on_trap :: Test TestResult -> Test TestResult)
let checkResult = if optVerbosity flags > 1 then verboseCheckWithResult else quickCheckWithResult
let checkGen gen remainingTests =
checkResult (Args Nothing remainingTests 1 (testLen flags) (optVerbosity flags > 0) (if optShrink flags then 1000 else 0))
(prop implA m_implB alive (checkTrapAndSave Nothing) archDesc (timeoutDelay flags) (optVerbosity flags) (optIgnoreAsserts flags) (optStrict flags) gen)
(prop implA m_implB alive (checkTrapAndSave Nothing) archDesc (timeoutDelay flags) (optVerbosity flags) (if (optSaveAll flags) then (saveDir flags) else Nothing) (optIgnoreAsserts flags) (optStrict flags) gen)

Check warning on line 343 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "if (optSaveAll flags) then (saveDir flags) else Nothing" ▫︎ Perhaps: "if optSaveAll flags then (saveDir flags) else Nothing"

Check warning on line 343 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "if (optSaveAll flags) then (saveDir flags) else Nothing" ▫︎ Perhaps: "if (optSaveAll flags) then saveDir flags else Nothing"
failuresRef <- newIORef 0
let checkFile (memoryInitFile :: Maybe FilePath) (skipped :: Int) (fileName :: FilePath)
| skipped == 0 = do putStrLn $ "Reading trace from " ++ fileName
Expand Down
28 changes: 19 additions & 9 deletions src/QuickCheckVEngine/MainHelpers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ import System.Timeout
import Data.IORef
import Data.Maybe
import Data.Binary
import Data.Time.Clock
import Network.Socket
import Network.Socket.ByteString.Lazy
import Test.QuickCheck
Expand Down Expand Up @@ -150,15 +151,14 @@ wrapTest = (<> single (diiEnd, Nothing, Nothing))
. (f <$>)
where f (MkInstruction i) = (diiInstruction i, Nothing, Nothing)

runImpls :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> Int -> Int -> Test TestResult
runImpls :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> Int -> Int -> Maybe FilePath -> Test TestResult
-> (Test TestResult -> IO a) -> (Test DII_Packet -> IO a) -> (Test DII_Packet -> IO a)
-> IO a
runImpls connA m_connB alive delay verbosity test onTrace onFirstDeath onSubsequentDeaths = do
runImpls connA m_connB alive delay verbosity saveDir test onTrace onFirstDeath onSubsequentDeaths = do
let instTrace = (\(x, _, _) -> x) <$> test
let insts = instTrace
currentlyAlive <- readIORef alive
if currentlyAlive then do
m_trace <- doRVFIDII connA m_connB alive delay verbosity insts
m_trace <- doRVFIDII connA m_connB alive delay verbosity saveDir test
case m_trace of
Just trace -> onTrace trace
_ -> onFirstDeath instTrace
Expand All @@ -170,11 +170,11 @@ runImpls connA m_connB alive delay verbosity test onTrace onFirstDeath onSubsequ
-- 'Test -> IO ()' to be performed on failure that takes in the reduced
-- 'Test' which caused the failure
prop :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> (Test TestResult -> IO ())
-> ArchDesc -> Int -> Int -> Bool -> Bool -> Gen (Test TestResult) -> Property
prop connA m_connB alive onFail arch delay verbosity ignoreAsserts strict gen =
-> ArchDesc -> Int -> Int -> Maybe FilePath -> Bool -> Bool -> Gen (Test TestResult) -> Property
prop connA m_connB alive onFail arch delay verbosity saveDir ignoreAsserts strict gen =
forAllShrink gen shrink mkProp
where mkProp test = whenFail (onFail test) (doProp test)
doProp test = monadicIO $ run $ runImpls connA m_connB alive delay verbosity test onTrace onFirstDeath onSubsequentDeaths
doProp test = monadicIO $ run $ runImpls connA m_connB alive delay verbosity saveDir test onTrace onFirstDeath onSubsequentDeaths
colourGreen = "\ESC[32m"
colourRed = "\ESC[31m"
colourEnd = "\ESC[0m"
Expand Down Expand Up @@ -204,8 +204,10 @@ prop connA m_connB alive onFail arch delay verbosity ignoreAsserts strict gen =
-- 'IORef Bool' for alive to 'False' indicating that further interaction with
-- the implementations is futile
doRVFIDII :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> Int
-> Int -> Test DII_Packet -> IO (Maybe (Test TestResult))
doRVFIDII connA m_connB alive delay verbosity insts = do
-> Int -> Maybe FilePath -> Test TestResult -> IO (Maybe (Test TestResult))
doRVFIDII connA m_connB alive delay verbosity saveDir test = do
let instTrace = (\(x, _, _) -> x) <$> test
let insts = instTrace
currentlyAlive <- readIORef alive
if currentlyAlive then do
result <- try $ do
Expand All @@ -228,6 +230,14 @@ doRVFIDII connA m_connB alive delay verbosity insts = do
when (isNothing m_traceA) $ putStrLn "Error: implementation A timeout. Forcing all future tests to report 'SUCCESS'"
when (isNothing m_traceAB) $ putStrLn "Error: implementation B timeout. Forcing all future tests to report 'SUCCESS'"
--
case saveDir of
Nothing -> do return ()
Just dir -> do
t <- getCurrentTime
let tstamp = [if x == ' ' then '_' else if x == ':' then '-' else x | x <- show t]
let prelude = "# Automatically generated test case\n"
writeFile (dir ++ "/random-test-" ++ tstamp ++ ".S") (prelude ++ (show test))
--
return $ fromMaybe (emptyTrace traceA) m_traceAB
case result of
Right t -> return $ Just $ (\((x,y),z) -> (x,y,z)) <$> t
Expand Down

0 comments on commit ce2c644

Please sign in to comment.