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 force RVFIv1 #66

Merged
merged 1 commit into from
Jan 21, 2025
Merged

Add option to force RVFIv1 #66

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
13 changes: 9 additions & 4 deletions src/QuickCheckVEngine/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,7 @@
, optIgnoreAsserts :: Bool
, csrIncludeRegex :: Maybe String
, csrExcludeRegex :: Maybe String
, optForceRVFIv1 :: Bool
} deriving Show

defaultOptions :: Options
Expand Down Expand Up @@ -134,6 +135,7 @@
, optSingleImp = False
, csrIncludeRegex = Nothing
, csrExcludeRegex = Nothing
, optForceRVFIv1 = False
}

options :: [OptDescr (Options -> Options)]
Expand Down Expand Up @@ -213,6 +215,9 @@
, Option [] ["csr-exclude-regex"]
(ReqArg (\ f opts -> opts { csrExcludeRegex = Just f }) "REGEX")
"Specify REGEX to exclude a subset of CSRs from tests"
, Option [] ["force-RVFI-v1"]
(NoArg (\ opts -> opts { optForceRVFIv1 = True }))
"Force implementations to use legacy v1 RVFI reporting"
]

commandOpts :: [String] -> IO (Options, [String])
Expand Down Expand Up @@ -284,14 +289,14 @@
(flags, _) <- commandOpts rawArgs
let verbosity = optVerbosity flags
when (verbosity > 1) $ print flags
let checkRegex incReg excReg str = (str =~ (fromMaybe ".*" incReg)) && (not $ str =~ fromMaybe "a^" excReg)

Check warning on line 292 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 292 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
, T.csrFilter = csrFilter }
-- initialize model and implementation sockets
implA <- rvfiDiiOpen (impAIP flags) (impAPort flags) verbosity "implementation-A"
m_implB <- if optSingleImp flags then return Nothing else Just <$> rvfiDiiOpen (impBIP flags) (impBPort flags) verbosity "implementation-B"
implA <- rvfiDiiOpen (impAIP flags) (impAPort flags) verbosity "implementation-A" (optForceRVFIv1 flags)
m_implB <- if optSingleImp flags then return Nothing else Just <$> rvfiDiiOpen (impBIP flags) (impBPort flags) verbosity "implementation-B" (optForceRVFIv1 flags)

addrInstr <- mapM (resolve "127.0.0.1") (instrPort flags)
instrSoc <- mapM (open "instruction-generator-port") addrInstr
Expand All @@ -302,7 +307,7 @@
quickCheckWithResult (Args Nothing 1 1 len (verbosity > 0) (if doShrink then 1000 else 0))
(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

Check warning on line 310 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 any ▫︎ Found: "or (hasTrap <$> trace)" ▫︎ Perhaps: "any hasTrap trace"
where hasTrap (_, a, b) = maybe False rvfiIsTrap a || maybe False rvfiIsTrap b
testSuffix = noShrink $ singleSeq [ csrrs 1 (unsafe_csrs_indexFromName "mcause") 0
, csrrs 1 (unsafe_csrs_indexFromName "mtval" ) 0
Expand Down Expand Up @@ -344,7 +349,7 @@
let checkResult = if verbosity > 1 then verboseCheckWithResult else quickCheckWithResult
let checkGen gen remainingTests =
checkResult (Args Nothing remainingTests 1 (testLen flags) (verbosity > 0) (if optShrink flags then 1000 else 0))
(prop implA m_implB alive (checkTrapAndSave Nothing) archDesc (timeoutDelay flags) verbosity (if (optSaveAll flags) then (saveDir flags) else Nothing) (optIgnoreAsserts flags) (optStrict flags) gen)

Check warning on line 352 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 352 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 Expand Up @@ -384,7 +389,7 @@
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 392 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 392 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 392 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))
Expand All @@ -409,9 +414,9 @@
connect sock (addrAddress addr)
putStrLn ("connected to " ++ dest ++ " ...")
return sock
rvfiDiiOpen ip port verb name = do
rvfiDiiOpen ip port verb name forceV1 = do
addr <- resolve ip port
soc <- open name addr
traceVer <- rvfiNegotiateVersion soc name verb
traceVer <- if forceV1 then pure 1 else rvfiNegotiateVersion soc name verb
return $ RvfiDiiConnection soc traceVer name
rvfiDiiClose (RvfiDiiConnection sock _ _) = close sock
Loading