From 86ed39ce3b5c5457b5990f650f004bd6d838354f Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 1 Oct 2021 11:38:50 +0100 Subject: [PATCH] Make RVFI packet debug use verbosity level 4 This makes the output a bit more readable when enabling verbose output --- src/QuickCheckVEngine/Main.hs | 21 ++++----- src/QuickCheckVEngine/MainHelpers.hs | 4 +- src/QuickCheckVEngine/RVFI_DII.hs | 6 +-- src/QuickCheckVEngine/RVFI_DII/RVFI.hs | 62 +++++++++++++++++--------- stack.yaml | 3 ++ 5 files changed, 59 insertions(+), 37 deletions(-) diff --git a/src/QuickCheckVEngine/Main.hs b/src/QuickCheckVEngine/Main.hs index b8a1a0e..3df06e4 100644 --- a/src/QuickCheckVEngine/Main.hs +++ b/src/QuickCheckVEngine/Main.hs @@ -280,15 +280,16 @@ main = withSocketsDo $ do -- parse command line arguments rawArgs <- getArgs (flags, _) <- commandOpts rawArgs - when (optVerbosity flags > 1) $ print flags + let verbosity = optVerbosity flags + when (verbosity > 1) $ print flags let checkRegex incReg excReg str = (str =~ (fromMaybe ".*" incReg)) && (not $ str =~ fromMaybe "a^" excReg) 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) (optVerbosity flags) "implementation-A" - m_implB <- if optSingleImp flags then return Nothing else Just <$> rvfiDiiOpen (impBIP flags) (impBPort flags) (optVerbosity flags) "implementation-B" + 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" addrInstr <- mapM (resolve "127.0.0.1") (instrPort flags) instrSoc <- mapM (open "instruction-generator-port") addrInstr @@ -308,9 +309,9 @@ main = withSocketsDo $ do p _ = True let askAndSave sourceFile contents m_trace testTrans = do writeFile "last_failure.S" ("# last failing test case:\n" ++ contents) - case m_trace of Just trace | optVerbosity flags > 0 -> do + case m_trace of Just trace | verbosity > 0 -> do putStrLn "Replaying shrunk failed test case:" - checkSingle (testTrans trace) 2 False (testLen flags) (const $ return ()) + checkSingle (testTrans trace) 3 False (testLen flags) (const $ return ()) return () _ -> return () when (optSave flags) $ do @@ -334,12 +335,12 @@ main = withSocketsDo $ do 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 + onTrace trace = askAndSave sourceFile (showAnnotatedTrace (isNothing m_implB) archDesc verbosity 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 checkResult = if verbosity > 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) (if (optSaveAll flags) then (saveDir flags) else Nothing) (optIgnoreAsserts flags) (optStrict flags) gen) + 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) failuresRef <- newIORef 0 let checkFile (memoryInitFile :: Maybe FilePath) (skipped :: Int) (fileName :: FilePath) | skipped == 0 = do putStrLn $ "Reading trace from " ++ fileName @@ -348,7 +349,7 @@ main = withSocketsDo $ do Just memInit -> do putStrLn $ "Reading memory initialisation from file " ++ memInit readDataFile testParams memInit Nothing -> return mempty - res <- checkSingle (wrapTest $ initTrace <> trace) (optVerbosity flags) (optShrink flags) (testLen flags) (checkTrapAndSave (Just fileName)) + res <- checkSingle (wrapTest $ initTrace <> trace) verbosity (optShrink flags) (testLen flags) (checkTrapAndSave (Just fileName)) case res of Failure {} -> do putStrLn "Failure." modifyIORef failuresRef (1 +) unless (optContinueOnFail flags) $ writeIORef alive False diff --git a/src/QuickCheckVEngine/MainHelpers.hs b/src/QuickCheckVEngine/MainHelpers.hs index 7448bc8..0710d60 100644 --- a/src/QuickCheckVEngine/MainHelpers.hs +++ b/src/QuickCheckVEngine/MainHelpers.hs @@ -86,7 +86,7 @@ instance {-# OVERLAPPING #-} Show (Test TestResult) where 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 []) +showAnnotatedTrace singleImp arch verbosity t = showTestWithComments t (\(x, _, _) -> show x) (\(_, a, b) -> Just . unlines . (("# " ++) <$>) . lines . (\(a, b) -> b) $ rvfiCheckAndShow True singleImp (has_xlen_64 arch) verbosity a b []) bypassShrink :: ShrinkStrategy bypassShrink = sequenceShrink f' @@ -197,7 +197,7 @@ prop connA m_connB alive onFail arch delay verbosity saveDir ignoreAsserts stric 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 strict (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) verbosity 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.hs b/src/QuickCheckVEngine/RVFI_DII.hs index 985ad96..b76f63d 100644 --- a/src/QuickCheckVEngine/RVFI_DII.hs +++ b/src/QuickCheckVEngine/RVFI_DII.hs @@ -89,7 +89,7 @@ recvRVFITrace conn verbosity tStruct = do let recv x = do active <- readIORef activeRef if active then do rvfiPkt <- recvRVFIPacket conn verbosity - when (verbosity > 1) $ putStrLn $ "\t" ++ show rvfiPkt + when (verbosity > 1) $ putStrLn $ "\t" ++ rvfiShowPacket rvfiPkt verbosity when (rvfiIsHalt rvfiPkt) $ writeIORef activeRef False return (x, Just rvfiPkt) else return (x, Nothing) @@ -105,9 +105,9 @@ rvfiNegotiateVersion sckt name verbosity = do -- high bits of that field to indicate their supported trace version rvfiPkt <- rvfiReadV1Response ((recvBlking sckt), name, verbosity) when (verbosity > 2) $ - putStrLn ("Received initial packet from " ++ name ++ ": " ++ show rvfiPkt) + putStrLn ("Received initial packet from " ++ name ++ ": " ++ rvfiShowPacket rvfiPkt verbosity) unless (rvfiIsHalt rvfiPkt) $ - error ("Received unexpected initial packet from " ++ name ++ ": " ++ show rvfiPkt) + error ("Received unexpected initial packet from " ++ name ++ ": " ++ rvfiShowPacket rvfiPkt verbosity) let supportedVer = rvfiHaltVersion rvfiPkt result <- diiSetVersion sckt (fromIntegral supportedVer) name verbosity when (result /= 2) $ diff --git a/src/QuickCheckVEngine/RVFI_DII/RVFI.hs b/src/QuickCheckVEngine/RVFI_DII/RVFI.hs index 5b69bce..3289f55 100644 --- a/src/QuickCheckVEngine/RVFI_DII/RVFI.hs +++ b/src/QuickCheckVEngine/RVFI_DII/RVFI.hs @@ -59,6 +59,7 @@ module QuickCheckVEngine.RVFI_DII.RVFI ( , rvfiReadDataPacketWithMagic , rvfiReadV1Response , rvfiReadV2Response +, rvfiShowPacket , rvfi_rd_wdata_or_zero ) where @@ -156,8 +157,17 @@ data RVFI_IntData = RVFI_IntData { , rvfi_rs2_rdata :: {-# UNPACK #-} !RV_WordXLEN , rvfi_rd_addr :: {-# UNPACK #-} !RV_RegIdx , rvfi_rd_wdata :: {-# UNPACK #-} !RV_WordXLEN - } - deriving (Show) +} + +instance Show RVFI_IntData where + show tok = (printf + "{RD: %02d, RWD: 0x%016x" (rvfi_rd_addr tok) (rvfi_rd_wdata tok)) ++ + (if rvfi_rs1_addr tok /= 0 then + printf "RS1: %02d, RS1D: 0x%016x" (rvfi_rs1_addr tok) (rvfi_rs1_rdata tok) + else "") ++ + (if rvfi_rs2_addr tok /= 0 then + printf "RS2: %02d, RS2D: 0x%016x" (rvfi_rs2_addr tok) (rvfi_rs2_rdata tok) + else "") ++ "}" data RVFI_MemAccessData = RVFI_MemAccessData { rvfi_mem_addr :: {-# UNPACK #-} !RV_WordXLEN @@ -188,7 +198,7 @@ connectionError (name, _) msg = do rvfiCheckMagicBytes :: BS.ByteString -> String -> ConnectionInfo -> IO () rvfiCheckMagicBytes magicBytes expected conn = do let expBytes = C8.pack expected - connectionDebugMessage 3 conn ("read header magic bytes: " ++ show magicBytes) + connectionDebugMessage 4 conn ("read header magic bytes: " ++ show magicBytes) when (magicBytes /= expBytes) $ connectionError conn ("received invalid data packet: got magic=" ++ show magicBytes ++ " but expected " ++ show expBytes) return () @@ -198,7 +208,7 @@ rvfiReadDataPacketWithMagic (reader, name, verbosity) size expectedMagic = do when (size < 8) $ errorWithContext name ("Invalid packet size:" ++ show size) msg <- reader size - connectionDebugMessage 3 (name, verbosity) ("read packet: " ++ hexStr msg) + connectionDebugMessage 4 (name, verbosity) ("read packet: " ++ hexStr msg) let (magic, bytes) = BS.splitAt 8 msg rvfiCheckMagicBytes magic expectedMagic (name, verbosity) return bytes @@ -208,14 +218,14 @@ type RVFIFeatures = Word64 rvfiReadV2Response :: (Int64 -> IO BS.ByteString, String, Int) -> IO RVFI_Packet rvfiReadV2Response (reader, name, verbosity) = do let connInfo = (name, verbosity) - connectionDebugMessage 3 connInfo "reading V2 packet..." + connectionDebugMessage 4 connInfo "reading V2 packet..." headerBytes <- rvfiReadDataPacketWithMagic (reader, name, verbosity) 64 "trace-v2" let (traceSizeBytes, payloadBytes) = BS.splitAt 8 headerBytes let traceSize = runGet getWord64le traceSizeBytes - connectionDebugMessage 3 connInfo ("trace-v2 common payload bytes: " ++ hexStr payloadBytes) + connectionDebugMessage 4 connInfo ("trace-v2 common payload bytes: " ++ hexStr payloadBytes) -- Ensure that we read all bytes in the packet let (basicData, availableFeatures) = runGet (isolate 48 rvfiDecodeV2Header) payloadBytes - connectionDebugMessage 3 connInfo ("features: " ++ (printf "0x%016x" availableFeatures)) + connectionDebugMessage 4 connInfo ("features: " ++ (printf "0x%016x" availableFeatures)) (intData, rf1, numBytes1) <- rvfiMaybeReadIntData (reader, name, verbosity) availableFeatures (memData, rf2, numBytes2) <- rvfiMaybeReadMemData (reader, name, verbosity) rf1 when (rf2 /= 0) $ @@ -316,7 +326,7 @@ rvfiDecodeMemData = do rvfiReadV1Response :: (Int64 -> IO BS.ByteString, String, Int) -> IO RVFI_Packet rvfiReadV1Response (reader, name, verbosity) = do msg <- reader 88 - connectionDebugMessage 3 (name, verbosity) ("read packet: " ++ hexStr msg) + connectionDebugMessage 4 (name, verbosity) ("read packet: " ++ hexStr msg) -- Note: BS.reverse since the decode was written in BE order return $ runGet (isolate 88 rvfiDecodeV1Response) (BS.reverse msg) @@ -390,11 +400,11 @@ rvfiEmptyHaltPacket = RVFI_Packet { instance Show RVFI_MemAccessData where show tok = printf - "MA: 0x%016x, MWD: %s, MWM: 0b%08b, MRD: %s, MRM: 0b%08b " + "MA: 0x%016x,%s MWM: 0b%08b,%s MRM: 0b%08b " (rvfi_mem_addr tok) -- MA - (printMemData wmask wdata) -- MWD + (if wmask /= 0 then printf " MWD: %s," (printMemData wmask wdata) else "") -- MWD wmask -- MWM - (printMemData rmask rdata) -- MRD + (if rmask /= 0 then printf " MRD: %s," (printMemData rmask rdata) else "") -- MRD rmask -- MRM where rmask = rvfi_mem_rmask tok rdata = toInteger . toNatural . rvfi_mem_rdata $ tok @@ -406,12 +416,20 @@ instance Show RVFI_MemAccessData where | mask <= 65535 = printf "0x%032x" value | otherwise = printf "0x%064x" value -instance Show RVFI_Packet where - show tok +rvfiShowPacket :: RVFI_Packet -> Int -> String +rvfiShowPacket tok verbosity | rvfiIsHalt tok = "halt token" + | verbosity > 3 = + (printf "O:%d Trap: %5s, PCRD: 0x%016x PCWD: 0x%016x, I: 0x%08x %s XL:%s" + (rvfi_order tok) (show $ rvfi_trap tok /= 0) (rvfi_pc_rdata tok) + (rvfi_pc_wdata tok) (rvfi_insn tok) (privString (rvfi_mode tok)) + (xlenString (rvfi_ixl tok))) ++ + " INT=" ++ (maybe "N/A" show $ rvfi_int_data tok) ++ + " MEM=" ++ (maybe "N/A" show $ rvfi_mem_data tok) ++ + " # " ++ (rv_pretty (MkInstruction (toInteger (rvfi_insn tok))) (rvfi_ixl tok)) | otherwise = printf - "Trap: %5s, PCWD: 0x%016x, RD: %02d, RWD: 0x%016x, %sI: 0x%016x %s XL:%s (%s)" + "Trap: %5s, PCWD: 0x%016x, RD: %02d, RWD: 0x%016x, %sI: 0x%08x %s XL:%s (%s)" (show $ rvfi_trap tok /= 0) -- Trap (rvfi_pc_wdata tok) -- PCWD (maybe 0 rvfi_rd_addr $ rvfi_int_data tok) -- RD @@ -509,15 +527,15 @@ assertCheck is64 x asserts -- | Compare 2 'RVFI_Packet's and produce a 'String' output displaying the -- the content of the packet once only for equal inputs or the content of -- each input 'RVFI_Packet' if inputs are not succeeding the 'rvfiCheck' -rvfiCheckAndShow :: Bool -> Bool -> Bool -> Maybe RVFI_Packet -> Maybe RVFI_Packet -> [(RVFI_Packet -> Bool, String, Integer, String)] -> (Bool, String) -rvfiCheckAndShow pedantic singleImp is64 x y asserts - | singleImp, Just x' <- x, assertFails <- assertCheck is64 x' asserts = (null assertFails, " " ++ show x' ++ (suffix assertFails)) - | Just x' <- x, Just y' <- y, isNothing (rvfiCheck pedantic is64 x' y'), assertFails <- assertCheck is64 y' asserts = (null assertFails, " " ++ show x' ++ (suffix assertFails)) +rvfiCheckAndShow :: Bool -> Bool -> Bool -> Int -> Maybe RVFI_Packet -> Maybe RVFI_Packet -> [(RVFI_Packet -> Bool, String, Integer, String)] -> (Bool, String) +rvfiCheckAndShow pedantic singleImp is64 verbosity x y asserts + | singleImp, Just x' <- x, assertFails <- assertCheck is64 x' asserts = (null assertFails, " " ++ rvfiShowPacket x' verbosity ++ (suffix assertFails)) + | Just x' <- x, Just y' <- y, isNothing (rvfiCheck pedantic is64 x' y'), assertFails <- assertCheck is64 y' asserts = (null assertFails, " " ++ rvfiShowPacket x' verbosity ++ (suffix assertFails)) | Just x' <- x, Just y' <- y, mismatch <- rvfiCheck pedantic is64 x' y' = (False, unpack (Diff.pretty (def {Diff.separatorText = Just . pack $ "^ A, B v: " ++ fromJust mismatch}) - (pack $ " " ++ show x' ++ suffix (maybe [] (\x' -> assertCheck is64 x' asserts) x)) - (pack $ " " ++ show y' ++ suffix (maybe [] (\y' -> assertCheck is64 y' asserts) y)))) - | otherwise = (False, " A < " ++ maybe "No report received" show x ++ suffix (maybe [] (\x' -> assertCheck is64 x' asserts) x) - ++ "\n B > " ++ maybe "No report received" show y ++ suffix (maybe [] (\y' -> assertCheck is64 y' asserts) y)) + (pack $ " " ++ rvfiShowPacket x' verbosity ++ suffix (maybe [] (\x' -> assertCheck is64 x' asserts) x)) + (pack $ " " ++ rvfiShowPacket y' verbosity ++ suffix (maybe [] (\y' -> assertCheck is64 y' asserts) y)))) + | otherwise = (False, " A < " ++ maybe "No report received" (flip rvfiShowPacket verbosity) x ++ suffix (maybe [] (\x' -> assertCheck is64 x' asserts) x) + ++ "\n B > " ++ maybe "No report received" (flip rvfiShowPacket verbosity) y ++ suffix (maybe [] (\y' -> assertCheck is64 y' asserts) y)) where suffix assertFails = foldr (\(_,f,v,_) acc -> printf "%s (assert %s == 0x%x)" acc f v) "" asserts ++ foldl (\x y -> x ++ "\n " ++ y) "" assertFails diff --git a/stack.yaml b/stack.yaml index b00bab5..9537d83 100644 --- a/stack.yaml +++ b/stack.yaml @@ -8,3 +8,6 @@ packages: # forks / in-progress versions pinned to a git hash. extra-deps: - bitwise-1.0.0.1 # not included in the default resolver set + - regex-tdfa-1.3.1.0@sha256:bec13812a56a904ff3510caa19fe1b3ce3939e303604b1bcb3162771c52311ba,6324 + - regex-base-0.94.0.1@sha256:35ff2d13c0e3ac364469c19e4c7c8775f5148977d8fcef58a424df0a10a53fa7,2608 + - regex-posix-0.96.0.1@sha256:b6421e5356766b0c0a78b6094ae2e3a6259b42c147b717283c03c1cb09163dca,2920