From 3b1ffef49f0ebb780ca6bad6af9cfc9b2aae8e67 Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 15:31:22 +0100 Subject: [PATCH 1/8] RV_C: make the c.slli64.hint (rd == 0) disassembly entry reachable c_slli64_raw also matches rd == 0 and came first in every table, so the c_slli64_hint0 entry in rv_c_common_disass was never used: 0x0002 printed as "c.slli64.hint x0". Move the entry ahead of c_slli64_raw in each XLEN table; CodecCheck now expects "c.slli64.hint". --- src/RISCV/RV_C.hs | 5 ++++- test/CodecCheck.hs | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/RISCV/RV_C.hs b/src/RISCV/RV_C.hs index 1925ca2..fcdab13 100644 --- a/src/RISCV/RV_C.hs +++ b/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" diff --git a/test/CodecCheck.hs b/test/CodecCheck.hs index 14aa50a..ca9dc66 100644 --- a/test/CodecCheck.hs +++ b/test/CodecCheck.hs @@ -242,7 +242,7 @@ rvcEntries = , ent "c_bnez" (E2 C.c_bnez) ["rs1'", "imm"] rv32c $ \v -> ops "c.bnez" [cr v "rs1'", sg 9 v "imm"] -- Quadrant 2 , ent "c_slli64" (E1 C.c_slli64) ["rs1_rd_nz"] rv128c $ \v -> ops "c.slli64" [xr v "rs1_rd_nz"] - , ent "c_slli64_hint0" (E0 C.c_slli64_hint0) [] rv32c $ \_ -> "c.slli64.hint x0" -- matches c_slli64_raw first + , ent "c_slli64_hint0" (E0 C.c_slli64_hint0) [] rv32c $ \_ -> "c.slli64.hint" , ent "c_slli64_hintx" (E1 C.c_slli64_hintx) ["rs1_rd_nz"] rv32c $ \v -> ops "c.slli64.hint" [xr v "rs1_rd_nz"] , ent "c_slli" (E2 C.c_slli) ["rs1_rd_nz", "nzuimm"] rv32c $ \v -> ops "c.slli" [xr v "rs1_rd_nz", un v "nzuimm"] , assuming (\v -> not (testBit (val v "nzuimm") 5)) $ -- shamt[5] set is c.slli.nse x0 on RV32 From 5108423aa48d6df0589bbef7b39ae717fce75d40 Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 15:32:43 +0100 Subject: [PATCH 2/8] Helpers: print sfence.vma operands as registers prettySfence formatted rs1/rs2 with int, so sfence.vma x27, x19 printed as "sfence.vma 27, 19". Use reg, as every other register operand does; CodecCheck now expects register names. --- src/RISCV/Helpers.hs | 2 +- test/CodecCheck.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/RISCV/Helpers.hs b/src/RISCV/Helpers.hs index 0e292c1..a2a9f4f 100644 --- a/src/RISCV/Helpers.hs +++ b/src/RISCV/Helpers.hs @@ -295,7 +295,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 = diff --git a/test/CodecCheck.hs b/test/CodecCheck.hs index ca9dc66..28b1aad 100644 --- a/test/CodecCheck.hs +++ b/test/CodecCheck.hs @@ -296,7 +296,7 @@ rv32iEntries = ++ [ ent n e ["rs1", "rs2", "imm"] rv32i $ \v -> ops n [xr v "rs2", mem (xr v "rs1") (sg 12 v "imm")] | (n, e) <- [("sb", E3 I.sb), ("sh", E3 I.sh), ("sw", E3 I.sw)] ] ++ [ ent "fence" (E2 I.fence) ["pred", "succ"] rv32i $ \v -> ops "fence" [un v "pred", un v "succ"] - , ent "sfence" (E2 I.sfence) ["rs1", "rs2"] rv32i $ \v -> ops "sfence.vma" [un v "rs1", un v "rs2"] + , ent "sfence" (E2 I.sfence) ["rs1", "rs2"] rv32i $ \v -> ops "sfence.vma" [xr v "rs1", xr v "rs2"] , ent "fence_tso" (E0 I.fence_tso) [] rv32i $ \_ -> "fence.tso" , ent "resrvd" (E0 I.resrvd) [] rv32i $ \_ -> "reserved" , ent "mret" (E0 I.mret) [] rv32i $ \_ -> "mret" From 9fb5a8f47d7a0aeea9b91a4d89a12cc90d6291a6 Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 16:36:57 +0100 Subject: [PATCH 3/8] rv_extract: cover the M extension and sfence.vma rv_extract, which bypassShrink uses to substitute registers when shrinking a failing test, had no entries for mul/mulh/mulhsu/mulhu/div/divu/rem/remu or sfence.vma, so shrinking never rewired their registers. Add rv32_m_extract (R-type, via RV32_I's extract_2op) and an sfence entry in rv32_i_extract. --- src/RISCV/InstInspect.hs | 2 +- src/RISCV/RV32_I.hs | 4 ++++ src/RISCV/RV32_M.hs | 10 +++++++++- 3 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/RISCV/InstInspect.hs b/src/RISCV/InstInspect.hs index a8bbf0c..90e96ec 100644 --- a/src/RISCV/InstInspect.hs +++ b/src/RISCV/InstInspect.hs @@ -109,7 +109,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 diff --git a/src/RISCV/RV32_I.hs b/src/RISCV/RV32_I.hs index 4a1e96d..45d7c68 100644 --- a/src/RISCV/RV32_I.hs +++ b/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 diff --git a/src/RISCV/RV32_M.hs b/src/RISCV/RV32_M.hs index b3b4302..eda3833 100644 --- a/src/RISCV/RV32_M.hs +++ b/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,12 @@ 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 = [ r --> extract_2op r + | r <- [ mul_raw, mulh_raw, mulhsu_raw, mulhu_raw + , div_raw, divu_raw, rem_raw, remu_raw ] ] + -- | Dissassembly of RV32 multiply/divide instructions rv32_m_disass :: [DecodeBranch String] rv32_m_disass = [ mul_raw --> prettyR "mul" From 3485b58f2dd2729da15e02943fb886c8e5d2abed Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 16:38:52 +0100 Subject: [PATCH 4/8] CodecCheck: address review comments; check rv_extract Changes from the review of the codec self-check: - Expected disassembly uses the source formatters (reg, reg', fpReg, fpReg', toSigned from RISCV.Helpers; name_scr, now top level in RV32_Xcheri) instead of copies of them in the test. - Argument generation retries up to 1000 draws instead of using suchThatMaybe, which made a single draw at size 0 and failed encoders with restricted fields (c.addi4spn, c.slli hint) at random. - The static per-entry checks are a separate pass (staticCheck) and are reported apart from the random checks. - Formats without arguments run once, the rest 200 times. New check: for every 32-bit format with register fields, rv_extract must return the encoded registers, re-encode to the original instruction, and substitute fresh registers without changing any other bit. The register mask comes from the token layout (encodingMask), not the field values. This check found the missing M/sfence.vma entries fixed in the previous commit. --- src/RISCV/Helpers.hs | 4 + src/RISCV/RV32_Xcheri.hs | 40 +++-- test/CodecCheck.hs | 358 +++++++++++++++++---------------------- 3 files changed, 183 insertions(+), 219 deletions(-) diff --git a/src/RISCV/Helpers.hs b/src/RISCV/Helpers.hs index a2a9f4f..aacee1f 100644 --- a/src/RISCV/Helpers.hs +++ b/src/RISCV/Helpers.hs @@ -103,7 +103,11 @@ module RISCV.Helpers ( , prettyIgnr3 -- * Others , reg +, reg' +, fpReg +, fpReg' , int +, toSigned , fpRoundingMode , PrivMode , privString diff --git a/src/RISCV/RV32_Xcheri.hs b/src/RISCV/RV32_Xcheri.hs index be4018a..5c6490c 100644 --- a/src/RISCV/RV32_Xcheri.hs +++ b/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] diff --git a/test/CodecCheck.hs b/test/CodecCheck.hs index 28b1aad..9079359 100644 --- a/test/CodecCheck.hs +++ b/test/CodecCheck.hs @@ -18,43 +18,28 @@ truncates each value to its field, so a mistake still builds and still produces legal-looking instructions. - Each entry below names an encoder and, in the encoder's parameter order, - the format field each parameter must land in. For every entry: - - static: the encoder is run at the 'Probe' result type, which records the - format string and the argument list it passed to 'encode'. The - argument count must equal the number of distinct fields, and - parameter k must land in the field the table names for it. - - random: distinct random values per field are encoded and - (a) decoded with the format ('rhsArgs'), which must give back - what 'encode' was given; - (b) disassembled with the module's own disassembly table, which - must print the expected text, written below per instruction - from the assembly syntax by field NAME, never by position; - (c) for RV32 instructions with an entry in 'rv_extract', the - extracted rs1/rs2/rd must be the encoded registers and - re-encoding them must give the same instruction. - - The table is hand-written: Haskell cannot list a module's encoders or - recover their parameter names. A new encoder is covered only once it is - added here. + Each entry names an encoder and, in its parameter order, the field each + parameter must land in. The encoder must route every parameter to that + field (static check); for random values, the module's disassembly table + must print the expected text and, for 32-bit instructions with registers, + 'rv_extract' must return them and re-encode the instruction. The 'rv_shrink' + tables are not checked. The table is hand-written: a new encoder is covered + only once it is added here. -} module Main (main) where -import Control.Monad (forM, unless) -import Data.Bits ((.&.), (.|.), bit, shiftL, testBit) +import Control.Monad (filterM, unless) +import Data.Bits ((.&.), (.|.), bit, complement, shiftL, testBit) import Data.List (elemIndex, intercalate, isInfixOf, sort) import Data.Maybe (fromMaybe, listToMaybe) import System.Exit (exitFailure) import Test.QuickCheck hiding ((.&.)) import Text.Printf (printf) -import InstrCodec ( Encode (..), Instruction (..), DecodeBranch, Token (..) - , tokenise, tokenWidth, rangedVars, rhsArgs, fromBitList - , decode, (#) ) -import qualified InstrCodec +import InstrCodec ( Encode (..), Instruction (..), DecodeBranch, Token (..), tokenise, tokenWidth + , rangedVars, decode ) +import RISCV.Helpers (reg, reg', fpReg, fpReg', int, toSigned) import RISCV.InstInspect (rv_extract, rv_pretty) import qualified RISCV.RV_C as C import qualified RISCV.RV32_I as I @@ -70,10 +55,6 @@ data Probe = Probe String [Integer] instance Encode Integer Probe where enc args fmt = Probe fmt args --- | The instruction the encoder builds when used at type 'Instruction' -probeInstr :: Probe -> Instruction -probeInstr (Probe fmt args) = enc args fmt - -- | An encoder, at its arity. Nullary encoders are monomorphic -- 'Instruction's (monomorphism restriction) and cannot be probed. data Enc = E0 Instruction @@ -93,6 +74,11 @@ runEnc (E2 f) [a, b] = f a b runEnc (E3 f) [a, b, c] = f a b c runEnc _ _ = error "runEnc: arity mismatch" +-- | The instruction the encoder builds from these arguments +instrOf :: Enc -> [Integer] -> Instruction +instrOf (E0 i) _ = i +instrOf e vs = let Probe fmt args = runEnc e vs in enc args fmt + -- * Formats fields :: String -> [String] @@ -102,8 +88,18 @@ fieldMask :: String -> String -> Integer fieldMask fmt v = foldl (.|.) 0 [bit i | Range w hi lo <- tokenise fmt, w == v, i <- [lo .. hi]] -fmtWidth :: String -> Int -fmtWidth = sum . map tokenWidth . tokenise +-- | The bits of the encoding that hold the named fields ('tokenise' lists the +-- tokens LSB first) +encodingMask :: String -> [String] -> Integer +encodingMask fmt names = go 0 (tokenise fmt) 0 + where + go _ [] m = m + go pos (t : ts) m = + let w = tokenWidth t + m' = case t of + Range n _ _ | n `elem` names -> foldl (.|.) m [bit i | i <- [pos .. pos + w - 1]] + _ -> m + in go (pos + w) ts m' -- * Table entries @@ -115,26 +111,26 @@ type Table = (String, [DecodeBranch String]) data Entry = Entry { eName :: String , eEnc :: Enc - , eParams :: [String] -- ^ field of each encoder parameter, in parameter order - , eTable :: Maybe Table -- ^ disassembly table to decode with - , eExpect :: Env -> String -- ^ expected disassembly - , eAssume :: Env -> Bool -- ^ restricts values to this encoding (see 'assuming') + , eParams :: [String] -- ^ field of each encoder parameter, in parameter order + , eDis :: Maybe (Table, Env -> String) -- ^ disassembly table and expected text + , eAssume :: Env -> Bool -- ^ restricts values to this encoding (see 'assuming') } ent :: String -> Enc -> [String] -> Table -> (Env -> String) -> Entry -ent name enc ps tbl expect = Entry name enc ps (Just tbl) expect (const True) +ent name e ps tbl expect = Entry name e ps (Just (tbl, expect)) (const True) -- | No disassembly check: the table decodes this encoding as something else noDis :: String -> Enc -> [String] -> Entry -noDis name enc ps = Entry name enc ps Nothing (const "") (const True) +noDis name e ps = Entry name e ps Nothing (const True) --- | Values outside this predicate decode as an earlier, overlapping entry --- of the disassembly table. Fields named *nz* are kept non-zero and --- fields named *n2* are kept /= 2 without needing this. +-- | Values outside this predicate decode as an earlier, overlapping entry of +-- the disassembly table. Fields named *nz* are kept non-zero and fields +-- named *n2* /= 2 by 'genArgs', which infers that from the name. assuming :: (Env -> Bool) -> Entry -> Entry assuming p e = e { eAssume = p } --- ** Expected-text helpers, by field name +-- ** Expected text, by field name. Register and immediate spelling comes from +-- RISCV.Helpers: the check is which field lands in which operand slot. val :: Env -> String -> Integer val env n = fromMaybe (error $ "expected text refers to unknown field " ++ n) @@ -147,32 +143,21 @@ ops m os = m ++ " " ++ intercalate ", " os mem :: String -> String -> String mem base off = base ++ "[" ++ off ++ "]" -xr, cr, fr, cfr, un :: Env -> String -> String -xr v n = "x" ++ show (val v n) -- integer register -cr v n = "x" ++ show (val v n + 8) -- RVC 3-bit integer register -fr v n = "f" ++ show (val v n) -- FP register -cfr v n = "f" ++ show (val v n + 8) -- RVC 3-bit FP register -un v n = show (val v n) -- unsigned immediate - -signed :: Int -> Integer -> Integer -signed w i = if testBit i (w - 1) then i - bit w else i +xr, cr, fr, cfr, un, scr :: Env -> String -> String +xr v n = reg (val v n) -- integer register +cr v n = reg' (val v n) -- RVC 3-bit integer register +fr v n = fpReg (val v n) -- FP register +cfr v n = fpReg' (val v n) -- RVC 3-bit FP register +un v n = int (val v n) -- unsigned immediate +scr v n = X.name_scr (val v n) -- special capability register -- | Signed immediate of width w sg :: Int -> Env -> String -> String -sg w v n = show (signed w (val v n)) +sg w v n = int (toSigned w (val v n)) -- | Signed immediate of width w held in units of 2 bytes (jal, branches) sg2 :: Int -> Env -> String -> String -sg2 w v n = show (signed w (val v n `shiftL` 1)) - --- | Special capability register names (the CHERI SCR numbering) -scr :: Env -> String -> String -scr v n = case val v n of - 0 -> "pcc"; 1 -> "ddc" - 3 -> "utidc"; 4 -> "utcc"; 5 -> "utdc"; 6 -> "uscratchc"; 7 -> "uepcc" - 11 -> "stidc"; 12 -> "stcc"; 13 -> "stdc"; 14 -> "sscratchc"; 15 -> "sepcc" - 27 -> "mtidc"; 28 -> "mtcc"; 29 -> "mtdc"; 30 -> "mscratchc"; 31 -> "mepcc" - i -> show i +sg2 w v n = int (toSigned w (val v n `shiftL` 1)) -- * The tables @@ -184,7 +169,7 @@ rv32i = ("rv32_i_disass", I.rv32_i_disass) rv32m = ("rv32_m_disass", M.rv32_m_disass) xcheri = ("rv32_xcheri_disass", X.rv32_xcheri_disass) --- | Every encoder exported by RISCV.RV_C +-- | Encoders exported by RISCV.RV_C rvcEntries :: [Entry] rvcEntries = -- Quadrant 0 @@ -270,7 +255,7 @@ rvcEntries = , ent "c_sdsp" (E2 C.c_sdsp) ["rs2", "uimm"] rv64c $ \v -> ops "c.sdsp" [xr v "rs2", un v "uimm"] ] --- | Every encoder exported by RISCV.RV32_I +-- | Encoders exported by RISCV.RV32_I rv32iEntries :: [Entry] rv32iEntries = [ ent n e ["rd", "rs1", "rs2"] rv32i $ \v -> ops n [xr v "rd", xr v "rs1", xr v "rs2"] @@ -303,7 +288,7 @@ rv32iEntries = , ent "ecall" (E0 I.ecall) [] rv32i $ \_ -> "ecall" , ent "ebreak" (E0 I.ebreak) [] rv32i $ \_ -> "ebreak" ] --- | Every encoder exported by RISCV.RV32_M +-- | Encoders exported by RISCV.RV32_M rv32mEntries :: [Entry] rv32mEntries = [ ent n e ["rd", "rs1", "rs2"] rv32m $ \v -> ops n [xr v "rd", xr v "rs1", xr v "rs2"] @@ -311,7 +296,7 @@ rv32mEntries = , ("mulhu", E3 M.mulhu), ("div", E3 M.div), ("divu", E3 M.divu) , ("rem", E3 M.rem), ("remu", E3 M.remu) ] ] --- | Every encoder exported by RISCV.RV32_Xcheri +-- | Encoders exported by RISCV.RV32_Xcheri xcheriEntries :: [Entry] xcheriEntries = [ ent n e ["rd", "cs1"] xcheri $ \v -> ops n [xr v "rd", xr v "cs1"] @@ -342,138 +327,116 @@ xcheriEntries = , ent "clc" (E3 X.clc) ["cd", "cs1", "imm"] xcheri $ \v -> ops "clc" [xr v "cd", mem (xr v "cs1") (sg 12 v "imm")] , ent "csc" (E3 X.csc) ["cs2", "cs1", "imm"] xcheri $ \v -> ops "csc" [xr v "cs2", mem (xr v "cs1") (sg 12 v "imm")] ] -groups :: [(String, [Entry])] -groups = [ ("RV_C", rvcEntries), ("RV32_I", rv32iEntries) - , ("RV32_M", rv32mEntries), ("RV32_Xcheri", xcheriEntries) ] +entries :: [Entry] +entries = rvcEntries ++ rv32iEntries ++ rv32mEntries ++ xcheriEntries -- * Static check --- | The format and the argument list, from running the encoder on its own --- parameter indices 0, 1, ... -probeIndices :: Enc -> Probe -probeIndices enc = runEnc enc (map fromIntegral [0 .. arity enc - 1]) - -staticCheck :: Entry -> [String] -staticCheck e = case eEnc e of - E0 _ -> [ eName e ++ ": the test table lists parameters for a nullary encoder" - | not (null (eParams e)) ] - enc -> - let n = arity enc - Probe fmt args = probeIndices enc - fs = fields fmt - ps = eParams e - pname i = if i >= 0 && i < length ps then ps !! i else "?" - param i = printf "parameter %d (%s)" (i + 1) (pname i) :: String - hdr = printf "%s: format \"%s\", fields %s" (eName e) fmt (show fs) :: String - arityErr = [ printf " the test table names %d parameter(s) %s for an encoder of arity %d" - (length ps) (show ps) n - | length ps /= n ] - namesErr = [ printf " the test table's parameter names %s are not the format's fields" - (show ps) - | null arityErr, sort ps /= sort fs ] - countErr = [ printf " the encoder passes %d argument(s) to encode, the format has %d field(s): %s" - (length args) (length fs) - (intercalate ", " (map (param . fromInteger) args)) - | length args /= length fs ] - routeErr = [ printf " field %s receives %s, expected %s" f (param a') want - | null (arityErr ++ namesErr) - , (f, a) <- zip fs args - , let a' = fromInteger a - , let wantIdx = elemIndex f ps - , wantIdx /= Just a' - , let want = maybe "no parameter" param wantIdx ] - errs = arityErr ++ namesErr ++ countErr ++ routeErr - in [ unlines (hdr : errs) | not (null errs) ] +-- | The encoder must pass one argument per field, routing parameter k to the +-- field the table names for it. Returns the errors, or the format string. +staticCheck :: Entry -> Either String String +staticCheck e@Entry{ eEnc = E0 _ } + | null (eParams e) = Right "" -- a nullary encoder has no format to probe + | otherwise = Left (eName e ++ ": the test table names parameters for a nullary encoder\n") +staticCheck e = + let ec = eEnc e + n = arity ec + Probe fmt args = runEnc ec (map fromIntegral [0 .. n - 1]) + fs = fields fmt + ps = eParams e + pname i = if i >= 0 && i < length ps then ps !! i else "?" + param i = printf "parameter %d (%s)" (i + 1) (pname i) :: String + hdr = printf "%s: format \"%s\", fields %s" (eName e) fmt (show fs) :: String + arityErr = [ printf " the test table names %d parameter(s) %s for an encoder of arity %d" + (length ps) (show ps) n + | length ps /= n ] + namesErr = [ printf " the test table's parameter names %s are not the format's fields" + (show ps) + | null arityErr, sort ps /= sort fs ] + countErr = [ printf " the encoder passes %d argument(s) to encode, the format has %d field(s): %s" + (length args) (length fs) + (intercalate ", " (map (param . fromInteger) args)) + | length args /= length fs ] + routeErr = [ printf " field %s receives %s, expected %s" f (param a') want + | null (arityErr ++ namesErr) + , (f, a) <- zip fs args + , let a' = fromInteger a + , let wantIdx = elemIndex f ps + , wantIdx /= Just a' + , let want = maybe "no parameter" param wantIdx ] + errs = arityErr ++ namesErr ++ countErr ++ routeErr + in if null errs then Right fmt else Left (unlines (hdr : errs)) -- * Random check --- | Can the random check run? The parameter names must be the format's --- fields, and the encoder must supply every field. -randomOk :: Entry -> Maybe String -randomOk e = case eEnc e of - E0 _ -> Nothing - enc -> let Probe fmt args = probeIndices enc - fs = fields fmt - in if length (eParams e) == arity enc - && sort (eParams e) == sort fs - && length args >= length fs - then Just fmt - else Nothing - -genArgs :: Entry -> String -> Gen [Integer] -genArgs e fmt = mapM gen1 ps `suchThat` ok +-- | Values for the parameters, masked to their fields by 'mkEnv'. A bounded +-- retry, so that an 'assuming' no value can meet fails instead of hanging. +genArgs :: Entry -> String -> Gen (Maybe [Integer]) +genArgs e fmt = draw (1000 :: Int) where - ps = eParams e - m = fieldMask fmt - gen1 p = choose (0, bit (topBit (m p) + 1) - 1) - topBit x = last [i | i <- [0 .. 63], testBit x i] - ok vs = let env = mkEnv e fmt vs - in all valid env && distinct vs && eAssume e env + draw 0 = return Nothing + draw k = do + vs <- mapM (\p -> choose (0, fieldMask fmt p)) (eParams e) + if ok vs then return (Just vs) else draw (k - 1) + ok vs = let env = mkEnv e fmt vs in all valid env && eAssume e env valid (p, v) = (not ("nz" `isInfixOf` p) || v /= 0) && (not ("n2" `isInfixOf` p) || v /= 2) - -- Whichever parameter lands in a field, the field's value identifies it - distinct vs = and [ (vj .&. m p) /= (vi .&. m p) - | (p, vi) <- zip ps vs, (q, vj) <- zip ps vs, p /= q ] mkEnv :: Entry -> String -> [Integer] -> Env mkEnv e fmt vs = [ (p, v .&. fieldMask fmt p) | (p, v) <- zip (eParams e) vs ] prop_entry :: Entry -> String -> Property -prop_entry e fmt = forAll (genArgs e fmt) $ \vs -> - let pr@(Probe _ args) = runEnc (eEnc e) vs - i = probeInstr pr - enc32 = unMkInstruction i - env = mkEnv e fmt vs - fs = fields fmt - hdr = printf "%s %s\n format: \"%s\"\n encoding: 0x%08x\n" - (eName e) (unwords [p ++ "=" ++ show v | (p, v) <- zip (eParams e) vs]) - fmt enc32 :: String - -- (a) InstrCodec: the format decodes to what encode was given - sent = [ a .&. fieldMask fmt f | (f, a) <- zip fs args ] - decoded = map fromBitList (rhsArgs (fmtWidth fmt # enc32) (InstrCodec.tag (tokenise fmt))) - codecP = counterexample - (hdr ++ printf " InstrCodec: fields %s decode as %s, encode was given %s" - (show fs) (show decoded) (show sent)) - (decoded == sent) - -- (b) the module's disassembly table - disP = case eTable e of - Nothing -> property True - Just (tname, tbl) -> - let want = eExpect e env - got = decode 32 i tbl - in counterexample - (hdr ++ printf " disassembly (%s)\n expected: %s\n got: %s" - tname want (maybe "no match" id got)) - (got == Just want) - -- (c) rv_extract, where the instruction has an entry - extractP = case rv_extract i of - (_, Nothing, Nothing, Nothing, _) -> property True - (_, rs2, rs1, rd, reenc) -> - let look ns = listToMaybe [v | (p, v) <- env, p `elem` ns] - want = (look ["rs2", "cs2"], look ["rs1", "cs1"], look ["rd", "cd"]) - i' = reenc (fromMaybe 0 rs2) (fromMaybe 0 rs1) (fromMaybe 0 rd) - in counterexample - (hdr ++ printf " rv_extract (rs2, rs1, rd) = %s, expected %s" - (show (rs2, rs1, rd)) (show want)) - ((rs2, rs1, rd) == want) - .&&. counterexample - (hdr ++ printf " rv_extract re-encodes as 0x%08x" (unMkInstruction i')) - (i' == i) - in codecP .&&. disP .&&. extractP - --- | Nullary encoders: one deterministic disassembly check -nullaryCheck :: Entry -> [String] -nullaryCheck e = case (eEnc e, eTable e) of - (E0 i, Just (tname, tbl)) -> - let want = eExpect e [] - got = decode 32 i tbl - in [ printf "%s: encoding 0x%08x\n disassembly (%s)\n expected: %s\n got: %s\n" - (eName e) (unMkInstruction i) tname want (maybe "no match" id got) - | got /= Just want ] - _ -> [] +prop_entry e fmt = forAllShow (genArgs e fmt) (maybe "no values" show) $ \mvs -> case mvs of + Nothing -> counterexample (eName e ++ ": no values satisfy the field constraints and 'assuming'") False + Just vs -> + let i = instrOf (eEnc e) vs + env = mkEnv e fmt vs + hdr = printf "%s %s\n format: \"%s\"\n encoding: 0x%08x\n" + (eName e) (unwords [p ++ "=" ++ show v | (p, v) <- zip (eParams e) vs]) + fmt (unMkInstruction i) :: String + disP = case eDis e of + Nothing -> property True + Just ((tname, tbl), expect) -> + let want = expect env + got = decode 32 i tbl + in counterexample + (hdr ++ printf " disassembly (%s)\n expected: %s\n got: %s" + tname want (maybe "no match" id got)) + (got == Just want) + look ns = listToMaybe [v | (p, v) <- env, p `elem` ns] + want = (look ["rs2", "cs2"], look ["rs1", "cs1"], look ["rd", "cd"]) + regFields = [p | p <- eParams e, p `elem` ["rs2", "cs2", "rs1", "cs1", "rd", "cd"]] + keep = complement (encodingMask fmt regFields) + -- every 32-bit instruction with registers must be in rv_extract + extractP + | sum (map tokenWidth (tokenise fmt)) /= 32 || null regFields = property True + | otherwise = case rv_extract i of + (_, rs2, rs1, rd, reenc) -> + let i' = reenc (fromMaybe 0 rs2) (fromMaybe 0 rs1) (fromMaybe 0 rd) + regs = choose (0, 31) :: Gen Integer + in counterexample + (hdr ++ printf " rv_extract (rs2, rs1, rd) = %s, expected %s" + (show (rs2, rs1, rd)) (show want)) + ((rs2, rs1, rd) == want) + .&&. counterexample + (hdr ++ printf " rv_extract re-encodes as 0x%08x" (unMkInstruction i')) + (i' == i) + -- bypassShrink re-encodes with other registers: they must land in the + -- register fields, and no other bit may change + .&&. forAll ((,,) <$> regs <*> regs <*> regs) (\(a, b, c) -> + let i2 = reenc a b c + (_, rs2', rs1', rd', _) = rv_extract i2 + slot old new = new <$ old + in counterexample + (hdr ++ printf " re-encoding with (rs2, rs1, rd) = %s gives 0x%08x, extracted as %s" + (show (a, b, c)) (unMkInstruction i2) (show (rs2', rs1', rd'))) + ( (rs2', rs1', rd') == (slot rs2 a, slot rs1 b, slot rd c) + && unMkInstruction i2 .&. keep == unMkInstruction i .&. keep)) + in disP .&&. extractP -- | rv_pretty: CHERI clc/csc share their encodings with RV64 ld/sd. With no ixl (Show, saved --- reproducers) or an RV32 trace they must print as clc/csc; only an RV64 trace (ixl 2) gives ld/sd. +-- reproducers) or an RV32 trace they must print as clc/csc; only an RV64 trace (ixl 2) gives +-- ld/sd. Only the mnemonic is compared: the operands are the disassembly check's job. prettyChecks :: [String] prettyChecks = [ printf "rv_pretty %s (ixl %s): expected %s, got \"%s\"\n" n (show ixl) want got @@ -486,21 +449,14 @@ prettyChecks = main :: IO () main = do - let entries = concatMap snd groups - static = concatMap staticCheck entries ++ concatMap nullaryCheck entries ++ prettyChecks - mapM_ putStr static - failures <- forM entries $ \e -> case randomOk e of - Nothing -> return 0 - Just fmt -> do - r <- quickCheckWithResult stdArgs { maxSuccess = 200, chatty = False } - (prop_entry e fmt) - if isSuccess r then return (0 :: Int) - else putStrLn (output r) >> return 1 - let nRandom = length [() | e <- entries, Just _ <- [randomOk e]] - printf "CodecCheck: %d encoders (%s); %d with random round-trip checks\n" - (length entries) - (intercalate ", " [printf "%s %d" g (length es) | (g, es) <- groups] :: String) - nRandom - printf "CodecCheck: %d static failure(s), %d random-check failure(s)\n" - (length static) (sum failures) - unless (null static && sum failures == 0) exitFailure + let checked = [ (e, staticCheck e) | e <- entries ] + staticErrs = [ err | (_, Left err) <- checked ] ++ prettyChecks + mapM_ putStr staticErrs + failed <- flip filterM [ (e, fmt) | (e, Right fmt) <- checked ] $ \(e, fmt) -> do + let runs = if arity (eEnc e) == 0 then 1 else 200 + r <- quickCheckWithResult stdArgs { maxSuccess = runs, chatty = False } (prop_entry e fmt) + unless (isSuccess r) (putStrLn (output r)) + return (not (isSuccess r)) + printf "CodecCheck: %d encoders, %d static/rv_pretty failure(s), %d random-check failure(s)\n" + (length entries) (length staticErrs) (length failed) + unless (null staticErrs && null failed) exitFailure From 55c83b555a336f3d996500b7c3feb0ffc43d213f Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 16:43:44 +0100 Subject: [PATCH 5/8] rv_pretty: build both table orders from the same lists The RV64 and non-RV64 branches listed the same disassembly tables twice in different orders. Build both from shared rv32/rv64/rest lists; each order is unchanged (RV64: each RV32 table followed by its RV64 counterpart; otherwise RV64 tables last, so clc/csc win over ld/sd). --- src/RISCV/InstInspect.hs | 30 +++++++++--------------------- 1 file changed, 9 insertions(+), 21 deletions(-) diff --git a/src/RISCV/InstInspect.hs b/src/RISCV/InstInspect.hs index 90e96ec..629aebd 100644 --- a/src/RISCV/InstInspect.hs +++ b/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) From 95bb5321609e5d7e2c08c061bf2a4d4e80e7e660 Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 16:57:57 +0100 Subject: [PATCH 6/8] Build the shared modules once as a library; run CodecCheck in CI The executable and the CodecCheck test suite each listed and compiled the same modules. Move everything but Main into an internal library, qcvengine-lib, that both depend on. It is a named library, not the package's main library, so the target QCVEngine still means only the executable (TestRIG's Makefile runs cabal list-bin QCVEngine). This needs cabal-version 2.4. CI built neither the test suite nor ran it, and only ran for master. Add cheriot-rebase, build with --enable-tests and run cabal test CodecCheck. cabal 3.8 predates GHC 9.8: use 3.12. --- .github/workflows/haskell.yml | 12 +++++---- QCVEngine.cabal | 47 ++++++++++++++++------------------- 2 files changed, 28 insertions(+), 31 deletions(-) diff --git a/.github/workflows/haskell.yml b/.github/workflows/haskell.yml index 34f0d3c..bb171fb 100644 --- a/.github/workflows/haskell.yml +++ b/.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 diff --git a/QCVEngine.cabal b/QCVEngine.cabal index 55fdd4a..321529e 100644 --- a/QCVEngine.cabal +++ b/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 From 190441d37731236da6fb64d435bb7e458d797221 Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 16:58:26 +0100 Subject: [PATCH 7/8] CodecCheck: check rv_extract's bypass flag; hint in all RV_C tables The bypass flag decides whether bypassShrink replaces an instruction by a move, and nothing checked it. Expect it set for cmove and for addi with immediate 0 only; random values almost never give addi 0, so that case is also a fixed check. The c.slli64.hint (rd == 0) fix changed four tables and only the RV32 one was checked: check RV64 and RV128 as well. rv32_m_extract: one entry per line, like the other tables. --- src/RISCV/RV32_M.hs | 12 +++++++++--- test/CodecCheck.hs | 28 +++++++++++++++++++++++++--- 2 files changed, 34 insertions(+), 6 deletions(-) diff --git a/src/RISCV/RV32_M.hs b/src/RISCV/RV32_M.hs index eda3833..3af4be9 100644 --- a/src/RISCV/RV32_M.hs +++ b/src/RISCV/RV32_M.hs @@ -81,9 +81,15 @@ 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 = [ r --> extract_2op r - | r <- [ mul_raw, mulh_raw, mulhsu_raw, mulhu_raw - , div_raw, divu_raw, rem_raw, remu_raw ] ] +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] diff --git a/test/CodecCheck.hs b/test/CodecCheck.hs index 9079359..bcbe07b 100644 --- a/test/CodecCheck.hs +++ b/test/CodecCheck.hs @@ -411,10 +411,14 @@ prop_entry e fmt = forAllShow (genArgs e fmt) (maybe "no values" show) $ \mvs -> extractP | sum (map tokenWidth (tokenise fmt)) /= 32 || null regFields = property True | otherwise = case rv_extract i of - (_, rs2, rs1, rd, reenc) -> + (bypass, rs2, rs1, rd, reenc) -> let i' = reenc (fromMaybe 0 rs2) (fromMaybe 0 rs1) (fromMaybe 0 rd) regs = choose (0, 31) :: Gen Integer in counterexample + (hdr ++ printf " rv_extract bypass flag = %s, expected %s" + (show bypass) (show (bypassExpected (eName e) env))) + (bypass == bypassExpected (eName e) env) + .&&. counterexample (hdr ++ printf " rv_extract (rs2, rs1, rd) = %s, expected %s" (show (rs2, rs1, rd)) (show want)) ((rs2, rs1, rd) == want) @@ -445,18 +449,36 @@ prettyChecks = , let got = rv_pretty i ixl , takeWhile (/= ' ') got /= want ] +-- | rv_extract's bypass flag, which makes bypassShrink replace the instruction by a move: set +-- only for the plain register moves, cmove and addi with immediate 0. +bypassExpected :: String -> Env -> Bool +bypassExpected n v = n == "cmove" || (n == "addi" && val v "imm" == 0) + +-- | Cases the random values almost never reach: addi with immediate 0 (the bypass), and the +-- c.slli64.hint (rd == 0) entry in the RV64 and RV128 tables (the entries check RV32 only). +fixedChecks :: [String] +fixedChecks = + [ printf "rv_extract (addi x%d, x%d, 0): bypass flag False, expected True\n" rd rs1 + | (rd, rs1) <- [(1, 2), (0, 0), (31, 17)] :: [(Integer, Integer)] + , let (bypass, _, _, _, _) = rv_extract (I.addi rd rs1 0) + , not bypass ] + ++ [ printf "%s: c_slli64_hint0 disassembles as %s, expected c.slli64.hint\n" tname (show got) + | (tname, tbl) <- [rv64c, rv128c] + , let got = decode 32 (C.c_slli64_hint0 :: Instruction) tbl + , got /= Just "c.slli64.hint" ] + -- * Driver main :: IO () main = do let checked = [ (e, staticCheck e) | e <- entries ] - staticErrs = [ err | (_, Left err) <- checked ] ++ prettyChecks + staticErrs = [ err | (_, Left err) <- checked ] ++ prettyChecks ++ fixedChecks mapM_ putStr staticErrs failed <- flip filterM [ (e, fmt) | (e, Right fmt) <- checked ] $ \(e, fmt) -> do let runs = if arity (eEnc e) == 0 then 1 else 200 r <- quickCheckWithResult stdArgs { maxSuccess = runs, chatty = False } (prop_entry e fmt) unless (isSuccess r) (putStrLn (output r)) return (not (isSuccess r)) - printf "CodecCheck: %d encoders, %d static/rv_pretty failure(s), %d random-check failure(s)\n" + printf "CodecCheck: %d encoders, %d static/fixed-case failure(s), %d random-check failure(s)\n" (length entries) (length staticErrs) (length failed) unless (null staticErrs && null failed) exitFailure From cf86db3a0dadac6488722ce6a1414d2016a7edf1 Mon Sep 17 00:00:00 2001 From: Henrik M Pedersen Date: Mon, 12 Oct 2026 17:03:55 +0100 Subject: [PATCH 8/8] GenCHERI: capcsr, counter CSRs with and without ASR CHERIoT lets code without ASR read mcycle, minstret, mcycleh, minstreth and cycle/time/instret(h), and requires ASR for any write (ext_check_CSR in cheri_addr_checks.sail). No template reached these CSRs: an ibex decoder allowlist that left out the four 0xB counters went unnoticed until CHERIoT RTOS hung on csrr mcycle. capcsr mixes reads and writes of them with clearASR. It is gated on has_cheri: CHERIoT arch strings name no Zicsr, and the CSR regexes decide which CSRs are reached. clearASR's two temporaries must be nonzero and distinct, otherwise mtcc gets a null, untagged or permissionless capability. --- src/QuickCheckVEngine/Main.hs | 4 +++ src/QuickCheckVEngine/Templates/GenCHERI.hs | 33 ++++++++++++++++++++- 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/src/QuickCheckVEngine/Main.hs b/src/QuickCheckVEngine/Main.hs index a646178..c6fafdd 100644 --- a/src/QuickCheckVEngine/Main.hs +++ b/src/QuickCheckVEngine/Main.hs @@ -287,6 +287,10 @@ allTests = [ , ("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) diff --git a/src/QuickCheckVEngine/Templates/GenCHERI.hs b/src/QuickCheckVEngine/Templates/GenCHERI.hs index 98c3f0d..e99eeea 100644 --- a/src/QuickCheckVEngine/Templates/GenCHERI.hs +++ b/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 ]) ]