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

Miscellaneous tidying from reading through #57

Merged
merged 4 commits into from
Jan 9, 2025
Merged

Miscellaneous tidying from reading through #57

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d444481
Move some CHERI tests from Utils.CHERI to GenCHERI
nwf Dec 31, 2024
80f475c
Be explicit about Templates.Utils.* imports
nwf Dec 31, 2024
c357f27
Test is not Arbitrary
nwf Dec 31, 2024
5cb14ab
mainhelpers function arg docs
nwf Dec 31, 2024
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
1 change: 0 additions & 1 deletion QCVEngine.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ executable QCVEngine
QuickCheckVEngine.TestTypes,
QuickCheckVEngine.Test,
QuickCheckVEngine.Template,
QuickCheckVEngine.Templates.Utils,
QuickCheckVEngine.Templates.Utils.General,
QuickCheckVEngine.Templates.Utils.FP,
QuickCheckVEngine.Templates.Utils.HPM,
Expand Down
1 change: 0 additions & 1 deletion src/QuickCheckVEngine/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,6 @@
import QuickCheckVEngine.RVFI_DII
import qualified QuickCheckVEngine.Template as T
import QuickCheckVEngine.Test
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.GenAll
import QuickCheckVEngine.Templates.GenArithmetic
import QuickCheckVEngine.Templates.GenMemory
Expand Down Expand Up @@ -282,7 +281,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 284 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 284 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 @@ -300,7 +299,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

Check warning on line 302 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 any ▫︎ Found: "or (hasTrap <$> trace)" ▫︎ Perhaps: "any hasTrap 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
Expand Down Expand Up @@ -340,7 +339,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) (if (optSaveAll flags) then (saveDir flags) else Nothing) (optIgnoreAsserts flags) (optStrict flags) gen)

Check warning on line 342 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: "if (optSaveAll flags) then (saveDir flags) else Nothing" ▫︎ Perhaps: "if optSaveAll flags then (saveDir flags) else Nothing"

Check warning on line 342 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: "if (optSaveAll flags) then (saveDir flags) else Nothing" ▫︎ Perhaps: "if (optSaveAll flags) then saveDir flags else Nothing"
failuresRef <- newIORef 0
let checkFile (memoryInitFile :: Maybe FilePath) (skipped :: Int) (fileName :: FilePath)
| skipped == 0 = do putStrLn $ "Reading trace from " ++ fileName
Expand Down Expand Up @@ -380,7 +379,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)

Check warning on line 382 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 382 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 382 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))
Expand Down
40 changes: 32 additions & 8 deletions src/QuickCheckVEngine/MainHelpers.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ import RISCV hiding (and, or)
import QuickCheckVEngine.RVFI_DII
import QuickCheckVEngine.Test
import qualified QuickCheckVEngine.Template as T
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.General

instance Show DII_Packet where
show (DII_End _) = "# Test end"
Expand Down Expand Up @@ -151,8 +151,16 @@ wrapTest = (<> single (diiEnd, Nothing, Nothing))
. (f <$>)
where f (MkInstruction i) = (diiInstruction i, Nothing, Nothing)

