InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy

InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy Michael Chesser1 , Paul Quirk2 , Douglas Cooke1 , Guy Farrelly1 , Surya Nepal3 , and Damith C. Ranasinghe1 1 Adelaide University 2 Defence Science and Technology Group 3 CSIRO

arXiv:2608.13042v1 [cs.CR] 13 Aug 2026

Abstract

from PIC microcontrollers to modern x86-64 and ARM/Thumb. Significantly, SLEIGH specifications underpin Ghidra [37], the dominant open source multi-architecture tool-chain for reverse engineering and binary analysis, and multi-architecture emulators such as Alligator from AirBus [10], Icicle [8], MetaEmu [7] and Styx [22]. In Ghidra’s disassembler and decompiler, SLEIGH specifications directly determine how binary code is decoded, lifted, and interpreted by analysts and automated scripts. As a result, SLEIGH specifications sit on the critical path of security workflows such as vulnerability discovery, malware analysis, fuzzing, firmware auditing, and program understanding. This widespread reliance amplifies the consequences of specification errors: flaws in SLEIGH can propagate across multiple tools, users, and workflows. Yet, despite this central role, the reliability of SLEIGH specifications remains an underexplored problem. In practice, SLEIGH specifications are large, painstakingly constructed artifacts that encode both instruction formats and their semantics. Developing faithful processor specifications is a non-trivial task. For instance, the ARM manual is 12,000 pages where complexities such as the operand dependent behavior of instruction mnemonics negates simplistic examination of mnemonics. Additionally, the 2025 edition of the Intel Software Developer’s Manual [1] exceeds 5000 pages. The specifications must capture subtle architectural behaviors across diverse and often poorly documented instruction set architectures. Further, to address the demand for rich, fast and safe computation, modern architectures are constantly evolving, with new instructions and features added each year1 , translating to an increase in instructions and complex instruction-bit encodings in ISAs. The painstaking construction and update of specifications to integrate architectural changes whilst maintaining backward

Processor specifications underpin critical security and program-analysis tools such as disassemblers, decompilers, and emulators, yet, their correctness is rarely examined. Errors in specifications distort program behaviour, obscure vulnerabilities, and enable analysis-evasion techniques. Validating processor specifications is a non-trivial task. Our study is a significant undertaking to enable, for the first time, the systematic validation of open-source SLEIGH language specifications, predominantly used by Ghidra. We design and implement a testing framework based on an automated oracle validation strategy by proxy. Our approach leverages the structure encoded in a specification itself to enumerate decodable instruction forms and generate targeted initial states. Then differentially test the successful decoding and emulation of those instructions by comparing emulators exercising the processor specification against hardware references. Applying InSPECtor across diverse, open-source specifications—x86-64, AArch64, ARM/Thumb, RISC-V, MSP430—embedding differences in specification styles, author preferences, and instruction set architecture designs, we uncovered over 38,920 discrepancies that led to 125 unique bugs with proposed fixes, identifying decoding and semantic defects as well as cross-vendor inconsistencies. We distill our findings into 8 concrete recommendations to drive future improvements. Our work underscores the importance of specification correctness and provides a practical tool to substantially improve the fidelity of SLEIGH processor specifications, strengthening the reliability of downstream security and analysis tools.

1

Introduction

SLEIGH is a domain-specific language (DSL) for describing 1 For instance, microprocessor advancements, such as Single Instruction, Multiple Data (SIMD), Arm Neon, Advanced Matrix Extensions (AMX), Advanced Vector Extensions (AVX) or cryptography extensions are often incorporated to cater to artificial intelligence, high-performance computing and security-focused workloads.

processor specifications that decode and translate instructions into the architecture-agnostic intermediate representation (IR), Pcode [38]. There are over 35 processor families expressed in SLEIGH specifications, covering a diverse range of processors 1

compatibility makes the specifications intrinsically susceptible to bugs. Even small mistakes—such as incorrect operand decoding, missing side effects, or inconsistent semantics can propagate silently through static and dynamic analysis tools. These errors may lead to misleading decompilation output and unsound program analyses, ultimately undermining the conclusions drawn by security practitioners; often exploited by malware to detect virtual environments [6] and hide from analysis [30, 34, 35]. Importantly, the critical dependency on SLEIGH specifications has not been met by a commensurate, open source assurance of its correctness. Therefore, we are motivated to improve the correctness of SLEIGH processor specifications.

• We design, implement, and evaluate the methodology in the prototype InSPECtor system for testing specifications, including, GenSYS—a test case generation tool that integrates these techniques and JuxtaPlayer—a robust differential testing environment capable of executing test cases on both emulators and hardware-assisted virtual machines. • We analyze the discovered bugs, identify their root causes, propose fixes, and distill 8 recommendations for improving the SLEIGH DSL to prevent future issues. Importantly, we use InSPECtor to test x86-64, AArch64, ARM/Thumb, RISC-V, and MSP430 SLEIGH specifications. Our work uncovered over 38,920 discrepancies. Manually triaging, categorizing and prioritizing the discrepancies, we identified the root causes of the discrepancies leading, the discovery of 125 unique bugs

By enhancing the veracity of SLEIGH processor specifications, we expect to drive improvements across all their applications.

with proposed fixes submitted to Ghidra maintainers. We open-source InSPECtor on GitHub https://github.com/SleighInSPECtor/

The Study. In this first study, we expend our effort to improve the veracity of the SLEIGH processor specifications with the hope of generalizing our learning outcomes to broader specification assurance research. Importantly, these specifications need to be updated and reassessed for correctness as ISAs evolve and new instructions are added. Our efforts will facilitate testing implementations thoroughly, and automating this process in the future. Previously, studies have examined improving the correctness of CPU emulators [24–26,39], hypervisors [3], processor hardware [17, 33, 36], disassembly veracity (textual representation accuracy) [18,29], while a few have tested the semantic correctness of binary lifters [9, 19] but specification level correctness has received less attention. Although the work in [27] considered usability of Pcode for formal analysis and the authors in [4] made significant strides to validate the veracity of Sail specification language described semantic models for significant parts of ARMv8-A, RISC-V, and CHERI-MIPS, the correctness of the extensive multi-architecture support within the SLEIGH specifications have not been examined. In seeking to design an approach to uncover specification bugs, we observe that a processor specification itself encodes enough structure to drive systematic validation. So, we introduce InSPECtor, a framework that automatically traverses SLEIGH specifications to enumerate decodable instructions, derive targeted execution states from semantic definitions, and perform differential testing against hardware reference systems. This enables high-coverage, specification-driven testing without redundant instruction exploration.

2

Instruction Encodings and SLEIGH Specifications Primer

Before describing our specification-driven testing approach, we briefly review ISA-level instruction encodings and the structure of SLEIGH specifications. Throughout this discussion, we use examples from a simplified ISA with a variable length instruction set, similar to x86-64, defined by the SLEIGH specification in Figure 12 . Instructions are represented as sequences of bytes, referred to as instruction encodings. Although each concrete instruction instance has its own binary representation, instruction encodings within an ISA typically share a common structure. Bits are grouped together to form fields that have specific meanings, such as the registers, immediate values, and addressing modes. For example, in the simplified ISA, addi r2,r3,0x1234 is encoded as follows:

i16=0x1234

op=1

rn=3 rd=3

0001001000110100 0000001 000 011 010 SLEIGH specifications exploit this structure by expressing decoding as a hierarchy of declarative rules. These rules, called constructors, are organized into groups called tables. The SLEIGH specification in Figure 1 is annotated with the key components of each constructor:

Our Contributions. In summary: • We propose symbolically traversing SLEIGH specification decoding rules, a new, systematic methodology that aims to exhaustively generate instruction encodings, extracting edge cases for testing and deriving initial input states that trigger these edge cases.

• Pattern section: defines the mapping from an instruction encoding to the other components of the specification using 2 For simplicity, we omit the parts of the specification that define the register and memory configuration of the ISA, as well as the mapping from field names to bit ranges in the instruction encoding.

2

Root constructors

Subtable Constructors

Subtable group name

1 Op: "nop" is op=1 & i16=0 { export 0; } 2 Op: "syscall" is op=0 & i16=1 { export 1; } Checks if the instruction bits are 000 in the op field and =1 in the i16 field 3 4 Imm0: is i16=0 {} 5 ImmX: i64 is i16 [ i64 = (i16 << 48) >> 48; ] { export i64; } 6 Derive the value of i64 based on the i16 field 7 Mem: [rn] is rn & i16=0 { export *rn; } 8 Mem: [rn + ImmX] is rn & ImmX { export *(rn + ImmX); } Return a reference to a location to be used by the parent 9 10 :^instruction is prefix=0xf8; instruction [ ctx.mem=1; ] {} Check if 0xf8 matches then move to next byte (prefix constructor) 11 12 :run Op is op=0 & Op { HwOp(Op); } 13 Recursively find a matching constructor from the Op subtable 14 :nop is op=1 & rd = rn & Imm0 { } 15 :mov rd,rn is op=1 & rd & rn & Imm0 { rd = rn; } 16 :addi rd,rn,ImmX is op=1 & rd & rn & ImmX { rd = rn + ImmX; } Instruction semantics in terms of simpler ops 17 18 :ld rd,Mem is ctx.mem=1 & op=1 & rd & Mem { rd = *Mem; } Legend: Pattern section

Decode actions

Display section

Semantics section

Figure 1: An example of a SLEIGH specification for a simple ISA with a variable length instruction set, such as x86-64. boolean expressions that reference the instruction encoding and the current decoder context—a SLEIGH-specific mechanism to encode or transfer information between constructors as discussed later.

tors. For example, context bits are often used to alter operand decoding in the presence of prefix bytes. Given this initial state, the decoder attempts to find a constructor whose pattern section matches the current state. Constructors are considered from most to least specific, where specificity is determined by the number of constrained bits in the pattern section3 . If no constructor matches, the encoding is treated as undecodable or invalid. When a match is found, the decoder applies the corresponding decode actions to update its state. It then recursively evaluates any subtables referenced in the pattern section using the updated state. Constructors in each subtable are matched and evaluated in the same way until the instruction is fully decoded. Once decoding is complete, the instruction semantics can be determined by evaluating the semantic section of the constructors matched during decoding, potentially substituting subtable references with the values exported by the corresponding constructors. As a concrete example, consider the addi r2,r3,0x1234 instruction from before. After extracting the fields from the instruction encoding, the decoder obtains: rd=2, rn=3, op=1, i16=0x1234. The decoder attempts to find a constructor in the root table that matches the current field values. The nop, mov, addi constructors all match the current opcode (op=1). However, nop is rejected because rd (2) != rn (3) and

• Decode actions: optional expressions, after the pattern section between ‘[ ]’, to specify how to update the decoder context when the pattern section is matched. • Display section: defines the textual representation of the instruction used for disassembly. • Semantic section: defines the meaning of the instruction in terms of the simpler ISA-independent operations (Pcode). Subtable constructors sharing a group name (e.g. Op) form a table and is responsible for decoding a particular aspect of the instruction, such as opcode matching or operand decoding, and is used at different points during the decoding process. Constructors that do not specify a table name (start with just ‘:’), are implicitly associated with a root table, and are the starting point for the decoding process. All other tables are used for decoding only when they appear in the pattern section of one of the root-level constructors such as Op on line 12. Employing a SLEIGH specification for decoding begins with two inputs: a sequence of bytes (the instruction encoding) and a set of context bits. Context bits are a SLEIGH-specific mechanism used for two purposes: i) to encode information relevant to decoding that is not directly present in the instruction encoding, such as the current processor mode (e.g., ARM vs. THUMB); and ii) to transfer information between construc-

3 Tie-breaking depends on the declaration order, and non-overlapping constructors can be matched out-of-order. However, the general principle is that constructors with more constraints are considered first.

3

GenSYS Instruction Generation

x86-64 AArch64

State Generation

∞

α = λξ

λ>σ

Ω≠λ

λ?

Deferred constraints SMT Solver Constructor Traversal

α = λξ

λ>σ

Ω≠λ

λ?

Generated instructions

RISC-V

Initial states

SLEIGH Specs

JuxtaPlayer State Setup

Single-step execution

Differential Analysis

Instr: 67 48 8b 00 Reg: RAX=100,RBX=10 State: Mem: 0x1000=00000000

Diffs

Test Corpus

Figure 2: A high-level overview of InSPECtor; the specification-driven test case generation (GenSYS detailed in Section 3.1 & 3.2) and differential testing (JuxtaPlayer detailed in Section 3.3) process to identify bugs or defects in the specification encodings. mov is rejected because i16 (0x1234) != 04 . The addi constructor matches, causing the decoder to evaluate any decode actions (none in this case), and to recurse into any referenced subtables. The addi constructor has a single referenced subtable ImmX. This subtable has a single constructor (Line 5) with no additional constraints (the bare i16 field is unconstrained), so it matches immediately, and the decode action computes i64=0x1234. At this point, all operands have been decoded5 , and the target disassembly is obtained by substituting these decoded values into the display section of the matched constructor, yielding addi r2,r3,0x1234. Similarly, the instruction semantics are obtained by substituting the decoded operands into the semantic section, resulting in the semantics for the instruction being: r2 = r3 + 0x1234. For a complete and technical description of SLEIGH DSL, interested readers are directed to the resource in [38]. For instruction generation, we are interested in traversing all possible decode paths and the task, primarily, requires considering the pattern and decode sections of the constructors we discussed in this section.

3

unique instruction recognized by a SLEIGH specification. However, testing every possible combination of operand and immediate values, is both computationally wasteful and unnecessary, since most operand variations do not affect an instruction’s core behavior. Instead, we generate all instructions with unique semantics by traversing a specification’s constructors as we detail in Section 3.1, and combine them with a representative subset of operand values: simple defaults, random selections, and values that force operand aliasing within the instruction semantics. In the following, we elaborate on the instruction generation and state generation methods in GenSYS followed by the testing method encapsulated in JuxtaPlayer.

3.1

Instruction Generation

For SLEIGH specifications, generating all instructions with unique semantics is equivalent to generating one instruction for each possible decode path in the specification. We can do this by determining which constraints on the instruction encoding must hold for a given constructor to be selected during decoding, and then solving those constraints to produce a concrete instruction encoding. Conceptually, this process can be viewed as a constraint satisfaction problem (CSP). In practice, however, efficiently collecting and solving all relevant constraints requires a complex traversal of the decode tree. In particular, the traversal must handle several kinds of constraints, account for implicit constraints introduced by overlapping constructors, manage decode actions that modify decoder state during traversal, and avoid unbounded recursion. The core of the traversal process is outlined in Algorithm 1. Starting from the root-level table, G ET I NSTRUCTIONS invokes the C ONSTRUCTORT RAVERSAL algorithm, which selects a constructor c for the current subtable t (forking the current state S if there were multiple valid choices), translates any constructor constraints for that constructor (T RANSLATE), and updates the current state S before recursively traversing any subtables. The output of C ONSTRUCTORT RAVERSAL

Methodology

We describe the design and implementation of InSPECtor to identify issues in SLEIGH specifications here. Figure 2 presents an overview of the approach where GenSYS systematically generates decodable instructions as test cases, effectively aiming to cover all instructions recognized by a SLEIGH specification. JuxtaPlayer applies a differential testing strategy, comparing the behavior of executing an instruction in a SLEIGH-based emulator with a hardware reference. The key idea here is to employ the SLEIGH-based emulator as a proxy for assessing the correctness of a target specification. Ideally we would systematically generate and test every 4 For the mov constructor, this requires evaluating the Imm0 constructor and backtracking which is described in more depth in Section 3.1.1. 5 Mapping register indices to specific registers is handled by attachments, which is described in Section 3.1.1.

4

