Adding WordVar to GecodeDRAFT

Gecode has a new variable type for fixed-width machine words. A WordVar is a word of 1 to 64 bits, where logical operators work bitwise, shifts move bits between positions, and masks select parts of a value. These are the bit vectors that SMT solvers such as Z3 have long supported, and they show up in software and hardware verification and in cryptanalysis.

Along with the variable, the branch has constraints for logical operations, shifts and rotations, wrapping and signed arithmetic, comparisons, and extracting and concatenating bit fields. Branchings, channels to BoolVar and IntVar, and MiniModel expressions let word constraints sit next to ordinary integer constraints in a model.

The domain of a WordVar has two parts. Following Michel and Van Hentenryck’s work on bit-vector constraints and Wang, Søndergaard, and Stuckey’s Wombit, it records which bits are known to be zero or one, so that propagation can work on all the bits of a word with a single machine operation. On top of that, it can keep an interval on the number that the word represents, interpreted as a signed or unsigned integer or as a floating-point value. Words of at most eight bits can also keep the exact set of their possible values. As we will see, the interval can make propagation much stronger.

A simple example: patching a CRC-32#

Bootloaders and update tools often accept a firmware or configuration image only if its CRC-32 matches a stored value. Say we need to change the baud rate in a 48-byte configuration record from 115200 to 921600, but the stored checksum has to stay the same. The record has four reserved bytes, and we can choose them so that the edited record keeps its old CRC-32.

The model is the standard bit-at-a-time CRC-32 used by zlib and Ethernet. Each byte of the record is an 8-bit word, and the 32-bit CRC state becomes a chain of word variables. A byte is XORed into the low bits of the state, and each of its eight bits then shifts the state right by one, XORing in the polynomial when the bit shifted out is one:

WordVar shift_out_bit(Home home, WordVar state) {
    BoolVar low_bit(home, 0, 1);
    channel(home, state, 0, low_bit);
    WordVar shifted(home, 32), feedback(home, 32), next(home, 32);
    WordVar zero(home, 32, {0});
    logical_shift_right(home, state, 1, shifted);
    ite(home, low_bit, crc32_polynomial, zero, feedback);
    rel(home, shifted, WOT_XOR, feedback, next);
    return next;
}

All bytes except the four reserved ones are fixed, and the CRC is fixed to the original checksum, 0x4be87813. As expected, Gecode finds the patch bytes b9 a0 0a cd at the root, without any search. Known bits propagate forward from the start of the record and backward from the checksum, and they meet at the patch bytes. A CRC is affine over GF(2), so the checksum determines four bytes between a known prefix and a known suffix uniquely. That is also why a CRC only protects against accidental corruption: anyone can change the data and keep the checksum.

Why not bit blasting?#

The standard way to handle bit vectors is bit blasting: each word becomes a set of Boolean variables, and each operation becomes a Boolean formula, typically clauses for a SAT solver. Z3 exposes this translation as its bit-blast tactic. We can do the same by hand in Gecode. The CRC state becomes 32 BoolVars, the shift is only a renaming, and the feedback needs one XOR for each one bit in the polynomial:

using State = std::array<BoolVar, 32>;

State shift_out_bit(Home home, const State& state) {
    State next;
    for (int i = 0; i < 31; i++) {
        if (crc32_polynomial & (1U << i)) {
            next[i] = BoolVar(home, 0, 1);
            rel(home, state[i + 1], BOT_XOR, state[0], next[i]);
        } else {
            next[i] = state[i + 1];
        }
    }
    next[31] = state[0];
    return next;
}

Here are the sizes of the three versions of the model, before any constants are folded:

All three find b9 a0 0a cd by propagation alone. Words do not change what is inferred here, since an XOR on masks computes the same thing as 32 Boolean XORs. The same holds when search is needed. If the reserved bytes must stay zero and we rename the device instead, choosing seven printable characters of its name, both Gecode models explore the same 144,399 nodes. It is a small search, and both models finish it in less than a second.

So on a CRC, WordVar gives us a smaller model that reads like the code it describes, not stronger propagation. A CRC is also close to the best case for bit blasting, since it is only shifts and XORs. Arithmetic and comparisons cost much more. In Z3’s translation, a 32-bit addition is 445 clauses, a multiplication 8,213 clauses, and an unsigned comparison 186 clauses, and each of them is a single propagator on words.

Those clauses pay off in a SAT solver, which is built for large formulas and learns new clauses from its conflicts. Decomposing words into BoolVars in Gecode brings none of that. It also hides the numbers: a bound on a word becomes a condition on a collection of bits, instead of an endpoint that an arithmetic propagator can use directly. So WordVar keeps the word as the unit of propagation. Which approach is faster on a given problem is still a question for experiments.

