Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 35 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
29 changes: 22 additions & 7 deletions scripts/repro/shift_fold_riscv_differential.py
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@
Exits nonzero on any mismatch or vacuity failure.
"""
import os
import re
import subprocess
import sys

Expand All @@ -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.
Expand Down Expand Up @@ -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):
Expand Down
Loading