is the complete set of constraints, which are solved using an SMT solver to produce concrete instruction encoding X. G ET I NSTRUCTIONS then restores a previously saved fork and selects a different constructor, repeating this process until every possible path has been explored. The algorithm’s state S consists of three components: i) an instruction bit vector I = b1 b2 · · · bn ; ii) a context bit vector C = b1 b2 · · · bm ; and iii) a collection of deferred constraints. Each bit in a bit vector may take either a fixed value (0 or 1) or an unknown value (?). Although the size of the instruction bit vector (n) may not be known until traversal is complete, this can be handled by defining an upper bound6 and ignoring any unreferenced bits after all constructors have been selected.

Deferred constraints are additional constraints on the instruction bit vector that cannot be resolved to a fixed value (e.g., inequalities). These constraints are solved simultaneously after the traversal process has completed and all constraints are known. By maintaining known instruction bits separately from deferred constraints, the algorithm can efficiently test satisfiability during traversal and prune large portions of the search space. For example, if a constructor in a subtable requires a particular bit to be 1, but that bit is already known to be 0 from an earlier constraint, then the corresponding subtree can be discarded immediately, significantly improving efficiency. Next, we detail the complex component of the method employed in the instruction generation algorithm design.

Algorithm 1 Instruction Generation 1: function G ET I NSTRUCTIONS 2: O ← {} ▷ The list of generated instructions (Output). 3: F ← {} ▷ The set of fork points for unselected paths. 4: S ← initial state, t ← root subtable 5: while S ̸= ∅ do 6: S, f ← C ONSTRUCTORT RAVERSAL(S, t) 7: F ← F ∪ f ▷ Add new fork points found during subtable traversal. 8: X ← S OLVE(S) ▷ Get instruction bytes satisfying all constraints. 9: if X is SAT then 10: O.push(X) 11: (S,t) ← F.pop() 12: return O

3.1.1

The following sections describes the method for translating the pattern section of each constructor into a combination of fixed bit patterns and deferred constraints encapsulating the T RANSLATE function in Algorithm 1. Simple constraints. Most constraints involve equality checks between a constant and a range of instruction or context bits. These constraints can be translated directly into fixed values for the corresponding bits in the instruction or context bit vector. If a new constraint is unsatisfiable given the previously fixed values, traversal stops and the algorithm continues with a different set of constructor choices. Otherwise, the newly constrained bits are updated and traversal continues. Example. Using specification in Figure 1, consider the run constructor on line 12 and the corresponding Op subtable:

13: 14: t: subtable to add constraints from 15: S: the current decoder state 16: function C ONSTRUCTORT RAVERSAL(S, t) 17: F ← {} 18: if S at traversal limit then 19: return (UNSAT, F) 20: c ← C URRENT C ONSTRUCTOR(S, t)

26: 27: 28: 29: 30: 31: 32: 33: 34: 35:

if S has unselected constructors then F.push(N EXT C ONSTRUCTOR(S, t)) S.simple ← S.simple ∧ T RANSLATE(c.simple) if S.simple is UNSAT then return (UNSAT, F) ▷ Terminate traversal early if simple constraints are UNSAT. S.deferred ← S.deferred ∧ T RANSLATE(c.cplx) ∧ T RANSLATE(c.attach) for oi in F IND OVERLAPS(S, c) do S.deferred ← S.deferred ∧ ¬T RANSLATE(oi ) S ← A PPLY D ECODE ACTIONS(S, c) for ti in S UBTABLES(c) do ▷ Recursively traverse subtables and merge constraints. S, f ← C ONSTRUCTORT RAVERSAL(S, ti ) F ←F∪ f if S is UNSAT then return (UNSAT, F) return (S, F)

1 2

Op: "nop" is op=1 & i16=0 { export 0; } Op: "syscall" is op=0 & i16=1 { export 1; }

12

:run Op

...

21: 22: 23: 24: 25:

Translating Constructor Constraints

is op=0 & Op

{ HwOp(Op); }

When the :run constructor is selected, the algorithm updates the instruction bit vector so that the bits corresponding to the op field are fixed to 0. It then attempts to select a constructor from the Op subtable by checking each constructor’s constraints against the current instruction bit vector. The Op:"nop" constructor requires the op field is equal to 1, which conflicts with the current value of 0, so it is immediately discarded. The Op:"syscall" constructor is compatible with the current instruction bit vector, so it is selected and traversal continues with the i16=1 constraint specified by the constructor. All simple constraints can be reduced to a bitwise maskand-compare operation. For example, when generating an instruction corresponding to run syscall, the final set of constraints passed to the SMT solver is (i & 0xfffffe00 == 0x00010000), where i denotes the instruction bit vector. Complex constraints. Beyond simple equality constraints, SLEIGH also allows constructors to use more complex con-

The size of the context bit vector (m) is simply a constant defined by the specification. Every bit in the instruction bit vector is initialized as unknown (Ii = ? for i ∈ 1, 2, · · · n), while the context bit vector is initialized to a fixed value determined by the current processor configuration (for our simple ISA specification in Figure 1, the context is initialized to 0). 6 Considering the largest possible instruction across all tested ISAs is 120

bits (15-byte x86-64 instructions), max(n) = 120.

5

Example. A possible set of attachments for our example specification in Figure 1 is as follows:

straints to match instructions. This includes both inequalities and constraints involving non-constant expressions. Unlike simple constraints, there is often no single value that can be assigned to the constrained bits to satisfy the constraint outright. One possible strategy would be to choose any value satisfying the constraint and continue traversal; however, such a choice may conflict with constraints introduced by later subtables, preventing valid instructions from being generated Another option would be to exhaustively explore all possible values, but this would require traversing an excessive number of paths and would generate many redundant instructions Instead, we elect to check that such constraints are potentially satisfiable (i.e., they do not already conflict with the existing simple constraints) and then add them to a list of deferred constraints, which are solved once traversal is complete. Once constructors for all subtables have been selected, the full set of constraints for the current instruction is known. To obtain a final instruction encoding, a symbolic expression is constructed from the instruction bit vector together with the deferred constraints. This expression is then passed to an SMT solver (Z3), which attempts to find a concrete assignment to all bits satisfying the combined constraints. If the solver succeeds, it returns a concrete instruction encoding; otherwise, it reports that the constraints are unsatisfiable. Example. As an example, consider the :nop constructor from line 14 of our example specification in Figure 1: 14 :nop

attach variables [rd rn] [_ r1 r2 r3 r4 r5 r6 r7]

Whenever rd or rn appears unconstrained in the specification (e.g., in the :mov and :addi constructors), its value is interpreted according to the attachment mapping. For example, ‘rd=1’ corresponds to r1; ‘rd=2’ corresponds to r2, and so forth. In this example, an attachment index of 0 has no associated register, indicated by the ‘_’ operator. To account for this, we treat such cases as implicit complex constraints: ‘rd != 0’ and ‘rn != 0’. For instruction generation, these constraints are handled in the same way as other complex constraints discussed previously. Implied constraints from overlapping constructors. The behavior of an instruction is primarily determined by its ‘opcode’ field,7 which specifies the operation performed on the instruction’s operands. In general, two instructions with the same opcode have the same semantics regardless of their operand values. However, some instructions can be represented as a specific sub-encoding of a more general instruction. For example, copying a value between registers (e.g., mov r0,r1) is semantically equivalent to adding zero to a source and storing the result in a destination register (e.g., addi r0,r1,0). These instructions are often referred to as ‘pseudo-instructions’, and many ISAs use them to reduce redundant encodings. Although SLEIGH specifications could ignore pseudoinstructions and always decode them as their generic counterparts, modeling them explicitly benefits both human and machine analysis—A more specific textual representation improves disassembly for human analysts, and defining specialized semantics can simplify both static and dynamic analysis. In addition to pseudo-instructions, some ISAs include instructions with more complex operand encodings that require special handling during decoding. For example, in both x8664 and MSP430, instruction encodings include ‘addressing mode’ bits that alter the interpretation of operand fields. To model such encodings, SLEIGH provides a mechanism known as constructor specialization, which allows multiple constructors within the same subtable to match the same instruction encoding. Recall (Section 2), the SLEIGH decoder prioritizes matching constructors from most to least constrained. Consequently, for an instruction to match a less constrained constructor, it must also avoid matching any overlapping constructors that would be considered first. This behavior must be modeled during generation to ensure that the generated instruction encoding matches the intended constructor. To do so, we treat the target constructor as if it carried an additional implied constraint requiring all preceding overlapping constructors to not match.

is op=1 & rd = rn & Imm0 { }

For an instruction to match this constructor, the rd and rn fields must be equal. This constraint cannot be translated directly into fixed values for the instruction bit vector, since there are many possible values for rd and rn that satisfy it. Rather than choosing an assignment prematurely, we add the constraint rd = rn to the list of deferred constraints. At the end of traversal, the final constraint passed to the SMT solver would therefore be ‘(i & 0xfffffe00 == 0x00000200) && (i.rd == i.rn)’. To optimize the process further, we check whether deferred constraints remain potentially satisfiable given the currently known bits. Suppose there is a deferred constraint ‘i16 > 0’. The algorithm then checks whether at least one bit in the range corresponding to i16 is either unknown or equal to 1. If a different constructor requires that i16=0, we can immediately reject it due to the ‘i16 > 0’ constraint, which avoids wasting time traversing impossible constructor combinations. Constraints imposed in attachments. Fields referenced by a constructor may be linked to attachments that control the interpretation of the underlying bits. While most attachments allow all field values, some SLEIGH specifications use attachments to mark certain operand values as invalid. To handle this during instruction generation, invalid values are excluded by introducing appropriate deferred constraints.

7 To keep instruction encodings compact, the full opcode may be split

over multiple fields depending on the ISA.

6

Example. Consider lines 14–16 of Figure 1:

brackets after the pattern section. Each decode action evaluates an arithmetic expression, possibly over context and/or instruction bits, and writes the result to a field in the context bit vector. Phased decoding. For phased decoding, context fields are used to split the decoding process into multiple phases, where previous phases can set context bits that are used as constraints in later phases. During instruction generation, this mechanism is straightforward to handle; at any point in the traversal, the phase has a fixed value, so only constructors for the current phase need to be considered. Phased decoding is not used in our example specification but we provide the following example (inspired by the AArch64 specification) to explain. Example. Consider the case where the immediate field is split across the instruction encoding:

14 :nop is op=1 & rd = rn & Imm0 { } 15 :mov rd,rn is op=1 & rd & rn & Imm0 { rd = rn; } 16 :addi rd,rn,ImmX is op=1 & rd & rn & ImmX { rd = rn + ImmX; }

To generate a mov instruction, we must avoid matching the :nop constructor. Since the only difference between the two constructors is the constraint ‘rd = rn’, we add its negation, ‘rd != rn’, to the list of deferred constraints for the :mov constructor. In rare cases, there are no unique constraints that can be added to distinguish between two overlapping constructors. For example, consider the :addi constructor in the example specification. This constructor overlaps with both :nop and :mov. Similar to before, we can avoid matching :nop by adding the constraint ‘rd != rn’. However, at the constructor level, the constraints for :mov and :addi are identical. The only difference between the two constructors is the final subtable (i.e., Imm0 and ImmX). Since subtables are evaluated only after a constructor has been selected, it may seem impossible for :addi to match. However, SLEIGH supports backtracking; if no constructor matches in a later subtable, the decoder may return to an earlier point in the process and try a different constructor. Therefore, to ensure that :addi is selected, we must force the SLEIGH decoder to backtrack from the :mov constructor. To achieve this, the generation algorithm inspects all constructors in the Imm0 subtable and adds additional constraints that ensure that no constructor matches. In this example, the Imm0 constructor requires ‘i16 = 0’, so we add the constraint ‘i16 != 0’. If the subtable contained multiple constructors, we would instead need a combined constraint ensuring that all of them fail to match. The final set of constraints the algorithm solves for the addi constructor:

:^instruction

is phase=0 & immhi & immlo & instruction [ phase=1; imm=(immhi<<8 | immlo); ] {} :mov rd,rn is phase=1 & op=0xf & rd & rn & imm=0 { rd = rn; } :addi rd,rn,imm is phase=1 & op=0xf & rd & rn & imm { rd = rn + imm; }

Assuming the phase context field is initialized to 0, only the first constructor matches the current context. The instruction generation algorithm therefore selects it and updates the context bit vector according to the decode actions. When the algorithm subsequently resolves the instruction8 subtable, it uses the updated context, which now has ‘phase=1’. Since the phase value is now 1, only the second and third constructors now match, allowing them to essentially exist as if they were separate subtables. The mov constructor demonstrates the usefulness of phased decoding, where it is able to define a constraint on the entire immediate value instead of separate constraints on each subfield. Prefix parsing. Prefixes are handled similarly, however in addition to updating the context bit vector, prefix constructors also consume part of the instruction bit vector during traversal. To handle this, the algorithm must track the offset used by subsequent constraints. Additionally, SLEIGH specifications (e.g., x86-64) may allow the same constructor to repeatedly match to support multiple prefixes. To avoid generating arbitrarily long encodings, we incorporate a traversal limit during the traversal process, which is a practical solution given that physical hardware will always have an upper limit on instruction length. Example. Consider the :ld constructor (line 18 of Figure 1):

(i & 0x0000fe00 == 0x00000200) && (i.rd != i.rn || i.i16 != 0) && Avoid :nop Avoid :mov (i.i16 != 0)

Notice that when we add constraints to resolve the overlap with the :nop constructor, we allow the overlap to be resolved either by negating the simple constraints or by backtracking, maximizing the flexibility the solver has to generate an encoding, allowing the algorithm to generate addi r0,r0,1. Self-referencing constructors and decode actions. SLEIGH allows constructors to be self-referencing, meaning that a constructor may reference the same subtable to which it belongs. This functionality is used for two main purposes: i) phased decoding and ii) optional prefix parsing. In both cases, the self-referencing constructor must be able to influence subsequent steps of the decoding process. To support this, constructors may specify decode actions in square

10 :^instruction is prefix=0xf8; instruction [ctx.mem=1] {} 18 :ld rd,Mem is ctx.mem=1 & op=1 & rd & Mem { rd = *Mem } 8 Recall that the instruction identifier is a special identifier that matches

the root subtable—constructors prefixed with just ‘:’.

7

3.1.3

For the :ld constructor to match, rather than one of the arithmetic instructions with the same opcode, the context field ctx.mem must be set to 1. This occurs only if the prefix constructor (line 10) is matched first; that constructor adds the constraint that the instruction must begin with the prefix byte (0xf8) and updates the context field ctx.mem to 1. Consequently, when the instruction generation algorithm tries to generate an encoding for the :ld constructor, it emits the following constraint9 : i & 0x0000fe00ff != 0x00000400f8. If the result of a decode action depends on unconstrained parts of the instruction encoding, the corresponding parts of the context bit vector become partially unknown. Because the only source of unknown values is the instruction bit vector, each such unknown context bit can be expressed as a function of instruction bits and constants. Any later constraint on those context bits can therefore be translated into a constraint on the instruction bit vector. These translated constraints are added to the deferred-constraint set and solved after traversal; such cases are, however, uncommon. Example. Consider the following extension to our example specification:

Listing 1: register_lists operand decoding in the ARM SLEIGH specification: Each register in the list can be either present or absent and there are 16 registers (r0 to r15) leading to 216 potential constructor combinations. After returning from C ONSTRUCTORT RAVERSAL, all constructors have been selected. However, when we attempt to solve the constraints to find a concrete instruction encoding (line 8), there can still be several bits in the encoding that remain unconstrained, or only partially constrained (e.g., imm > 0). These ‘free’ bits correspond either to generic operands or to unused bits that do not affect the instruction. As a result, each instruction typically has a range of valid encodings. Exhaustively generating and testing every combination of these free bits would reintroduce the same exponential explosion we are trying to avoid. Instead, the algorithm generates a smaller representative set of solutions that covers the most interesting cases. To do this, S OLVE (line 8) attempts to identify possible edge cases in the instruction encoding. It uses Z3’s support for minimizing and maximizing values [5] to generate test cases at the minimum and maximum encodings permitted by the constraints, which helps expose potential off-by-one errors in partial constraints. For example, for the :nop constructor from line 14 of our example specification, the complex constraint ‘rd = rn’ Z3 generates encodings corresponding to ‘rd = rn = 0’ and ‘rd = rn = 7’. Next, analysis of the instruction’s semantics identifies any registers that could alias with operands derived from the unconstrained bits. Additional constraints are then added to the instruction bit vector to force operands to match the aliasing register, generating targeted cases for each potential alias.

Rd2: ctx.rd2 is ctx.rd2 < 7 & ctx.rd2 { ... } Mem2: is rn & ImmX { ... } :ld2 rd,Rd2,Mem is op=2 & rd & Rd2 & Mem & Mem2 [ctx.rd2 = rd+1; ] { ... }

The instruction generation algorithm must track that ctx.rd1 is equivalent to rd+1, and ensure that an subsequent constraint on ctx.rd1 is mapped to a corresponding constraint on rd. For example, the ‘ctx.rd1 < 7’ constraint in the Rd2 subtable becomes ‘rd+1 < 7’. 3.1.2

Solving Instruction Encodings

Avoiding Excess Constructor Combinations

SLEIGH specifications use attachments to map the numer-

ical value of a field to a specific register. However, more complex relationships between fields which cannot be easily expressed with attachments are sometimes required. In such cases, specifications resort to mapping field values through separate constructors, which can induce an exponential number of constructor combinations. For example, ARM allows any combination of the registers r0 to r15 to appear in the register lists used by the load/store-multiple instructions LDMIA and STMIA. The corresponding decoding specification (Listing 1) requires traversing approximately 216 paths to cover all operand combinations. To avoid generating an instruction for every combination, the algorithm tracks which constructors have already been covered and prunes them during subtable traversal when this type of explosion is detected (traversal limit on line 18).

3.2

State Generation

The behavior of an executed instruction depends on the state of the processor. Therefore, to comprehensively test a specification, we need to explore not only changes to the instruction bytes but also to the initial input state. The state is made

9 Constraints simplified; in practice, additional constraints are required

for overlap resolution and attachments.

8

Group Addition/Subtraction Multiplication/Division Zero/Sign Extension Boolean Bitwise Shifts Comparisons Overflow conditions Floating point Branches

Example Pcode Operations I NTA DD, I NT S UB I NT M ULT, I NT D IV, I NT S DIV I NT Z EXT, I NT S EXT B OOL X OR, B OOL O R, . . . I NT X OR, I NT O R, . . . I NT L EFT, I NT R IGHT, . . . I NT E QUAL, I NT L ESS, . . . I NT C ARRY, I NT B ORROW, . . . F LOATA DD, F LOAD S UB, . . . C BRANCH

Edge cases Overflow/underflow, result negative, result zero. Operands negative/zero. Input all ones or all zeros, output non-negative and negative. Result true/false. Result zero/non-zero. Oversized shift operand, overflowing result, sign-bit set. Operands equal or ±1. Result true/false. Operands with interesting floating point values (e.g. NaN). Condition is true and path constraints for future operations.

Table 1: Edge cases used for generating initial interesting input states from Pcode operations. up of several components, including the values of ISA-level registers, memory, and processor-specific internal state (e.g., model-specific registers, caches, and micro-architectural resources). For specification testing, we assume the internal state is fixed and is reset between instruction executions. However, both ISA-level registers and memory are allowed to vary.

r2 = r0 IntAdd r1 ZF = r2 IntEqual 0 NF = r2 IntSignedLessThan 0

The ADD instruction is broken into four Pcode operations. Consider the second operation, r2 = r0 IntAdd r1, r0 and r1 are inputs to the instruction and are replaced with symbolic variables ar0 , br1 (line 5 of Algorithm 2), the E DGE C ASES method returns the following three assertions10 :

Algorithm 2 State Generation (from Pcode edge cases) 1: function G EN I NPUT S TATES(P) ▷ P: List of Pcode oper-

ations for an instruction. G ← {} ▷ Output G: Set of edge case triggering input states. 3: S ← initial symbolic state 4: for pi in P do 5: (a, b) ← S.get(pi .inputs) ▷ Get the current symbolic value of the inputs. 6: o ← S YMBOLISE(a, pi .op, b) ▷ Symbolically execute pi . 7: for e in E DGE C ASES(pi .op) do 8: s ← S OLVE(A SSERT((a, b, o) triggers e)) ▷ Find a concrete input s triggering e. 9: if s is SAT then 10: G ← G∪s 11: S.set(pi .output, o) ▷ Update the symbolic state with the output of pi . 12: return G

ar0 + br1 overflows,

2:

ar0 + br1 = 0,

ar0 + br1 s< 0

Values for ar0 , br1 are obtained symbolically solving the assertions using an SMT solver (e.g., for the third assertion ar0 = 0, br1 = −1). After saving saving valid edge-case triggering inputs, the algorithm updates the symbolic state (line 11) such that, r0 = ar0 + br1 . This means, when generating edge cases for the later Pcode operation ZF = r2 IntEqual 0, we actually generate edge cases for ar0 + br1 = 0. All assertions are solved independently; the state generation process does not attempt to find initial input states that simultaneously solve multiple assertions. This avoids an exponential explosion of assertion combinations, many of which would be unsatisfiable. In practice, complex input states are still generated from later Pcode operations because any preceding Pcode operations that modify inputs to the operation are incorporated in symbolic expressions. In some cases, previous operations can restrict the possible values of the operands; this makes the edge cases unsatisfiable and causes no corresponding input state to be generated. For many ISAs, instructions may update status register bits (flags) when specific conditions occur while executing the instruction. In SLEIGH specifications, these conditions are checked using individual Pcode operations, which will have edge-case-triggering inputs generated for them. This can result in the state generation process producing duplicate input states, since the conditions checked by the instruction are often the same as the edge cases defined for state generation. Example. In the example code above, the same initial input state that satisfies (r0 + r1 s< 0) (edge case for addition), also

Although many specification bugs are discoverable with an arbitrary initial state, certain bugs may manifest only when an instruction is executed under extremely specific initial conditions. To allow us to test these cases, Algorithm 2 is used to generate interesting input states by identifying potential edge cases from the semantics section of the specification. We exploit the fact that SLEIGH breaks up instructions up into simpler operations (Pcode) to express each edge case as an assertion in terms of the inputs and/or output of a specific operation. By systematically defining edge cases for each Pcode operation and generating initial states that trigger each edge case, it is possible to find discrepancies even when the semantics are only subtly incorrect. Example. Consider an ADD instruction that also needs to update various arithmetic flags, for example on x86-64 the Pcode for ADD r0,r0,r1 is as follows:

10 s< represents a signed less-than operation.

OF = r0 IntCarry r1

9

satisfies (r2 = −1) (edge case for comparisons) since r2 = r0+r1. However, this redundancy is useful because it ensures that missing or incorrectly implemented semantics are still tested. In cases where exact duplicates are generated, they are automatically removed before the test cases are executed. A summary of the edge cases used for state generation is provided in Table 1. The motivation for these edge cases and how they interact with more complex Pcode operations such as branches and memory accesses is in Appendix D.

by the state generation algorithm. The instruction pointer (i.e., RIP) is positioned at the instruction address, and the system is set up to execute a single step. The execution may succeed or raise an exception. In either event, the final system state is recorded, including modified memory values, registers, and any exception information, for later comparison. Notably, for performance, instead of mapping the entire address space, JuxtaPlayer lazily maps the memory whenever a memory exceptions occur and replays the instruction.

3.3

4

Differential Testing Environment

We use a differential testing strategy to discover bugs in SLEIGH specifications using the generated test-cases. The strategy is implemented in JuxtaPlayer, which executes the test cases on two different systems: i) an emulator derived from the SLEIGH specification under test; and ii) hardwarebased reference systems.

Evaluation

We focus our evaluation on five important and diverse SLEIGH specifications (x86-64, AArch64, ARM/Thumb, RISC-V, and MSP430) to assess coverage, discrepancy patterns, and bug prevalence across diverse ISA designs. This section summarizes the results for all ISAs. All instructions were generated using the SLEIGH specification from Ghidra 10.3.11 GenSYS is executed on a Threadripper Pro 5995WX with 64 GB RAM12 . Through the evaluation, we seek to answer the following questions:

• SLEIGH-Based Emulator Configuration. JuxtaPlayer uses Icicle [8], a SLEIGH-based emulator, to execute Pcode operations from the SLEIGH specification. Icicle supports the execution of individual instructions (single-stepping) within all of the test architectures and provides APIs for directly reading and writing the system state required for differential testing. Icicle also supports tracking exceptions that occur during execution, making it possible to handle memory faults as described above.

• How generalizable is InSPECtor in traversing the ISA variants of SLEIGH specification constructions of various authors and contributors? (Section 4.1) • How effective is InSPECtor at finding bugs in SLEIGH specifications? (Section 4.2) • What is the nature and impact of the bugs found by InSPECtor? (Section 4.2 and Appendix E)

• Hardware-Based Reference (KVM). Our goal is to ensure SLEIGH specifications accurately reflect the behavior of real hardware, therefore, we use hardware as an oracle. We support hardware-assisted virtual machines (VMs) for x86-64, AArch64 and ARM/Thumb—detailed in Appendix F.

• How effective are the techniques employed by InSPECtor? (Section 4.3)

4.1

• Hardware-Based Reference (Debugger). Available MSP430 and RISC-V hardware did not support virtualization extensions, therefore it was not possible to use KVM-based VMs. As an alternative, we use userspace and hardware debuggers, that still allow us to execute instructions on real hardware while still allowing the system state to be manipulated and observed. For the MSP430 reference system, we use an MSP430FR5969 microcontroller which allows single-stepping instructions and reading/writing of the system state. For RISC-V we use the BeagleV®-Ahead containing a quad-core Xuantie C910 processor which implements RV64GC including the 0.7.1 draft version of the vector extension, and use ptrace on Linux for debugging. We defer technical details of the approaches to Appendix F.

Test Case Generation

A means to objectively assess the test coverage of a given specification is necessary for assurance and evaluation of the testing method to understand its effectiveness. Analogous to considering code-coverage metrics as a proxy for a bug-based metric in software testing [16,21] or fuzzing [12], we consider measuring constructor coverage as a proxy for the testing coverage of a given specification. Given the fundamental unit of syntax in SLEIGH is a constructor, constructor coverage is a meaningful evaluation metric. We compute constructor coverage as: Constructor Coverage =

Constructors Used in Generation . Total Constructors in a Spec.

Further, to demonstrate the efficiency of the generation process, we also report the test Generation Time.

Before an instruction is executed, the environment is configured to match the initial state defined by the test case. This includes a region of memory containing the instruction bytes with the execute permission set. Registers and other memory regions are then initialized according to the values produced

11 Commit: 104d9592485c2fb6c7ab5177c71d8d70140a3d03 12 The traversal process is single threaded, while state-generation was run

in parallel using 8 threads.

10

Architecture x86-64 AArch64 ARM/Thumb RISC-V MSP430

Generation Time (s) Traversal Solving State Gen 491.99 1019.56 425.45 0.24 90.09 573.02 1387.26 691.99 59.11 0.07 39.69 6.76 0.09 46.10 557.15

Generated Tests Instructions States 71,797 713,231 25,042 123,407 30,521 207,716 9,725 39,393 7,440 124,784

Constructor Coverage 97% 97% 96% 99% 90%

N/A 77 104 50 4 1

Missing Constructors Redun. Incom. Bugs 5 0 4 41 4 0 79 2 3 6 1 0 79 0 0

Table 2: Summary of the generation process execution for each architecture. For missing constructors, N/A: Not applicable (only used different SLEIGH config), Redun.: Redundant constructors, Incom.: Unreferenced constructors due to incomplete specifications, Bugs: root-caused bugs in the specification. Architecture x86-64 AArch64 ARM/Thumb RISC-V MSP430

Execs/s 176,404 3,723 3,572 1,012 0.164

Raw 349,897 52,833 78,251 15,682 93,043

Groups 18,827 7,342 9,785 937 2,028

Unimplemented 9159 5127 4652 322 145

Alignment 653 21 12 0 0

Exception 2467 1451 4182 373 468

Flags 3627 5 32 8 163

Float 605 426 376 222 0

PC 257 0 10 1 68

State 2059 312 521 11 1184

Table 3: Discrepancies found by running JuxtaPlayer on the testcases generated by GenSYS. Raw: total number of discrepancies (including variations to input state). Groups: unique constructor combinations for which at least one discrepancies was found. Each of these groups was then assigned a category based on observing: the set of differences (exception state and memory/register values) and the operations in the SLEIGH semantics for the constructor combination. Generation Results. GenSYS was used to generate instructions and states for x86-64, AArch64, ARM/Thumb, RISC-V and MSP430. The results are summarized in Table 2. These results represent unique constructor combinations, i.e. instructions, including variants, and input states covering the edge cases defined in Section 3.2.

• Specification Issues (Bugs). A small set of the missing constructors represent issues in the SLEIGH specification.

4.2

Differential Testing Analysis

Across all architectures, JuxtaPlayer discovered 589,713 discrepancies between the output states of the SLEIGH-based emulator and the hardware reference system corresponding to 38,920 unique constructor combinations after grouping. However, many of these stem from hardware/processor-specific instructions (see Appendix C), or from instructions that are not fully implemented in the specification13 . Analyzing the discrepancies enabled us to identify 125 unique bugs. In the following sections, we describe the discovered discrepancies, the analysis process and the specification bugs. We also present an analysis of root causes and sources of errors we uncovered along with bug examples.

Although the instruction generation process employed by GenSYS exhaustively explores the SLEIGH specification, as

indicated by the coverage metrics, there was a total of 460 constructors without corresponding test cases identified by GenSYS. We manually investigated each missing constructor and categorized them into the following categories and report them in Table 2: • Not Applicable. Many of the missed constructors correspond to other processor modes or extensions (e.g., for x86-64 real mode or protected mode, for AArch64 pointer authentication), that the SLEIGH configuration excludes at runtime. Since we do not use alternate modes, these constructors are not applicable and can be ignored.

4.2.1

Discrepancy Analysis and Specification Bugs

In general, discrepancies correspond to either bugs or SLEIGH specification limitations. In Table 3, discrepancies are first grouped by unique constructor combinations and then assigned to categories we describe here, using an ordered set of heuristics. This categorization serves two purposes. First, it separates discrepancies that are unlikely to correspond to actionable SLEIGH bugs—for example, those involving unmodeled hardware state or undefined behavior—from dis-

• Redundant. A large proportion of the missing constructors correspond to cases where they completely overlap with a set of more specific constructors. While these redundant constructors are benign and have no impact on the specification’s correctness, they can be removed to simplify the specification and improve maintainability. • Incomplete. Some parts of the specification are incomplete, and the missing constructors correspond to cases where a subtable constructor is fully implemented, but the parent constructor is missing.

13 SLEIGH allows custom Pcode operations as placeholders for instructions during decompilation. Since no Pcode is associated with these operations, they cannot be emulated and analyzed using differential testing.

11