The WordVar domain#

A WordVar describes its possible values in two ways. The bits say which positions are known to be zero or one. The optional interval bounds the value of the word, representing an unsigned or signed integer or a floating-point number. Each description captures sets that the other cannot, and together they propagate more than either does alone.

Known bits#

Consider a four-bit word with the pattern 1?0?, where the question marks are unknown bits. Its possible values are 1000, 1001, 1100, and 1101, or 8, 9, 12, and 13. Two masks describe this domain:

A word belongs to the domain when it has every one bit in lo and no one bits outside hi. The unknown bits vary independently, so this representation is usually called a cube. A cube can describe sets with gaps. The values 8, 9, 12, and 13 are not consecutive, and the interval from 8 to 13 would also include 10 and 11.

However many bits are unknown, operations on the domain are a few machine instructions on the two masks. Intersecting two cubes, for example, is:

new_lo = x.lo | y.lo
new_hi = x.hi & y.hi

The intersection is empty if new_lo & ~new_hi is nonzero, and the word is assigned when lo == hi.

Numeric bounds#

A WordVar can have optional numeric bounds in addition to its known bits. They matter most for arithmetic and comparisons. Consider a model with interchangeable word variables. Permuting them changes nothing, so we can require them to be in numeric order, x ≤ y ≤ z, to avoid exploring each permutation.

This order carries information that a cube cannot express. If x is at least 5 and z is at most 10, then y lies between 5 and 10, from 0101 to 1010. Every bit takes both values somewhere in that interval, so the smallest cube that covers it is ????, which admits all sixteen words.

A bounded WordVar keeps the interval next to its cube.¹ Suppose y must be even as well. The pattern ???0 and the interval from 5 to 10 together describe exactly 6, 8, and 10, which neither manages alone. The constructor takes the width, the domain type (here unsigned), the interval, and the known bits as a mask of the fixed positions and their values:

WordVar even_between_5_and_10(Home home) {
    return WordVar(home, 4, WDT_UNSIGNED, 5, 10, known_bits(0b0001, 0));
}

The two descriptions are kept synchronized. Each endpoint moves to the nearest value that the cube admits, computed from the masks in one step rather than by trying values. For the even word, 5 conflicts with the zero in the low bit, so the minimum moves to 6. Information also flows the other way. All values between two endpoints share the high bits that the endpoints have in common, so a narrow interval fixes bits. If the maximum drops to 7, only 6 remains, and all four bits become fixed. The examples in the explorer below go through these steps.

Some sets fall through both descriptions. For the even-parity three-bit words 000, 011, 101, and 110, every bit varies and the interval is [0, 6], so the domain still admits 1, 2, and 4.

Exact value sets for small words#

A word of at most eight bits has at most 256 values, few enough to store the domain as an exact set. A WordVar created with WVS_EXACT keeps that set inside the variable, next to its cube and any bounds, and the even-parity domain is then exact:

WordVar even_parity(Home home) {
    return WordVar(home, 3, {0b000, 0b011, 0b101, 0b110}, WDT_CUBE, WVS_EXACT);
}

The cube is always the bit pattern shared by the values in the set, and the bounds are its smallest and largest value. A change to any of the three is passed on to the others. Removing a single value, for example with a disequality to a constant, leaves a hole that neither the cube nor the interval could express.

Unsigned, signed, or floating point#

The numeric bounds come with a choice of what the word represents. A WordVar is created as plain bits (WDT_CUBE), as an unsigned integer (WDT_UNSIGNED), as a two’s-complement signed integer (WDT_SIGNED), or as a number in one of five floating-point formats, such as WDT_FP32. The choice stays fixed for the variable, and a floating-point format also fixes the width:

Plain, unsigned, and signed words of at most eight bits can also keep an exact value set when they are created with one.

Floating-point support is still under development on the branch, so the formats and the operations available for each of them may change. Not every format has every operation yet: binary16, for example, has conversions, classification, and sign operations, but no arithmetic.

Signed and floating-point words reuse the unsigned machinery. For signed words, flipping the sign bit maps their order onto the unsigned one. Floating-point bounds follow the IEEE 754 total order of the format: negative NaNs, negative infinity, the negative numbers, -0, +0, the positive numbers, positive infinity, and positive NaNs. Setting the sign bit of a positive encoding and complementing a negative one maps this order onto the unsigned order as well. An interval on a float word is therefore an interval of floats, and the floating-point constraints use it as one. Here x lies in [1, 1.5] and y in [3, 3.5]:

WordVar sum_of_intervals(Home home) {
    WordVar x(home, WDT_FP32, 1.0, 1.5);
    WordVar y(home, WDT_FP32, 3.0, 3.5);
    WordVar z(home, WDT_FP32);
    fp_add(home, x, y, z);
    return z;
}

Propagation narrows the sum z to [4, 5], with the endpoints computed exactly under IEEE 754 rounding to nearest even. An optional policy argument selects other rounding modes and other treatments of subnormals and NaNs. The interval feeds the bits here as well. All values in [1, 1.5] share their sign and exponent, so nine bits of x and ten bits of the sum are known before any search.

The integer word constraints also accept float words and act on their bits, so masking out the sign bit or extracting the exponent needs no conversion. When a model needs the same bits in a second reading, such as the unsigned integer behind a float, reinterpret returns a new word of the other domain type, and the two stay linked in both directions.

Propagation#

In constraint programming, propagation is how constraints are implemented. Each constraint removes the values from its variables’ domains that cannot be part of any solution, and every removal can wake up other constraints, until nothing more changes. For a WordVar, removing values means fixing bits, moving bounds, and, for a word with a value set, removing values from the set. All three are cheap operations on whole machine words.

Logical operations#

For z = x OR y, a bit that must be one in either input must be one in the result. A bit that cannot be one in either input cannot be one in the result:

z.lo |= x.lo | y.lo
z.hi &= x.hi | y.hi

Propagation also works backwards. If a result bit is zero, both input bits must be zero. If a result bit is one and one input cannot supply it, the other input must:

x.hi &= z.hi
x.lo |= z.lo & ~y.hi & mask

The same rules apply with x and y exchanged, and mask selects the bits within the width of the word. Suppose x = ?0??, y = 0010, and the result is fixed to 1010. The high result bit must come from x, and the low result bit forces the low bit of x to zero, leaving x = 10?0. The third bit stays open, since y already supplies that result bit.

The mask rules treat the operands as independent, so they cannot see that x XOR x is always zero, even when every bit of x is unknown. WordVar handles aliased operands separately.

Arithmetic that wraps around#

Word addition, subtraction, and multiplication wrap at the width, so for four bits, 1111 + 0001 = 0000. Numeric bounds help when the ranges rule out wrapping. If four-bit a lies in [2, 4] and b in [3, 5], their sum lies in [5, 9], and a bound on the result can in turn restrict the operands. With a in [14, 15] and b in [1, 2], though, the sums are 15, 0, and 1, and treating the result as the interval [15, 17] would be wrong. Bounded propagators check that wrapping is impossible before using interval reasoning, and otherwise fall back on the bits.

Propagators apply every bound move they deduce, whatever the width of the word, just as they do for IntVar. Also as for IntVar, propagation can then converge very slowly on large domains, so models should avoid cycles of constraints that move each other’s bounds a little at a time.²

Gecode reports changes to the bits and to the bounds as separate events. Restricting a word to [5, 10] may fix no bits, but an ordering constraint still needs to wake up and pass the new bounds on. In the other direction, a bounded arithmetic propagator can run its cheap interval rules first, and do the more expensive bit reasoning only when some bits became fixed. Removing values from a value set without changing the bits or the bounds is a third kind of event.

A small complete model#

We can put these pieces together in a model with three interchangeable four-bit words. Each is even and between 5 and 10, so each starts out as 6, 8, or 10. Their bitwise OR must be 1110, or 14. The OR is symmetric in the three words, so we can order them to remove equivalent permutations.

#include <gecode/word.hh>
#include <gecode/search.hh>
#include <iostream>
#include <memory>

using namespace Gecode;

class OrderedWords : public Space {
public:
    WordVarArray words;

    OrderedWords()
        : words(*this, 3, 4, WDT_UNSIGNED, 5, 10, known_bits(0b0001, 0)) {
        WordVar combined(*this, 4, {14});
        rel(*this, WOT_OR, words, combined);
        rel(*this, words[0], WRT_ULQ, words[1]);
        rel(*this, words[1], WRT_ULQ, words[2]);
        branch(*this, words, WORD_VAR_NONE(), WORD_VAL_SPLIT_MIN());
    }

    OrderedWords(OrderedWords& s) : Space(s) {
        words.update(*this, s.words);
    }

    Space* copy(void) override {
        return new OrderedWords(*this);
    }
};

