4 Approach

We present an approach for systematically discovering and analyzing instructions on a CPU. We provide an overview of the three main components of this approach: 1.) the CPU observer, 2.) enumeration based on encoding analysis, and 3.) synthesis.

4.1 CPU Observer

In order to analyze instructions, we need a CPU observer. This CPU observer needs to be fast, sandboxed and unrestricted. It needs to be fast, because we will perform tens of millions of observations for each instruction we analyze. Instruction execution must be sandboxed, such that it does not affect our analysis tool or the operating system in unintended ways. There must be as few restrictions on the input CPU state as possible, so that we can freely observe as much of the behavior of the instruction as possible.

There are two common ways to observe instruction execution: in-process observation [2, 8–10] and out-of-process observation [10]. Neither of these methods fulfill all requirements. Therefore, we have developed a new instruction observation method.

Both in-process observation and out-of-process observation ultimately execute an instruction in a userspace process. After execution, control over program flow is regained using the trap flag, guard pages or interrupt instructions. A guard page is an unmapped page that is placed in memory right after the instruction. When the CPU has executed the instruction and attempts to load the next instruction, a page fault is triggered. This page fault is intercepted by the program, and used to regain control. The trap flag is a debugging flag available on many modern CPU architectures, including x86-64. It triggers a CPU interrupt after executing a single instruction. This interrupt is intercepted by the program, and used to regain control. Interrupt instructions are special debugging instructions that trigger a debugging interrupt. On x86-64, the INT3 instruction is commonly used for this purpose. After execution, the result is saved and normal program execution is resumed by loading the original program state from memory.

In-process observation consists of storing the program state in memory, placing the instruction at a known memory address, and then jumping to that address. This approach is fast, but not sandboxed, and the input CPU states cannot use the address space used by the program itself or reserved by the kernel (Linux reserves half of the address space).

Out-of-process observation consists of spawning a separate observation process. This observation process is then instrumented using a debugging interface like ptrace. CPU state can be modified through this interface, and memory can be mapped and unmapped by placing assembly for the correct system calls in the memory of the observation process and executing it via the debugging interface. While this approach provides some sandboxing, it shares many of the same restrictions on input CPU states as in-process observation, and is very slow because the debugging interface has a lot of overhead.

We have developed a new observation approach based on hardware-accelerated virtualization and fast communication via shared memory. The approach is depicted in Figure Figure 2. It consists of two components: a process running on the host machine, and a small bare-metal observer binary running in a virtual machine. Using a ring buffer [21], these components can communicate without the overhead of syscalls. The observer running in the virtual machine performs context switches to userspace to observe instructions. This provides hardware-enforced protection to the observer from the effects of the instruction execution.

The observer repeatedly reads an observation request from the ring buffer, executes the request, and then writes the result back to the ring buffer. Observation requests are executed similar to how an operating system performs context switches between processes. Whereas an operating system typically restores CPU state from a process control block, the observer restores CPU state from the observation request in the ring buffer. It then switches to userspace, allows the CPU to execute an instruction, and then regains control. Finally, the observer saves the CPU state directly to the observation result in the ring buffer.

To regain control, the observer uses INT3 interrupt instruction by default. If we detect that the instruction does not increment the program counter by the length of the instruction (e.g., the instruction is a branching instruction), we are unable to predict the address where we need to place the INT3 interrupt instruction. In that case, we fall back to using the trap flag. We use the INT3 interrupt instruction by default, because it does not require writing a flag in the debugging registers and is therefore faster.

4.2 Enumeration

The goal of enumeration is discovering all in-scope instructions on a CPU. We do this by repeatedly selecting an uncovered instruction, and analyzing it.

For large instruction sets like x86-64, it is impossible to enumerate every individual bitstring. For example, the MOVABS RAX, 0x152, instruction contains a 64-bit immediate value. It is impossible to exhaustively enumerate all $2^{64}$ values of this immediate. We instead skip over parts of the instruction space using 1.) bitpatterns from encodings, 2.) randomized search and 3.) tunneling.

As described in Section Section 2, every encoding represents a group of instructions described by its bitpattern. During enumeration, we run encoding analysis on each valid instruction. We then use the bitpattern from the resulting encoding to skip all instructions it matches. This is depicted in Figure Figure 3. For example, for MOVABS RAX, 0x152 encoding analysis will yield an encoding with a bitpattern containing two parts: a 64-bit part for the immediate value and a 4-bit part for the destination register. This allows us to skip the $2^{68}-1$ other instructions covered by this encoding.

