Remove support for __CPROVER_allocated_memory [depends-on: #6747]

regression/cbmc/Pointer28/main.c

@@ -1,7 +1,6 @@
 int main()
 {
   int *p = (int *)4;
-  __CPROVER_allocated_memory(4, sizeof(int));
   int i;
   int **q;
   char *pp;
@@ -21,7 +20,6 @@ int main()
     __CPROVER_assert(p == 0, "i==0 => p==NULL");
 
   q = (int **)8;
-  __CPROVER_allocated_memory(8, sizeof(int *));
   *q = &i;
   **q = 0x01020304;
   __CPROVER_assert(i == 0x01020304, "**q");

regression/cbmc/Pointer28/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --little-endian
+--pointer-check --little-endian --mmio-regions 4:4,8:8
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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/cprover_builtin_headers.h

@@ -46,7 +46,6 @@ __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
-void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
 
 // float stuff
 int __CPROVER_fpclassify(int, int, int, int, int, ...);

src/ansi-c/goto_check_c.cpp

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #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, [email protected]
 #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;
@@ -84,13 +89,6 @@ class goto_check_ct
     const irep_idt &function_identifier,
     goto_functiont &goto_function);
 
-  /// Fill the list of allocations \ref allocationst with <address, size> for
-  ///   every allocation instruction. Also check that each allocation is
-  ///   well-formed.
-  /// \param goto_functions: goto functions from which the allocations are to be
-  ///   collected
-  void collect_allocations(const goto_functionst &goto_functions);
-
 protected:
   const namespacet &ns;
   std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
@@ -327,6 +325,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:
@@ -420,35 +420,19 @@ static exprt implication(exprt lhs, exprt rhs)
   }
 }
 
-void goto_check_ct::collect_allocations(const goto_functionst &goto_functions)
+void goto_check_ct::parse_mmio_regions(const std::string &regions)
 {
-  for(const auto &gf_entry : goto_functions.function_map)
+  for(const std::string &range : split_string(regions, ',', true, true))
   {
-    for(const auto &instruction : gf_entry.second.body.instructions)
-    {
-      if(!instruction.is_function_call())
-        continue;
+    const auto sep = range.find(':');
+    if(sep == std::string::npos || sep + 1 == range.size())
+      continue;
 
-      const auto &function = instruction.call_function();
-      if(
-        function.id() != ID_symbol ||
-        to_symbol_expr(function).get_identifier() != CPROVER_PREFIX
-          "allocated_memory")
-        continue;
+    const std::string start = range.substr(0, sep);
+    const std::string size = range.substr(sep + 1);
 
-      const code_function_callt::argumentst &args =
-        instruction.call_arguments();
-      if(
-        args.size() != 2 || args[0].type().id() != ID_unsignedbv ||
-        args[1].type().id() != ID_unsignedbv)
-        throw "expected two unsigned arguments to " CPROVER_PREFIX
-              "allocated_memory";
-
-      DATA_INVARIANT(
-        args[0].type() == args[1].type(),
-        "arguments of allocated_memory must have same type");
-      allocations.push_back({args[0], args[1]});
-    }
+    allocations.push_back(
+      {convert_integer_literal(start), convert_integer_literal(size)});
   }
 }
 
@@ -2402,8 +2386,6 @@ void goto_check_c(
 {
   goto_check_ct goto_check(ns, options, message_handler);
 
-  goto_check.collect_allocations(goto_functions);
-
   for(auto &gf_entry : goto_functions.function_map)
   {
     goto_check.goto_check(gf_entry.first, gf_entry.second);

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) */ \