crepancies that more directly indicate errors in decoding or instruction semantics. Second, it provides a consistent link between the observed form of a discrepancy and the mechanism used to detect it, which makes the results easier to interpret. • Unimplemented: Discrepancies corresponding to either: unimplemented behavior—caused by placeholder semantic operations in the SLEIGH specification; or unsupported behavior—use of architectural state not represented in our model, such as model-specific registers (MSRs) or other hardware state not defined at the ISA level. These are detected by the presence of placeholder operations (e.g., unimpl blocks or custom pcodeop definitions), or the use of unmodeled registers in semantics. Unimplemented behaviors often arise for recently added ISA features, or instructions with difficult semantics to directly express in Pcode. Unsupported behavior typically corresponds to hardware-specific operations may depend on implementation-specific hardware details rather than ISAdefined semantics. • Exception: Discrepancies in the type or metadata (e.g., faulting address) of an exception raised by the SLEIGH semantics relative to the hardware reference. This category is detected whenever the primary difference is an exception outcome rather than a final-state mismatch. It also captures cases caused by ISA feature mismatches (e.g., instructions from some ISA extensions not present on the hardware reference, but included in the SLEIGH specification). Exceptions are also frequently related to unpredictable/undefined behavior. For example, on ARM/Thumb some instructions can be encoded with the program counter (PC) as a destination register, which is listed as unpredictable behavior in the architecture. The SLEIGH specification treats this as ignoring the operation in many cases, while the hardware reference raises an exception. Unfortunately, the variability of exception sources makes it difficult to automatically separate out true issues in this category from unpredictable/undefined behavior. • Alignment: Discrepancies related to alignment issues. They are separated out as a special case of exception discrepancies since these are generally unfixable without adding additional semantics to SLEIGH—see Section 5.1. • Flags: Discrepancies in architectural flags, such as condition-code or status bits. These are detected when the only observed state difference is in the flag register set. We isolate this class because flag behavior for some architectures is frequently related to undefined or unpredictable cases, and therefore benefits from a separate analysis. • Float: Discrepancies in registers or memory that arise along an execution path containing floating-point Pcode operations. These are detected by tracking whether the corresponding SLEIGH semantics use floating-point Pcode. This category is separated from general state discrepancies because some differences may reflect limitations of the

Architecture

Decoding

x86-64 AArch64 ARM/Thumb RISC-V MSP430

16 0 0 2 2 16

Total

Semantics Ordering 0 1 0 1 6 9

Incorrect Semantics 12 22 15 12 26 87

Aliasing

Total

4 0 2 3 1 9

32 23 17 18 35 125

Table 4: Summary of discrepancies and bug types by architecture. We detail the bugs for each architecture in Appendix G.

Pcode floating-point model rather than errors that can be fixed by modifying the SLEIGH specification. • PC: Discrepancies in the final program counter, including incorrect branch targets or advancement to the next instruction—e.g., from decoding the wrong instruction length on x86-64. These are detected when execution ends at a program counter different to the oracle. Such cases are strong indicators of decoding errors and therefore often correspond directly to SLEIGH specification bugs. • State: Any remaining discrepancy in registers or memory not captured by the preceding categories. This is the residual class used when the final architectural state differs but no more specific heuristic applies. In practice, these cases are often the most interesting, as they may indicate incorrect semantics, missing side effects, or incorrect handling of particular operand forms. Notably, the categories above serve as a prioritization mechanism for analysis as much as a descriptive taxonomy since discrepancies in classes are difficult to directly associate with a specific error in the SLEIGH specification. While each discrepancy corresponds to a possible bug, each bug usually results in many different discrepancies To analyze the discrepancies within a group, we manually aggregate discrepancies based on mnemonic, semantics and overlapping constructors, and then a representative example is selected to study. Time to triage a unique bug takes approximately 4 hours on average; the time varies significantly depending on root-cause complexity. Followed by a considerable time to craft, test and document suitable fixes for Ghidra maintainers. This process enabled us to identify 125 unique bugs, where: A bug = A unique root-cause fixed in an ISA. Consequently, the bug count is not the number of buggy instructions, which would be an inflated number. Tables for the unique bugs based on our analysis of discrepancies for x86-64, AArch64, ARM/Thumb, RISC-V and MSP430 ISAs are reported in Appendix G. To highlight the types of SLEIGH issues encountered across the specifications in the bugs discovered, we categorize the bugs described in Appendix G and summarize the results in Table 4. The classes of issues we identified in the bugs impact either decoding or semantics of an instruction. We elaborate on the classes of bugs in I-1 – I-15 in more detail, with bug examples, and provide 12

additional bug case studies beyond the examples therein in Appendix E.

ping constructors are under-constrained. This bug causes the wrong instruction semantics and disassembly to be used for the instructions associated with an unreachable constructor.

4.2.2

I-4 Over constrained constructors. Several constructors have additional constraints that are not present in the underlying ISA. For example on x86-64, two constructors require a specific bit in the decoder context to be matched. However, this bit is only set in 32-bit protected mode, even though the associated instructions are also valid in 64-bit long mode. This issue likely stems from a mismatch in the way context bits are used in the SLEIGH specification. On real hardware, the protected mode bit is set in long mode, but the SLEIGH specification only sets an equivalent bit when configured for 32-bit mode. The impact of this bug is that the corresponding instructions are incorrectly treated as invalid in long mode.

Decoding Issues

In general, decoding issues occur when incorrect constructor constraints prevent the correct instruction implementation from being selected. We detail these in the following. I-1 Redundant and out-of-order prefixes. Instruction prefixes are one of the most complex aspects of x86-64 instruction encoding and causes discrepancies between hardware vendors (see Section C), security-critical CPU bugs [28], and severe performance issues [13]. Similarly, the x86-64 SLEIGH specification contains many prefix-related decoding issues. x86-64 instructions allow redundant and duplicate prefixes; however, the SLEIGH implementation assumes that at most one of each prefix is present. For example, when multiple operand-size (66) or address-size (67) override prefixes appear, the specification misinterprets these prefixes, leading to discrepancies. Additionally, the 64-bit extension to the ISA introduces a new class of prefixes (the REX prefix) with different decoding rules compared to legacy prefixes. According to the ISA reference, there must be at most one REX prefix present, and it must follow all legacy prefixes. However, both the Intel and AMD CPUs tested are more lenient during decoding; any REX prefixes that precede legacy prefixes are ignored, and they allow multiple REX prefixes, only using the final one. The SLEIGH specification does not replicate this behavior; instead, it rejects all instructions where there are multiple REX prefixes, or the prefix is not the last one. While compilers avoid emitting unnecessary prefixes, thus reducing the impact of this issue on real-world code, such prefixes occasionally appear in handcrafted assembly for lowlevel performance optimizations. For example, OpenSSL uses redundant prefixes to align code to micro-architecturally friendly boundaries [2]. I-2 Context handling issues. An earlier version of the x8664 SLEIGH specification used a single context field for both indicating whether long mode (64-bit) instructions were decodable and for tracking the current address size. This design assumed that long mode could be inferred from the address size, because it has a different default setting compared to other processor modes. However, including an address-size override prefix (67) changes the current address size, causing the specification to mistakenly assume that the processor is not in long mode. Although the specification was later refined to introduce a dedicated context bit for long mode, many long mode instructions still reference the operand-size bit, resulting in discrepancies. I-3 Overlapping constructors. Some constructors are unreachable because every instruction encoding that matches them is instead matched by a different constructor (with different semantics). Further analysis revealed that many overlap-

I-5 Constructor ordering. For x86-64 specifically there was also several issues related to constructor ordering. Two unreachable constructors, corresponding to 64-bit variants of instructions, share the same encoding as their 32-bit counterparts, except for a mandatory REX.W prefix. However, the 32-bit variant allows the prefix to be present and is always matched first, preventing any encoding from matching the 64bit variant. This bug likely originates from unclear ordering rules. Since the 64-bit variant is not strictly more constrained than the 32-bit variant, the decoder defaults to the declaration order. This issue causes the wrong register sizes (32-bit instead of 64-bit) to be used for the instruction, resulting in incorrect disassembly and semantics. 4.2.3

Semantics Ordering Issues

I-6 Semantic ordering issues arise when correct outcomes are dependent on a specific order of operations which are not followed. This was common in the MSP430 ISA which makes heavy use of addressing modes to augment its basic instructions. These modes include direct and offset indexing, and address auto incrementing among others. All of which are available to the MOV instruction leading to cases such as MOV.W @R7+, 0x0(R7). The MSP430 was found to execute this instruction by resolving and incrementing the source register, before resolving the destination, performing the instruction’s operations with the pre-incremented value, and writing back the result. This causes loading the destination 0x0(R7) to be impacted by the increment of the source @R7+. This differed from the SLEIGH implementation which always performed the increment as the last operation of the instruction. This also occurred in pseudo-instructions such as POP.W SP (MOV.W @SP+, SP) even though they had separate Pcode semantics. Semantic ordering issues where also found outside of addressing modes in AArch64. The NGCS instruction’s output was written to the destination register, and then the flags where calculated off that registers value. However when using the zero register as the destination register no write is 13

performed, and the flags are always incorrectly calculated from the fixed value of zero. 4.2.4

instructions swap a value into the float CSRs by moving the source register to the CSR and the value in the CSR to the destination register. The Pcode implementation of this instruction attempted to do this without using a temporary, causing the value in the source register to be overwritten. This lack of a temporary when using aliased registers also occurs in the compressed instruction extension with the C.JALR ra instructions. This instruction should jump to the address held in the ra register and replace its value with the address of the following instruction, but was found to instead execute the instruction at the following address. Additionally in both RISC-V and AArch64 the zero register must always read the value 0, and writes to the zero register must be ignored, both contain bugs. The RISC-V SLEIGH specification handles these cases by using a subtable to export a temporary variable instead of the zero register. Many instructions do not do this and instead directly reference the zero register. This allows the instructions to write non-zero values to the zero register when it is used as a destination. The destination register for some instructions is intended to be 32 bits instead of the full register width. To handle this, a constructor rdW is used, which creates a temporary of the right size, sets its value to that of the destination register, and exports the temporary. When an instruction attempts to write to this aliased register, it would change the temporary but not the destination register. This prevented the FCVT instructions from outputting any result.

Incorrect Semantics Issues

Incorrect or missing semantics bugs appear when an implementation uses the incorrect operations, or does not implement all behaviors of an instruction. This was the largest category of bugs, but also contained the most subtle and unique mistakes. For example in AArch64 the BCAX instruction performed an or operations instead of an xor, and STLRB stored a word sized value instead of byte. In addition to these subtle issues, there where several wider classes of issues. I-7 Missing floating point semantics. The RISC-V floating point extensions encode smaller precision floats as NANboxed inside the larger registers, by setting all the unused upper bits to 1’s. However, the SLEIGH specification does not use this encoding for single precision floats when writing to the registers, nor does it propagate un-NAN-boxed values as NAN’s, causing all initial floating point test cases to fail. The extra logic that fixing this issue added to the start and end of all floating point instructions was not able to be filtered out by Ghidra’s decompiler, causing the decompilation to become bloated. I-8 Default values and behaviors. RISC-V defines specific result values for arithmetic exceptions. On divide by zero the division instruction should return 2width − 1, and the remainder should be the dividend. Currently there is no zero check before the division, resulting in this behavior being dependent on the execution environment default.

4.2.6

The problems we discussed previously can be addressed through careful editing of processor specifications. However, there are numerous issues requiring more fundamental design changes to simultaneously support accuracy of both decompilation and emulation use cases; we discuss these next.

I9 Incorrect register lists. To implement instructions operating on groups of registers in SLEIGH, recursive subtables are used where the different constructors conditionally include the Pcode semantics for that register. This occurs in MSP430, AArch64, and ARM/Thumb, with MSP430 having an issue where it did not correctly handle register wrapping, and ARM/Thumb having an issue where the registers where pushed in the wrong order. However, this style of implementation inherently requires duplicated sets of constructors based on the number of registers, requiring the same fix to be applied to each constructor in the set. 4.2.5

Unresolvable Issues

I-11 Unimplemented operations. The SIMD and vector instructions across x86-64 and AArch64 are partially implemented in Pcode and partially with added custom Pcode ops, with the semantic section of RISC-V’s vector extension completely unimplemented. A full Pcode implementation of these is possible, but would bloat the generated disassembly, and output Pcode for static analysis tools. I-12 Floating point issues. Floating point instructions contributed to a large number of discrepancies as many of the features which architectures use of the IEEE 754 standard are not exposed at the SLEIGH level. SLEIGH does not enforce a rounding mode and instead uses the environment’s default, while modern architectures (x86-64, AArch64, RISCV) provide a means to change the default rounding mode, as well as override the rounding mode for individual instructions. Architectures with hardware support for floating point numbers generally include the common encodings of FP32 and FP64 which are supported in SLEIGH. However, x8664 and AArch64 also support the FP16 and BF16 encoding

Aliasing Issues

I-10 The SLEIGH specification implements instructions using multiple Pcode operations, and when the source and destination operands refer to the same register or memory location, incorrectly ordering these operations can result in incorrect semantics. This issue is often observed in the implementation of SIMD instructions (x86-64, ARM/Thumb), where the destination register is frequently modified before the source register is fully read. For RISC-V this occurs in the Control and Status Register extension in the FSCSR/FSFLAGS/FSFRM instructions. These 14

Category Decoding Semantic Ordering Incorrect Semantics Aliasing

Unimpl. 5 0 1 0

Exec. 11 0 1 0

Flags 0 1 8 0

Float 0 0 4 0

PC 0 1 6 0

State 9 7 66 10

without adding additional semantics to SLEIGH as we discuss in Section 5.1. To generate results, we used the related discrepancies leading to the identification of the bug during triaging to conduct the analysis. The associations in Table 5 demonstrates that systematic discrepancy detection serves as a strong indicator for underlying correctness problems. The distribution of bugs in Table 5 suggests State related issues should be prioritized in analysis. Although discrepancy classes are difficult to attribute directly to bugs, Sate and Exception related discrepancies are strong indicators of errors in the SLEIGH specification.

Table 5: Summary of the the root-cause bugs triaged and fixed and their association to observed discrepancies types.

which SLEIGH does not have. SLEIGH also chooses to propagate NAN payloads, while the IEEE 754 standard leaves this to the implementers discretion. This differs from RISC-V and conditionally AArch64 which always return the canonical NAN. Properly fixing these discrepancies would require better floating point support from SLEIGH.

4.3

In this section we investigate the effectiveness of the designed technique to traverse a given specification to generate encoded instructions and discover specification bugs.

I-13 Unpredictable behavior. A number of discrepancies for x86-64, AArch64, and ARM/Thumb came from defined unpredictable outputs in their related ISA specifications. However these currently cannot be fixed as there is no single correct behavior.

Instruction Generation. To quantify the contribution of individual components in GenSYS, we perform an ablation study over its constructor traversal and constraint-solving techniques. We focus on three key aspects to evaluate: i) Simple constraints only (ignoring all deferred constraints); ii) Explicit constraints only (solve deferred constraints, but excludes implied constraints from overlapping constructors); and iii) No backtracking (solve all constraints, but assume backtracking from subtables is impossible) versus GenSYS (solve all constraints with backtracking allowed). We report two metrics to understand impact: i) ∆ Accuracy—the decrease in generation accuracy relative to GenSYS, where where accuracy is the percentage of generated instructions whose decode path matches the target constructors; and ii) Missed—the number of constructors for which no valid instruction encoding was found, despite a valid encoding being found by GenSYS. Table 6 shows that simple constraint solving alone, Simple Only, significantly reduces accuracy, particularly when applied to the MSP430 and RISC-V SLEIGH specifications. Without translating simple constraints, many generated instructions match different constructors than those intended, resulting in missed constructors during testing. Although, Explicit constraints only, shows a reduced accuracy drop, especially for MSP430, accuracy drops remain above 12% for