The enumeration algorithm is depicted in Algorithm 1. It takes no inputs, and produces a set of encodings $𝐸$, covering all valid instructions in the instruction space. It makes use of five functions: NextUncoveredInstruction, IsValidInstruction, RandomizedSearch, Tunnel and AnalyzeEncoding.

The function NextUncoveredInstruction takes as input a set of covered instructions $𝑆$. It returns an instruction $𝐼$ which is not in the set of covered instruction $𝑆$. In our implementation, we start at the byte sequence 00 and then sequentially return all other byte sequences in lexicographical order. We picked a lexicographical ordering because it is simple to implement. The actual order is not relevant for the algorithm.

The function IsValidInstruction takes as input an instruction $𝐼$ and checks if it is valid, i.e., if executing it does not cause the CPU to throw the undefined instruction exception.

The function RandomizedSearch takes as input an instruction $𝐼$ and performs a randomized search for the first valid instruction after $𝐼$. We use $𝐼$ as lower bound and the highest possible instruction ($\text{FFFFFFFF}\dots$) as upper bound for the search. We then repeatedly pick random byte sequences within the search range. If the random byte sequence is a valid instruction, we reduce the upper bound. When the upper bound has not changed for 250000 iterations, it returns the set of instructions between $𝐼$ and the upper bound.

The function Tunnel takes as input an instruction $𝐼$ and performs tunneling [8–10] to find the first valid and analyzable instruction. Tunneling initially steps through byte sequences one-by-one. Every $2^8$ steps the step size is multiplied by $2^8$. Whenever the instruction length changes, the step size is reset to zero. This makes the number of steps needed to skip over an instruction with an invalid 64-bit immediate value $2^8\ast 8$ instead of ${\left(2^8\right)}^8$. Once a valid and analyzable instruction is found, it returns the set of instructions between $𝐼$ and the valid and analyzable instruction.

The function AnalyzeEncoding takes as input an instruction $𝐼$ and runs encoding analysis on the instruction. Encoding Analysis is described in Section Section 4.3. Encoding analysis returns an encoding $𝑒$. This encoding has a bitpattern, which represents the set of instructions covered by the encoding.

The algorithm repeatedly selects the next instruction not yet covered, and analyzes it. If the next instruction is not a valid instruction, randomized search is used to skip it and all consecutive invalid instructions. If it is a valid instruction, encoding analysis is run. Normally, encoding analysis produces an encoding. If this is the case, the bitpattern is used to skip over all other instructions covered by the encoding. Finally, in some cases encoding analysis might be unable to analyze the instruction. This can happen for example when the instruction violates some of the assumptions we have listed in Section Section 2.2.1. In such a case, we do not have a bitpattern, and we also cannot use randomized search. Instead, we resort to tunneling [8–10].

Skipping using bitpatterns guarantees that we do not skip over valid instructions. Randomized search and tunneling may cause us to skip over valid instructions. We therefore use bitpattern based skipping whenever possible.

As the instruction’s length is often determined by a few bits in a single byte of the instruction, tunneling generally works correctly. However, there are edge-cases where this does not work. For example, consider the case where byte sequences 1b00-1cff are invalid, except for 1c05. In this case, tunneling will step through 1b00-1bff in steps of 1, but after checking 1c00 the step size is increased to 256, which means the next instruction checked is 1d00. This skips over the valid instruction 1c05. Because of these limitations, we skip instructions using bitpatterns or randomized search whenever possible.

Randomized search is more reliable than tunneling, but only applicable for invalid instructions. It might still skip over valid instructions. This can be the case when the chance of finding the valid instruction in 250000 tries is low. We picked the threshold through testing against tunneling. Randomized search with a threshold of 250000 iterations performs better or equivalent to tunneling for all in-scope areas of the x86-64 instruction space. In particular, it correctly handles the tunneling edge-case described above.

4.3 Encoding Analysis

The goal of encoding analysis is to generate an encoding, i.e., parts and dataflows, from a concrete instruction bitstring. We propose a novel infer-generalize-specialize approach. This approach consists of three steps: inferring dataflows, generalizing the dataflows into an encoding, and specializing the resulting encoding. The infer step produces dataflows which are consistent with all concrete observations. The generalization step uses these dataflows as a basis to form a generalized encoding.

The generalization step is purely speculative, and might produce an encoding with incorrect generalizations. Generalizations are incorrect when the dataflows in the resulting encoding are not consistent with actual CPU behavior. To counter this, the specialization step removes these by specializing the encoding for cases where a generalization is proven incorrect via an observation.

