How InSPECtor Explores the Decoder
This chapter examines GenSYS, the InSPECtor component that turns a SLEIGH specification into a systematic set of instruction encodings. The specific question is how to reach meaningful constructor paths in a large, variable-length decoder without guessing bytes at random or enumerating every operand value. Understanding that mechanism lets the reader interpret constructor coverage correctly: it is evidence that the generator reached the model’s represented paths, not proof that every legal behavior has been validated.
The key design choice is to use the specification’s structure as a guide. A SLEIGH decoder already contains constraints, tables, context transitions, operand relationships, and semantic choices. GenSYS follows those relationships, preserves the conditions that must hold together, and asks a solver for concrete bytes only after it knows what a complete path requires.
Generation starts with a path, not a random byte string
A random byte string begins with almost no knowledge of the processor. It may be invalid, may stop decoding at the first byte, or may land repeatedly in common instruction forms while missing rare combinations of prefixes, modes, operand encodings, and constructor precedence. Even when a random string executes, it does not explain which part of the specification it exercised. Randomization can vary values, but it does not understand the grammar that makes an instruction form reachable.
GenSYS starts at the other end. It treats the SLEIGH specification as a tree of decoding choices and asks what must be true for each choice to complete. The goal is not to make every possible byte pattern. It is to generate instructions with distinct constructor paths and semantics, then choose representative values within those paths. This distinction makes the generator aware of the model’s intended structure before any concrete test is executed.
At the beginning of a traversal, the instruction bits are symbolic. A bit can be fixed to zero or one when a constructor requires it, or remain unknown when the path has not constrained it. Decoder context is represented similarly, except that some context fields begin with fixed values defined by the processor configuration. A third component holds deferred constraints that cannot safely be converted into individual fixed bits. The resulting symbolic state records three different kinds of information: what the instruction encoding currently says, what the decoder context currently says, and what relationships still have to be satisfied.
The traversal selects a constructor in the current table and translates the constructor’s requirements into that state. The simplest requirements compare a field with a constant. If a constructor requires an operation field to equal a particular value, the corresponding instruction bits can be fixed immediately. If the new requirement conflicts with a bit already fixed by an earlier constructor, the path is unsatisfiable and can be discarded without exploring its remaining subtables. This early pruning is one of the main advantages of understanding the specification rather than sampling the byte space blindly.
Not every requirement has a single bit pattern. A constructor may require two fields to be equal, impose an inequality, or compare a field with an expression involving other fields. Assigning arbitrary values as soon as such a condition appears can create a false dead end later. GenSYS therefore keeps these relationships as deferred constraints while continuing to traverse. Once the path has selected all of its constructors and accumulated the conditions, an SMT solver such as Z3 searches for a concrete assignment that satisfies them together.
The difference is important even in a small example. Suppose a path requires two register fields to be equal. The generator could choose a register immediately, but that choice would be premature: a later subtable or attachment might restrict the available values. Keeping the equality symbolic lets later constraints participate in the same decision. Conversely, if an earlier fixed bit already makes an inequality impossible, the traversal can reject the path before invoking the solver. Fixed information is used for fast pruning; relational information is preserved for global solving.
Overlap adds a condition that may not be written directly on the constructor being generated. SLEIGH can contain a general constructor and a more specific constructor that both match the same broad opcode family. The decoder gives the more specific form priority. To generate an encoding for the general form, GenSYS must therefore add a negative condition that prevents the earlier form from matching. It may do this by negating the earlier constructor’s constraints or by forcing its subtable to fail. Without that implied exclusion, a generated byte string could satisfy the intended general rule but be decoded by the real SLEIGH engine as the more specific rule.
Attachments contribute another layer. A field value can be mapped to a register or another operand through an attachment, and an attachment can mark certain values invalid. A field that appears unconstrained in the pattern is consequently not always free to take every numerical value. GenSYS incorporates the attachment’s exclusions as additional constraints. This keeps the concrete encoding consistent not only with the visible pattern but also with the meanings assigned to its fields.
Decode actions change the state as traversal proceeds. A constructor can derive a context field from instruction bits, or set a mode flag that affects a later subtable. The generator must apply that action at the same point at which the decoder would apply it. In phased decoding, an early constructor can split an instruction into stages: the later stage is not evaluated under the initial context, but under the context produced by the first stage. A generated encoding that ignores this transition may satisfy a later pattern in isolation while never reaching it in a real decode.
Self-referencing constructors make the same issue more visible. They can be used to parse optional or repeated prefixes. A prefix consumes part of the instruction bit vector, updates context, and sends decoding back through a related rule. The generator has to track the current offset so that later constraints refer to the right bytes. It also needs a traversal limit, because a specification that permits repeated prefixes could otherwise create an unbounded symbolic search even though physical instruction encodings have a finite length.
Dynamic context can remain symbolic. If a decode action computes a context value from instruction bits that are not yet fixed, a later pattern depends on an expression rather than a known Boolean. GenSYS carries that dependency forward and eventually translates it into a constraint over the instruction bits. Replacing it with a convenient constant would be faster, but it would test a different path from the one the specification describes.
Backtracking is the final part of the path search. A constructor can be locally compatible with the current state and still lead to failure when a referenced subtable is evaluated. The decoder can return to the earlier table and try another constructor. GenSYS maintains unselected alternatives so that a failed continuation does not terminate the whole generation process. This is more than a search optimization: it mirrors the decoder’s semantics, in which a choice is valid only if the complete path can be completed.
The flow is deliberately different from “generate bytes, then see what happened.” A path is selected first, its positive and negative conditions are accumulated, context changes are applied, and only then does the solver choose bytes. If the solver reports unsatisfiable, the path does not become a mysterious random failure; it is a combination of constructor choices that cannot coexist. If it succeeds, the resulting encoding comes with a clear explanation of which represented path it was intended to exercise.
The hard part is choosing enough cases, not every case
A complete constructor path can still contain many free fields. Register operands may have several legal values. Immediate fields may allow almost every number. Memory offsets may vary over a large range. Testing every combination would recreate the combinatorial explosion that the structured traversal is intended to avoid, while adding little information when those variations do not change the core semantics.
GenSYS therefore seeks a representative set of solutions for each unique semantic path. The goal is to cover different instruction forms and important value boundaries, not to claim that one arbitrary encoding stands for every possible input. This is a deliberate trade-off: the corpus becomes feasible, and the generator can spend effort on paths and conditions that distinguish behavior, while some value-specific defects may still require additional cases.
The solver helps choose those cases rather than merely finding the first satisfying assignment. For a partially constrained field, it can minimize and maximize the permitted value. Extremes expose boundary conditions that a middle-of-the-range assignment would avoid. If a constructor requires an immediate to be nonzero, a solver-generated boundary case close to zero is more informative than a randomly selected large value. If two fields must be equal, minimum and maximum equal assignments exercise different widths and bit patterns without enumerating every pair.
The generator also looks at the semantics associated with a path for potential aliasing. Two operands that usually refer to different registers may legally name the same register or memory location. When an instruction is represented as several p-code operations, that choice can reveal whether the specification reads all of its inputs before modifying a destination. GenSYS adds constraints for such aliasing cases because they are behaviorally meaningful, not because every alias must be tested for every instruction.
This is the difference between representative generation and random sampling. Random sampling might eventually choose an equal-register case, a boundary immediate, or a required prefix, but the probability can be very low when the valid region is small or the encoding has a complicated structure. GenSYS identifies those conditions from the specification and asks directly for assignments that satisfy them. The method is still finite and selective; its advantage is that selection follows the model’s constraints and semantics.
The resulting measure is constructor coverage: the number of constructors used during generation divided by the total number of constructors in a specification. This is a meaningful structural measure because constructors are the fundamental units of SLEIGH syntax and because the generator’s objective is to reach distinct paths through them. It answers a specific question: how much of the represented decoding structure was exercised by generated cases?
It does not answer every assurance question. A constructor can be reached while its p-code is wrong. A set of representative values can miss a defect that occurs only for another operand combination. A specification can omit an instruction entirely, in which case no constructor path exists for GenSYS to explore. And a feature may be absent from the hardware or processor configuration used for the experiment, leaving related constructors intentionally unavailable. Coverage must therefore be read as evidence about reachability, not as a probability that the specification is correct.
The study’s treatment of missing constructors illustrates that distinction. The authors investigated constructors for which generation produced no test case and separated cases that were not applicable in the chosen configuration from redundant constructors, incomplete parts of a specification, and a small set of specification issues. These categories have different meanings. An unavailable processor mode is not the same problem as a constructor that can never win because of overlap, and neither is the same as a missing parent rule that prevents an otherwise implemented subtable from being reached.
Recursive operand definitions make this classification necessary. A register-list encoding can be described as a sequence of conditional choices, one per possible register. With sixteen registers, the simplified ARM-style example has approximately 2^16 possible paths. Generating every combination would spend most of the budget on variations that do not provide a new semantic path. GenSYS tracks which constructor combinations have already been covered and prunes redundant exploration, while retaining the cases that reveal distinct choices.
The traversal limit is another explicit boundary rather than a hidden promise. It prevents repeated-prefix or self-referential definitions from producing an unbounded search. The paper argues that real hardware has a maximum instruction length, so a valid encoding should normally be found within an appropriate limit, but the limit still has to be configured and checked. A path that is absent from the generated corpus may reflect a specification problem, an unavailable feature, redundancy, or a search boundary; it cannot be interpreted correctly without examining the reason.
This makes GenSYS a structural assurance mechanism. It improves the question from “Did random bytes happen to execute?” to “Can the generator produce an encoding for each represented constructor path, under the same context, precedence, attachments, and subtable dependencies that the decoder uses?” That is a much stronger way to explore a specification. It remains only one half of validation, however. The solver can establish that a byte sequence satisfies the model’s constraints; it cannot establish that the model’s semantic result matches a physical processor.
The next step is to supply that missing evidence without throwing away the structure GenSYS has recovered. The same p-code semantics that describe a constructor’s effects can identify initial states likely to expose arithmetic, flag, memory, floating-point, and aliasing mistakes. Execution against a hardware reference then tests whether the generated model behaves as its source specification claims—and as the processor actually behaves.