runImpls :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> Int -> Int -> Maybe FilePath -> Test TestResult
-> (Test TestResult -> IO a) -> (Test DII_Packet -> IO a) -> (Test DII_Packet -> IO a)
runImpls :: RvfiDiiConnection -- ^ Implementation A connection
-> Maybe RvfiDiiConnection -- ^ Implementation B connection
-> IORef Bool -- ^ Implementations still alive?
-> Int -- ^ RVFI-DII delay
-> Int -- ^ Verbosity
-> Maybe FilePath -- ^ Optional save directory for failed tests
-> Test TestResult -- ^ Test to run
-> (Test TestResult -> IO a) -- ^ Callback: report from implementations
-> (Test DII_Packet -> IO a) -- ^ Callback: first implementation disconnect
-> (Test DII_Packet -> IO a) -- ^ Callback: already disconnected implementations
-> IO a
runImpls connA m_connB alive delay verbosity saveDir test onTrace onFirstDeath onSubsequentDeaths = do
let instTrace = (\(x, _, _) -> x) <$> test
Expand All @@ -169,10 +177,20 @@ runImpls connA m_connB alive delay verbosity saveDir test onTrace onFirstDeath o
-- for equivalence. It receives among other things a callback function
-- 'Test -> IO ()' to be performed on failure that takes in the reduced
-- 'Test' which caused the failure
prop :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> (Test TestResult -> IO ())
-> ArchDesc -> Int -> Int -> Maybe FilePath -> Bool -> Bool -> Gen (Test TestResult) -> Property
prop :: RvfiDiiConnection -- ^ Implementation A connection
-> Maybe RvfiDiiConnection -- ^ Implementation B connection
-> IORef Bool -- ^ Implementations still alive?
-> (Test TestResult -> IO ()) -- ^ Callback on falsification
-> ArchDesc -- ^ Archictecture description
-> Int -- ^ RVFI-DII Delay
-> Int -- ^ Verbosity
-> Maybe FilePath -- ^ Optional save directory for failed tests
-> Bool -- ^ Ignore embedded asserts in tests
-> Bool -- ^ Strict RVFI response comparison
-> Gen (Test TestResult) -- ^ Test generator
-> Property
prop connA m_connB alive onFail arch delay verbosity saveDir ignoreAsserts strict gen =
forAllShrink gen shrink mkProp
forAllShrink gen shrinkTest mkProp
where mkProp test = whenFail (onFail test) (doProp test)
doProp test = monadicIO $ run $ runImpls connA m_connB alive delay verbosity saveDir test onTrace onFirstDeath onSubsequentDeaths
colourGreen = "\ESC[32m"
Expand Down Expand Up @@ -203,8 +221,14 @@ prop connA m_connB alive onFail arch delay verbosity saveDir ignoreAsserts stric
-- 'Just (traceA, traceB)', otherwise 'Nothing' and sets the provided
-- 'IORef Bool' for alive to 'False' indicating that further interaction with
-- the implementations is futile
doRVFIDII :: RvfiDiiConnection -> Maybe RvfiDiiConnection -> IORef Bool -> Int
-> Int -> Maybe FilePath -> Test TestResult -> IO (Maybe (Test TestResult))
doRVFIDII :: RvfiDiiConnection -- ^ Implementation A connection
-> Maybe RvfiDiiConnection -- ^ Implementation B connection
-> IORef Bool -- ^ Implementations still alive?
-> Int -- ^ RVFI-DII delay
-> Int -- ^ Verbosity
-> Maybe FilePath -- ^ Optional save directory for failed tests
-> Test TestResult -- ^ Input instruction sequence
-> IO (Maybe (Test TestResult))
doRVFIDII connA m_connB alive delay verbosity saveDir test = do
let instTrace = (\(x, _, _) -> x) <$> test
let insts = instTrace
Expand Down
3 changes: 2 additions & 1 deletion src/QuickCheckVEngine/Templates/GenAll.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,8 @@ import Test.QuickCheck
import RISCV
import RISCV.ArchDesc
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.FP
import QuickCheckVEngine.Templates.Utils.General

genAll :: Template
genAll = readParams $ \params -> random $ do
Expand Down
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenArithmetic.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ import Test.QuickCheck
import RISCV.RV32_I
import RISCV.RV64_I
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.General

gen_rv32_i_arithmetic :: Template
gen_rv32_i_arithmetic = random $ do
Expand Down
3 changes: 2 additions & 1 deletion src/QuickCheckVEngine/Templates/GenAtomics.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,8 @@ import RISCV.RV32_A
import RISCV.RV64_A
import RISCV.RV32_Xcheri
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.CHERI
import QuickCheckVEngine.Templates.Utils.General

gen_rv32_a :: Template
gen_rv32_a = readParams $ \p -> genAtomics False (has_cheri (archDesc p))
Expand Down
72 changes: 70 additions & 2 deletions src/QuickCheckVEngine/Templates/GenCHERI.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,21 @@ module QuickCheckVEngine.Templates.GenCHERI (
gen_simple_cclear,
gen_simple_fpclear,
randomCHERITest,
randomCHERIRVCTest
randomCHERIRVCTest,
genCHERIinspection,
genCHERIarithmetic,
genCHERImisc,
genCHERIcontrol
) where

import Test.QuickCheck
import Control.Monad
import RISCV
import InstrCodec
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.CHERI
import QuickCheckVEngine.Templates.Utils.FP
import QuickCheckVEngine.Templates.Utils.General
import QuickCheckVEngine.Templates.GenArithmetic
import QuickCheckVEngine.Templates.GenFP
import QuickCheckVEngine.Templates.GenCompressed
Expand Down Expand Up @@ -163,3 +169,65 @@ gen_simple_fpclear = random $ do

randomCHERITest :: Template
randomCHERITest = fp_prologue $ repeatTillEnd genRandomCHERITest

genCHERIinspection :: Template
genCHERIinspection = random $ do
srcAddr <- src
srcData <- src
dest <- dest
imm <- bits 12
longImm <- bits 20
fenceOp1 <- bits 3
fenceOp2 <- bits 3
csrAddr <- frequency [ (1, return (unsafe_csrs_indexFromName "mccsr"))
, (1, return (unsafe_csrs_indexFromName "mcause"))
, (1, bits 12) ]
return $ dist [ (1, instUniform $ rv32_xcheri_inspection srcAddr dest)
, (1, instUniform $ rv32_i srcAddr srcData dest imm longImm fenceOp1 fenceOp2) ] -- TODO add csr