I-14 Memory alignment exceptions. Many SIMD and atomic operations have stricter alignment requirements than standard load/store instructions. When an operand is provided at an insufficiently aligned address, an exception should be generated. However, there is no mechanism to annotate these requirements in a SLEIGH specification, meaning the emulator is unaware that an exception should occur. While extra Pcode could be used, this case is better handled by adding explicit alignment to memory accesses. I-15 Missing instruction semantics. The x86-64 specification does not implement the auxiliary carry flag (AF) in any instruction, resulting in discrepancies in almost all arithmetic instructions. This is a known limitation of the specification (treated as a single bug) and likely remains unfixed because the auxiliary carry flag is rarely used in modern programs. Importantly, based on our in-depth analysis of the issues uncovered, we detail possible solutions in recommended modifications to the SLEIGH DSL in Section 5.1. 4.2.7

Effectiveness of Techniques

Discrepancy-Bug Associations

Although the relationship between discrepancies and bugs is not a simple one-to-one mapping, Table 5 discusses how triaged and fixed bugs in Table 4 relate to relevant observed discrepancies to distinguish those that relate to the bugs. Notably, a single bug may manifest in different types of discrepancies while a single discrepancy may be the result of multiple types of bugs. We observe up to three separate bugs triggered by a single discrepancy. Multiple discrepancies from the same bug are common, especially when incorrect semantics are encountered. Hence these numbers represent a lower bound. In addition, recall that Alignment related discrepancies are separated since these are generally unfixable

Arch. x86-64 AArch64 ARM/Thumb RISC-V MSP430

Simple Only ∆ Acc (↓) Missed 16.7% 995 13.2% 98 30.4% 302 57.7% 38 69.6% 388

Explicit Only ∆ Acc (↓) Missed 12.3% 65 13.7% 79 15.9% 80 54.7% 38 41.9% 58

No Backtracking ∆ Acc (↓) Missed 0% 0 0% 11 0% 75 0% 0 0% 0

Table 6: Summary of instruction generation accuracy (based on constructors used for decoding compared to generation), and missed constructors compared to GenSys, when solving techniques are removed. 15

each ISA. Then, with No Backtracking only, all of the generated instructions’ decode path matches the target constructors, as with GenSYS, but leads to Missed constructors. Overall, disabling constraint translation components significantly impact the method and instruction generation for all the tested ISAs where large parts of the specification can remaining untested.

Naive Approach

the SLEIGH specification contains a bug where the float-tointeger cast operation (trunc) is missing in the constructors that handle cases where the destination operand size matches the floating-point source operand size. These instructions have a complex encoding that requires a specific prefix byte and a multi-byte opcode, consequently they were never generated by the random approach. GenSYS generates constraints that force the appropriate prefix byte when generating this instruction and is able to find this bug. PACKUSWB. This instruction converts 16-bit signed words (ranging from −215 to 215 − 1) in the source operand into 8-bit unsigned bytes (from 0 to 28 − 1) for the destination operand. Values outside the destination range are saturated (i.e., negative values become 0 and values greater than 255 become 255). However, the SLEIGH specification contains an off-by-one error in a comparison operation, causing an input of 255 to be converted to zero. This bug occurs only for one specific input value, making it unlikely to be found by random testing. Through the edge-cases on the SLEIGH semantics, GenSYS generates a targeted states that test values near boundary conditions and is able to find this bug.

GenSYS

Figure 3: Constructors hit in the x86-64 SLEIGH specification and bugs found with the naive approach for testing with JuxtaPlayer. Notably, GenSYS generation and the execution of the resulting testcases takes <40 minutes for x86-64.

5

Comparison to naive approach. To further evaluate the overall effectiveness of the instructions and states generated by GenSYS, we can compare it to a naive approach devoid of our key techniques. Instead of modeling the SLEIGH decoding process we simply select a constructor at random, set any bits that have fixed constraints for that constructor, and fill any remaining bits with random values. For each generated instruction, we randomize the input state to derive the instruction used by JuxtaPlayer for testing. We compare the random approach to GenSYS on x86-64 across two metrics: i) Constructors Hit—the number of constructors for which at least one generated instruction correctly decodes to that constructor; and ii) Bugs—the number of bugs triggered from the 32 root-cause bugs discovered for x86-64. Notably, fully validating bug metrics would require a significant amount of manual analysis, as indeed performed in our primary analysis with InSPECtor, for the randomly generated instructions. Therefore, we automatically determine whether a bug was triggered. We manually annotated each bug with the conditions required for that bug to be detectable— a “canary" based on the constructors containing the bug. We provide canaries for each bug in our open-source GitHub repository. The results of the naive approach are shown in Figure 3. After generating 1.1 × 107 testcases taking 8 hours, the naive approach failed to generate any instruction that matches 1249 constructors (38% miss rate) and failed to find 15 bugs (47% miss rate). To better illustrate the failures of the naive approach, we consider two of the missed bugs below: CVTSS2SI/CVTSD2SI. These instructions are used to convert scalar floating-point values into integers. However,

Discussion

In addition to the limitations of this work and potential for future work, potential changes to the design of the SLEIGH specification language are discussed below. These suggested changes allow for improved maintainability, versatility, fidelity and understandability of SLEIGH specifications.

5.1

Recommendations for Improving SLEIGH

The SLEIGH language is demonstrably effective for specifying instruction semantics, Ghidra has over 35 ISAs expressed in SLEIGH. However, our study reveals that SLEIGH lacks features and constructs needed to express complex instruction behaviors suited for its applications in security workflows. Based on the issues uncovered in differential test result analysis in Section 4.2, we propose extensions to the SLEIGH language that could potentially lead to fewer bugs in specifications. We codify these broadly in: i) General recommendations based on the issues we uncovered in Section 4.2.2-4.2.5. These aim to better support the key use cases for SLEIGH whilst reducing the incidence of bugs when authoring and maintaining specifications; and ii) Recommendations to address the unresolvable issues identified in Section 4.2.6.

5.1.1

General Recommendations

The modifications to SLEIGH described here mainly aim to improve its expressiveness and usability to reduce bugs when authoring and maintaining specifications. 16

#1: Provide for decompiler hints Adding support for decompiler hints can enable highfidelity SLEIGH specifications to improve both emulation and decompliation.

prone and contribute to non-obvious aliasing issues such as those reported in I10 accounting for 9 out of the 125 bugs. A major subtlety is that the export statement is not evaluated alongside the rest of the semantic section; instead, it is evaluated at the point it is referenced in the semantic section of the parent constructor. Consequently, copying a register’s value to a temporary and then exporting the temporary behaves differently from exporting the register directly. For example, in bugs discovered in the x86-64 specification with aliasing issues, the SLEIGH specification code modifies the register in the main constructor, not realizing that the modifications also affect referenced registers in subtables. This could be avoided by introducing more logical accessor functions for exporting values—for example, forcing the use of temporaries—or by introducing warnings when a potential reference overlaps with a register modified in the parent constructor. #4: Move to inline helper functions Support both decompilation and emulation needs by facilitating runtime selection of the desired instruction fidelity with inline helper functions.

Interestingly, as the fidelity of the SLEIGH semantics improve, the readability and overall quality of the resulting decompiled code can, in some cases, actually decline. These readability regressions typically arise from specific, rare edge cases that compilers guarantee cannot occur, but which the decompiler is unable to reliably rule out. Examples include handling offsets to 20-bit addresses on MSP430 or differences in the bit-level representation of NaN values. Introducing decompiler hints—such as annotations indicating that certain conditions are likely—would allow high-fidelity Pcode to be retained for emulation, while still enabling the decompiler to make simplifying assumptions that improve decompilation quality. Decompiler hints can ensure a specification is simultaneously accurate and useful for decompilation to provide a more effective solution to issues such as I7 and I8 . #2: Design templated constructors and arrays Add complex language constructs to reduce manual code duplication and copy-paste bugs, & improve readability and maintainability of specifications.

SLEIGH currently relies on black-box functions—e.g. define pcodeop <name>—for instructions that are too complex to model using Pcode or not fully implemented as we have come across in issues such as I7 and I8 and partially implemented SIMD and vector instructions identified in I11 . The desire is to eventually replace these black-box functions with Pcode semantics; however, in rare cases the opposite occurs; black-box functions are used to replace Pcode semantics. For example, the Pcode semantics for the x86-64 instruction FXSAVE were replaced with the black-box _fxsave operation, matching the compiler intrinsic used in C to generate the instruction. This simplifies decompilation but prevents its use for emulation. To facilitate dynamic selection of the desired fidelity of instruction semantics, we propose moving to inline helper functions. For example, an emulator can maximize instruction fidelity by handling every edge case, while decompilation could represent the code as an intrinsic function.

Often, the same issue in one constructor is repeated in others due to duplicate logic in the specification. Multiple issues have resulted from these copy-and-paste type duplications, such as the issues we fixed identified in I9 . This code duplication is partly necessitated by the limited expressiveness of the SLEIGH language, particularly in representing loop and array-like constructs. When an instruction requires a repeated action, such as assigning values to a list of registers (as seen in Listing 1), the only available option is to manually write each assignment. This not only contributes to bugs when writing specifications, but also makes the specification harder to read and maintain. Consequently, complex instructions are sometimes left unimplemented, as found in I11 . This issue could be addressed by extending the SLEIGH language to support defining arrays and templated constructors. Possible syntax for this extension is shown in Appendix H, featuring a template for the reglist constructor with the variable i used for indexing into arrays to obtain both the constraints for the templated constructor and the target register. #3: Design accessor functions export statement behaviors are error-prone. Design logical accessor functions for exporting values to manage dependencies.

5.1.2

Recommendations to Address Unresolvable Issues

To address problems that are infeasible or impractical to resolve under the current SLEIGH rules, as identified in issues I11 – I14 , we propose the following specific recommendations to extend the SLEIGH DSL. #5: Provide for SIMD extensions I11 Mapping SIMD semantics to Pcode in the SLEIGH DSL is cumbersome due to the many near-identical operations used. Introduce vectorised Pcode operations or structured looping constructs to express SIMD instruction semantics.

To pass information between subtables, SLEIGH allows the semantics section to return a reference to a value, variable, or memory location using an export statement (the final statement of the section). But, due to the subtleties of how this statement operates, using export statements can be error-

Modern ISAs increasingly add instructions for working 17

with lanes of data—e.g. SIMD and vector instructions—yet expressing their semantics in SLEIGH is cumbersome and error-prone. Consequently, we observe poor decompilation quality and a track record of bugs in the subset of instructions that have been defined. However, as these instructions are adopted by more programs, strong support in SLEIGH specifications has become a necessity. Further, we take the extensive use of custom Pcode operations and the partial SIMD implementations we found as a sign that a new group should be added to the Pcode instruction set for SIMD operations. Decompilation could be partially improved by allowing the decompiler to hide internal details with the inline helper functions described previously; however, this may not benefit advanced decompilation techniques such as de-vectorization— i.e., translating a sequence of vector instructions back into a loop over scalar elements. Introducing new vectorized Pcode operations would make expressing SIMD constructs simpler, although this requires any analysis dependent on Pcode to also account for the new operations. Alternatively, more structured looping constructs could be introduced to SLEIGH, which could be automatically unrolled for unstructured analysis while being accounted for during decompilation.

sis tools to identify program portability issues, arising from either compiler bugs or manually written code, and assist in analyzing malware that exploits such discrepancies to detect the execution environment. #8: Alignment requirements for memory operations I14 Introduce explicit inclusion of alignment information to memory operations. Currently, SLEIGH only supports specifying a global alignment for all memory operations within an ISA; this can lead to discrepancies in the exception state after executing instructions in emulation with stricter alignment requirements. Adjusting the Pcode L OAD/S TORE operations to include alignment information or introducing new naturally-aligned memory operations are possible resolutions. Provisions for operation level alignment can improve emulation accuracy. This alignment information is also useful for static analysis, such as detecting potentially unaligned accesses, improved type inference, and enabling constant propagation algorithms to make assumptions about the value of registers holding aligned pointers.

#6: Provide floating-point operation descriptions I12 Design structures to encode floating-point operations and rounding modes.

5.2

Other Processor Specifications

InSPECtor is designed to address the challenges posed by

the SLEIGH DSL in its extensive and diverse set of processor specifications but its core ideas—symbolically traversing a specification’s decoding rules, extracting edge cases and state generation—can extend to other specification languages such as Sail or VADL. At a high level, languages such as VADL [15] and Sail [32] share structural similarities with SLEIGH: they describe instruction encodings alongside executable or interpretable semantics. VADL, as implemented in OpenVADL [15], provides a concise and formal representation of processor architectures, with explicit modeling of instruction formats and behavior. Similarly, Sail [32] offers a rich, formally grounded language for ISA semantics, often used in verification settings for architectures such as ARM. These commonalities suggest that our approach could generalize along two main dimensions. First, specification traversal—i.e., systematically enumerating decoding paths, instruction variants, or semantic rules—can be adapted to any language that exposes structured instruction definitions. Second, symbolic solving can be applied as long as the specification can be translated into a constraint representation. In principle, both VADL and Sail provide sufficient structure and formalism to support these operations. However, adopting our approach requires solving challenges pertinent to the specification language, and traversal in each specification language is fundamentally different because each language exposes different normalized representation and structure. In particular, more formally grounded specification languages such as Sail support richer decoding constructors (e.g., complex control flow), which can signif-

The minimal set of floating-point operations described in SLEIGH are insufficient to precisely capture the complete behavior of floating-point instructions supported in modern ISAs. There are no Pcode operations for performing unsigned conversions between integers and floating-point values, and no method to encode different rounding modes. Adding new Pcode operations for floating-point conversions and rounding modes would allow the SLEIGH specification to be more precise. However, this would require any analysis that uses Pcode to be updated to account for new operations. This is a significant drawback, as it requires modifying all existing analyses and tools that rely on Pcode. Alternatively, many of the semantics could instead be encoded as hints—similar to the existing branch hints—which would allow tools, such as a decompiler, to selectively ignore new operations, treating them as more generic cases. #7: Explicit unpredictable/undefined values I13 Allow better handling or precise isolation of undefined or unpredictable outputs in ISAs. A considerable number of discrepancies across all architectures arise from differences in outputs that are designated as undefined or unpredictable in the ISA reference. Many of these also lead to discrepancies between different hardware implementations of the same ISA. A remedy is to add a single new Pcode operation to annotate registers that have unpredictable values. This would allow discrepancies due to these operations to be isolated more precisely, enable analy18

icantly increase solver complexity or introduce path explosion during specification traversal, requiring more aggressive pruning or summarization. Then, translating semantics into efficient encodings for a symbolic solver could be non-trivial, if the abstractions do not map directly to bit-precise constraints. Consequently, the primary effort is likely to lie not in redesigning the symbolic methodology itself, but in bridging language-specific representations into a model suitable for constraint solving and automated exploration challenges posed by the specification language’s descriptions of processors.

5.3

work should consider not only correctness but also achieving completeness attributes to specification testing. Some ISAs include instructions that alter the execution of subsequent code. For example, to allow for a more compact instruction encoding, ARM/Thumb includes an If-Then-Else (ITE) instruction in THUMB mode that changes up to four consecutive instructions into variants that are conditionally executed based on the value of the status register. Since the approach presented here generates and tests a single instruction at a time, it does not test these cases. Therefore, future work can consider advancing the generation process to identify and generate the necessary instruction sequences to test these variants in the specification.

False Positives

6

In general, discrepancies correspond to either bugs or limitations in the SLEIGH specification, thus defining a false positive is hard. Each discrepancy identified represents a possible bug, but cannot be easily deduplicated without manual effort, so we report discrepancies, as done in related works in CPU emulator testing [24–26]. Then, we discuss bugs in the context of root-causes fixed, not the number of buggy instructions, a more inflated number. The large number of discrepancies found for many of the identified bugs is a major contributor to the observed difference between the bug and discrepancy counts. In addition to discrepancies mapped to root-causes, other contributors include ISA-defined unpredictable behaviours, unimplemented semantics, or issues which cannot be fixed without extending SLEIGH, discussed further in Section 4.2.6. Due to limitations of the SLEIGH language, these issues do not represent an error in the specification, and consequently could be considered false positives; however, our recommendations for improving SLEIGH, discussed in Section 5.1, would allow addressing the sources of these discrepancies while helping to improve specification veracity.

