New option --mmio-regions to specify memory regions

This new option will enable us to eventually drop support for
__CPROVER_allocated_memory, which
1) requires awkward scanning of goto functions in goto_check_c,
2) wrongly suggests these declarations are limited to some scope, and
3) yields a spurious undefined-function warning in symex.

Author: tautschnig

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;

src/ansi-c/goto_check_c.cpp

@@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
+#include <util/string_utils.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
@@ -44,6 +45,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 #include <optional>
 
+#include "literals/convert_integer_literal.h"
+
 class goto_check_ct
 {
 public:
@@ -76,6 +79,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_option("mmio-regions"));
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -327,6 +332,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 std::string &regions);
 };
 
 /// Allows to:
@@ -452,6 +459,22 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions)
   }
 }
 
+void goto_check_ct::parse_mmio_regions(const std::string &regions)
+{
+  for(const std::string &range : split_string(regions, ',', true, true))
+  {
+    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,8 @@ 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_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) */ \