genCHERIarithmetic :: Template
genCHERIarithmetic = random $ do
srcAddr <- src
srcData <- src
dest <- dest
imm <- bits 12
longImm <- bits 20
fenceOp1 <- bits 3
fenceOp2 <- bits 3
csrAddr <- frequency [ (1, return (unsafe_csrs_indexFromName "mccsr"))
, (1, return (unsafe_csrs_indexFromName "mcause"))
, (1, bits 12) ]
return $ dist [ (1, instUniform $ rv32_xcheri_arithmetic srcAddr srcData imm dest)
, (1, instUniform $ rv32_i srcAddr srcData dest imm longImm fenceOp1 fenceOp2) ] -- TODO add csr

genCHERImisc :: Template
genCHERImisc = random $ do
srcAddr <- src
srcData <- src
dest <- dest
imm <- bits 12
longImm <- bits 20
fenceOp1 <- bits 3
fenceOp2 <- bits 3
srcScr <- elements [0, 1, 28, 29, 30, 31]
csrAddr <- frequency [ (1, return (unsafe_csrs_indexFromName "mccsr"))
, (1, return (unsafe_csrs_indexFromName "mcause"))
, (1, bits 12) ]
return $ dist [ (1, instUniform $ rv32_xcheri_misc srcAddr srcData srcScr imm dest)
, (1, instUniform $ rv32_i srcAddr srcData dest imm longImm fenceOp1 fenceOp2) ] -- TODO add csr

genCHERIcontrol :: Template
genCHERIcontrol = random $ do
srcAddr <- src
srcData <- src
dest <- dest
imm <- bits 12
longImm <- bits 20
fenceOp1 <- bits 3
fenceOp2 <- bits 3
csrAddr <- frequency [ (1, return (unsafe_csrs_indexFromName "mccsr"))
, (1, return (unsafe_csrs_indexFromName "mcause"))
, (1, bits 12) ]
return $ dist [ (2, instUniform $ rv32_xcheri_control srcAddr srcData dest)
, (1, inst (csetbounds dest srcData srcAddr))
, (2, instUniform $ rv32_i srcAddr srcData dest imm longImm fenceOp1 fenceOp2) ] -- TODO add csr
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenCSRs.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ module QuickCheckVEngine.Templates.GenCSRs (
import RISCV.RV32_I
import RISCV.RV32_Zicsr
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.General

gen_rv32_i_zicsr :: Template
gen_rv32_i_zicsr = readParams $ \param -> random $
Expand Down
3 changes: 2 additions & 1 deletion src/QuickCheckVEngine/Templates/GenCompressed.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,8 @@ module QuickCheckVEngine.Templates.GenCompressed (

import RISCV.RV_C
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.Compressed
import QuickCheckVEngine.Templates.Utils.General

gen_rv_c :: Template
gen_rv_c = random $ do
Expand Down
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenControlFlow.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ import InstrCodec
import Test.QuickCheck
import RISCV.RV32_I
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.General

gen_rv32_i_controlflow :: Template
gen_rv32_i_controlflow = genControlFlow
Expand Down
3 changes: 2 additions & 1 deletion src/QuickCheckVEngine/Templates/GenFP.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,8 @@ module QuickCheckVEngine.Templates.GenFP (
import InstrCodec
import RISCV
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.FP
import QuickCheckVEngine.Templates.Utils.General
import Test.QuickCheck

gen_rv32_f :: Template
Expand Down
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenHPM.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ module QuickCheckVEngine.Templates.GenHPM (

import RISCV
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.HPM
import QuickCheckVEngine.Templates.RandomTest

genHPM :: Template
Expand Down
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenMemory.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ import RISCV.RV64_I
import RISCV.RV32_Xcheri
import RISCV.RV_CSRs
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.General
import Data.Bits
import qualified RISCV.ArchDesc as Arch

Expand Down
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenMulDiv.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ module QuickCheckVEngine.Templates.GenMulDiv (
import RISCV.RV32_M
import RISCV.RV64_M
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.General

gen_rv32_m :: Template
gen_rv32_m = genMulDiv False
Expand Down
4 changes: 3 additions & 1 deletion src/QuickCheckVEngine/Templates/GenTransExec.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,9 @@ import RISCV.RV_CSRs
import RISCV.ArchDesc
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.GenMemory
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.CHERI
import QuickCheckVEngine.Templates.Utils.HPM
import QuickCheckVEngine.Templates.Utils.General
import QuickCheckVEngine.RVFI_DII.RVFI
import QuickCheckVEngine.Templates.GenMemory
import Data.Bits
Expand Down
3 changes: 2 additions & 1 deletion src/QuickCheckVEngine/Templates/RandomTest.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,8 @@ module QuickCheckVEngine.Templates.RandomTest (
import Test.QuickCheck
import RISCV
import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils
import QuickCheckVEngine.Templates.Utils.FP
import QuickCheckVEngine.Templates.Utils.General

-- | 'randomTest' provides a 'Template' for a random test
randomTest :: Template
Expand Down
53 changes: 0 additions & 53 deletions src/QuickCheckVEngine/Templates/Utils.hs
View file
Open in desktop

This file was deleted.

Loading
Loading