From cea1f331cf821f3e1590bf455062d28b19a67ce3 Mon Sep 17 00:00:00 2001 From: Franz Fuchs Date: Thu, 25 Apr 2024 10:56:43 +0100 Subject: [PATCH] Changed pendantic to strict and changed default behaviour --- src/QuickCheckVEngine/Main.hs | 14 +++++++------- src/QuickCheckVEngine/MainHelpers.hs | 4 ++-- src/QuickCheckVEngine/RVFI_DII/RVFI.hs | 22 +++++++++++----------- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/QuickCheckVEngine/Main.hs b/src/QuickCheckVEngine/Main.hs index 44d5aa5..33427c0 100644 --- a/src/QuickCheckVEngine/Main.hs +++ b/src/QuickCheckVEngine/Main.hs @@ -98,7 +98,7 @@ data Options = Options , testLen :: Int , optSingleImp :: Bool , optShrink :: Bool - , optPedantic :: Bool + , optStrict :: Bool , optSave :: Bool , optContinueOnFail:: Bool , optIgnoreAsserts :: Bool @@ -125,7 +125,7 @@ defaultOptions = Options , timeoutDelay = 6000000000 -- 60 seconds , testLen = 2048 , optShrink = True - , optPedantic = True + , optStrict = False , optSave = True , optContinueOnFail= False , optIgnoreAsserts = False @@ -184,9 +184,9 @@ options = , 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" @@ -293,7 +293,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) (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 @@ -335,7 +335,7 @@ main = withSocketsDo $ do 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 diff --git a/src/QuickCheckVEngine/MainHelpers.hs b/src/QuickCheckVEngine/MainHelpers.hs index f97103c..2d1a742 100644 --- a/src/QuickCheckVEngine/MainHelpers.hs +++ b/src/QuickCheckVEngine/MainHelpers.hs @@ -171,7 +171,7 @@ runImpls connA m_connB alive delay verbosity test onTrace onFirstDeath onSubsequ -- '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 @@ -179,7 +179,7 @@ prop connA m_connB alive onFail arch delay verbosity ignoreAsserts pedantic gen 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 diff --git a/src/QuickCheckVEngine/RVFI_DII/RVFI.hs b/src/QuickCheckVEngine/RVFI_DII/RVFI.hs index e6488a3..1914c65 100644 --- a/src/QuickCheckVEngine/RVFI_DII/RVFI.hs +++ b/src/QuickCheckVEngine/RVFI_DII/RVFI.hs @@ -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 ""