Each of these three steps require the generation of random CPU states. In the rest of this subsection, we first describe how this is done, and then provide details on each of the three steps of the infer-generalize-specialize approach.

4.3.1 Random CPU State Generation

For small CPU architectures, it is sometimes possible to exhaustively verify all possible input states. For modern architectures such as x86-64, exhaustive verification is impossible without access to hardware designs. We therefore can only verify the semantics that we generate on a subset of all possible input states.

Uniformly distributed random input states are often not useful for fuzzing. For example, when incrementing a 32-bit value we only have a 1 in $2^{32}$ chance of seeing a carry in the highest bit if we pick uniformly distributed random numbers (the only case where this happens is 0xFFFFFFFF). Interesting inputs often contain many consecutive zeros or ones. Therefore, our random generation is based on the computation $\left({𝑅}_{64}\ll {𝑅}_{𝑧}\right)\gg {𝑅}_{𝑘}$ where $\ll$ and $\gg$ are bit shifts, ${𝑅}_{64}$ is a uniformly distributed random 64-bit number and ${𝑅}_{𝑧},{𝑅}_{𝑘}$ are random uniformly distributed valid bit shift counts. The resulting number is then randomly negated or kept as-is. This computation produces numbers where the number of leading and trailing zeros and ones are approximately uniformly distributed. This random generation needs to run billions of times for each encoding we analyze. Improving quality of the random numbers reduces the speed at which we are able to generate new random numbers. We have therefore opted to use this simple expression consisting of only two bit shifts.

4.3.2 Inferring Dataflows

For a given an instruction $𝐼$ consisting of $𝑁$ bits, we analyze the instruction $𝐼$ as well as the bit-flipped variants $\text{flip}\left(𝐼,𝑛\right)$ for each $0\le 𝑛<𝑁$, where $\text{flip}\left(𝐼,𝑛\right)$ bit-flips the $𝑛$th bit in $𝐼$. This produces dataflows for $𝑁+1$ instructions that we will generalize into an encoding. The analysis is run separately for each of the $𝑁+1$ instructions.

Inferring dataflows consists of analyzing memory accesses and dataflows. Analyzing memory accesses consists of finding a set of accesses $𝑀$ as defined in Section Section 2 that encompass all memory accessed by an instruction. This makes it possible to reduce the CPU state to include just the parts of memory that are read or written by the instruction. Analyzing dataflows consists of finding a set of source and destination tuples $\left(𝑆,𝐷\right)$ that accurately describes all data-dependencies between the input and output CPU state of the instruction.

The algorithm for identifying memory accesses is shown in Algorithm 2. It takes as input an instruction $𝐼$ and produces the set of memory accesses $𝑀$ performed by $𝐼$. It makes use of three functions: FindPageFaults, FindAddressComputations and AccessGeneratesPageFaultOnNextPage.

The function FindPageFaults takes as inputs the instruction $𝐼$ and the current set of memory accesess $𝑀$. It generates the set of page faults $𝑃$ that happens when instruction $𝐼$ is executed on a set of randomly generated CPU states where all accesses in $𝑀$ are mapped.

The function FindAddressComputation takes as input instruction $𝐼$, the current set of memory accesses $𝑀$ and a set of page faults $𝑃$. It aims to find an address computation $𝑎$ that is consistent with all page faults $𝑃$. A computation is consistent with a page fault it the computation either returns the same address as the page fault, or if there is a computation in $𝑀$ that already maps to the same page.

The function AccessGeneratesPageFaultOnNextPage takes as input instruction $𝐼$, the current set of memory accesses $𝑀$, the new address computation $𝑎$ and a size $𝑛$. It generates a CPU state which places the new access $𝑎$ exactly $𝑛$ bytes away from the end of a page, and executes instruction $𝐼$ on this state. It returns whether the execution of instruction $𝐼$ caused a page fault at the first address of the next page.

Algorithm 2 infers memory accesses iteratively. Each iteration, we generate a set of page faults $𝑃$ that occur with the current set of memory accesses $𝑀$. If $𝑃$ is not empty, this means that the instruction $𝐼$ performs memory accesses that we have not covered in $𝑀$. We find a computation that is consistent with all page faults $𝑃$, and then determine the size of the access by generating input states that place the access near the end of a page. If we place the access too close to the end of the page, such that it does not entirely fit on the page, we will get a page fault. By iteratively increasing the distance to the end of the page until the access fits on the page, we can determine the size of the access. We then extend the set of memory accesses $𝑀$ with the new computation $𝑎$ and size $𝑛$, and repeat this process.

