Struct ArmSemantics 

pub struct ArmSemantics;

ARM semantics encoder

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

Implementations

impl ArmSemantics

pub fn new() -> Self

Create a new ARM semantics encoder

pub fn encode_op(&self, op: &ArmOp, state: &mut ArmState)

Encode an ARM operation and return the resulting state

This models the effect of executing the ARM instruction on the processor state.

pub fn extract_result(&self, state: &ArmState, reg: &Reg) -> BV

Extract the result value from a register after execution

impl ArmSemantics

pub fn encode_sequence_br( &self, arm_ops: &[ArmOp], state: &mut ArmState, ) -> Result<(), String>

Branch-taking guarded symbolic execution of an ARM sequence, deriving state.may_trap from the emitted guard structure (VCR-VER-002, #166).

Forward-branch DAG execution over the op list: every instruction carries the disjunction of the path conditions that reach it (if-conversion), BCondOffset routes guards forward, and a Udf accumulates its path guard into ArmState::may_trap — and does NOT fall through (a trap halts execution, so the code after a guarded UDF is reached only via the guard’s skip branch). This makes the ARM trap condition a DERIVED term: a lowering whose guard was dropped, inverted, or aimed at the wrong register derives a trap condition that fails the preservation VC — unlike the previous structural Udf-presence proxy, which only saw that some trap existed.

Branch targets are resolved in bytes via the shipped byte-size estimator (synth_synthesis::optimizer_bridge::estimate_arm_byte_size, the #511 estimator that CI pins against the encoder), matching the encoder’s target = branch + 4 + 2*offset halfword rule. A target that lands mid-instruction, a backward branch (loop), an op outside the modeled subset, or any label/call control flow is a loud Err — never a silent accept.

pub fn branch_spans_are_value_dead(arm_ops: &[ArmOp]) -> bool

Whether the sequence’s branch structure is VALUE-DEAD: every op inside a branch-skipped span writes no register/VFP state (Udf, Cmp, Cmn, nested BCondOffset only), and no op anywhere in the sequence turns flags into a register value (SetCond).

Under this condition the final REGISTER state is path-independent — every register-writing op executes on every path, in program order — so the straight-line value pass Self::encode_sequence_value_straightline computes exactly the registers any non-trapping real path produces. The flag writes a taken branch skips (e.g. the div_s overflow guard’s CMN behind BNE +3) can only influence which PATH is taken — the trap side, which Self::encode_sequence_br derives with full path sensitivity — and never a register value, because SetCond (the only flag→register op in the modeled subset) is excluded outright.

This is what lets the div/rem trap VC keep its value clause STRUCTURALLY aligned with the WASM side (bvsdiv/MLS terms identical after canonicalization): an ite(guard, …) wrapper on an SDIV/MLS operand un-shares the 32×32 multiplier/divider circuits and sends the UNSAT proof off the CDCL cliff term.rs documents (observed: rem_s value clause 15+ min with the ite, sub-second without).

pub fn encode_sequence_value_straightline( &self, arm_ops: &[ArmOp], state: &mut ArmState, ) -> Result<(), String>

Straight-line VALUE execution of a trap-guarded sequence: branches and UDFs are register no-ops, every other op executes unconditionally via the same modeled subset as the branch-taking executor.

ONLY sound when Self::branch_spans_are_value_dead holds (see its doc for the argument); callers must check it first. Produces ite-free register terms, keeping the trap VC’s value clause structurally aligned with the WASM encoding.

Trait Implementations

impl Default for ArmSemantics

fn default() -> Self

Returns the “default value” for a type.