Fix, simplify and speed up Boolean function evaluation

[julianspeith]

Found while investigating why HAWKEYE S-box identification was slow on the OpenTitan benchmark: a sample showed 96% of the run inside BooleanFunction::compute_truth_table(). Digging into that turned up three correctness problems in constant folding, a large amount of avoidable work, and a gap in the simplification rules.

Correctness

Additions and subtractions were silently truncated to 32 bit. Add and Sub masked their result with 0xffffffff before truncating it to the width of the operands, so anything wider lost its upper bits. A 33 bit 2^31 + 2^31 returned 0 instead of 2^32, and a 33 bit 0 - 1 returned 0xffffffff instead of 0x1ffffffff. The mask was also redundant, Const() already takes exactly as many bits as the operands are wide.

Eq overclaimed on undefined bits. 0b00X1 == 0b0001 returned a definite 0, although the two would be equal if that X turned out to be zero. It now returns X, unless another bit already tells the values apart. That is how Ult, Ule, Slt and Sle already behaved.

Sdiv, Udiv, Srem and Urem were not implemented and made evaluation of any function containing them fail. They are translated to bvsdiv, bvudiv, bvsrem and bvurem when handed to an SMT solver, so the folding follows those definitions, including a division by zero yielding all ones as the quotient and the dividend as the remainder. Restoring long division is used rather than 64 bit integer arithmetic, so the operations work at any width like Mul does.

Simplification of the word level operations

BooleanFunction::simplify() runs the rule set and then hands the result to ABC. ABC works on single bits, so it collapses things like A ^ (A ^ B) even though there is no rule for it, but it cannot reach the word level operations. Those are exactly the ones the rule set covered least: Zext and Sext had no rules at all, Slice had two, each comparison had one.

None of these was simplified before:

ZEXT(A, |A|)                 =>  A
SEXT(A, |A|)                 =>  A
ZEXT(ZEXT(A, n), m)          =>  ZEXT(A, m)
SEXT(SEXT(A, n), m)          =>  SEXT(A, m)
SLICE(SLICE(A, i, j), k, l)  =>  SLICE(A, i+k, i+l)
SLICE(CONCAT(A, B), i, j)    =>  SLICE(B, i, j) or SLICE(A, i-|B|, j-|B|)
SLICE(ZEXT(A, n), i, j)      =>  0               for i >= |A|
SLICE(ZEXT(A, n), i, j)      =>  SLICE(A, i, j)  for j < |A|
SLICE(SEXT(A, n), i, j)      =>  SLICE(A, i, j)  for j < |A|
0 <=u A                      =>  1
A <=u 111...1                =>  1
111...1 <u A                 =>  0
A == ~A                      =>  0
A == 1, A == 0               =>  A, ~A     for a single bit
ITE(A, 1, 0), ITE(A, 0, 1)   =>  A, ~A     for a single bit

Only extensions of the same kind collapse, ZEXT(SEXT(A, n), m) is not ZEXT(A, m). A slice of a concatenation or of an extension is only reduced when it falls entirely into one part, a slice crossing the boundary would not get shorter.

This mainly helps the word level users such as module_identification, solve_fsm and z3_utils. It does nothing for the truth table path, which does not go through simplify() at all.

Performance

Evaluating a function walks its nodes and hands each to simplify(), which builds a std::vector<BooleanFunction> of operands and returns a BooleanFunction. Each of those owns a vector of nodes whose nodes own a string and a vector of values, so one AND of two bits costs several heap allocations. 63% of the evaluation went to malloc and free.

When every variable is bound to a constant, which is always the case for a truth table, no sub-expression can survive and that detour is unnecessary. SymbolicExecution now folds such a function on a stack of plain values, falling back to the general path as soon as a variable is not constant. To avoid a second implementation of the operator semantics, the switch that applies a node to constant operands moved into ConstantPropagation::fold(), shared by the new path and by constant_propagation().

Resolving variables goes through the new SymbolicState::get_bindings(). Using get() per variable built a Boolean function as the key and looked it up in a std::map keyed by whole Boolean functions, comparing them node by node and therefore string by string.

Measured on a 50 node function over 8 variables, 256 rows per truth table:

	ms per truth table
before	5.17
this PR	1.94	2.7x
with the changes on bugfix/misc too	1.64	3.15x

Tests

evaluate() was only covered for Var, Not, And, Or, Xor, Add, Sub and Mul. Added coverage for everything the folding touches: shifts and rotates including shifting by at least the bit width, slice, concat, zero and sign extension, all five comparisons using bit patterns that compare the other way round once read as signed, Ite, and the propagation of undefined values through the bitwise and arithmetic operations.

The four new operations are checked against reference implementations of their SMT-LIB definitions for every pair of 4 bit operands including every division by zero, plus an 80 bit division to cover the arbitrary width path. Factory level tests cover the four factory functions themselves.

The new simplification rules are checked by enumerating every assignment of the variables and comparing the value before and against after simplification, rather than by asserting one particular output shape, plus a check that anything was simplified at all.

All operator tests were written against the unmodified code first, so that they characterise the existing behaviour rather than the new one, except where this PR deliberately changes it.

Note on merge order

This branch and bugfix/misc both touch symbolic_execution.cpp, the latter in the operand loop of constant_propagation() and this one by rewriting that function to delegate to fold(). Whichever lands second needs a small manual resolution.

🤖 Generated with Claude Code