Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add option to save all traces #49

Merged
merged 1 commit into from
Jun 14, 2024
Merged

Add option to save all traces #49

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 8 additions & 3 deletions src/QuickCheckVEngine/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@
, optShrink :: Bool
, optStrict :: Bool
, optSave :: Bool
, optSaveAll :: Bool
, optContinueOnFail:: Bool
, optIgnoreAsserts :: Bool
, csrIncludeRegex :: Maybe String
Expand Down Expand Up @@ -127,6 +128,7 @@
, optShrink = True
, optStrict = False
, optSave = True
, optSaveAll = False
, optContinueOnFail= False
, optIgnoreAsserts = False
, optSingleImp = False
Expand Down Expand Up @@ -193,6 +195,9 @@
, 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 @@ -277,7 +282,7 @@
rawArgs <- getArgs
(flags, _) <- commandOpts rawArgs
when (optVerbosity flags > 1) $ print flags
let checkRegex incReg excReg str = (str =~ (fromMaybe ".*" incReg)) && (not $ str =~ fromMaybe "a^" excReg)

Check warning on line 285 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: Move brackets to avoid $ ▫︎ Found: "(str =~ (fromMaybe \".*\" incReg))\n && (not $ str =~ fromMaybe \"a^\" excReg)" ▫︎ Perhaps: "(str =~ (fromMaybe \".*\" incReg))\n && not (str =~ fromMaybe \"a^\" excReg)"

Check warning on line 285 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: "str =~ (fromMaybe \".*\" incReg)" ▫︎ Perhaps: "str =~ fromMaybe \".*\" incReg"
let archDesc = arch flags
let csrFilter idx = checkRegex (csrIncludeRegex flags) (csrExcludeRegex flags) (fromMaybe "reserved" $ csrs_nameFromIndex idx)
let testParams = T.TestParams { T.archDesc = archDesc
Expand All @@ -293,7 +298,7 @@
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 @@
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"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Slight issue: users might be surprised if they passed "save-all", forgot to pass a directory, and lose all the tests. I wonder if it's convenient to give an error early on in that case? We could also have separate options "failures-dir" and "tests-dir" that the user can set separately.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, locally I had put that check into TestRIG run script. I might merge this PR and then see if I can get the failure and test directories separated.

failuresRef <- newIORef 0
let checkFile (memoryInitFile :: Maybe FilePath) (skipped :: Int) (fileName :: FilePath)
| skipped == 0 = do putStrLn $ "Reading trace from " ++ fileName
Expand Down Expand Up @@ -375,12 +380,12 @@
where attemptTest (label, description, archReqs, template) =
if archReqs archDesc then do
putStrLn $ label ++ " -- " ++ description ++ ":"
(if optContinueOnFail flags then repeatTillTarget else (\f t -> f t >> return ())) ((numTests <$>) . (doCheck (wrapTest <$> (T.genTest testParams template)))) (nTests flags)

Check warning on line 383 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: Use void ▫︎ Found: "f t >> return ()" ▫︎ Perhaps: "void (f t)"

Check warning on line 383 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: "(numTests <$>)\n . (doCheck (wrapTest <$> (T.genTest testParams template)))" ▫︎ Perhaps: "(numTests <$>)\n . doCheck (wrapTest <$> (T.genTest testParams template))"

Check warning on line 383 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: "wrapTest <$> (T.genTest testParams template)" ▫︎ Perhaps: "wrapTest <$> T.genTest testParams template"
else
putStrLn $ "Warning: skipping " ++ label ++ " since architecture requirements not met"
repeatTillTarget f t = if t <= 0 then return () else f t >>= (\x -> repeatTillTarget f (t - x))
Just sock -> do
doCheck (liftM (wrapTest . singleSeq . (MkInstruction <$>)) $ listOf (genInstrServer sock)) (nTests flags)

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

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase 

Warning in main in module Main: Use fmap ▫︎ Found: "liftM" ▫︎ Perhaps: "fmap"
return ()
--
rvfiDiiClose implA
Expand Down
28 changes: 19 additions & 9 deletions src/QuickCheckVEngine/MainHelpers.hs
View file
Open in desktop
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
Loading