Repository navigation
Codeccheck review - #2
Open
henrikpedersen-oss wants to merge 8 commits into
Open
henrikpedersen-oss wants to merge 8 commits into
henrikpedersen-oss wants to merge 8 commits into
Conversation
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".
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.
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.
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.
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).
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.
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.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
CodecCheck: address review, check rv_extract; capcsr template.