From af79085dadb7af00506305e3862e3467cb9460c6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 30 Mar 2026 17:51:08 +0000 Subject: [PATCH] Document supported inline assembly instructions Add doc/cprover-manual/modeling-inline-asm.md listing the assembly instructions that CBMC's remove_asm pass translates (x86 fences and FP control, ARM barriers, Power sync instructions, and lock/xchg atomics). Note that unrecognized instructions are silently removed. Link the new page from the manual index. Fixes: #6374 Co-authored-by: Kiro (autonomous agent) --- doc/cprover-manual/index.md | 1 + doc/cprover-manual/modeling-inline-asm.md | 58 +++++++++++++++++++++++ 2 files changed, 59 insertions(+) create mode 100644 doc/cprover-manual/modeling-inline-asm.md diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 12e1a9c046b..83b0a2eb85b 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -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 diff --git a/doc/cprover-manual/modeling-inline-asm.md b/doc/cprover-manual/modeling-inline-asm.md new file mode 100644 index 00000000000..65215d9eeb6 --- /dev/null +++ b/doc/cprover-manual/modeling-inline-asm.md @@ -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. + +### Supported Instructions + +#### x86 + +| Instruction | Effect in CBMC | +|---|---| +| `mfence` | Full memory fence | +| `lfence` | Load memory fence | +| `sfence` | Store memory fence | +| `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 | + +#### 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. +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.