Skip to content

Commit

Permalink
Allow CSR filter argument
Browse files Browse the repository at this point in the history
  • Loading branch information
@PeterRugg
PeterRugg committed Aug 15, 2023
1 parent b94f101 commit ff9ef87
Show file tree
Hide file tree
Showing 10 changed files with 108 additions and 127 deletions.
19 changes: 16 additions & 3 deletions src/QuickCheckVEngine/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}

module Main (main) where

Expand Down Expand Up @@ -101,6 +102,8 @@ data Options = Options
, optSave :: Bool
, optContinueOnFail:: Bool
, optIgnoreAsserts :: Bool
, csrIncludeRegex :: Maybe String
, csrExcludeRegex :: Maybe String
} deriving Show

defaultOptions :: Options
Expand All @@ -127,6 +130,8 @@ defaultOptions = Options
, optContinueOnFail= False
, optIgnoreAsserts = False
, optSingleImp = False
, csrIncludeRegex = Nothing
, csrExcludeRegex = Nothing
}

options :: [OptDescr (Options -> Options)]
Expand Down Expand Up @@ -197,6 +202,12 @@ options =
, Option [] ["single-implementation"]
(NoArg (\ opts -> opts { optSingleImp = True }))
"Run with only implementation A, testing asserts only (if enabled)"
, Option [] ["csr-include-regex"]
(ReqArg (\ f opts -> opts { csrIncludeRegex = Just f }) "REGEX")
"Specify REGEX to test only a subset of CSRs"
, Option [] ["csr-exclude-regex"]
(ReqArg (\ f opts -> opts { csrExcludeRegex = Just f }) "REGEX")
"Specify REGEX to exclude a subset of CSRs from tests"
]