After inferring all memory accesses, we can infer the dataflows.

The algorithm for inferring dataflows is shown in Algorithm 3. It takes as input an instruction $𝐼$ and the set of memory accesses $𝑀$ for this instruction, produced by Algorithm 2. It makes use of two functions: FuzzForDataflow and Reduce.

The function FuzzForDataflow takes as input the instruction $𝐼$, the set of memory accesses $𝑀$, and the set of found byte-wise dataflows ${𝐷}_{𝑏}$. It returns a dataflow $\left({𝑏}_{𝑠},{𝑏}_{𝑑}\right)$, which represents a dataflow between byte ${𝑏}_{𝑠}$ in the input state and byte ${𝑏}_{𝑑}$ in the output state. We say that there is a dataflow $\left({𝑏}_{𝑠},{𝑏}_{𝑑}\right)$ if there is some input CPU state for which a change to the value of ${𝑏}_{𝑠}$ causes the value of ${𝑏}_{𝑑}$ in the output CPU state to change. The function only returns dataflows that are not already present in the set of found byte-wise dataflows ${𝐷}_{𝑏}$. It uses fuzzing to try and find a pair of CPU states which demonstrates the existence of a dataflow. If no dataflow is found, it returns None.

The fuzzing strategy consists of generating a random CPU state, and then generating another state by randomly changing some part of the state. This can be a single byte, a subset of all bytes not present in the sources in the hypothesis, or all bytes except some subset of the sources in the hypothesis. We exclude some sources of the hypothesis to ensure that we can find sources for destinations that are already present in the hypothesis. That is, if we already know that a modification in ${𝑏}_{𝑠}$ causes a change in ${𝑏}_{𝑑}$, we must generate pairs of states where ${𝑏}_{𝑠}$ is identical to be able to discover that a modification in ${𝑏}_{{𝑠}^{\prime }}$ also causes a change in ${𝑏}_{𝑑}$.

The function Reduce reduces the dataflows between individual bytes in the CPU state to dataflows between storage locations, by merging byte dataflows of consecutive bytes, and translating byte indices to storage location names. It takes as input the set of found byte-wise dataflows ${𝐷}_{𝑏}$, and returns a set of dataflows $𝐷$ as described in Section Section 2.2. This makes the dataflows usable in encodings and reduces noise. Because we rely on fuzzing, sometimes not all dataflows are found. By merging dataflows, the chances of this showing up in the resulting dataflows are reduced.

4.3.3 Generalizing Dataflows into Encodings

We generalize an encoding from the set of inferred dataflows from the previous Section. For each bit-flipped instruction $\text{flip}\left(𝐼,𝑛\right)$, we compare the dataflows and memory accesses against those of the original instruction $𝐼$.

Bit-flipping has been shown to be effective for guiding disassembler fuzzing [22]. Rather than guiding a fuzzer, we use bit-flipping to determine which bits are likely to belong to parts of the encoding. This requires more extensive analysis of the changes that occur when flipping a bit.

In modern general-purpose instruction sets like x86-64, bits in an instruction often serve a single purpose. For example, there can be a bit in an instruction that is used in the selection of the source register. That bit typically is not also used for other things such as a memory computation or a destination register. When changing those bits, only the source register changes. This reduces the complexity of the instruction decoder in the CPU, as those bits can be wired directly to the register bank without further processing. We check for changes that are common uses of bits that serve a single purpose:

1. If a register in the dataflows changes, the bit is a register-bit candidate
2. If the output of some dataflows changes, the bit is an immediate-bit candidate
3. If the offset of a memory access changes, the bit is an immediate-bit candidate
4. If a memory computation changes, the bit is a memory-computation-bit candidate
5. If more than one of the above apply, the bit is unknown

We form parts from using the candidates found from comparing the bit-flipped instruction variants. Each candidate affects certain storage locations in the dataflows or memory accesses. We consider candidates to be similar if they affect the same storage locations in the dataflows and memory accesses. Each set of similar register-bit candidates forms a register part. Consecutive and similar immediate-bit candidates from immediate value parts. Each set of similar memory-computation-bit candidates form memory computation parts. Two parts conflict if they both share one or more affected storage locations. We repeatedly remove the smallest part until there are no conflicting parts.

For register parts, we additionally enumerate every value to determine the exact register. We do this separately for each register part. For example, if we have three register parts, each 4 bits in size, we will run per-instruction dataflow analysis on 33 more instructions, 11 for each register part. The other five possible values for each register part have already been analyzed during the bit-flipping phase.