5.4

Related Work

We acknowledge the significant efforts devoted in past studies to test CPU emulators. EmuFuzzer [26] tested x86-64 CPU emulators using a hardware reference to detect structures within the instruction by observing when mutating a particular byte causes an exception. KEmuFuzz [25] extends EmuFuzzer by adding support for fuzzing virtual machines and hypervisors through carefully crafted templates that include snippets of both user- and system-level instructions, but retained the same instruction generation method as EmuFuzzer. The approach is suited for testing x86-64 emulators running in protected mode (32-bit instructions), requires filtering branch instructions due to execution environment limitations, and only identifies imprecise byte-level structure in instructions. In contrast, PokeEMU [24] generates test instructions by symbolically executing the emulator’s binary instruction decoding logic. This is similar to the constructor traversal process adopted in GenSYS, but applied to the emulator binary. Fast PokeEMU [39] builds on PokeEMU by reducing test case execution overhead by merging multiple instructions into a single test case. In contrast to InSPECtor, PokeEMU does not generate edge case-triggering input states, as the value of input operands is not used in the decoding logic. Further, InSPECtor’s objective to guarantee complete constructor coverage implies that the method devised can find bugs in unreachable constructors. Other testing strategies are found in studies examining binary lifters. For instance, MeanDiff [20] compares binary lifters by translating each intermediate representation (IR) into a common IR. Once translated, an SMT solver is employed to check for symbolic equivalence; this circumvents the need to assess the impact of specific input states. However, due to the complexity of the translation process, certain complex instructions are omitted from analysis. In contrast, JuxtaPlayer, akin to CPU-emulator testing methods, uses a hardware oracle as a reference system and determines equivalence by testing carefully selected initial input states, avoiding the need to check the symbolic equivalence of semantically complex instructions, such as floating-point operations. No-

Limitations & Future Work

Despite our extensive efforts, our work is not without limitations. Although we sought to test the correctness of a specification, our approach will not determine the completeness of a specification. Because in the specification-driven approach, instructions missing from a SLEIGH specification are not tested. However, these instructions exhibit a well-defined failure mode: whenever an unknown instruction encoding is encountered, an invalid instruction exception will be generated in, for instance, SLEIGH-based emulators. This behavior typically makes any missed instructions easy to detect in real-world targets. But, in disassemblers, missing instruction in specifications can impact control-flow recovery where invalid instructions are used as heuristics for identifying unreachable or invalid code regions. In these cases, missing instructions may cause the analysis to misattribute controlflow errors, making it harder to localize the root cause. Future 19

tably, a prior study analyzed the limitation of Pcode’s formal semantics [27]. This lead to several recommendations to improve the Pcode definitions, documentation and resolve bugs in Ghidra. This complements the recommendations resulting from our extensive work across five ISAs to improve SLEIGH and the processor specifications in Section 5.1 Alongside these studies, we also acknowledge studies developing techniques to uncovering flaws in hardware-assisted virtual machines [3, 14] or methods to uncover discrepancies in the textual representation of instructions generated by disassemblers [29]. Other approaches aim to detect unexpected changes in the processor state of individual hardware CPUs arising from undocumented instructions [11, 23], manufacturing defects [33], or hardware implementation issues [33]. In general, similar to our study, these works across several domains also aim to identify discrepancies. Notably, discrepancies, even one known to differ between hardware implementations, can be exploited by malware for emulator or VM detection, as demonstrated in previous studies [30,34,35].

7

The authors would like thank and acknowledge Om Mandavia for the preliminary investigations into developing instruction generation strategies for the project.

A

Ethical Considerations

Our work presents a method and tool design for testing and evaluating processor specifications focusing on the open source SLEIGH specifications. Our goal is to improve the truthfulness of the tools used by the security community, such as Ghidra and CPU emulators, that rely on the truthfulness of the SLEIGH specifications, and thereby helping to improve the security of software systems and the safety and security of end-users of those systems. Through our analysis with InSPECtor, we identified a substantial number of defects in existing SLEIGH specifications. While documenting these issues is essential for improving the correctness and reliability of disassembly and analysis frameworks, public discussion of such defects carries some dual-use risks. In particular, an adversarial actor could potentially misuse specification inconsistencies to craft binaries that evade static or dynamic analysis, mislead emulators, or otherwise undermine defensive tooling. To mitigate these risks, we followed established responsible-disclosure practices. All defects discovered during this work were communicated directly to the Ghidra project maintainers, together with the corresponding fixes that we validated internally. Our intention is to strengthen the ecosystem of analysis tools rather than expose previously unknown issues without remediation. We emphasize that any future defects uncovered through the use of this tool should likewise be discussed and disclosed responsibly to the maintainers of the Ghidra project following the guidelines therein. Despite these dual-use concerns, we believe that the benefits of improving specification quality, strengthening capabilities and correctness of widely used analysis tools—employing those specifications—-used by security practitioners and improving transparency outweigh the risks or potential for misuse. Ultimately, our commitment to responsible disclosure and to support the maintainers of widely used tooling guided the design of this work and will continue to guide its future development.

Conclusion

This paper introduced a methodology for generating instructions and initial input states that fully explore all machine code sequences decodable by SLEIGH processor specifications. This led to the development of InSPECtor with GenSYS and JuxtaPlayer tools. GenSYS is an instruction and state generator used to produce over 1,208,531 test cases across 5 different ISAs, covering all instructions and addressing modes, as well as edge cases. The test cases were used to evaluate the correctness of specifications using a differential testing strategy, realized in JuxtaPlayer. The tool executes each test case in both a SLEIGH-based emulator and a hardware-based reference system, followed by a comparison of their final states to identify discrepancies. This process revealed systematic issues in 5 SLEIGH specifications and highlighted areas where improvements to SLEIGH specification language could reduce future defects. Improving the veracity of SLEIGH specifications enhances the reliability and confidence in downstream tools that depend on their correctness. Importantly, our work represents a significant and sustained effort to improve SLEIGH specifications and introduces tools and a test strategy for automated correctness testing.

B Acknowledgements

Open Science

We release full source code for InSPECtor, and make all artifacts publicly available online at https://doi.org/10.6084/m9.figshare.32507811, including. • GenSYS, the main implementation of our techniques, used to traverse the SLEIGH specifications and generate the test cases summarized in Table 2.

The work was supported by the Next Generation Technology Fund (NGTF)—administered by Commonwealth Scientific and Industrial Research Organisation’s (CSIRO’s) Data61 and Defence Science and Technology Group (DSTG) in Australia, The Advanced Strategic Capabilities Accelerator (ASCA) program (ASCA-EDT-CHALLENGES) and DSTG, Australia. 20

• JuxtaPlayer used for executing the test cases on both realworld hardware and in SLEIGH emulators. As well as for for identifying and grouping the discrepancies for Table 3.

[9] Sandeep Dasgupta, Sushant Dinesh, Deepan Venkatesh, Vikram S. Adve, and Christopher W. Fletcher. Scalable validation of binary lifters. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), page 655–671, 2020.

• Documentation on how to use each tool in the form of multiple README files, and on how to recreate the ablation study in Section 4.3.

[10] Flavian Dola and Guillaume Orlando. Ghidralligator: Emulate and fuzz the embedded world. https://www. cyber.airbus.com/ghidralligator_emulate_an d_fuzz_the_embedded_world/, 2023.

• Bug Fixes individualized in our fork of the Ghidra project while they undergo the review process.

References

[11] Christopher Domas. Breaking the x86 ISA. Black Hat, 2017.

[1] Intel® 64 and ia-32 architectures software developer’s manual. https://www.intel.com/content/www/us /en/developer/articles/technical/intel-sdm .html, October 2025.

[12] Andrea Fioraldi, Dominik Maier, Heiko Eißfeldt, and Marc Heuse. AFL++: Combining incremental steps of fuzzing research. In USENIX Workshop on Offensive Technologies (WOOT), 2020.

[2] Open SSL Github. https://github.com/openssl /openssl/blob/afd8e29c360376420ea676581aa5 d50b6027d069/crypto/bn/asm/x86_64-mont.pl #L1168-L1169, 2025. Access 26 March 2026.

[13] Agner Fog. The microarchitecture of intel, amd and via cpus: An optimization guide for assembly programmers and compiler makers. https://www.agner.org/op timize/microarchitecture.pdf, 2023.

[3] Nadav Amit, Dan Tsafrir, Assaf Schuster, Ahmad Ayoub, and Eran Shlomo. Virtual cpu validation. In Symposium on Operating Systems Principles (SOSP), pages 311–327, 2015.

[14] Pedro Fonseca, Xi Wang, and Arvind Krishnamurthy. MultiNyx: a multi-level abstraction framework for systematic analysis of hypervisors. In European Conference on Computer Systems (EuroSys), pages 1–12, 2018.

[4] Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for armv8-a, RISC-v, and CHERI-MIPS. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019.

[15] Florian Freitag, Linus Halder, Benedikt Huber, Benjamin Kasper, Michael Nestler, Kevin Per, Matthias Raschhofer, Alexander Ripar, Johannes Zottele, and Andreas Krall. Openvadl: An open source implementation of the vienna architecture description language. In Architecture of Computing Systems (ARCS), pages 156–171, 2026.

[5] Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein. νZ-an optimizing SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 194–199, 2015.

[16] Rahul Gopinath, Carlos Jensen, and Alex Groce. Code coverage for suite evaluation by developers. In International conference on software engineering (ICSE), pages 72–82, 2014.

[6] Jeremy Blackthorne, Alexei Bulazel, Andrew Fasano, Patrick Biernat, and Bülent Yener. Avleak: Fingerprinting antivirus emulators through black-box testing. In USENIX Workshop on Offensive Technologies (WOOT), 2016.

[17] Jaewon Hur, Suhwan Song, Dongup Kwon, Eunjin Baek, Jangwoo Kim, and Byoungyoung Lee. Difuzzrtl: Differential fuzz testing to find CPU bugs. In IEEE Symposium on Security and Privacy (SP), pages 1286–1303, 2021.

[7] Zitai Chen, Sam L Thomas, and Flavio D Garcia. Metaemu: An architecture agnostic rehosting framework for automotive firmware. In ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 515–529, 2022.

[18] Muhui Jiang, Tianyi Xu, Yajin Zhou, Yufeng Hu, Ming Zhong, Lei Wu, Xiapu Luo, and Kui Ren. EXAMINER: Automatically locating inconsistent instructions between real devices and CPU emulators for ARM. In ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 846–858, 2022.

[8] Michael Chesser, Surya Nepal, and Damith C Ranasinghe. Icicle: A re-designed emulator for grey-box firmware fuzzing. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2023. 21

[19] Soomin Kim, Markus Faerevaag, Minkyu Jung, SeungIl Jung, DongYeop Oh, JongHyup Lee, and Sang Kil Cha. Testing intermediate representations for binary analysis. In IEEE/ACM International Conference on Automated Software Engineering (ASE), page 353–364, 2017.

[30] Roberto Paleari, Lorenzo Martignoni, Giampaolo Fresi Roglia, and Danilo Bruschi. A fistful of red-pills: How to automatically generate procedures to detect cpu emulators. In USENIX Workshop on Offensive Technologies (WOOT), volume 41, page 86, 2009.

[20] Soomin Kim, Markus Faerevaag, Minkyu Jung, Seungll Jung, DongYeop Oh, JongHyup Lee, and Sang Kil Cha. Testing intermediate representations for binary analysis. In IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 353–364, 2017.

[31] OpenSBI Project and Contributors. RISC-V open source supervisor binary interface (opensbi). https: //github.com/riscv- software- src/opensbi, 2026. [32] Alastair Reid. Trustworthy specifications of ARM® v8-A and v8-M system level architecture. In Formal Methods in Computer-Aided Design (FMCAD), pages 161–168, 2016.

[21] Pavneet Singh Kochhar, Ferdian Thung, and David Lo. Code coverage and test suite effectiveness: Empirical study with real bugs in large systems. In IEEE international conference on software analysis, evolution, and reengineering (SANER), pages 560–564, 2015.

[33] Kostya Serebryany, Maxim Lifantsev, Konstantin Shtoyk, Doug Kwan, and Peter Hochschild. SiliFuzz: Fuzzing CPUs by proxy. arXiv preprint arXiv:2110.11519, 2021.

[22] a Leidos Company Kudu Dynamics, LLC. Styx emulator. https://github.com/styx-emulator/styx-e mulator, 2025.

[34] Hao Shi, Abdulla Alwabel, and Jelena Mirkovic. Cardinal pill testing of system virtual machines. In USENIX Security Symposium (USENIX Security), pages 271–285, 2014.

[23] Xixing Li, Zehui Wu, Qiang Wei, and Haolan Wu. Uisfuzz: An efficient fuzzing method for cpu undocumented instruction searching. IEEE Access, 7:149224–149236, 2019.

[35] Hao Shi, Jelena Mirkovic, and Abdulla Alwabel. Handling anti-virtual machine techniques in malicious software. ACM Transactions on Privacy and Security (TOPS), 21(1):1–31, 2017.

[24] Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. Pathexploration lifting: Hi-Fi tests for Lo-Fi emulators. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 337–348, 2012.

[36] Flavien Solt, Katharina Ceesay-Seitz, and Kaveh Razavi. Cascade: CPU fuzzing via intricate program generation. In USENIX Security Symposium (USENIX Security), pages 1–18, 2024.

[25] Lorenzo Martignoni, Roberto Paleari, Giampaolo Fresi Roglia, and Danilo Bruschi. ACM SIGSOF testing system virtual machines. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 171–182, 2010.

[37] The National Security Agency (NSA). Ghidra: Software reverse engineering framework. https://ghidra-s re.org/, 2019.

[26] Lorenzo Martignoni, Roberto Paleari, Giampaolo Fresi Roglia, and Danilo Bruschi. Testing CPU emulators. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 261–272, 2009.

[38] The National Security Agency (NSA). SLEIGH: A language for rapid processor specification. https: //ghidra.re/ghidra_docs/languages/html/sle igh.html, 2023.

[27] Nico Naus, Freek Verbeek, Dale Walker, and Binoy Ravindran. A formal semantics for p-code. In Verified Software. Theories, Tools and Experiments (VSTTE), page 111–128, 2022.

[39] Qiuchen Yan and Stephen McCamant. Fast PokeEMU: Scaling generated instruction tests using aggregation and state chaining. In ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments (VEE), pages 71–83, 2018.

[28] Tavis Ormandy. Reptar. https://lock.cmpxchg8b .com/reptar.html, 2023.

C

[29] Roberto Paleari, Lorenzo Martignoni, Giampaolo Fresi Roglia, and Danilo Bruschi. N-Version disassembly: Differential testing of x86 disassemblers. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 265–274, 2010.

Hardware Discrepancies

x86-64. For x86-64, we experimented with different hardware reference systems for differential testing, an Intel(R) Xeon(R) CPU E5-2660 v4 CPU and an AMD Ryzen 9 7950X (the CPU used for the final results). However, between the two CPUs, 22

