# Apex Returns to CompCert: A Bug Added After Six CPU-Years of Fuzzing

> Apex returned to CompCert and found a bug in code added after its famous fuzzing campaign. A 32-bit choice became a 64-bit jump-table index.
Author: Cantina
Published: September 16, 2026
Topics: CompCert, Compiler Security, Fuzzing, Formal Verification, Apex, Research
Canonical URL: https://www.cantina.security/blog/compcert-x86-64-switch-miscompilation

[Apex](https://www.cantina.security/apex), Cantina's autonomous OffSec agent, found that CompCert 3.0 through 3.17 could generate incorrect x86-64 code for a valid C `switch` statement and cause the resulting program to read beyond its jump table, crash or jump to an unintended address. The public reproducer does not demonstrate remote exploitation or reliable attacker control of that address.

CompCert fixed the bug in [version 3.18](https://github.com/AbsInt/CompCert/releases/tag/v3.18), released August 30, 2026, so upgrade to 3.18 or later and assess whether affected x86-64 programs need to be rebuilt and retested.

## Introduction

[Apex](https://www.cantina.security/apex), Cantina's autonomous OffSec agent, found that [CompCert](https://compcert.org/) versions 3.0 through 3.17 could miscompile a correct C `switch` statement for x86-64 by treating the switch as a 32-bit number and then using all 64 bits of the physical processor register to look up the next instruction. Leftover data in the upper 32 bits could push that lookup beyond the jump table and make the compiled program fault or continue at an address the developer never selected. CompCert fixed the bug in [PR #595](https://github.com/AbsInt/CompCert/pull/595) and released the correction in [version 3.18](https://github.com/AbsInt/CompCert/releases/tag/v3.18).

This was Apex's second take on CompCert after finding and reproducing [three bugs around the edges of its verified core](https://www.cantina.security/blog/how-we-found-three-bugs-in-a-compiler-proven-correct). Two of those findings pointed to physical registers and the code that prints final assembly, so Apex returned to those handoffs and found a fourth separate flaw where the same concerns met.

A well-known 2011 Csmith campaign tested the CompCert version available at the time and could not have tested this bug because CompCert added the affected x86-64 jump-table code five years later in 2016.

## What CompCert is, and why it matters

A processor cannot run C source code, and a compiler translates that source into the machine instructions the processor executes.

Most developers never inspect those final instructions because they rely on the basic promise that if the source says "choose option 8" the executable will still choose option 8.

CompCert is built to make that promise strong by compiling most of the C language for ARM, PowerPC, RISC-V and x86 processors through main compilation passes backed by machine-checked mathematical proofs that the generated code preserves the behavior allowed by the source program.

CompCert is intended for embedded software beyond research and the project announced in March 2026 that the compiler had been qualified for the MFC_NG computer used in ATR 42 and ATR 72 aircraft. This shows the level of assurance expected from the compiler, although the public evidence does not show that the affected x86-64 path was used in that aircraft system or caused an incident in any deployed product.

The proof covers defined parts of the compiler while a complete toolchain also has to parse input, follow processor and operating-system rules, print assembly text and hand that text to an assembler. Some of those steps sit outside the proved translation and need their own checks.

This bug lived in one of those final steps because CompCert's formal x86 model held the correct 32-bit value while the OCaml printer emitted an x86-64 instruction that indexed the table with all 64 physical bits.

## How a switch becomes a jump table

A developer might write:

```c
switch (choice) {
    case 7:
        return first_action();
    case 8:
        return second_action();
    case 9:
        return third_action();
}
```

For a compact group of choices a compiler can turn this into a jump table, which lists the destinations for each choice. The compiler maps each choice to an entry, allowing the program to read the destination from that slot and jump there. The entry number can differ from the case value if the compiler adjusts the index.

The table lookup is safe only if the value checked by the compiler is the same value used by the processor, but those values could differ here.

## One value in C, another at the processor

CompCert's regression test captures the problem with this 64-bit value:

```c
// CompCert-small-tests/regression/switch.c
volatile long long gremlin = 0x1234567800000008;

printf("f(gremlin) = %d\n", f((unsigned int) gremlin));
```

The cast to `unsigned int` discards the upper half:

```text
original 64-bit value:  0x1234567800000008
value after 32-bit cast:         0x00000008
switch choice:                            8
expected result:                         22
```

The C program and CompCert's formal semantics both see `8` while the physical 64-bit register could still contain `0x12345678` in its upper half. The x86-64 printer used the full register as the table index and therefore included the bits the C cast had removed from the value.

That created two versions of the same choice:

| Layer | Value used for the jump-table lookup |
| --- | --- |
| C source | `8` |
| CompCert model | `8` |
| Vulnerable x86-64 instruction | `0x1234567800000008` |

The source and the model selected entry 8 while the processor was told to calculate an address from the much larger value.

## The mismatch in `TargetPrinter.ml`

CompCert represents its internal jump-table instruction as `Pjmptbl`, whose formal semantics accepts a 32-bit integer called a `Vint` and uses `Int.unsigned n` to select the table entry:

```text
selector = unsigned_value_of_32_bit_integer(register)
destination = jump_table[selector]
```

The vulnerable x86-64 printer instead used the register directly in a 64-bit address calculation:

```text
base = address of jump table
offset = read 4 bytes at base + (register64 * 4)
destination = base + offset
jump to destination
```

The patch to [`x86/TargetPrinter.ml`](https://github.com/AbsInt/CompCert/commit/736b181a58c076475792bf815c6c06a814c7b5a8) shows the missing step in the faulty code:

```diff
- fprintf oc "\tmovslq\t(%a, %a, 4), %a\n" ireg tmp1 ireg r ireg tmp2;

+ (* Normalize r to 32-bit unsigned *)
+ fprintf oc "\tmovl\t%a, %a\n" ireg32 r ireg32 tmp2;
+ fprintf oc "\tmovslq\t(%a, %a, 4), %a\n" ireg tmp1 ireg tmp2 ireg tmp2;
```

The old code indexed the table with the full 64-bit register `r` while the fix first copies its low 32 bits with `movl` and indexes with the temporary register.

Writing to a 32-bit register on x86-64 clears the upper 32 bits of the matching 64-bit register, so the new instruction produces the same unsigned 32-bit value used by CompCert's model and makes the processor look up entry 8.

## What the compiled program could do

The faulty address calculation could read outside the jump table.

- If the calculated address was unmapped, the read could fault and stop the program.
- If the address was readable, the processor could treat four unrelated bytes as a signed offset and jump to an unintended address.

This is a wrong-code bug because valid source can produce an executable that behaves in a way the source program did not allow. Reviewing the C code alone would not reveal the bad instruction because the error entered during compilation.

The public reproducer proves the incorrect lookup without demonstrating remote exploitation, reliable control of the final jump target or an incident in deployed software. As of September 16, 2026, neither the maintainer's PR nor the CompCert 3.18 release notes assigns a severity level or CVSS score to this issue.

## What the fuzzing result did and did not cover

Csmith tests compilers by generating unusual but valid C programs and comparing how different compilers execute them. Its 2011 paper reported that Csmith could not find a wrong-code error in the under-development CompCert version despite about six CPU-years of testing. The researchers had found earlier bugs in unverified front-end code and a PowerPC constraint that the assembler caught, but not the middle-end wrong-code failures seen in other compilers.

The 2011 result applies only to the CompCert code that existed then and cannot establish the behavior of code added afterward.

The RIP-relative x86-64 jump-table implementation entered CompCert on [October 11, 2016](https://github.com/AbsInt/CompCert/commit/e73d255ec045983787ed935ad02d31d45353a2b1). A fuzzer could find this bug in principle, but it would need to create a specific chain:

1. Keep nonzero data in the upper half of a 64-bit value.
2. Cast that value to 32 bits.
3. Carry it through the physical register without clearing the upper half.
4. Use it in a dense `switch` that becomes a jump table.

The public record does not show whether a later fuzzing campaign generated that combination, although CompCert's new regression test does because it was written with the faulty assumption known.

## Why Apex returned to the same codebase

Apex had found two relevant patterns in CompCert through an earlier mismatch between its register model and the state held by physical XMM registers on Windows and another issue in assembly-printing code outside the proved compiler passes.

Those findings narrowed the next search as Apex followed values across the handoff between the formal model, processor rules and final output. The fourth issue combined both themes when a modeled 32-bit value became a 64-bit physical index in the assembly printer.

Apex autonomously discovered the flaw. The [public PR](https://github.com/AbsInt/CompCert/pull/595) credits Christos Papakonstantinou of Cantina Security with reporting it to the CompCert project.

## How CompCert fixed it

CompCert made three related changes:

1. The x86-64 printer now zero-extends the 32-bit selector before using it as a 64-bit index.
2. A regression test keeps nonzero upper bits in the source value and confirms that the compiled program still chooses case 8.
3. A review of the same assumption found a much less practical RISC-V edge case. CompCert added [an assertion](https://github.com/AbsInt/CompCert/commit/70077daf12314ca564bdd65449e714778b620f14) that prevents jump tables with more than `2^31` entries.

The vulnerable x86-64 implementation first appeared in October 2016 and shipped in CompCert 3.0 through 3.17 before the correction shipped in CompCert 3.18 on August 30, 2026.

Teams that compile x86-64 software with an affected version should upgrade to [CompCert 3.18](https://github.com/AbsInt/CompCert/releases/tag/v3.18) or later and assess whether programs built with versions 3.0 through 3.17 need to be rebuilt and retested.

## The proof stopped before the faulty printer

The proof selected the correct table entry but the failure happened afterward when code outside that proof mapped the modeled value to a physical register. This does not invalidate CompCert's theorem but shows why a security review must state exactly where a guarantee ends and follow the same value through the code that comes next.

The 2011 fuzzing result described a specific version and new x86-64 code created another path to inspect five years later, showing why testing must follow the software as it changes.

## Disclosure timeline

1. **October 11, 2016:** CompCert added the affected RIP-relative x86-64 jump-table implementation.
2. **August 23, 2026:** CompCert opened PR #595 for the bug discovered by Apex and reported by Cantina.
3. **August 23, 2026:** CompCert added the regression test.
4. **August 27, 2026:** CompCert merged the x86-64 fix, regression test, and RISC-V guard.
5. **August 30, 2026:** CompCert released version 3.18 with the correction.

## Frequently asked questions

### Did the bug invalidate CompCert's proof?

The proved `Pjmptbl` model selected the correct 32-bit value and the mismatch appeared later in the OCaml printer that emitted x86-64 assembly, so the bug did not invalidate CompCert's proof.

### Did this bug survive six CPU-years of fuzzing?

The 2011 Csmith campaign tested an earlier CompCert and could not have tested this bug because the affected x86-64 code was added in 2016.

### Which CompCert versions are affected?

The faulty implementation shipped in CompCert 3.0 through 3.17 and CompCert 3.18 contains the fix.

### Was exploitation demonstrated?

The regression proves an out-of-table lookup that can fault or use unrelated bytes as a jump offset without establishing remote exploitation or reliable control of the destination.

## Follow the instruction all the way down

[Apex](https://www.cantina.security/apex), Cantina's autonomous OffSec agent, follows security decisions across source code, generated output and running systems to reproduce failures and verify fixes.

## Sources

- [CompCert PR #595](https://github.com/AbsInt/CompCert/pull/595)
- [x86-64 fix commit](https://github.com/AbsInt/CompCert/commit/736b181a58c076475792bf815c6c06a814c7b5a8)
- [CompCert regression test](https://github.com/AbsInt/CompCert-small-tests/commit/4df7312a3ff71037c20856dfeff727e36c77848e)
- [RISC-V follow-up guard](https://github.com/AbsInt/CompCert/commit/70077daf12314ca564bdd65449e714778b620f14)
- [CompCert 3.18 release](https://github.com/AbsInt/CompCert/releases/tag/v3.18)
- [CompCert project](https://compcert.org/)
- [Csmith compiler-testing paper](https://www-leland.stanford.edu/class/cs343/resources/finding-bugs-compilers-annotated.pdf)
- [Cantina's first CompCert technical analysis](https://www.cantina.security/blog/how-we-found-three-bugs-in-a-compiler-proven-correct)