New option --mmio-regions to specify memory regions

regression/cbmc/memory_allocation1/cmdline.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+main.c
+--pointer-check -DCMDLINE --mmio-regions 0x10:4
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$
+^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
+^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$
+^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: SUCCESS$
+^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,11 @@
+CORE
+main.c
+--bounds-check -DCMDLINE --mmio-regions 0x1000:400,0x11000:400 --mmio-regions 0x21000:400,0x31000:400
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$
+^\[main\.array_bounds\.[67]\] line 40 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
+^\*\* 1 of 12 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/memory_allocation2/main.c

@@ -24,10 +24,12 @@ static buffert(*const buffers[4]) = {BUF0, BUF1, BUF2, BUF3};
 
 main()
 {
+#ifndef CMDLINE
   __CPROVER_allocated_memory(BUF0_BASE, sizeof(buffert));
   __CPROVER_allocated_memory(BUF1_BASE, sizeof(buffert));
   __CPROVER_allocated_memory(BUF2_BASE, sizeof(buffert));
   __CPROVER_allocated_memory(BUF3_BASE, sizeof(buffert));
+#endif
 
   _cbmc_printf2(sizeof_buffers, sizeof(buffers));
   _cbmc_printf2(sizeof_buffers_0, sizeof(buffers[0]));
@@ -36,4 +38,7 @@ main()
   buffers[0]->buffer[0];
   buffers[0]->buffer[BUFFER_SIZE - 1];
   buffers[0]->buffer[BUFFER_SIZE]; // should be out-of-bounds
+  buffers[1]->buffer[0];
+  buffers[2]->buffer[0];
+  buffers[3]->buffer[0];
 }

regression/cbmc/memory_allocation2/test.desc

@@ -4,8 +4,8 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$
-^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
-^\*\* 1 of 6 failed
+^\[main\.array_bounds\.[67]\] line 40 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
+^\*\* 1 of 12 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/ansi-c/goto_check_c.cpp

@@ -44,6 +44,8 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <optional>
 
+#include "literals/convert_integer_literal.h"
+
 class goto_check_ct
 {
 public:
@@ -76,6 +78,8 @@ class goto_check_ct
     error_labels = _options.get_list_option("error-label");
     enable_pointer_primitive_check =
       _options.get_bool_option("pointer-primitive-check");
+
+    parse_mmio_regions(_options.get_list_option("mmio-regions"));
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -327,6 +331,8 @@ class goto_check_ct
   /// \returns a pair (name, status) if the match succeeds
   /// and the name is known, nothing otherwise.
   named_check_statust match_named_check(const irep_idt &named_check) const;
+
+  void parse_mmio_regions(const optionst::value_listt &regions);
 };
 
 /// Allows to:
@@ -463,6 +469,22 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions)
   }
 }
 
+void goto_check_ct::parse_mmio_regions(const optionst::value_listt &regions)
+{
+  for(const std::string &range : regions)
+  {
+    const auto sep = range.find(':');
+    if(sep == std::string::npos || sep + 1 == range.size())
+      continue;
+
+    const std::string start = range.substr(0, sep);
+    const std::string size = range.substr(sep + 1);
+
+    allocations.push_back(
+      {convert_integer_literal(start), convert_integer_literal(size)});
+  }
+}
+
 void goto_check_ct::invalidate(const exprt &lhs)
 {
   if(lhs.id() == ID_index)

src/ansi-c/goto_check_c.h

@@ -44,6 +44,7 @@ void goto_check_c(
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
   "(pointer-primitive-check)"                                                  \
+  "(mmio-regions):"                                                            \
   "(retain-trivial-checks)"                                                    \
   "(error-label):"                                                             \
   "(no-assertions)(no-assumptions)"                                            \
@@ -64,6 +65,8 @@ void goto_check_c(
   " --nan-check                  check floating-point for NaN\n" \
   " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
   " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \
+  " --mmio-regions addr:sz,...   list of start-address:size address ranges\n" \
+  "                              permitted for read/write access\n" \
   " --retain-trivial-checks      include checks that are trivially true\n" \
   " --error-label label          check that label is unreachable\n" \
   " --no-built-in-assertions     ignore assertions in built-in library\n" \
@@ -86,6 +89,9 @@ void goto_check_c(
   options.set_option("nan-check", cmdline.isset("nan-check")); \
   options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
+  if(cmdline.isset("mmio-regions")) \
+    options.set_option( \
+      "mmio-regions", cmdline.get_comma_separated_values("mmio-regions")); \
   options.set_option("retain-trivial-checks", \
                      cmdline.isset("retain-trivial-checks")); \
   options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \