Codeccheck review

.github/workflows/haskell.yml

@@ -2,9 +2,9 @@ name: Haskell CI
 
 on:
   push:
-    branches: [ "master" ]
+    branches: [ "master", "cheriot-rebase" ]
   pull_request:
-    branches: [ "master" ]
+    branches: [ "master", "cheriot-rebase" ]
 
 permissions:
   contents: read
@@ -29,10 +29,12 @@ jobs:
       - uses: haskell-actions/setup@v2
         with:
           ghc-version: '9.8'
-          cabal-version: '3.8'
+          cabal-version: '3.12'
       - name: Install dependencies
         run: |
           cabal update
-          cabal build --only-dependencies
+          cabal build --only-dependencies --enable-tests all
       - name: Build
-        run: cabal build all
+        run: cabal build --enable-tests all
+      - name: Codec self-check
+        run: cabal test --test-show-details=direct CodecCheck

QCVEngine.cabal

@@ -1,13 +1,15 @@
+cabal-version:       2.4
 name:                QCVEngine
 version:             0.1.0.0
 build-type:          Simple
 extra-source-files:  README.md
-cabal-version:       >=1.10
 
-executable QCVEngine
+-- Everything but Main, shared by the executable and the CodecCheck test suite. A named
+-- (internal) library, so that the target QCVEngine still means only the executable
+-- (cabal list-bin QCVEngine in TestRIG's Makefile).
+library qcvengine-lib
   hs-source-dirs:      src
-  main-is:             QuickCheckVEngine/Main.hs
-  other-modules:       InstrCodec,
+  exposed-modules:     InstrCodec,
                        RISCV,
                        RISCV.Helpers,
                        RISCV.ArchDesc,
@@ -74,31 +76,24 @@ executable QCVEngine
                        directory >= 1.3.8.5
   default-language:    Haskell2010
 
+-- hs-source-dirs is Main's own directory, not src, so the other modules come from the library
+-- instead of being compiled into the executable a second time.
+executable QCVEngine
+  hs-source-dirs:      src/QuickCheckVEngine
+  main-is:             Main.hs
+  build-depends:       qcvengine-lib,
+                       base >=4.9, time, network >=2.8, bytestring >=0.10,
+                       filemanip >=0.3, QuickCheck >= 2.12 && < 2.15,
+                       regex-tdfa >= 1.3, containers >= 0.6.5.1,
+                       cereal >= 0.5.8.3, temporary >= 1.3, directory >= 1.3.8.5
+  default-language:    Haskell2010
+
 -- Encoder/decoder self-check of the RISC-V instruction descriptions:
 -- cabal test CodecCheck
 test-suite CodecCheck
   type:                exitcode-stdio-1.0
-  hs-source-dirs:      test, src
+  hs-source-dirs:      test
   main-is:             CodecCheck.hs
-  other-modules:       InstrCodec,
-                       RISCV.Helpers,
-                       RISCV.ArchDesc,
-                       RISCV.InstInspect,
-                       RISCV.RV32_I,
-                       RISCV.RV32_M,
-                       RISCV.RV32_A,
-                       RISCV.RV32_F,
-                       RISCV.RV32_D,
-                       RISCV.RV32_Zifencei,
-                       RISCV.RV32_Zicsr,
-                       RISCV.RV32_Xcheri,
-                       RISCV.RV64_I,
-                       RISCV.RV64_M,
-                       RISCV.RV64_A,
-                       RISCV.RV64_F,
-                       RISCV.RV64_D,
-                       RISCV.RV_C,
-                       RISCV.RV_CSRs
-  build-depends:       base >=4.9, split >=0.2, regex-posix >=0.95,
-                       QuickCheck >= 2.12 && < 2.15
+  build-depends:       qcvengine-lib,
+                       base >=4.9, QuickCheck >= 2.12 && < 2.15
   default-language:    Haskell2010

src/QuickCheckVEngine/Main.hs

@@ -287,6 +287,10 @@
            , ("capmisc",    "Xcheri Extension Capability Miscellaneous Verification", has_cheri,                                T.repeatTillEnd genCHERImisc)
            , ("capcontrol", "Xcheri Extension Capability Control Flow Verification",  has_cheri,                                T.repeatTillEnd genCHERIcontrol)
            , ("capcache",   "Xcheri Extension Cache Verification",                    has_cheri,                                T.repeatTillEnd gen_rv32_Xcheri_cache)
+             -- has_cheri, not has_icsr: CHERIoT arch strings (e.g. rv32emcZifencei_Xcheriot) name no
+             -- Zicsr. Which CSRs are reached is decided by --csr-include-regex/--csr-exclude-regex
+             -- (guardCSR), as for the csrr in randomCHERITest.
+           , ("capcsr",     "CHERIoT Counter CSR ASR Permission Verification",        has_cheri,                                T.repeatTillEnd genCHERIoTCounterCSR)
            , ("capcache64", "RV64 Xcheri Extension Cache Verification",               andPs [has_cheri, has_xlen_64],           T.repeatTillEnd gen_rv64_Xcheri_cache)
            , ("capdecode",  "Xcheri Extension Capability Decode Template",            has_cheri,                                T.repeatTillEnd capDecodeTest)
            , ("cloadtags",  "Xcheri Extension CLoadTags Template",                    andPs [has_cheri, not . has_nocloadtags], T.repeatTillEnd cLoadTagsTest)
@@ -307,11 +311,11 @@
   (flags, _) <- commandOpts rawArgs
   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 = fromList $ filter csrFilter $ [0..4095] }
   -- initialize model and implementation sockets
   implA <- rvfiDiiOpen (impAIP flags) (impAPort flags) verbosity "implementation-A" (optForceRVFIv1 flags)
   m_implB <- if optSingleImp flags then return Nothing else Just <$> rvfiDiiOpen (impBIP flags) (impBPort flags) verbosity "implementation-B" (optForceRVFIv1 flags)
@@ -327,7 +331,7 @@
         quickCheckWithResult (Args Nothing 1 1 len (verbosity > 0) (if doShrink then 100000 else 0))
                              (prop implA m_implB alive statsTmp 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 $ map Instr [ csrrs 1 (unsafe_csrs_indexFromName "mcause") 0
                                                             , csrrs 1 (unsafe_csrs_indexFromName "mtval" ) 0 ]
@@ -369,7 +373,7 @@
   let checkResult = if verbosity > 1 then verboseCheckWithResult else quickCheckWithResult
   let checkGen gen remainingTests =
         checkResult (Args Nothing remainingTests 1 (testLen flags) (verbosity > 0) (if optShrink flags then 100000 else 0))
                     (prop implA m_implB alive statsTmp (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
@@ -409,7 +413,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/Templates/GenCHERI.hs

@@ -42,7 +42,8 @@ module QuickCheckVEngine.Templates.GenCHERI (
   genCHERIinspection,
   genCHERIarithmetic,
   genCHERImisc,
-  genCHERIcontrol
+  genCHERIcontrol,
+  genCHERIoTCounterCSR
 ) where
 
 import Test.QuickCheck
@@ -237,3 +238,33 @@ genCHERIcontrol = random $ do
   return $ dist [ -- (2, instUniform $ rv32_xcheri_control srcAddr srcData dest) -- CHERIoT lacks cinvoke and jalr_cap (jalr.cap) instr
                   (1, inst (csetbounds dest srcData srcAddr))
                 , (2, instUniform $ rv32_i srcAddr srcData dest imm longImm fenceOp1 fenceOp2) ] -- TODO add csr
+
+-- | Exercise the counter CSRs that CHERIoT permits without the ASR permission.
+--   ext_check_CSR() in cheri_addr_checks.sail admits *reads* of mcycle (0xB00),
+--   minstret (0xB02), mcycleh (0xB80), minstreth (0xB82) and the unprivileged
+--   cycle/time/instret(h) shadows while PCC lacks ASR, but requires ASR for any
+--   write.  Reads and writes are mixed with clearASR, so both halves of that
+--   rule are reached.  clearASR writes PCC without ASR to mtcc and then jumps to
+--   the null capability, so it traps into that mtcc; ASR does not come back
+--   within a test, and only the accesses before the first clearASR have it.
+--
+--   No other template reaches these: allowedCsrsRO in randomCHERITest holds
+--   only mcause, and the other genCHERI* templates leave CSRs as "TODO add csr".
+--   That gap let an ibex_decoder safe-list covering just 0xC00-0xC9F -- omitting
+--   the four 0xB counters -- go unnoticed until CHERIoT RTOS hung on csrr mcycle.
+genCHERIoTCounterCSR :: Template
+genCHERIoTCounterCSR = random $ do
+  srcData    <- src
+  -- clearASR writes mtcc from tmpReg masked by tmpReg2: with x0 or the same register for both,
+  -- mtcc gets a null, untagged or permissionless capability and every later trap fetches from it
+  tmpReg     <- src `suchThat` (/= 0)
+  tmpReg2    <- src `suchThat` (\r -> r /= 0 && r /= tmpReg)
+  dest       <- dest
+  counterCsr <- elements $ map unsafe_csrs_indexFromName
+                  [ "mcycle", "minstret", "mcycleh", "minstreth"
+                  , "cycle",  "time",     "instret"
+                  , "cycleh", "timeh",    "instreth" ]
+  return $ dist [ (10, csrr dest counterCsr)
+                , (10, csrw counterCsr srcData)
+                , (10, mconcat [ clearASR tmpReg tmpReg2, csrr dest counterCsr ])
+                , (10, mconcat [ clearASR tmpReg tmpReg2, csrw counterCsr srcData ]) ]

src/RISCV/Helpers.hs

@@ -103,7 +103,11 @@ module RISCV.Helpers (
 , prettyIgnr3
 -- * Others
 , reg
+, reg'
+, fpReg
+, fpReg'
 , int
+, toSigned
 , fpRoundingMode
 , PrivMode
 , privString
@@ -295,7 +299,7 @@ prettyF pred succ =
 
 -- | Pretty printer for sfence.vma instructions
 prettySfence rs2 rs1 =
-  concat ["sfence.vma ", int rs1, ", ", int rs2]
+  concat ["sfence.vma ", reg rs1, ", ", reg rs2]
 
 -- | R-type, 2-operand instruction pretty printer
 prettyR_2op instr cs1 cd =

src/RISCV/InstInspect.hs

@@ -80,27 +80,15 @@ rv_pretty instr ixl = case decode 32 instr instList of
   Just i -> i
   where -- RV64 ld/sd share their encodings with CHERI clc/csc, so the first table to match wins.
         -- Decode as RV64 only when the trace says RV64 (ixl 2); otherwise (RV32, or no ixl, as
-        -- in Show) the RV32 and Xcheri tables come first.
-        instList | ixl == Just 2 =    rv32_i_disass ++ rv64_i_disass
-                                   ++ rv32_m_disass ++ rv64_m_disass
-                                   ++ rv32_a_disass ++ rv64_a_disass
-                                   ++ rv32_f_disass ++ rv64_f_disass
-                                   ++ rv32_d_disass ++ rv64_d_disass
-                                   ++ rv32_zicsr_disass
-                                   ++ rv32_zifencei_disass
-                                   ++ rv32_xcheri_disass
-                                   ++ rv_c_disass ixl
-                 | otherwise   =    rv32_i_disass
-                                   ++ rv32_m_disass
-                                   ++ rv32_a_disass
-                                   ++ rv32_f_disass
-                                   ++ rv32_d_disass
-                                   ++ rv32_zicsr_disass
-                                   ++ rv32_zifencei_disass
-                                   ++ rv32_xcheri_disass
-                                   ++ rv_c_disass ixl
-                                   ++ rv64_i_disass ++ rv64_m_disass ++ rv64_a_disass
-                                   ++ rv64_f_disass ++ rv64_d_disass
+        -- in Show) the RV32 and Xcheri tables come first and the RV64 tables last.
+        instList | ixl == Just 2 = concat (zipWith (++) rv32 rv64) ++ rest
+                 | otherwise     = concat rv32 ++ rest ++ concat rv64
+        rv32 = [rv32_i_disass, rv32_m_disass, rv32_a_disass, rv32_f_disass, rv32_d_disass]
+        rv64 = [rv64_i_disass, rv64_m_disass, rv64_a_disass, rv64_f_disass, rv64_d_disass]
+        rest =    rv32_zicsr_disass
+               ++ rv32_zifencei_disass
+               ++ rv32_xcheri_disass
+               ++ rv_c_disass ixl
 
 instance Show Instruction where
   show i@(MkInstruction v) = printf ".4byte 0x%08x # %s" v (rv_pretty i Nothing)
@@ -109,7 +97,7 @@ rv_extract :: Instruction -> ExtractedRegs
 rv_extract instr = case decode 32 instr extractList of
   Nothing -> (False, Nothing, Nothing, Nothing, (\a b c -> instr))
   Just i -> i
-  where extractList = rv32_i_extract ++ rv32_xcheri_extract
+  where extractList = rv32_i_extract ++ rv32_m_extract ++ rv32_xcheri_extract
 
 rv_shrink :: Instruction -> [Instruction]
 rv_shrink instr = case decode 32 instr shrinkList of

src/RISCV/RV32_I.hs

@@ -292,6 +292,9 @@ extract_uimm instr uimm rd = (False, Nothing, Nothing, Just rd, \x y z -> encode
 extract_nodst :: String -> Integer -> Integer -> Integer -> ExtractedRegs
 extract_nodst instr imm rs2 rs1 = (False, Just rs2, Just rs1, Nothing, \x y z -> encode instr imm x y)
 
+extract_sfence :: Integer -> Integer -> ExtractedRegs
+extract_sfence rs2 rs1 = (False, Just rs2, Just rs1, Nothing, \x y z -> encode sfence_raw x y)
+
 rv32_i_extract :: [DecodeBranch ExtractedRegs]
 rv32_i_extract = [ add_raw    --> extract_2op add_raw
                  , slt_raw    --> extract_2op slt_raw
@@ -330,6 +333,7 @@ rv32_i_extract = [ add_raw    --> extract_2op add_raw
                  , sb_raw     --> extract_nodst sb_raw
                  , sh_raw     --> extract_nodst sh_raw
                  , sw_raw     --> extract_nodst sw_raw
+                 , sfence_raw --> extract_sfence
 --               , fence_raw  --> noextract
 --               , fence_tso_raw --> noextract
 --               , resrvd_raw --> noextract

src/RISCV/RV32_M.hs

@@ -52,12 +52,14 @@ module RISCV.RV32_M (
 , remu
 -- * RV32 multiply/divide, others
 , rv32_m_disass
+, rv32_m_extract
 , rv32_m
 ) where
 
 import Prelude hiding (rem, div)
 
-import RISCV.Helpers (prettyR)
+import RISCV.Helpers (prettyR, ExtractedRegs)
+import RISCV.RV32_I (extract_2op)
 import InstrCodec (DecodeBranch, (-->), encode, Instruction)
 
 mul_raw           =                   "0000001 rs2[4:0] rs1[4:0] 000 rd[4:0] 0110011"
@@ -77,6 +79,18 @@ rem rd rs1 rs2    = encode rem_raw             rs2      rs1          rd
 remu_raw          =                   "0000001 rs2[4:0] rs1[4:0] 111 rd[4:0] 0110011"
 remu rd rs1 rs2   = encode remu_raw            rs2      rs1          rd
 
+-- | Register extraction for rv_extract (all R-type)
+rv32_m_extract :: [DecodeBranch ExtractedRegs]
+rv32_m_extract = [ mul_raw    --> extract_2op mul_raw
+                 , mulh_raw   --> extract_2op mulh_raw
+                 , mulhsu_raw --> extract_2op mulhsu_raw
+                 , mulhu_raw  --> extract_2op mulhu_raw
+                 , div_raw    --> extract_2op div_raw
+                 , divu_raw   --> extract_2op divu_raw
+                 , rem_raw    --> extract_2op rem_raw
+                 , remu_raw   --> extract_2op remu_raw
+                  ]
+
 -- | Dissassembly of RV32 multiply/divide instructions
 rv32_m_disass :: [DecodeBranch String]
 rv32_m_disass = [ mul_raw    --> prettyR "mul"

src/RISCV/RV32_Xcheri.hs

@@ -111,6 +111,7 @@ module RISCV.RV32_Xcheri (
 -- , amoswap_q -- CHERIoT lacks amoswap_q (amoswap.c/q) atomic instr
 -- * RISC-V CHERI, others
 , rv32_xcheri_disass
+, name_scr
 , rv32_xcheri_extract
 , rv32_xcheri_shrink
 , rv32_xcheri
@@ -355,24 +356,27 @@ pretty_2src instr src2 src1 = concat [instr, " ", reg src1, ", ", reg src2]
 -- | Pretty-print a special capability read/write instruction
 pretty_cspecialrw instr idx cs1 cd =
   concat [instr, " ", reg cd, ", ", name_scr idx, ", ", reg cs1]
-  where name_scr 0 = "pcc"
-        name_scr 1 = "ddc"
-        name_scr 3 = "utidc"
-        name_scr 4 = "utcc"
-        name_scr 5 = "utdc"
-        name_scr 6 = "uscratchc"
-        name_scr 7 = "uepcc"
-        name_scr 11 = "stidc"
-        name_scr 12 = "stcc"
-        name_scr 13 = "stdc"
-        name_scr 14 = "sscratchc"
-        name_scr 15 = "sepcc"
-        name_scr 27 = "mtidc"
-        name_scr 28 = "mtcc"
-        name_scr 29 = "mtdc"
-        name_scr 30 = "mscratchc"
-        name_scr 31 = "mepcc"
-        name_scr idx = int idx
+
+-- | Name of a special capability register (SCR) index
+name_scr :: Integer -> String
+name_scr 0 = "pcc"
+name_scr 1 = "ddc"
+name_scr 3 = "utidc"
+name_scr 4 = "utcc"
+name_scr 5 = "utdc"
+name_scr 6 = "uscratchc"
+name_scr 7 = "uepcc"
+name_scr 11 = "stidc"
+name_scr 12 = "stcc"
+name_scr 13 = "stdc"
+name_scr 14 = "sscratchc"
+name_scr 15 = "sepcc"
+name_scr 27 = "mtidc"
+name_scr 28 = "mtcc"
+name_scr 29 = "mtdc"
+name_scr 30 = "mscratchc"
+name_scr 31 = "mepcc"
+name_scr idx = int idx
 
 -- | Dissassembly of CHERI instructions
 rv32_xcheri_disass :: [DecodeBranch String]

src/RISCV/RV_C.hs

@@ -336,6 +336,7 @@ rv_c_32_disass = [ pad c_fld_raw          --> prettyCL_F "c.fld"
                  , pad c_addw_raw         --> prettyCA "c.addw.res"
 
                  , pad c_slli_nse_raw     --> prettyCI_swap "c.slli.nse"
+                 , pad c_slli64_hint0_raw --> "c.slli64.hint" -- before c_slli64_raw, which also matches rd == 0
                  , pad c_slli64_raw       --> prettyCI_reg "c.slli64.hint"
                  , pad c_fldsp_raw        --> prettyCI_F "c.fldsp"
                  , pad c_flwsp_raw        --> prettyCI_F "c.flwsp"
@@ -357,6 +358,7 @@ rv_c_64_disass = [ pad c_fld_raw          --> prettyCL_F "c.fld"
                  , pad c_subw_raw         --> prettyCA "c.subw"
                  , pad c_addw_raw         --> prettyCA "c.addw"
 
+                 , pad c_slli64_hint0_raw --> "c.slli64.hint" -- before c_slli64_raw, which also matches rd == 0
                  , pad c_slli64_raw       --> prettyCI_reg "c.slli64.hint"
                  , pad c_ldsp_res_raw     --> prettyCI_imm  "c.ldsp.res"
                  , pad c_ldsp_raw         --> prettyCI      "c.ldsp"
@@ -378,6 +380,7 @@ rv_c_128_disass = [ pad c_lq_raw           --> prettyCL   "c.lq"
                   , pad c_subw_raw         --> prettyCA "c.subw"
                   , pad c_addw_raw         --> prettyCA "c.addw"
 
+                  , pad c_slli64_hint0_raw --> "c.slli64.hint" -- before c_slli64_raw, which also matches rd == 0
                   , pad c_slli64_raw       --> prettyCI_reg "c.slli64"
                   , pad c_lqsp_res_raw     --> prettyCI_imm "c.lqsp.res"
                   , pad c_lqsp_raw         --> prettyCI     "c.lqsp"
@@ -407,6 +410,7 @@ rv_c_multi_disass = [ pad c_lq_raw           --> prettyIgnr3 "c.fld (RV32DC/RV64
                     , pad c_addw_raw         --> prettyCA "c.addw.res (RV32C) / c.addw (RV64C/RV128C)"
 
                     , pad c_slli_nse_raw     --> prettyIgnr2 "c.slli.nse (RV32C) / c.slli (RV64C/RV128C)"
+                    , pad c_slli64_hint0_raw --> "c.slli64.hint" -- before c_slli64_raw, which also matches rd == 0
                     , pad c_slli64_raw       --> prettyCI_reg "c.slli64.hint (RV32C/RV64C) / c.slli64 (RV128C)"
                     , pad c_lqsp_res_raw     --> prettyIgnr1 "c.fldsp (RV32DC/RV64DC) / c.lqsp.res (RV128C)"
                     , pad c_lqsp_raw         --> prettyIgnr2 "c.fldsp (RV32DC/RV64DC) / c.lqsp (RV128C)"
@@ -451,7 +455,6 @@ rv_c_common_disass = [ pad c_illegal_raw      --> "c.illegal"
                      , pad c_beqz_raw         --> prettyCB_sig 9 "c.beqz"
                      , pad c_bnez_raw         --> prettyCB_sig 9 "c.bnez"
 
-                     , pad c_slli64_hint0_raw --> "c.slli64.hint"
                      , pad c_slli_hint_raw    --> prettyCI_imm "c.slli.hint"
                      , pad c_slli_raw         --> prettyCI_swap "c.slli"
                      , pad c_lwsp_res_raw     --> prettyCI_imm  "c.lwsp.res"