int main() {
    auto root = std::make_unique<OrderedWords>();
    DFS<OrderedWords> search(root.get());
    root.reset();
    while (auto* next = search.next()) {
        std::unique_ptr<OrderedWords> solution(next);
        std::cout << solution->words[0].val() << ' '
                  << solution->words[1].val() << ' '
                  << solution->words[2].val() << '\n';
    }
}

WRT_ULQ is unsigned less than or equal, so repeated values are allowed. The model produces five solutions:

6 6 8
6 6 10
6 8 8
6 8 10
6 10 10

Removing the two ordering constraints gives 18 solutions, the permutations of these five. WORD_VAL_SPLIT_MIN() splits the numeric interval and tries the lower half first, and propagation then moves the new endpoints past the holes in the cube. Other value selectors branch on a single unknown bit: the lowest, the highest, or a random one.

Word expressions#

MiniModel’s WordExpr expressions let a model read like the code it checks. To find the midpoint between two array indices, we might compute (low + high) / 2. When both indices are large, the sum overflows, a bug that sat in widely used binary search implementations for years before Joshua Bloch wrote about it in 2006. With WordVar, the routine computes on 32-bit words, and the exact midpoint uses one more bit, so that its sum cannot wrap:

void midpoint_overflow(Home home, WordVar low, WordVar high) {
    WordExpr routine = div(low + high, 2);
    WordExpr exact = div(zero_extend(low, 33) + zero_extend(high, 33), 2);
    rel(home, zero_extend(routine, 33) != exact);
}

With low and high as unsigned 32-bit words and a WORD_VAL_SPLIT_MAX() branching, search splits their intervals, trying the upper half first. It finds low = high = 0xffffffff after 65 nodes, one for each bit of the two inputs plus the root.

The same model is awkward with Gecode’s IntVar. Integer variables use exact arithmetic, so (low + high) / 2 never overflows, and the wrap has to be modelled by hand, for example with a carry variable that subtracts 2³² from the sum. More fundamentally, an IntVar holds values between -2³¹ + 2 and 2³¹ - 2, so neither 32-bit unsigned inputs such as 0xffffffff nor their 33-bit sum fit at all. The model would have to split each word into smaller pieces and propagate the carries between them, which is a coarse version of bit blasting. With WordVar, the words and their wrapping arithmetic are the variables and constraints themselves.

Examples on the branch#

The branch includes four application examples.

• word-bit-trick.cpp checks bit tricks against reference versions. Besides the midpoint, it checks the classic trick for rounding up to a power of two, which goes wrong for zero.
• word-crc-patch.cpp is the complete CRC-32 patching model.
• word-sha1-preimage.cpp recovers the unknown bits of a message block from its digest, for SHA-1 reduced to a number of steps. With the defaults, 16 steps and 164 unknown bits, it needs 14 search nodes.
• word-float-error.cpp finds and proves the worst-case error of an FP8 multiply-accumulate a*b+c compared to FP32, for inputs in an activation-like range. The worst case is a cancellation: with a = 0.28125, b = 1.875, and c = -0.5, the product rounds to 0.5 in FP8, and the FP8 result is 0 instead of 0.02734375. That is an error of 14 units in the last place of FP8.

When is WordVar useful?#

WordVar is useful when machine words are one part of a larger combinatorial problem. That covers several kinds of models:

• Models that mix machine arithmetic with integer, Boolean, and scheduling constraints, and use Gecode’s search heuristics and symmetry breaking on all of them.
• Models where words carry numeric meaning, such as an order between variables, a range of printable characters, or an interval of floats, which known bits alone describe poorly.
• Searches for inputs, such as patch bytes for a checksum, a preimage of a reduced hash, a counterexample to a bit trick, or the worst-case rounding error of a small float format.
• Models that should read like the code they describe, with one constraint per operation instead of one per bit.

WordVar is less suited to proving that something can never happen. Finding the overflow in (low + high) / 2 took 65 nodes, because search only had to find one bad pair of inputs. Proving that the alternative (low & high) + ((low ^ high) >> 1) always gives the exact midpoint is a different task: there is nothing to find, so search has to rule out every pair. Propagation cannot see that the carries in the two computations agree until the inputs are almost assigned. The proof takes under a second for 10-bit words, but every extra bit makes the search four times larger, so 32 bits is out of reach.³ SAT-based SMT solvers learn clauses from conflicts and reuse that reasoning across the search, and WordVar in Gecode has nothing comparable.

So if a problem is all bit vectors and the question is a proof, an SMT solver is the better tool. If machine words are part of a combinatorial problem, WordVar lets a Gecode model handle them as words with a compact encoding.