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 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 ]) ] diff --git a/src/RISCV/Helpers.hs b/src/RISCV/Helpers.hs index 0e292c1..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 @@ -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 = diff --git a/src/RISCV/InstInspect.hs b/src/RISCV/InstInspect.hs index a8bbf0c..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) @@ -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 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..3af4be9 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,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" 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/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..bcbe07b 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 @@ -242,7 +227,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 @@ -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"] @@ -296,14 +281,14 @@ 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" , 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,120 @@ 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 + (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) + .&&. 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 @@ -482,25 +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 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 ++ 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/fixed-case failure(s), %d random-check failure(s)\n" + (length entries) (length staticErrs) (length failed) + unless (null staticErrs && null failed) exitFailure