We do not aim to recover the exact encoding such as described in, for example, the Intel Reference Manual. This would be impossible, as we infer encodings bottom-up, rather than top-down. We also do not aim to identify every part in an encoding. The primary goal is to produce encodings that make enumeration feasible. This only requires identifying some subset of parts that is large enough to allow efficient skipping of instructions.

4.3.4 Specializing Encodings

Specialization aims to fix any incorrect generalizations that might have occurred. Dataflows are generalized into an encoding based on heuristics. This happens without any verification: generalization is based on heuristics, it does not use observations. Since generalization only looks at single bit-flips, more complex interactions between multiple bits are not accounted for.

The original instruction $𝐼$ is used as the ground truth for specialization. We try to find another instruction ${𝐼}^{\prime }$ also covered by the encoding, where the sources (i.e., registers or memory) can be assigned values such that at least one destination has a different output after executing $𝐼$ compared to ${𝐼}^{\prime }$. If we find such an instruction ${𝐼}^{\prime }$, the encoding is not describing the instruction correctly. We fix this by removing bits from parts to ensure that the encoding no longer covers ${𝐼}^{\prime }$.

To determine which bit to remove, we first find many instructions using the method above. We then find the index of the bit that most often differs from the original instruction $𝐼$, and remove this bit. To remove a bit, we simply replace it with the concrete value from $𝐼$. For example, consider the case where $𝐼=\text{00000000 11000001}$ which we have generalized into an encoding with bitpattern 00000000 110bb0aa. To remove the last bit, we replace it with the last bit of $𝐼$, which is a 1: 00000000 110bb0a1. Additionally, the part mapping of the bitpatterns and the dataflows have to be updated accordingly to account for the change of aa into a.

We use fuzzing to identify incorrect generalizations. The fuzzing strategy consists of generating pairs of CPU input states that are identical except for the instruction that is executed.

4.4 From Encoding to Semantics

We implement existing program synthesis techniques to demonstrate the amenability of encodings to automated synthesis. Program synthesis consists of generating a program from a specification. As we assume no access to the hardware designs of the CPU, the only specification we can generate are input/output examples (I/O examples). An I/O example is a tuple consisting of the inputs provided to the program, and the corresponding correct output. For example, an I/O example for a function $𝑓\left({𝑥}_0,{𝑥}_1\right)=𝑦$ might be ${𝑥}_0=4,{𝑥}_1=2,𝑦=6$.

For each encoding, synthesis has a timeout of 7.5 minutes. This timeout has been chosen such that it allows sufficient time for synthesizing more complex semantics, while keeping the runtime acceptable. Because synthesis uses randomly generated I/O examples, runtime varies based on the quality of the I/O examples. If synthesis failed or timed out, this might be because the first few I/O examples were low-quality. This might have caused synthesis to spend most of the allotted time searching in the wrong direction. Starting with a clean slate with different random I/O examples can resolve this. Therefore, we re-run synthesis a second time if the first attempt failed or timed out.

An encoding consists of multiple dataflows. Each dataflow can be synthesized independently. We represent the dataflow as a function $☐({𝑥}_0,{𝑥}_1,\dots )=𝑦$, where ${𝑥}_0,{𝑥}_1,$ etc. are the sources of the dataflow, and $𝑦$ is the destination. We use program synthesis to find an implementation for function $☐$.

We need a synthesis algorithm that can operate on I/O examples, is efficient, and is suited for synthesizing CPU semantics. By combining existing techniques, we construct such an algorithm.

We use Counter-Example Guided Inductive Synthesis (CEGIS) [23, 24]. CEGIS consists of two parts, a learner and an oracle. The learner repeatedly forms hypotheses, and the oracle provides counterexamples to these hypotheses. This process repeats until the hypothesis is correct, i.e., the oracle cannot present a counterexample.

Our learner is an I/O example-based synthesis algorithm. It generates hypotheses based on the I/O examples it has received from the oracle. Our oracle is a fuzzer that will verify the hypothesis against at most 2 million randomly generated input states. It uses the CPU as the ground truth, and tries to find counterexamples that show that the hypothesis is not equivalent to the actual CPU behavior.