we also identified a large number of discrepancies. Many of these discrepancies are expected. The x86-64 ISA contains several instructions for interacting with model-specific registers or internal processor state (e.g., RDTSC, CLZERO, CPUID) and others for interacting with external hardware (RDRAND), all of which yield processor-specific outputs. Additionally, the processors support distinct sets of ISA and vendor-specific additions/extensions, leading to several additional discrepancies, partially attributed to the AMD processor being newer than the Intel processor. Expected differences also include instructions that are explicitly listed in the ISA manual (from both vendors) as producing outputs with undefined values. This mostly occurs in arithmetic operations for which certain flags are listed as undefined after the instruction is executed, allowing for more flexibility in the hardware implementation. For example, a considerable number of discrepancies are related to the AMD processor not setting the auxiliary carry flag (AF), which was originally intended for binary-coded decimal (BCD) operations and is rarely used in modern programs. However, there are also four notable discrepancies that are neither caused by ISA extensions nor explicitly marked as having undefined outputs:

necessary to accurately assess the correctness of the x86-64 SLEIGH specification. A vast majority of these discrepancies were filtered out during analysis based on their instruction mnemonic to avoid incorrectly attributing them to bugs in the SLEIGH specification. MSP430. For some discrepancies between the hardware and SLEIGH specification, the SLEIGH specification was more faithful to the documentation. For example, the documentation shows the lowest bit of the stack pointer register being fixed to zero and clarifies that it is always even aligned. This gives the impression that bit 0 is hardwired to 0 and that it is not possible to write an odd value to the register. However, the hardware was found to allow and to use odd stack pointer values. This causes data pushed by PUSH.B and PUSH.W to overlap as word memory accesses are forcefully aligned to word boundaries, but byte memory accesses are not. Another behavior that differed between hardware and documentation was the CMPA SR, SR instruction. This instruction should compare the status register with itself and then set the flags based on the result, but was found to interpret the status register in the destination register position as zero. The documentation states that the status register outside of word accesses in the register addressing mode belongs to the constant generator. But this is not consistent with the constant generator register as it returns the register addressing mode value of zero in both positions. Issues with constraints in the SLEIGH specification being too relaxed allowed us to find undocumented instructions. The MSP430X extension word is assigned the encoding space from 0x14XX to 0x1CXX, but is defined as only using the encoding of 0x14XX (where XX and the 8th bit are ignored). The constructor in SLEIGH which builds the extension word only checks bits 11–15, and ignores bits 9–10 which should be set to 0. This allowed us to find a special case where the SXTX.W instruction is used with the register addressing mode and bits 8–10 of the extension word set (bit 8 being the zero carry bit). Normally the SXTX.W instruction signextends a byte in the destination register to a word size, but this illegal encoding of the instruction sign-extends a word to address size. However, the documentation does not contain this encoding, nor an instruction to sign-extend a word to address size. RISC-V. The RISC-V SLEIGH specification includes all extensions for a given base instruction set. As the test cases are generated from this there is no way to separate out extensions that are not supported by the hardware being tested. This led to a significant number of illegal instruction exceptions as the hardware could not run the instruction. Another source of illegal instructions was the Control and Status Register extension. These registers are used to control how the hardware functions and to receive status information from the hardware. The SLEIGH implementation of this extension includes every possible CSR, giving them the generic name of csrXXX where they have not yet been assigned a use. However, the

1. Control-flow instructions with an address-size override prefix (66) are interpreted differently on the two processors. On the Intel CPU, the prefix is respected and the destination address is truncated to 16 bits, while the AMD CPU ignores the prefix and uses the full 64-bit address. 2. Subtle differences in prefix decoding cause the instruction encoding [f3 47 90] to be decoded as a PAUSE instruction on the Intel CPU, but as an XCHG instruction on the AMD CPU. 3. The VGATHER/VPGATHER* family of instructions load values from memory based on an index and a mask register. Both the index and mask operands are vector registers; however, only the lower 64 bits of the mask are used. The Intel CPU fills the upper bits of the mask register with the value of the most significant bit of the original value, while the AMD CPU leaves the upper bits unchanged. 4. RCPPS and RSQRTPS (and other variants) perform approximate reciprocal and reciprocal square root operations respectively using different approximation algorithms on Intel and AMD CPUs, resulting in discrepancies. The issues above that stem from non-standard instruction encodings or input values are highly unlikely to be encountered in real-world programs. Of these issues, only the fourth is likely to impact real-world programs. However, since the associated instructions are explicitly documented as approximations, programmers should already be careful when using them. Nonetheless, knowing these discrepancies exist is 23

hardware faults with an illegal instruction exception on instructions that access these CSRs as they are not implemented and have no function. The set of CSRs which can be used for testing is further reduced by the privilege level the hart is running on, as accesses to those on a higher level will also raise an illegal instruction exception.

D

one. Edge cases are defined corresponding to each overflowchecking operation. Floating-point operations. For floating-point operations, the operands are constrained to extreme and special values (such as extremely small or large values, NaN, or ±Inf). Floatingpoint operations are challenging to evaluate symbolically, which prevents us from solving subsequent edge cases that use the result of a floating-point operation. However, within a single instruction, integer and floating-point operations are typically not performed on the same inputs.

Pcode Edge Cases

Below we describe additional details for the edge cases defined for individual Pcode operations (Table 1):

Branches. Branches are handled by forking the symbolic state at each branch operation and adding an assertion for the branch condition. For most branch operations, when the condition is true, the operation jumps to a different instruction. However, SLEIGH also allows branches to Pcode operations within the same instruction (internal Pcode branches). For the outgoing edge of external branches, edge case generation stops when the branch is taken, since instructions are individually tested. Internal loops (where the branch jumps backwards within the instruction) are handled by unrolling the loop a fixed number of times (e.g., 10) and generating edge cases for each unrolled iteration.

Addition and subtraction. For I NTA DD and I NT S UB, edge cases that test integer overflows/underflows and output values that are negative or zero are potentially interesting. Inputs corresponding to these edge cases are likely to set or clear various CPU flags, testing that the flags are properly updated by the SLEIGH specification, and that the correct set of overflow checks are used. Multiplication and division. Since there are both signed and unsigned variants of multiplication and division, edge cases are defined to identify when the incorrect variant is used. It is also useful to include edge cases for division by zero, as the behavior varies across ISAs.

Memory accesses. When a value is loaded from memory, it may be used as an input to subsequent operations. To generate edge case-triggering operands for these operations, memory is included as part of the initial input state. Whenever a load occurs, the state generator introduces a new symbolic input variable representing the value returned from the load and records the expression for the address from which the value is loaded. Since not all addresses are valid for every architecture, additional constraints are used to restrict the addresses to valid ranges and, for some architectures, to ensure that the address is properly aligned for the access size. Constraints are also added to ensure memory accesses are consistent, so that multiple loads from the same address return the same value. For stores, the same constraints are applied to the address (to prevent invalid access exceptions from occurring), but the written value is ignored. It is technically possible for the value written by a store to be later loaded; however, there are no instructions in any of the tested ISAs where this occurs, so it can be ignored for the purpose of state generation.

Zero and sign extension. For these operations, bugs are most likely to result from using the incorrect type of extension. To identify these bugs, edge cases that ensure negative inputs of various bit-widths are used. For example, an input for a 16-bit extension would be 0xFFFF. Boolean operations. Given that there are only four input combinations for boolean operations, it is possible to test all outputs by constraining the inputs to each of the four combinations. Bitwise operations. In SLEIGH, bitwise operations are used for three purposes: implementing ISA-level bitwise operations, extracting and inserting bits, and as an alternative to boolean operations. Misuse of these operations can be detected by forcing the inputs to be extreme values (e.g., all bits set to 0 or 1). Shifting operations. Overflows are also possible in shift operations, and the behavior of oversized shifts varies between ISAs. Edge cases are defined to constrain the shift operand to a value that exceeds the total number of bits in the type. Additional edge cases are defined to test whether the correct type of shift (arithmetic versus logical) is used, by constraining the inputs to be negative or positive values.

E

Further Bug Case Studies

Incorrect MSP430X Constants. MSP430 instructions use the following word to hold 16-bit constants for indexing, absolute addressing, and immediate values. MSP430X extends these constants to 20 bits, with the upper 4 bits sourced from the preceding extension word. In the SLEIGH specification for MSP430X the upper 4 bits were missing from all uses of the 20 bit constants. Preventing these instructions from representing any negative number, or positive numbers larger than

Comparisons. For comparisons, it is desirable to detect cases of off-by-one errors and where the wrong comparison operator is used. To achieve this, constraints are used to enforce that operands are equal or differ by ±1. Overflow conditions. SLEIGH explicitly calculates various overflow conditions by using specific operations for each 24

Extension Word Instruction c0 18

1c 42 Address

4a 00

Current Ghidra Disassembly MOVX.W &DAT_0000004a, R12

branches to no longer be reachable.

Disassembly With Fix MOVX.W &GlobalVar, R12

F

Differential Testing Environments

F.1 SLEIGH-based Emulator Configuration Figure 4: An example of the MSP430 bug where the upper 4 bits of 20 bit constants are ignored. This shows Ghidra failing to resolve the symbol as it uses the wrong address.

JuxtaPlayer uses Icicle [8], a SLEIGH-based emulator, to execute Pcode operations from the SLEIGH specification. Icicle supports the execution of individual instructions (single-

stepping) within all of the test architectures and provides APIs for directly reading and writing the system state required for differential testing. Icicle also supports tracking exceptions that occur during execution.

216 , including memory addresses. The effects of this can be observed in Ghidra’s disassembly when moving the .data section outside of the first 64KB of memory (Figure 4). RISC-V CSRRW/CSRRWI. The CSRRW instruction atomi-

F.2

cally swaps a value into a Control and Status Register (CSR). In the case where the zero register x0 is used as the destination register, no read should be performed, preventing any CSR read side-effects. Currently, the SLEIGH specification checks if the source register is x0 rather than the destination register. This prevents handling the case where the value of the CSR is read and then cleared, as using CSRRW rd, csr, x0 will cause the CSR to be cleared without returning any value, leading to missing data in decompilation and emulation. This appears in OpenSBI [31] where the CSRRWI instruction is used to read the MTOPEI status register and clear it. The CSR instructions where also the only instruction that could write non-zero values to x0. During normal emulation and analysis this has little impact as the constant 0 is returned on SLEIGH reads to x0. However, the GDB tool queries the emulator for register values, including the now non-zero zero register. This then causes single stepping branches which compare to x0 to fail. As instead of properly single stepping, GDB places a breakpoint at the incorrectly-computed next instruction address, and continues execution.

KVM-based Reference Systems

Since our goal is to ensure that SLEIGH specifications accurately reflect the behavior of real hardware, we use real hardware as the reference system for differential testing. Where possible, hardware-assisted virtual machines (VMs) are used to support this goal. These VMs create isolated virtual execution environments that can be used to efficiently execute instructions on the underlying hardware. By carefully configuring the VM state, it is possible to construct an environment analogous to that of the emulator. Hardware virtualization differs between ISAs and even between different vendors of the same ISA.14 Fortunately, the Linux kernel provides a hardware virtualization driver, KVM (Kernel-based Virtual Machine), which exposes a consistent interface for manipulating hardware VMs. KVM supports all the essential features for differential testing, allowing us to read and write register values, allocate memory, and singlestep the processor. However, some additional configuration is required to ensure that the VM environment matches the assumptions made by the SLEIGH specification. This configuration is performed by JuxtaPlayer using KVM APIs, below we describe the x8664 specific configuration steps; the ARM/Thumb and AArch64 configurations requires similar steps. x86-64 processors support multiple execution modes (e.g., real mode, protected mode, and long mode), each of which can change the semantics of a particular instruction encoding. Therefore, hardware VMs must be configured to run in the correct mode (i.e., long mode for x86-64). To do this, the relevant bits in control registers, such as EFER (Extended Feature Enable Register), are set to enable ISA extensions related to long mode execution, and the global descriptor table (GDT) is set up to ensure that the memory region containing the instruction bytes is interpreted as 64-bit code. To ensure all instructions are available, JuxtaPlayer enables additional extensions, such as SSE and AVX, by setting bits

AArch64 STRLB/STRLH. These instructions store a byte/half-word to memory. However, the SLEIGH specification did not set the size of the operation, causing the entire 32-bit register value to be written to memory. This results in bytes adjacent in memory to the target being corrupted, impacting emulation accuracy. AArch64 LD2R/LD3R/LD4R. These instructions load multiple values from memory, and store repeating copies of each value into different SIMD registers. However, the SLEIGH specification only wrote to the last register given. This results in only one value being loaded from memory and stored in a register. Disassembly or emulation based on values intended to be loaded into earlier registers would yield incorrect results. AArch64 RMIF. This instruction sets the CPU flags based on an input value and a bit-mask. However, the SLEIGH specification did not correctly filter based on the bit-mask. All masked bits would be set to the value of the NG flag. This can impact both disassembly and emulation, as many flags influencing branches could be overwritten, causing some

14 Intel CPUs implement a set of virtualization extensions called VT-x, while AMD CPUs implement a different set of extensions called AMD-V (or SVM—Secure Virtual Machine).

25

in the appropriate control registers and configuring the VM’s CPUID. To handle memory accesses, JuxtaPlayer also configures the page table, a hierarchical data structure used for hardware address translation, to map the instruction page and any additional memory from the test case’s initial input state. The final challenge is to support single-stepping in the VM execution environment. On both the Intel and AMD CPUs, single-stepping is implemented by setting the trap flag (TF), which causes a debug exception after each instruction returning control to the hypervisor, which in turn returns control to JuxtaPlayer. KVM automatically handles this process, making it straightforward to single-step instructions in most cases. However, this debug exception can be suppressed by higher priority exceptions (e.g., memory violations) that occur during instruction execution. If such an exception occurs, control is not returned to the hypervisor; instead, the processor executes the corresponding exception handler. If no handler is present, a ‘triple fault’ occurs, resetting the VM and losing the state needed for differential analysis. To prevent this, JuxtaPlayer defines exception handlers that immediately exit back to the hypervisor. The VM is configured to use these handlers by setting the appropriate entries in the interrupt descriptor table (IDT), updating the task state segment (TSS), and mapping memory for the exception stack. When exceptions occur, we recover the exception reason using a combination of the RIP (instruction pointer) and CR3 (faulting address) registers.

F.3

of an instruction writing an unknown value to any MMIO register, requiring the microcontroller to be fully reset between testcases to ensure a clean state. For RISC-V we use the BeagleV®-Ahead containing a quad-core Xuantie C910 processor which implements RV64GC including the 0.7.1 draft version of the vector extension. This board is capable of running Linux however lacks support for KVM. Instead ptrace was used to seize control of a newly created process as an isolated execution environment. The required memory regions would then be mapped into the process, and the initial regions unmapped. To account for ptrace’s missing support for single stepping, the test cases were first executed with memory filled with c.ebreak instructions to detect jumps. Instructions without jumps were re-executed with memory populated with the testcase specified values. RISC-V jump instructions do not load from memory, allowing the execution with incorrect memory values to be used as the final result. Using ptrace instead of KVM limits testing to only unprivileged instructions.

Hardware Reference Systems

For MSP430 and RISC-V, we did not have access to hardware that supported hardware virtualization extensions, making it impossible to use KVM-based VMs for differential testing. In these cases, alternative approaches where required to execute instructions on real hardware while still allowing the system state to be manipulated and observed. These alternative approaches are generally less efficient and robust than hardware virtualization, but since the ISAs in question are typically simpler they suffice for differential testing. As the reference system for MSP430, we use a MSP430FR5969 microcontroller which contains an EEM (Energy-Efficient Microcontroller Emulator) module that can single-step instructions and read/write the system state. This microcontroller used disjointed memory regions for code, ram, MMIO peripherals, and other functions, with the gaps either trapping on access or allowing reads with a constant value. To keep the test environment consistent, breakpoints were used to detect memory accesses outside of the generic memory ranges, as no form of memory protection was available. However only 2 breakpoints could be enabled at once and no resulting information from the breakpoint was reported. This required nops to be inserted after the instruction under test for different trapping addresses, and each test case to be repeat multiple times in a greater/less than scan. The lack of any form of memory protection also allowed the possibility 26

