diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8a524c4..aa0a949 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -268,3 +268,38 @@ jobs: run: pip install wasmtime unicorn pyelftools - name: Run two-move execution oracle run: python scripts/repro/cmp_select_two_move_differential.py + + rv32-shift-fold-oracle: + name: rv32 immediate-shift-fold execution oracle + # VCR-ORACLE-001 (#242, #472): EXECUTE the RV32 immediate-shift-fold lever + # under unicorn (UC_ARCH_RISCV) in BOTH flag states and diff vs wasmtime. The + # lever ships flag-off (SYNTH_RV_SHIFT_FOLD) awaiting the on-silicon flip, so + # nothing else exercises the flag-on path; this continuously validates it + # (slli/srli/srai folds incl. the &31 mask on >=32 and negative amounts, and + # the variable-shift non-fold) against regression — the RV32 analogue of the + # cmp-select oracle above. Isolated job: emulation deps pip-installed here ONLY. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v5 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v5 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools + - name: Run RV32 shift-fold execution oracle + env: + SYNTH: ./target/debug/synth + run: python scripts/repro/shift_fold_riscv_differential.py diff --git a/scripts/repro/shift_fold_riscv_differential.py b/scripts/repro/shift_fold_riscv_differential.py index 90bb90f..9b0886b 100644 --- a/scripts/repro/shift_fold_riscv_differential.py +++ b/scripts/repro/shift_fold_riscv_differential.py @@ -23,7 +23,6 @@ Exits nonzero on any mismatch or vacuity failure. """ import os -import re import subprocess import sys @@ -39,7 +38,9 @@ ) WAT = "scripts/repro/shift_fold.wat" -SYNTH = "./target/release/synth" +# Default to the release binary for local dev; CI sets SYNTH=./target/debug/synth +# (it builds `cargo build -p synth-cli`, debug) so the isolated oracle job stays fast. +SYNTH = os.environ.get("SYNTH", "./target/release/synth") CODE, LIN, STK, RET = 0x100000, 0x40000, 0x90000, 0x200000 # (export name, list of argument tuples). Each function returns its result in a0. @@ -67,11 +68,25 @@ def compile_elf(out, fold): def syms_and_code(elf): - dis = subprocess.run([SYNTH, "disasm", elf], capture_output=True, text=True).stdout - syms = {m.group(2): int(m.group(1), 16) - for m in re.finditer(r'^([0-9a-f]{8}) <(\w+)>:', dis, re.M)} - code = ELFFile(open(elf, "rb")).get_section_by_name(".text").data() - return syms, code + """Return ({export_name: text_relative_offset}, text_bytes). + + Read function addresses straight from the ELF symbol table, NOT by scraping + `synth disasm` text — the disasm backend/format is host-dependent (on a bare + CI runner it decodes RISC-V bytes with the wrong decoder and the symbol-line + regex matches nothing). synth emits the symtab with an EMPTY section name, so + find it by sh_type, and make addresses .text-relative by subtracting the + section's sh_addr (0 for a relocatable object, but subtract defensively). + """ + f = ELFFile(open(elf, "rb")) + text = f.get_section_by_name(".text") + base = text["sh_addr"] + syms = {} + for s in f.iter_sections(): + if s.header.sh_type == "SHT_SYMTAB": + for sym in s.iter_symbols(): + if sym.name: + syms[sym.name] = sym["st_value"] - base + return syms, text.data() def text_len(elf):