commandOpts :: [String] -> IO (Options, [String])
Expand Down Expand Up @@ -265,8 +276,11 @@ main = withSocketsDo $ do
rawArgs <- getArgs
(flags, _) <- commandOpts rawArgs
when (optVerbosity flags > 1) $ print flags
let checkRegex incReg excReg str = (str =~ (fromMaybe ".*" incReg)) && (not $ str =~ (fromMaybe "a^" excReg))
let archDesc = arch flags
let testParams = T.TestParams { T.archDesc = archDesc }
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"
Expand Down Expand Up @@ -354,8 +368,7 @@ main = withSocketsDo $ do
Nothing -> do
case instrSoc of
Nothing -> do let tests = [ template | template@(label,_,_,_) <- allTests
, label =~ (fromMaybe ".*" (testIncludeRegex flags))
, not(label =~ (fromMaybe "a^" (testExcludeRegex flags)))]
, checkRegex (testIncludeRegex flags) (testExcludeRegex flags) label ]
when (null tests) $ putStrLn "Warning: no tests selected"
mapM_ attemptTest tests
where attemptTest (label, description, archReqs, template) =
Expand Down
5 changes: 3 additions & 2 deletions src/QuickCheckVEngine/Template.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ module QuickCheckVEngine.Template (

import Test.QuickCheck
import Data.Semigroup (Semigroup(..))
import RISCV (Instruction(..))
import RISCV (Instruction(..), CSRIdx)
import RISCV.ArchDesc
--import Data.Kind
--import Control.Applicative (liftA2)
Expand All @@ -90,7 +90,8 @@ import QuickCheckVEngine.RVFI_DII
-- | Micellaneous data indicating global parameters to
-- influence test generation, which should be passed
-- recursively to sub-templates.
data TestParams = TestParams { archDesc :: ArchDesc }
data TestParams = TestParams { archDesc :: ArchDesc
, csrFilter :: CSRIdx -> Bool }

data Template = TemplateEmpty
| TemplateSingle Instruction
Expand Down
3 changes: 2 additions & 1 deletion src/QuickCheckVEngine/Templates/GenAll.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ import QuickCheckVEngine.Templates.Utils
genAll :: Template
genAll = readParams $ \params -> random $ do
imm <- bits 12
csrIdx <- csr (csrFilter params)
src1 <- src
src2 <- src
src3 <- src
Expand Down Expand Up @@ -88,7 +89,7 @@ genAll = readParams $ \params -> random $ do
] | has_d desc && has_xlen_64 desc]
++ [[ (8, instUniform rv32_zifencei)
] | has_ifencei desc]
++ [[ (8, instUniform (rv32_zicsr src1 dest imm uimm))
++ [[ (8, maybe mempty (\idx -> instUniform (rv32_zicsr src1 dest idx uimm)) csrIdx)
] | has_icsr desc]
++ [[ (8, instUniform (rv32_xcheri desc src1 src2 srcScr imm mop dest))
] | has_cheri desc]
Expand Down
12 changes: 7 additions & 5 deletions src/QuickCheckVEngine/Templates/GenCHERI.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,18 +105,20 @@ genRandomCHERITest = readParams $ \param -> random $ do
csrAddr <- frequency [ (1, return (unsafe_csrs_indexFromName "mccsr"))
, (1, return (unsafe_csrs_indexFromName "mcause")) ]
srcScr <- elements $ [0, 1, 28, 29, 30, 31] ++ (if has_s arch then [12, 13, 14, 15] else []) ++ [2]
srcCsr <- elements [ unsafe_csrs_indexFromName "sepc"
, unsafe_csrs_indexFromName "mepc" ]
srcCsrRO <- elements [ unsafe_csrs_indexFromName "scause"
, unsafe_csrs_indexFromName "mcause" ]
let allowedCsrs = filter (csrFilter param) [ unsafe_csrs_indexFromName "sepc"
, unsafe_csrs_indexFromName "mepc" ]
let allowedCsrsRO = [ unsafe_csrs_indexFromName "scause"
, unsafe_csrs_indexFromName "mcause" ]
srcCsr <- if null allowedCsrs then return Nothing else Just <$> elements allowedCsrs
srcCsrRO <- elements allowedCsrsRO
return $ dist [ (5, legalLoad)
, (5, legalStore)
, (5, legalCapLoad srcAddr dest)
, (5, legalCapStore srcAddr)
, (10, instUniform $ rv32_i srcAddr srcData dest imm longImm fenceOp1 fenceOp2)
, (10, instUniform $ rv32_xcheri arch srcAddr srcData srcScr imm mop dest)
, (10, inst $ cspecialrw dest srcScr srcAddr)
, (5, instUniform $ rv32_zicsr srcData dest srcCsr mop)
, (5, maybe mempty (\idx -> instUniform $ rv32_zicsr srcData dest idx mop) srcCsr)
, (5, csrr dest srcCsrRO)
, (10, switchEncodingMode)
, (10, cspecialRWChain)
Expand Down
6 changes: 3 additions & 3 deletions src/QuickCheckVEngine/Templates/GenCSRs.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,12 +42,12 @@ import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils

gen_rv32_i_zicsr :: Template
gen_rv32_i_zicsr = random $
do any_csr <- bits 12
gen_rv32_i_zicsr = readParams $ \param -> random $
do any_csr <- csr $ csrFilter param
--valid_csr <- csr
uimm <- bits 5
src1 <- src
dest <- dest
-- TODO mix csr instructions with some i instructions
let insts = rv32_zicsr src1 dest any_csr uimm
let insts = maybe mempty (\idx -> rv32_zicsr src1 dest idx uimm) any_csr
return $ instUniform insts
2 changes: 1 addition & 1 deletion src/QuickCheckVEngine/Templates/GenFP.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ genFP has_f has_d has_xlen_64 = random $ do
++ [ rv32_d src1 src2 src3 dest rm imm | has_d ]
++ [ rv64_f src1 dest rm | has_f && has_xlen_64 ]
++ [ rv64_d src1 dest rm | has_d && has_xlen_64 ]
let epilogue = inst $ csrrs dest (unsafe_csrs_indexFromName "fcsr") 0
let epilogue = csrr dest (unsafe_csrs_indexFromName "fcsr")
return $ shrinkScope $ noShrink fp_prologue
<> repeatTillEnd (instUniform $ concat insts)
<> noShrink epilogue
15 changes: 8 additions & 7 deletions src/QuickCheckVEngine/Templates/GenMemory.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,6 @@ import Test.QuickCheck
import RISCV.RV32_I
import RISCV.RV32_A
import RISCV.RV32_Zifencei
import RISCV.RV32_Zicsr
import RISCV.RV64_I
import RISCV.RV32_Xcheri
import RISCV.RV_CSRs
Expand Down Expand Up @@ -202,17 +201,19 @@ gen_pte_perms = random $
add 5 5 6,
lui 7 0x40000,
slli 7 7 1,
sd 7 1 0,
csrrw 0 (unsafe_csrs_indexFromName "satp") 5,
csrrwi 0 (unsafe_csrs_indexFromName "sccsr") (clg0 * 4)]
sd 7 1 0]
<>
csrw (unsafe_csrs_indexFromName "satp") 5
<>
csrwi (unsafe_csrs_indexFromName "sccsr") (clg0 * 4)
<>
(noShrink $ inst $ sfence 0 0)
<> mconcat [
inst sret,
instUniform [ccleartag 3 3, cmove 3 3],
instUniform [sw 0 3 16, sq 0 3 16],
instUniform [lw 4 0 16, lq 4 0 16],
inst $ csrrwi 0 (unsafe_csrs_indexFromName "sccsr") (clg1 * 4),
csrwi (unsafe_csrs_indexFromName "sccsr") (clg1 * 4),
instUniform [lw 4 0 16, lq 4 0 16],
inst $ cgettag 5 4,
inst ecall]
Expand Down Expand Up @@ -242,7 +243,7 @@ gen_pte39_trans_core lxReg addrReg pteReg = random $
li64 lxReg l1pa,
inst $ sd lxReg pteReg 0,
li64 pteReg satp,
inst $ csrrw 0 (unsafe_csrs_indexFromName "satp") pteReg,
csrw (unsafe_csrs_indexFromName "satp") pteReg,
li64 addrReg addrInitial]
<>
(noShrink $ inst $ sfence 0 0)
Expand Down Expand Up @@ -280,7 +281,7 @@ gen_pte48_trans_core lxReg addrReg pteReg = random $
li64 lxReg l1pa,
inst $ sd lxReg pteReg 0,
li64 pteReg satp,
inst $ csrrw 0 (unsafe_csrs_indexFromName "satp") pteReg,
csrw (unsafe_csrs_indexFromName "satp") pteReg,
li64 addrReg addrInitial]
<>
(noShrink $ inst $ sfence 0 0)
Expand Down
89 changes: 40 additions & 49 deletions src/QuickCheckVEngine/Templates/GenTransExec.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,6 @@ import Test.QuickCheck
import RISCV.RV32_I
import RISCV.RV64_I
import RISCV.RV32_Xcheri
import RISCV.RV32_Zicsr
import RISCV.RV32_F
import RISCV.RV32_D
import RISCV.RV_CSRs
Expand Down Expand Up @@ -187,7 +186,7 @@ genTSCTorture = random $ do
, instUniform $ rv32_i_mem src1 src2 dest imm fenceOp1 fenceOp2
]
return $ mconcat [ access_inst
, inst $ csrrs src2 sstatus 0
, csrr src2 sstatus
, inst $ sret
]