G

Bug Tables

SLEIGH Issue Memory operands decoded incorrectly with address override and REX.W prefixes. 0x82 allowed as an alternative opcode for 0x80 in long-mode (should be invalid). 64-bit SBB instruction does not sign-extend the 32-bit immediate operand. Incorrect semantics for CMOV instructions if source = destination register. Multiple SIMD instructions behave incorrectly if source = destination register. LZCNT instruction behaves incorrectly if source = destination register. Destination address incorrect when base address register matches source register. MOVSXD/MOVZX with 16-bit destination decoded as having a 32-bit destination. PEXTR* instructions do not write to memory when destination is a memory operand. String instructions with a 32-bit operand size fail to zero upper bits of operands. Loop instructions with a 32-bit operand size fail to zero upper bits of RCX. Instructions with repeat prefix do not set RIP correctly when RCX = 1. XCHG with 32-bit operand size fails to zero upper bits. CMPXCHG8B fails to zero the upper bits of 64-bit registers. Bits 96 to 128 not compared in CMPPS semantics. Decoding issue for MOV reg,imm8 instructions with address override and REX prefix. Wrong casting operation used in CVT instructions. REX prefix causes NOP to be decoded as a 32-bit XCHG which zeroes the upper bits. Destination of bit-scan instructions is modified when source operand is zero. Carry flag for rotate instructions should not be set when count operand is zero. BSWAP with operand size override interpreted as 32-bit instead of 16-bit instruction. POPF with address size / operand size overrides is not decodable. ModRM:reg (w) destination encoding handled incorrectly (multiple instructions). Many instructions with a ‘no-prefix’ constraint are decoded when prefixes is present. PACKUSWB is incorrect when the value to convert is exactly 0x00ff. Address size prefix not handled in bit test instructions. MOV instructions can reference invalid control registers. MOV to/from debug registers with REX.R prefix are not treated as invalid. Lockable INC missing reg_opcode constraint. Redundant and out-of-order prefixes are handled incorrectly. Instructions invalid in long-mode are decoded with address override prefix. No-prefix constraint not checked in several places.

Fix Status Assigned Merged (11.2) Merged (11.2) Merged (11.2) Merged (11.2) Assigned Assigned Merged (11.1) Merged (11.2) Assigned Assigned Pending Assigned Assigned Merged (11.2) Assigned Merged (11.2) Assigned Pending Assigned Pending Merged (11.4) Assigned Pending Merged (11.2) Pending Pending Pending Assigned Pending Pending Pending

Encoding [67 43 . . . ] [82 f8 00] [4f 1d ff . . . ] [0f 40 00] [0f 5a c0] [f3 0f bd c0] [0f c1 00] [66 40 63 c0] [66 40 0f . . . ] [67 af] [67 e2 0a] [f2 a4] [87 00] [0f c7 08] [0f c2 c0 00] [67 48 b7 00] [f2 0f 2d c0] [40 90] [0f bc f1] [48 d3 d0] [66 0f c8] [66 67 9d] [0f c5 00 00] [66 0f 37] [66 0f 67 c0] [67 48 0f . . . ] [0f 20 08] [44 0f 23 c0] [fe 3f] [66 66 . . . ] [67 . . . ] [66 0f 37]

Disassembly Many instructions (invalid) SBB RAX,-0x1 CMOVO EAX,[RAX] CVTPS2PD XMM0, XMM0 LZCNT EAX,EAX XADD [RAX], EAX MOVSXD AX,AX PEXTRB [RDX], XMM0, 0x0 SCASD [EDI] LOOP RIP+10 MOVSB.REPNE RDI,RSI XCHG [RAX], EAX CMPXCHG8B [RAX] CMPEQPS XMM0,XMM0 MOV DIL,0x0 CVTSD2SI EAX, XMM0 NOP BSF ESI,ECX RCL RAX,CL BSWAP AX POPF (invalid) GETSEC PACKUSWB XMM0, XMM0 BTC [EAX],RAX MOV RAX, CR1 (invalid) (invalid) Many instructions AAA GETSEC

Table 7: Issues discovered and fixed in the x86-64 SLEIGH specification. Example instruction encodings and disassembly are provided to aid interpretation, however there are typically multiple encodings with the same issue.

SLEIGH Issue Incorrect operator used in vdup. ldaexd behaves incorrectly when registers alias. vselgt checks the wrong condition. Incorrect constraints used in THUMB encoding of vdup. VMVN operands are reversed in output. Some instructions that modify PC do not handle the THUMB bit correctly. Immediates used in thumb shift operations not decoded correctly. ldrsh.w/ldrsb.w treat the loaded value as a pointer. vst2 uses wrong registers when reglist encoding wraps. Arithmetic operations with shifted immediate do not handle the carry bit correctly. PC relative encodings for FLDM*X/FSTM*X load from the wrong address. PC relative encodings for STR/STRT load from the wrong address. Aliasing issue between index and destination register for ldrexd. vpush/vpop order elements in reverse. vmov.8/16/32 calculates register subslices incorrectly. addrmode3 loads input as pointer instead of returning it as an address. sha1su1.32/sha1su1.32 performs shift on incorrectly sized register.

Fix Status Merged (12.1) Merged (11.2) Merged (12.1) Merged (12.1) Merged (12.0) Assigned Assigned Merged (12.1) Assigned Assigned Assigned Assigned Merged (12.1) Assigned Assigned Assigned Merged (11.2)

Encoding [10 0b e0 ee] [d2 e8 f0 2b] [a1 7a 7a fe] [a0 ee 90 0b] [e0 05 f0 f3] [c7 46] [5f ea 10 00] [bf f9 00 00] [80 e3 40 f4] [10 ea 70 00] [03 fb 9f bc] [10 f0 8f e5] [9f 0f b0 e1] [2d ed 02 0a] [10 0b 40 ee] [d8 00 cf e1] [f2 07 c7 e0]

Disassembly vdup.8 q0,r0 ldaexd r2,r11,[r2] vselgt.f32 s15,s21,s3 vdup.32 q8,r0 vmvn q8,q8 mov pc,r8 lsrs.w r0,r0,#0x20 ldrsh.w r0,[0x10004] vst2.32 {d30,d31,d0,d1} ... ands.w r0,r0,r0, ror #0x1 fldmiaxlt pc, d15 str pc,[0x10018] ldrexd r0,r1,[r2] vpush s0,s1 vmov.8 d0[0x0],r0 ldrd r0,r1,[0x10] sha1su0.32 q8,q8,q8

Table 8: Issues discovered in the ARM32/Thumb specification. Example instruction encodings and disassembly are provided to aid interpretation, however there are typically multiple encodings with the same issue.

27

SLEIGH Issue RMIF uses the wrong value for masked flags. SHA1H uses a shift operation instead of rotate. XAR performs an or operation instead of a xor. BCAX performs an or operation instead of a xor. FMLSL/FMLAL use integer instead of floating point operations. EOR3 performs an or operation instead of a xor. FMLS wrong operand used in calculation. FMLAL2/FMLSL2 use the wrong register subslices RAX1 uses a shift and or operation instead of a rotate and xor. SBCS/NGCS flags incorrect when destination is XZR. LDURSB zero extends value instead of sign extending it. STLRB/STLRH store the wrong sized value. LDPSW loads the wrong sized value. LDRSH/LDRSB sign-extend the result to the wrong size. FRINT* operations perform an integer round instead of a float round. FMLS does not perform a vectorised operation. FMOV performs a float cast instead of a copy. FADDP orders input vectors incorrectly in fused vector operations. FMLA uses wrong element size for vector operations. LDAPR does not actually load the value from memory. RMIF performs a shift instead of a rotate. 32-bit variant of LDAR loads the wrong sized value. ld2r/ld3r/ld4r write to the wrong destination registers.

Fix Status Assigned Merged (12.1) Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Merged (12.1) Assigned Assigned Assigned Assigned Assigned Assigned Merged (12.1) Assigned Merged (12.1) Merged (11.4)

Encoding [00 04 00 ba] [00 08 28 5e] [1d b1 93 ce] [d4 09 25 ce] [00 40 80 0f] [00 00 00 ce] [80 51 20 5f] [22 82 86 2f] [b4 8e 60 ce] [9f 03 1d 7a] [e0 03 c0 38] [e0 83 80 08] [e0 77 c0 68] [e0 03 c0] [00 40 e6 1e] [80 51 20 5f] [00 00 e6 1e] [52 15 43 2e] [e7 0e 41 0e] [e0 c3 a0 f8] [cf 87 1f ba] [e0 83 a0 f8] [e0 c3 60 0d]

Disassembly rmif x0, #0x0, #0x0 sha1h s0, s0 xar v29.2D, v8.2D, v19.2D, #0x2c bcax v20.16B, v14.16B, v5.16B, v2.16B fmlsl v0.2S, v0.2H, v0.H[0x0] eor3 v0.16B, v0.16B, v0.16B, v0.16B fmls h0, h12, v0.H[0x2] fmlal2 v2.2S, v17.2H, v6.H[0x0] rax1 v20.2D, v21.2D, v0.2D sbcs wzr, w28, w29 ldursb w0, [sp] strlb w0, [sp] ldpsw x0, x29, [sp], #0x0 ldrsh w0, [sp] frintn s0, s0 fmls v19.2S, v26.2S, v14.2S fmov w0, h0 faddp v18.4H, v10.4H, v3.4H fmla v7.4H, v23.4H, v1.4H ldapr x0, [sp] rmif x30, #0x3f, #0xf ldar w0, [sp] ld2r {v0.8B, v1.8B}, [sp]

Table 9: Issues discovered in the AArch64 specification. Example instruction encodings and disassembly are provided to aid interpretation, however there are typically multiple encodings with the same issue.

SLEIGH Issue CSR instructions can write to the zero register. FSCSR/FSRM/FSFLAGS write to the zero register. CSRRW/CSRRWI fail to write to destination when the source is zero. Incorrect value is returned on divide by zero and remainder by zero. Incorrect value is returned on division overflow. Reserved instructions in the compressed extension are not decoded correctly. Jumps in the compressed extension fail to align PC. ‘C.JALR ra’ jumps to the next instruction instead of the value in ra. C.ADDI variants with the zero register as the destination should decode as a NOP. FSCSR/FSRM/FSFLAGS fail to swap value when source and destination registers alias. Floating-point instructions fail to set exceptions flags. Floating point instructions do not support NaN boxing. FCLASS.S/FCLASS.D are not fully implemented. FCVT and FMV fails to update destination register. FMV.x.w missing sign-extension. FMV.x.d writes wrong value to destination. FCVT.wu.s/d and FCVT.lu.s/d implements unsigned truncation incorrectly. FCVT with integer destination fail to sign extend result.

Fix Status Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned

Encoding [73 a0 02 34] [73 90 12 00] [f3 12 00 34] [b3 47 00 02] [33 c5 c5 02] [02, 40] [82 87] [82 90] [05 00] [f3 92 12 00] [ .. ] [ .. ] [d3 12 00 e0] [53 f0 00 42] [d3 02 00 e0] [53 05 05 e2] [d3 72 10 c0] [d3 72 00 c0]

Disassembly CSRRS zero, mscratch, t0 FSFLAGS t0 CSRRW t0, mscratch, zero DIV a0, zero, zero DIV a0, a1, a2 (invalid) C.JR a5 C.JALR ra C.NOP FSFLAGS t0, t0 Many instructions Many instructions FCLASS.s t0, ft0 FCVT.d.s ft0, ft1 FMV.x.w t0, ft0 FMV.x.d a0, fa0 FCVT.wu.s t0, ft0 FCVT.w.s t0, ft0

Table 10: Issues discovered in the RISC-V specification. Example instruction encodings and disassembly are provided to aid interpretation, however there are typically multiple encodings with the same issue.

28

SLEIGH Issue Address instructions should use special immediate instead of SR and CG. SUBA carry flag is inverted. Indexed addressing mode does not wrap correctly. Upper bits of 20 bit registers not zeroed on smaller register writes. Upper bits of 20 bit immediates are ignored when extension word is present. RRUX instruction missing. Overflow bit in RRCX not reset. PC not word aligned after indirect branches. Symbolic mode does not sign extend immediates. 16 and 20 bit memory accesses are not word aligned. Sign extended immediates are not masked to 20 bit. POPM incorrectly writes values to SP or CG. Address sized values written to PC are restricted to lower 64KB of memory. PC as a source in the register addressing mode has the wrong value. PC as a source in the index addressing mode has the wrong value. Signed 20 bit values are not always properly handled. Aliasing issue with source and destination registers in ADDA and SUBA. Register indirect, and indexed addressing modes cannot access memory above 64KB. Destination for POP.B, POP.W, and POPX instructions incorrect when SP is an input. MOV, MOVX, MOVA, and BRA @Rn+ do not correctly order operations. CALLA decrements SP too early. POPX does not jump when destination operand is PC. RRAM.W and RLAM.W compute negative flag incorrectly. Extension word instructions that write to the CG register should be invalid. PUSHM pushes wrong value for PC and SP. PUSHM does not correctly handle wrapping. SXT does not sign extend up to 20 bits. The 20 bit indirect auto increment addressing mode increments by the wrong value. PUSHX incorrectly orders SP register decrement. RRCX.A uses the wrong mask value. RRAX and SXTX, and RRCX and SWPBX instruction encodings overlap. RLAX with rpt prefix does not handle PC as the destination register correctly. rpt instructions are invalid in non-register addressing modes. Variations of the address instructions do not jump when the destination is PC. Writes to the status register and operation flags are ordered incorrectly.

Fix Status Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Pending Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Pending Assigned Assigned Assigned Assigned Assigned Assigned Assigned Assigned Pending

Encoding [ef 02] [ff 0f] [8f 43 10 00] [0f 10] [0f 18 70 12 ...] [40 19 0f 10] [40 18 0f 10] [c0 0f] [10 10 fe ff] [2f 00 01 1c] [8f 0f ff ff] [21 17] [00 18 70 50 ...] [cf 00] [3f 00 00 00] [df 03] [ef 0f] [2f 10] [f1 41 00 00] [3f 4f] [41 13] [00 18 70 41] [5f 02] [83 00 0a 00] [11 15] [f5 15] [8f 11] [00 18 7f 10] [00 18 41 12] [00 18 4f 10] [40 18 cf 11] [00 18 40 50] [40 18 13 12] [e0 03] [02 10]

Disassembly ADDA #4, R15 SUBA R15, R15 MOV #0, 0x10(R15) RRC.W R15 PUSHX.A #0xF0000 RRUX.W R15 RRCX.W R15 BRA R15 RRC.W SYM MOVA &0x1C01, R15 MOVA #-1, R15 POPM #3, R3 ADDX.A #0xa, PC MOVA PC, R15 MOVA 0x0(PC), R15 TSTA R15 ADDA R15, R15 RRC.W @R15 POP.B 0x0(SP) MOV.W @R15+, R15 CALLA SP POPX.A PC RLAM.W #1, R15 (invalid) PUSHM #2, SP PUSHM.W #16,R5 SXT R15 RRCX.A @R15+ PUSHX.A SP RRCX.A R15 (invalid) RLAX.A PC PUSHX #1 INCDA PC RRC.W SR

Table 11: Issues discovered in the MSP430X specification. Example instruction encodings and disassembly are provided to aid interpretation, however there are typically multiple encodings with the same issue.

29

H SLEIGH Extensions

Listing 2: Example syntax for an extension to the SLEIGH language that allows arrays and templated constructors to be defined.

30

Related documents

• InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy#615206
• InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy#614239
• Static validation for declarative service orchestration: enabling reliable CI/CD and MLOps pipelines#201540
• Automated Testing and Repair for Verified Compilers Generated by a Coding Agent#422329
• Fidelity Probes for Specification--Code Alignment#1116286