Support --mmio-region in cbmc

Add --mmio-region to cbmc so that per-region MMIO instrumentation is
available without requiring goto-instrument as a separate step. The
option is handled in process_goto_program, which is shared by cbmc,
goto-analyzer, goto-diff, and the C++ API.

Per-region instrumentation runs before the callback model so that
declared regions get precise array-backed modeling while callbacks
can still handle remaining dereferences.

Extract parse_mmio_regions() into mm_io.h/mm_io.cpp to eliminate
duplicated region-parsing and overlap-checking logic.

Add cmdline.desc tests for all existing tests that use
__CPROVER_allocated_memory (memory_allocation1/2, Pointer28, union12,
pointer-overflow2, cbmc-incr-smt2/pointer_from_int) with #ifndef
CMDLINE guards so the same source works with both mechanisms.

Includes cbmc man page entry and updated CProver manual and
goto-instrument man page with cross-references.

Co-authored-by: Kiro (autonomous agent) <[email protected]>

Author: tautschnig

doc/cprover-manual/modeling-mmio.md

@@ -75,11 +75,13 @@ functions, there are two approaches available.
 
 #### Per-region object model (recommended)
 
-Use `--mmio-region <address>:<size>` (with `goto-instrument` or `cbmc`) to
-declare each contiguous MMIO region as an individual object. Each region becomes
-a byte array in the symbol table, named `__CPROVER_mmio_region_0x<address>`.
-Reads and writes to addresses within a declared region are redirected to the
-corresponding array element.
+Use `--mmio-region <address>:<size>` to declare each
+contiguous MMIO region as an individual object. Each region becomes a byte array
+in the symbol table, named `__CPROVER_mmio_region_0x<address>`. Reads and writes
+to addresses within a declared region are redirected to the corresponding array
+element.
+
+This option is supported by both `cbmc` and `goto-instrument`.
 
 This approach avoids the scalability problems of the single-array callback model:
 each write only updates the targeted region object rather than the entire memory