Expand All @@ -196,10 +195,10 @@ prepareBSCExcpsGen = random $ do
let fcsr = unsafe_csrs_indexFromName "fcsr"
let mstatus = unsafe_csrs_indexFromName "mstatus"
let a0 = 10
return $ instSeq [ (lui a0 2)
, (csrrs 0 mstatus a0)
, (addi a0 0 192)
, (csrrs 0 fcsr a0)
return $ mconcat [ inst $ lui a0 2
, csrs mstatus a0
, inst $ addi a0 0 192
, csrs fcsr a0
]


Expand Down Expand Up @@ -239,46 +238,37 @@ prepareTSCGen = random $ do
let medeleg = unsafe_csrs_indexFromName "medeleg"
let sedeleg = unsafe_csrs_indexFromName "sedeleg"
let stval = unsafe_csrs_indexFromName "stval"
return $ instSeq [ (lui s1 0x100)
, (csrrc 0 mstatus s1)
, (lui s1 0x1)
, (csrrc 0 mstatus s1)
, (lui s1 0x1)
, (addi s1 s1 0x800)
, (csrrs 0 mstatus s1)
, (auipc s2 0)
, (addi s2 s2 16)
, (csrrw 0 mepc s2)
, (lui s2 0xa)
, (csrrw 0 medeleg s2)
]
<>
setUpPageTable
<>
(setupHPMEventSel counterReg hpmCntIdx evt)
<>
(enableHPMCounterM counterReg hpmCntIdx)
<>
instSeq [ (mret)
, (lui s0 0xfffe0)
, (addi s0 s0 1)
, (slli s0 s0 0x1b)
, (addi s0 s0 1)
, (slli s0 s0 0x13)
, (addi s0 s0 2)
, (csrrw 0 satp s0)
, (addi s1 s1 256)
, (csrrc 0 sstatus s1)
, (lui s2 2)
]
<>
(enableHPMCounterS counterReg hpmCntIdx)
<>
(li64 s2 0x80004000)
<>
instSeq[ (csrrw 0 sepc s2)
, (csrrw 0 stval s2)
, (sret)
return $ mconcat [ inst $ lui s1 0x100
, csrc mstatus s1
, inst $ lui s1 0x1
, csrc mstatus s1
, inst $ lui s1 0x1
, inst $ addi s1 s1 0x800
, csrs mstatus s1
, inst $ auipc s2 0
, inst $ addi s2 s2 16
, csrw mepc s2
, inst $ lui s2 0xa
, csrw medeleg s2
, setUpPageTable
, setupHPMEventSel counterReg hpmCntIdx evt
, enableHPMCounterM counterReg hpmCntIdx
, inst $ mret
, inst $ lui s0 0xfffe0
, inst $ addi s0 s0 1
, inst $ slli s0 s0 0x1b
, inst $ addi s0 s0 1
, inst $ slli s0 s0 0x13
, inst $ addi s0 s0 2
, csrw satp s0
, inst $ addi s1 s1 256
, csrc sstatus s1
, inst $ lui s2 2
, enableHPMCounterS counterReg hpmCntIdx
, li64 s2 0x80004000
, csrw sepc s2
, csrw stval s2
, inst $ sret
]

-- | Verify Data Capability Speculation Constraint (CSC)
Expand All @@ -297,7 +287,8 @@ gen_csc_data_verify = random $ do
, inst $ csealentry sldReg bitsReg
, inst $ candperm nopermReg bitsReg 0
, inst $ ccleartag bitsReg bitsReg
, inst $ lw tmpReg1 capReg 0 ]
, inst $ lw tmpReg1 capReg 0
]
let body = surroundWithHPMAccess_core False hpmEventIdx_dcache_miss (repeatTillEnd (genCSCDataTorture capReg tmpReg1 bitsReg sldReg nopermReg authReg)) tmpReg0 hpmCntIdx Nothing
let epilog = instAssert (addi tmpReg0 tmpReg0 0) 0
return $ shrinkScope $ noShrink prolog <> body <> noShrink epilog
Expand Down Expand Up @@ -466,8 +457,8 @@ gen_tsc_verify = random $ do
, li64 addrReg1 0x80001800
, li64 addrReg2 0x80012000
, li64 addrReg3 0x80008000
, inst $ csrrs tmpReg cntrIdx 0 ]
, csrr tmpReg cntrIdx ]
let body = repeatN (20) (genTSCTorture)
let epilog = mconcat [ inst $ csrrs counterReg cntrIdx 0
let epilog = mconcat [ csrr counterReg cntrIdx
, instAssert (sub counterReg counterReg tmpReg) 0 ]
return $ shrinkScope $ noShrink prolog <> body <> noShrink epilog
56 changes: 9 additions & 47 deletions src/QuickCheckVEngine/Templates/Utils/FP.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,57 +34,19 @@

module QuickCheckVEngine.Templates.Utils.FP (
fp_prologue
, fp_prologue_length
) where

import InstrCodec
import RISCV
import QuickCheckVEngine.Template

prologue_list :: ArchDesc -> [Instruction]
prologue_list arch = [ lui 1 2
, csrrs 0 (unsafe_csrs_indexFromName "mstatus") 1
, csrrs 0 (unsafe_csrs_indexFromName "fcsr") 0
]
++ (if has_f arch || has_d arch then
[ fmv_w_x 0 0
, fmv_w_x 1 0
, fmv_w_x 2 0
, fmv_w_x 3 0
, fmv_w_x 4 0
--, fmv_w_x 5 0
--, fmv_w_x 6 0
--, fmv_w_x 7 0
--, fmv_w_x 8 0
--, fmv_w_x 9 0
--, fmv_w_x 10 0
--, fmv_w_x 11 0
--, fmv_w_x 12 0
--, fmv_w_x 13 0
--, fmv_w_x 14 0
--, fmv_w_x 15 0
, op 16 0
, op 17 0
, op 18 0
, op 19 0
, op 20 0
--, op 21 0
--, op 22 0
--, op 23 0
--, op 24 0
--, op 25 0
--, op 26 0
--, op 27 0
--, op 28 0
--, op 29 0
--, op 30 0
--, op 31 0
--, op 32 0
] else [])
where op = if has_d arch then fmv_d_x else fmv_w_x
import QuickCheckVEngine.Templates.Utils.General

fp_prologue :: Template
fp_prologue = readParams $ \param -> instSeq $ prologue_list $ archDesc param

fp_prologue_length :: ArchDesc -> Int
fp_prologue_length = length . prologue_list
fp_prologue = mconcat [ inst $ lui 1 2
, csrs (unsafe_csrs_indexFromName "mstatus") 1
, csrs (unsafe_csrs_indexFromName "fcsr") 0
, readParams $ \p -> if has_f (archDesc p) || has_d (archDesc p)
then mconcat $ [inst $ fmv_w_x i 0 | i <- [0..4]]
++ [inst $ (if has_d (archDesc p) then fmv_d_x else fmv_w_x) i 0 | i <- [16..20]]
else mempty
]
Loading

0 comments on commit ff9ef87

Please sign in to comment.