Skip to content

Document supported inline assembly instructions #8937

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Document supported inline assembly instructions #8937

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions doc/cprover-manual/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@
* [Floating Point](modeling/floating-point/)
* [Generating Environments](goto-harness/)
* [Memory-mapped I/O](modeling/mmio/)
* [Inline Assembly](modeling/inline-asm/)
* [Shadow Memory](modeling/shadow-memory/)

8. Build Systems
Expand Down
58 changes: 58 additions & 0 deletions doc/cprover-manual/modeling-inline-asm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
[CPROVER Manual TOC](../../)

## Modeling Inline Assembly

CBMC supports GCC-style (`asm`/`__asm__`) and MSVC-style (`__asm {}`)
inline assembly syntax. During verification, the `remove_asm` pass
translates recognized instructions into equivalent goto-program
operations. **Unrecognized instructions are silently removed**, which
may lead to unsound results if the assembly has side effects that
matter for the property being verified.
Comment on lines +6 to +10
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This says “Unrecognized instructions are silently removed”, but in src/assembler/remove_asm.cpp any unknown instruction sets unknown=true and then the pass discards all translated instructions for that asm statement (even ones it recognized earlier). Consider clarifying that an asm statement containing any unrecognized instruction is dropped entirely.

Copilot uses AI. Check for mistakes.

### Supported Instructions

#### x86

| Instruction | Effect in CBMC |
|---|---|
| `mfence` | Full memory fence |
| `lfence` | Load memory fence |
| `sfence` | Store memory fence |
Comment on lines +19 to +20
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The table states lfence/sfence are load/store fences, but CBMC currently models __asm_lfence and __asm_sfence as a full __CPROVER_fence (same as mfence) in src/ansi-c/library/x86_assembler.c. Please update the documented effect (or adjust the underlying model if the intent is to distinguish them).

Suggested change
| `lfence` | Load memory fence |
| `sfence` | Store memory fence |
| `lfence` | Full memory fence (modeled same as `mfence`) |
| `sfence` | Full memory fence (modeled same as `mfence`) |

Copilot uses AI. Check for mistakes.
| `fstcw` / `fnstcw` | Store FP control word (maps to `__CPROVER_rounding_mode`) |
| `fldcw` | Load FP control word (maps to `__CPROVER_rounding_mode`) |
| `xchg` / `xchgl` | Exchange; wrapped in atomic section with full fence |
| `lock` prefix | Wraps the following instruction in an atomic section with full fence |
Comment on lines +23 to +24
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

xchg/xchgl and the lock prefix are listed as supported and “wrapped in an atomic section with full fence”, but remove_asm doesn’t actually translate these instructions: xchg only flips an internal x86_32_locked_atomic flag and then is treated as unknown, causing the whole asm statement to be dropped. Please either remove these from the supported list or clarify their current behavior (or implement proper modeling).

Copilot uses AI. Check for mistakes.

#### ARM

| Instruction | Effect in CBMC |
|---|---|
| `dmb` | Data memory barrier (full fence) |
| `dsb` | Data synchronization barrier (full fence) |
| `isb` | Instruction synchronization barrier |

#### Power

| Instruction | Effect in CBMC |
|---|---|
| `sync` | Full memory barrier |
| `lwsync` | Lightweight sync (all fences except WR) |
| `isync` | Instruction sync (no fence effect on its own) |

### Operand Handling

For GCC extended assembly, CBMC processes the output (`=r`, `+r`) and
input (`r`, `m`) operand lists. Output operands are assigned
nondeterministic values when the instruction is not otherwise modeled.
Comment on lines +44 to +46
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The claim that output operands are assigned nondeterministic values when an instruction is not otherwise modeled doesn’t match remove_asm: for unknown instructions the asm statement is turned into skip with no assignments, and for modeled fences (e.g., mfence) outputs aren’t written either. Please update this section to reflect the actual behavior (outputs only change when the modeled helper writes through an output pointer, e.g., fstcw/fnstcw/fldcw).

Suggested change
For GCC extended assembly, CBMC processes the output (`=r`, `+r`) and
input (`r`, `m`) operand lists. Output operands are assigned
nondeterministic values when the instruction is not otherwise modeled.
For GCC extended assembly, CBMC parses the output (`=r`, `+r`) and
input (`r`, `m`) operand lists, but in most cases the operands do not
directly influence the generated goto program. For recognized fence
instructions (for example, `mfence`, `lfence`, `sfence`, `dmb`), the
inline assembly is replaced by appropriate fence operations and the
C-level output operands are not written. For unrecognized instructions,
the entire asm statement is removed (translated to `skip`) with no
assignments to outputs and no introduction of nondeterministic values.
Output operands only have an effect when the modeled helper for a
particular instruction reads or writes through a memory operand
(pointer) associated with that output, such as in the handling of
`fstcw` / `fnstcw` / `fldcw`, which map to `__CPROVER_rounding_mode`.

Copilot uses AI. Check for mistakes.
Clobber lists are parsed but do not affect verification.

### Limitations

- Only the instructions listed above are modeled. All other assembly
instructions are silently ignored (removed from the program).
- No diagnostic is emitted for unrecognized instructions. Use
`goto-instrument --show-goto-functions` to inspect whether assembly
was translated or dropped.
- Complex atomic operations beyond `lock`/`xchg` are not modeled.
- MSVC-style `__asm` blocks are parsed but instruction support is the
same as for GCC-style.
Comment on lines +56 to +58
Copy link

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The limitations section says MSVC-style __asm support is “the same as for GCC-style”, and mentions atomics “beyond lock/xchg”. In remove_asm.cpp, MSVC-style modeling only covers the x86 *f?stcw, fldcw, and *fence instructions (no ARM/Power, and no effective lock/xchg modeling). Please adjust these bullets to match the actual supported subset.

Suggested change
- Complex atomic operations beyond `lock`/`xchg` are not modeled.
- MSVC-style `__asm` blocks are parsed but instruction support is the
same as for GCC-style.
- For GCC-style inline assembly, complex atomic operations beyond the
basic `lock`/`xchg` patterns listed above are not modeled as single
atomic operations.
- MSVC-style `__asm` blocks are parsed; currently only the x86
`mfence`/`lfence`/`sfence`, `fstcw`/`fnstcw`, and `fldcw` instructions
are modeled. ARM/Power instructions and `lock`-prefixed / `xchg`
instructions are not modeled for MSVC-style inline assembly.

Copilot uses AI. Check for mistakes.
Loading