@@ -89,6 +91,12 @@ For example, given firmware that accesses a UART at `0x40000000` (256 bytes) and
 a GPIO controller at `0x40001000` (64 bytes):
 
 ```sh
+# Directly with cbmc:
+cbmc --mmio-region 0x40000000:256 \
+  --mmio-region 0x40001000:64 \
+  --no-pointer-check --no-bounds-check firmware.c
+
+# Or via goto-instrument:
 goto-cc -o firmware.gb firmware.c
 goto-instrument --mmio-region 0x40000000:256 \
   --mmio-region 0x40001000:64 \

doc/man/cbmc.1

@@ -322,6 +322,29 @@ print test suite for coverage criterion (requires \fB\-\-cover\fR)
 \fB\-\-mm\fR MM
 memory consistency model for concurrent programs (default: sc)
 .TP
+\fB\-\-mmio\-region\fR \fIaddress\fR:\fIsize\fR
+Define a contiguous memory\-mapped I/O region starting at \fIaddress\fR with the
+given \fIsize\fR in bytes. The \fIaddress\fR may use a \fB0x\fR prefix for
+hexadecimal notation. This option may be repeated to define multiple regions.
+Regions must not overlap.
+.IP
+Each region is modeled as an individual byte\-array object in the symbol table.
+Reads from and writes to constant addresses that fall within a declared region
+are mapped directly to the corresponding array element. Symbolic addresses are
+handled via a conditional dispatch over all declared regions.
+.IP
+Use \fB\-\-no\-pointer\-check\fR and \fB\-\-no\-bounds\-check\fR when verifying
+programs with MMIO regions, since integer addresses used for memory\-mapped I/O
+are not valid pointers from CBMC's perspective.
+.IP
+Example:
+.EX
+.in +4n
+cbmc \-\-mmio\-region 0x40000000:256 \-\-mmio\-region 0x40001000:64 \\
+  \-\-no\-pointer\-check \-\-no\-bounds\-check firmware.c
+.in
+.EE
+.TP
 \fB\-\-malloc\-may\-fail\fR
 allow malloc calls to return a null pointer
 .TP

doc/man/goto-instrument.1

@@ -407,6 +407,8 @@ This per\-region model avoids the scalability problems of the single unbounded
 write only updates the targeted region object rather than the entire memory
 array. Both options can be combined.
 .IP
+This option is also supported directly by \fBcbmc\fR(1).
+.IP
 Example:
 .EX
 .in +4n

regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.c

@@ -1,7 +1,9 @@
 int main()
 {
   int *p = (int *)4;
+#ifndef CMDLINE
   __CPROVER_allocated_memory(4, sizeof(int));
+#endif
 
   __CPROVER_assert(p == 4, "p == 4: expected success");
   __CPROVER_assert(p != 0, "p != 0: expected success");

regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int_cmdline.desc

@@ -0,0 +1,15 @@
+CORE
+pointer_from_int.c
+-DCMDLINE --mmio-region 0x4:4 --trace --no-pointer-check --no-bounds-check
+\[main\.assertion\.1\] line \d+ p == 4: expected success: SUCCESS
+\[main\.assertion\.2\] line \d+ p != 0: expected success: SUCCESS
+\[main\.assertion\.3\] line \d+ p == 0x1020304: expected success: SUCCESS
+\[main\.assertion\.4\] line \d+ p != 0: expected success: SUCCESS
+\[main\.assertion\.5\] line \d+ p != 0: expected failure: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Same as pointer_from_int.desc but uses --mmio-region instead of
+__CPROVER_allocated_memory.

regression/cbmc/Pointer28/cmdline.desc

@@ -0,0 +1,11 @@
+KNOWNBUG no-new-smt
+main.c
+-DCMDLINE --mmio-region 0x4:4 --mmio-region 0x8:8 --little-endian --no-pointer-check --no-bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The per-region byte-array model does not support storing and loading
+pointer values through MMIO regions, so the **q test case fails.

regression/cbmc/Pointer28/main.c

@@ -1,7 +1,9 @@
 int main()
 {
   int *p = (int *)4;
+#ifndef CMDLINE
   __CPROVER_allocated_memory(4, sizeof(int));
+#endif
   int i;
   int **q;
   char *pp;
@@ -21,7 +23,9 @@ int main()
     __CPROVER_assert(p == 0, "i==0 => p==NULL");
 
   q = (int **)8;
+#ifndef CMDLINE
   __CPROVER_allocated_memory(8, sizeof(int *));
+#endif
   *q = &i;
   **q = 0x01020304;
   __CPROVER_assert(i == 0x01020304, "**q");

regression/cbmc/memory_allocation1/cmdline.desc

@@ -0,0 +1,10 @@
+CORE broken-smt-backend paths-lifo-expected-failure
+main.c
+-DCMDLINE --mmio-region 0x10:4 --no-pointer-check --no-bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
+^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/memory_allocation1/main.c

@@ -4,7 +4,9 @@ int main()
 {
   int *p=0x10;
 
+#ifndef CMDLINE
   __CPROVER_allocated_memory(0x10, sizeof(int));
+#endif
   *p=42;
   assert(*p==42);
   *(p+1)=42;

regression/cbmc/memory_allocation2/cmdline.desc

@@ -0,0 +1,14 @@
+KNOWNBUG
+main.c
+-DCMDLINE --mmio-region 0x1000:400 --mmio-region 0x11000:400 --mmio-region 0x21000:400 --mmio-region 0x31000:400 --no-pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.array_bounds\.[1-2]\] .*: SUCCESS$
+^\[main\.array_bounds\.3\] .* upper bound in buffers\[.*0\]->buffer\[.*100\]: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The per-region MMIO model uses byte arrays, so structured access via
+buffers[0]->buffer[N] does not preserve the original array bounds.
+All three bounds checks fail instead of only the out-of-bounds one.