The fuzzer uses three random generation techniques: normal generation, generation with equalities and generation from interesting inputs. Normal generation re-uses the random generation from encoding analysis, described in Section Section 4.3. Generation with equalities also uses the random generation from encoding analysis, but chooses one storage location at random and copies its value to another storage location chosen at random. This produces an input state where two storage locations are equal. Finally, generation from interesting inputs randomly picks an interesting input state, and randomly modifies a storage location, a single byte in a storage location, or a single bit in a storage location. An input state is interesting if it disproved any of the previous hypotheses.

Our learner uses decision trees to scale synthesis to larger problems, and uses enumerative program synthesis to synthesize individual expressions in the decision tree. We synthesize Boolean decision trees using a divide-and-conquer technique based on work by Alur et al. [25]. Decision trees have conditions (integer expressions returning only 1-bit values) on non-leaf nodes, and integer expressions on leaf nodes.

Since we need to synthesize programs from only I/O examples, our only choice of search technique is enumerative program synthesis. Rather than enumerating all possible programs from a grammar, we enumerate over programs derived from a list of templates. A template is an expression that contains zero or more holes. Synthesis consists of enumerating all possible ways to fill holes, for each template. In contrast to synthesis using grammars, a hole can only be filled with a constant or an input. We use separate lists of templates for integer expressions and conditions.

The choice for template-based synthesis is primarily motivated by performance benefits. By using a set of templates that is known and enumerable at compile-time, we are able to compile the templates to machine code. This significantly reduces the overhead of template evaluation, and increases synthesis performance.

We use 143 templates for integer expressions, and 553 templates for conditions (of which 351 are derived automatically from 39 integer expressions). These templates are handwritten. The integer expression templates consist of (combinations of) arithmetic operations such as addition or multiplication, and logical operations, such as AND, OR, or bitshifts. The Boolean templates primarily consist of zero checks, sign checks and parity computations derived from the integer expressions. They also contain more generic conditions such as $\_+\_<\left(\_\ll \_\right)$. We see that these conditions end up being used, for example, to saturate addition ($𝐴+𝐵<\left(1\ll 8\right)$).

Compared to Godefroid and Taly [6], we define many more templates. This is explained by counting differences, scope differences and flexibility differences. Godefroid and Taly’s templates are parameterized by operand size and operation, while we use separate templates for each combination of parameters. For example, Godefroid and Taly’s “Bit-wise group” flag output template corresponds to around 30 of our templates. While Godefroid and Taly’s scope is limited to x86-32 ALU instructions, our scope is all userspace non-floating point instructions. Additionally, we include x86-64 extensions such as BMI that Godefroid and Taly do not support. Godefroid and Taly’s flag templates are tailored to the specific operation that is being synthesized. For example, all flag outputs of Godefroid and Taly’s “Bit-wise group” must be a combination of up to three Boolean terms over the main output. Our templates are defined independently of a main output, which is necessary because we do not have access to a disassembler library to identify the main output.

Expressions are synthesized by filling in templates with holes. Each template contains zero or more holes. A hole can be filled with a constant or an input ${𝑥}_{𝑖}$. Although individual expressions are constrained to predefined templates, the combination of multiple templates in decision trees makes this approach efficient. For example, a conditional jump instruction might perform a computation similar to $\ast \text{if}\ast \left(\neg 𝑎\wedge \neg 𝑏\oplus 𝑐\right)\oplus 𝑑\ast \text{then}\ast 𝑥+𝑛\ast \text{else}\ast 𝑥+2\ast \text{fi}\ast$ to update the instruction pointer. It would be infeasible to generate such an expression in one go. However, because we generate a decision tree we can split this expression into six sub-expressions: $𝑎$, $𝑏$, $𝑐$, $𝑑$, $𝑥+𝑛$ and $𝑥+2$. All of these expressions are very easy to synthesize.

An expression consists of function calls and terms. Expressions always operate on signed 128-bit integer values. Function calls are simple built-in operations, e.g., addition or bit shifting. Terms are either constant values or inputs. Constant values $𝐶$ can be $0..16$, $8𝑛-1$ and $8𝑛$, where $1\le 𝑛\le 8$. An input is the value of a source, i.e., ${𝑥}_{𝑖}$, and an interpretation.

Dataflow sources and destinations can be integer values smaller than 128 bits (e.g., 64-bit general-purpose registers) or byte sequences (e.g., memory). Therefore, inputs must be converted to 128-bit integer values, and outputs must be converted back to the right size. Inputs can be interpreted as signed or unsigned, and big-endian or little-endian values. Outputs are converted back by taking the lower $𝑁$ bits of the 128-bit output of the expression. When a destination is a byte sequence, the output can either be encoded to bytes as big-endian or as little-endian.