Changed pendantic to strict and changed default behaviour

CTSRD-CHERI · Apr 25, 2024 · cea1f33 · cea1f33
1 parent 123be4b
commit cea1f33
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 20 deletions.
diff --git 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
@@ -171,15 +171,15 @@ 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
         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

diff --git 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 ""