Struct ArmState 

pub struct ArmState {
    pub registers: Vec<BV>,
    pub flags: ConditionFlags,
    pub vfp_registers: Vec<BV>,
    pub memory: Vec<BV>,
    pub locals: Vec<BV>,
    pub globals: Vec<BV>,
    pub may_trap: Bool,
    pub unmodeled: Option<String>,
}

ARM processor state representation in SMT

Z3 0.19 uses thread-local context – no lifetime parameters needed.

Fields

registers: Vec<BV>

General purpose registers R0-R15

flags: ConditionFlags

Condition flags (N, Z, C, V)

vfp_registers: Vec<BV>

VFP (floating-point) registers

memory: Vec<BV>

Memory model (simplified for bounded verification)

locals: Vec<BV>

Local variables (for WASM verification)

globals: Vec<BV>

Global variables (for WASM verification)

may_trap: Bool

VCR-VER-002 (#166): the accumulated condition under which the executed sequence TRAPS (reaches a UDF). false in a fresh state; encode_op sets it unconditionally on a Udf, and the branch-taking executor ArmSemantics::encode_sequence_br conditions it on the path guard the UDF is reached under — this is the ARM-side trap term the trap-preservation VC compares against the WASM op’s trap condition.

unmodeled: Option<String>

#923: the FIRST ARM op ArmSemantics::encode_op was asked to execute and has no semantics for, recorded by the _ => {} default arm instead of being silently dropped.

Before this field existed the default arm was a silent register no-op, which makes an unmodeled instruction INVISIBLE to the value VC: a lowering that computes the right value and then destroys it (measured: i32.add → ADD r0,r0,r1 ; UXTB r0,r0, which returns (x+y) & 0xFF on silicon) came back Verified. The trap path already defended itself — ArmSemantics::exec_trap_subset_op’s doc says this default “must never green-wash a trap derivation” — but its defence was a hand-maintained allowlist that had drifted: Rsb (a SHIPPED sel-DSL rule’s instruction), I32TruncF32S and I32TruncF32U were all allowlisted to DELEGATE to encode_op, which does not model them.

Recording it here rather than in a second list is deliberate: the modeled set keeps exactly one source of truth (the match arms), so it cannot rot. Consumers turn a set field into a loud decline — crate::TranslationValidator’s value VC into VerificationError::UnsupportedOperation, exec_trap_subset_op into its own Err.

Implementations

impl ArmState

pub fn new_symbolic() -> Self

Create a new ARM state with symbolic values

pub fn get_reg(&self, reg: &Reg) -> &BV

Get register value

pub fn set_reg(&mut self, reg: &Reg, value: BV)

Set register value

pub fn get_vfp_reg(&self, reg: &VfpReg) -> &BV

Get VFP register value

pub fn set_vfp_reg(&mut self, reg: &VfpReg, value: BV)

Set VFP register value