Make RVFI packet debug use verbosity level 4

src/QuickCheckVEngine/Main.hs

@@ -280,15 +280,16 @@
   -- 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
@@ -299,7 +300,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
         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
@@ -308,9 +309,9 @@
               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 @@
       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 @@
                               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
@@ -379,7 +380,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)
                       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))

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

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) $

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

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