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

Changed pedantic to strict and changed default behaviour #44

Merged
merged 1 commit into from
Apr 25, 2024
Merged

Changed pedantic to strict and changed default behaviour #44

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
14 changes: 7 additions & 7 deletions src/QuickCheckVEngine/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@
, testLen :: Int
, optSingleImp :: Bool
, optShrink :: Bool
, optPedantic :: Bool
, optStrict :: Bool
, optSave :: Bool
, optContinueOnFail:: Bool
, optIgnoreAsserts :: Bool
Expand All @@ -125,7 +125,7 @@
, timeoutDelay = 6000000000 -- 60 seconds
, testLen = 2048
, optShrink = True
, optPedantic = True
, optStrict = False
, optSave = True
, optContinueOnFail= False
, optIgnoreAsserts = False
Expand Down Expand Up @@ -184,9 +184,9 @@
, Option ['L'] ["test-length"]
(ReqArg (\ f opts -> opts { testLen = read f }) "TEST-LENGTH")
"Generate tests up to TEST-LENGTH instructions long"
, Option ['R'] ["relaxed-comparison"]
(NoArg (\ opts -> opts { optPedantic = False }))
"Only compare key RVFI fields"
, Option [] ["strict-comparison"]
(NoArg (\ opts -> opts { optStrict = True }))
"Compare all RVFI fields"
, Option ['S'] ["disable-shrink"]
(NoArg (\ opts -> opts { optShrink = False }))
"Disable shrinking of failed tests"
Expand Down Expand Up @@ -277,7 +277,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 280 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 280 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 +293,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) (optPedantic flags) (return test))
(prop implA m_implB alive onFail archDesc (timeoutDelay flags) verbosity (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 @@ -335,7 +335,7 @@
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) (optPedantic flags) gen)
(prop implA m_implB alive (checkTrapAndSave Nothing) archDesc (timeoutDelay flags) (optVerbosity flags) (optIgnoreAsserts flags) (optStrict flags) gen)
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 +375,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 378 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 378 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 378 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 383 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
4 changes: 2 additions & 2 deletions src/QuickCheckVEngine/MainHelpers.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
{-# LANGUAGE TypeSynonymInstances #-}

Check warning on line 1 in src/QuickCheckVEngine/MainHelpers.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase 

Warning in module QuickCheckVEngine.MainHelpers: Unused LANGUAGE pragma ▫︎ Found: "{-# LANGUAGE TypeSynonymInstances #-}" ▫︎ Note: Extension TypeSynonymInstances is implied by FlexibleInstances
{-# LANGUAGE FlexibleInstances #-}
--
-- SPDX-License-Identifier: BSD-2-Clause
Expand Down Expand Up @@ -85,13 +85,13 @@

showTraceInput t = show ((\(x, _, _) -> x) <$> t)

showAnnotatedTrace singleImp arch t = showTestWithComments t (\(x, _, _) -> show x) (\(_, a, b) -> Just . unlines . (("# " ++) <$>) . lines . (\(a, b) -> b) $ rvfiCheckAndShow True singleImp (has_xlen_64 arch) a b [])

Check warning on line 88 in src/QuickCheckVEngine/MainHelpers.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase 

Warning in showAnnotatedTrace in module QuickCheckVEngine.MainHelpers: Use snd ▫︎ Found: "\\ (a, b) -> b" ▫︎ Perhaps: "snd"

bypassShrink :: ShrinkStrategy
bypassShrink = sequenceShrink f'
where f' :: Test TestResult -> Test TestResult -> [Test TestResult]
f' a b = foldr f [] a
where f (DII_Instruction _ x, _, _) = ((if is_bypass then ((a <>) <$> (singleShrink (s (def0 m_rd_x) (def0 m_rs1_x)) b)) else []) ++)

Check warning on line 94 in src/QuickCheckVEngine/MainHelpers.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase 

Suggestion in bypassShrink in module QuickCheckVEngine.MainHelpers: Redundant bracket ▫︎ Found: "if is_bypass then\n ((a <>) <$> (singleShrink (s (def0 m_rd_x) (def0 m_rs1_x)) b))\nelse\n []" ▫︎ Perhaps: "if is_bypass then\n (a <>) <$> (singleShrink (s (def0 m_rd_x) (def0 m_rs1_x)) b)\nelse\n []"
where (is_bypass, _, m_rs1_x, m_rd_x, _) = rv_extract . MkInstruction . toInteger $ x
s old new (DII_Instruction t i, ra, rb) = single <$>
[ (DII_Instruction t . fromInteger . unMkInstruction $ reencode_i (def0 m_rs2_i) new (def0 m_rd_i), ra, rb)
Expand Down Expand Up @@ -171,15 +171,15 @@
-- '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 pedantic gen =
prop connA m_connB alive onFail arch delay verbosity 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
colourGreen = "\ESC[32m"
colourRed = "\ESC[31m"
colourEnd = "\ESC[0m"
colourise (b, s) = (b, (if b then colourGreen else colourRed) ++ s ++ colourEnd)
diffFunc asserts (DII_Instruction _ _, a, b) = colourise $ rvfiCheckAndShow pedantic (isNothing m_connB) (has_xlen_64 arch) a b asserts
diffFunc asserts (DII_Instruction _ _, a, b) = colourise $ rvfiCheckAndShow strict (isNothing m_connB) (has_xlen_64 arch) a b asserts
diffFunc _ (DII_End _, _, _) = (True, "Test end")
diffFunc _ _ = (True, "")
handleAsserts (ReportAssert False s, _) = do putStrLn $ "Failed assert: " ++ s
Expand Down
22 changes: 11 additions & 11 deletions src/QuickCheckVEngine/RVFI_DII/RVFI.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -477,26 +477,26 @@ checkOptionalField cond msg showF a b = _checkField cond msg (optionalFieldsSame

-- | Compare 'RVFI_Packet's
rvfiCheck :: Bool -> Bool -> RVFI_Packet -> RVFI_Packet -> Maybe String
rvfiCheck pedantic is64 x y
rvfiCheck strict is64 x y
| rvfiIsHalt x = if rvfi_halt x == rvfi_halt y then Nothing else Just "expected halt package"
| otherwise = case errors of [] -> Nothing
xs -> Just $ intercalate ", " xs
where errors = catMaybes
[ checkField (pedantic || rvfi_trap x == 0) "insn" printHex (maskUpper False (rvfi_insn x)) (maskUpper False (rvfi_insn y)),
[ checkField (strict || rvfi_trap x == 0) "insn" printHex (maskUpper False (rvfi_insn x)) (maskUpper False (rvfi_insn y)),
checkField True "trap" show (rvfi_trap x) (rvfi_trap y),
checkField True "halt" show (rvfi_halt x) (rvfi_halt y),
checkOptionalField True "mode" show (rvfi_mode x) (rvfi_mode y),
checkOptionalField True "XLEN" show (rvfi_ixl x) (rvfi_ixl y),
checkField (pedantic || rvfi_trap x == 0) "rd_addr" show (getRDAddr x) (getRDAddr y),
checkField (pedantic || rvfi_trap x == 0) "rd_wdata" printHex (getRDWData is64 x) (getRDWData is64 y),
checkField pedantic "rs1_addr" show (getRS1Addr x) (getRS1Addr y),
checkField pedantic "rs1_rdata" printHex (getRS1RData is64 x) (getRS1RData is64 y),
checkField pedantic "rs2_addr" show (getRS2Addr x) (getRS2Addr y),
checkField pedantic "rs2_rdata" printHex (getRS2RData is64 x) (getRS2RData is64 y),
checkField (strict || rvfi_trap x == 0) "rd_addr" show (getRDAddr x) (getRDAddr y),
checkField (strict || rvfi_trap x == 0) "rd_wdata" printHex (getRDWData is64 x) (getRDWData is64 y),
checkField strict "rs1_addr" show (getRS1Addr x) (getRS1Addr y),
checkField strict "rs1_rdata" printHex (getRS1RData is64 x) (getRS1RData is64 y),
checkField strict "rs2_addr" show (getRS2Addr x) (getRS2Addr y),
checkField strict "rs2_rdata" printHex (getRS2RData is64 x) (getRS2RData is64 y),
checkField True "pc_wdata" printHex (maskUpper is64 (rvfi_pc_wdata x)) (maskUpper is64 (rvfi_pc_wdata y)),
checkField (pedantic || ((maybe 0 rvfi_mem_wmask (rvfi_mem_data x)) /= 0)) "mem_addr" printHex (getMemAddr is64 x) (getMemAddr is64 y),
_checkField (pedantic || rvfi_trap x == 0) "mem_wdata" (compareMemData is64 x y rvfi_mem_wmask rvfi_mem_wdata) "", -- TODO: context
_checkField (pedantic || rvfi_trap x == 0) "mem_rdata" (compareMemData is64 x y rvfi_mem_rmask rvfi_mem_rdata) "" -- TODO: context
checkField (strict || ((maybe 0 rvfi_mem_wmask (rvfi_mem_data x)) /= 0)) "mem_addr" printHex (getMemAddr is64 x) (getMemAddr is64 y),
_checkField (strict || rvfi_trap x == 0) "mem_wdata" (compareMemData is64 x y rvfi_mem_wmask rvfi_mem_wdata) "", -- TODO: context
_checkField (strict || rvfi_trap x == 0) "mem_rdata" (compareMemData is64 x y rvfi_mem_rmask rvfi_mem_rdata) "" -- TODO: context
]
printHex x = "0x" ++ showHex x ""

Expand Down
Loading