Add new --allocate-size-check option to goto_check()

The option adds an assertion to check that not more memory is allocated
with __CPROVER_allocate() than cbmc can address. Since the primitive is
used by the models of malloc(), etc., this also guarantees that those
function don't allocate more memory than can be addressed.

Author: danpoe

src/analyses/goto_check.cpp

@@ -75,6 +75,8 @@ class goto_checkt
     error_labels=_options.get_list_option("error-label");
     enable_pointer_primitive_check =
       _options.get_bool_option("pointer-primitive-check");
+    enable_allocate_size_check =
+      _options.get_bool_option("allocate-size-check");
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -195,6 +197,8 @@ class goto_checkt
   /// \param guard: the condition under which the operation happens
   void pointer_primitive_check(const exprt &expr, const guardt &guard);
 
+  void allocate_size_check(const side_effect_exprt &expr, const guardt &guard);
+
   /// Returns true if the given expression is a pointer primitive such as
   /// __CPROVER_r_ok()
   ///
@@ -256,6 +260,7 @@ class goto_checkt
   bool enable_built_in_assertions;
   bool enable_assumptions;
   bool enable_pointer_primitive_check;
+  bool enable_allocate_size_check;
 
   typedef optionst::value_listt error_labelst;
   error_labelst error_labels;
@@ -1229,6 +1234,29 @@ void goto_checkt::pointer_primitive_check(
     guard);
 }
 
+void goto_checkt::allocate_size_check(
+  const side_effect_exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_allocate_size_check)
+    return;
+
+  const exprt size_expr = expr.operands().front();
+
+  binary_relation_exprt bre(
+    size_expr,
+    ID_le,
+    ns.lookup(CPROVER_PREFIX "max_malloc_size").symbol_expr());
+
+  add_guarded_property(
+    bre,
+    "more memory allocated than can be addressed by cbmc",
+    "allocate",
+    expr.source_location(),
+    expr,
+    guard);
+}
+
 bool goto_checkt::is_pointer_primitive(const exprt &expr)
 {
   // we don't need to include the __CPROVER_same_object primitive here as it
@@ -1812,6 +1840,15 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   {
     pointer_primitive_check(expr, guard);
   }
+  else if(expr.id() == ID_side_effect)
+  {
+    const auto &side_effect_expr = to_side_effect_expr(expr);
+
+    if(side_effect_expr.get_statement() == ID_allocate)
+    {
+      allocate_size_check(side_effect_expr, guard);
+    }
+  }
 }
 
 void goto_checkt::check(const exprt &expr)
@@ -1934,6 +1971,8 @@ void goto_checkt::goto_check(
         flag_resetter.set_flag(enable_nan_check, false);
       else if(d.first == "disable:pointer-primitive-check")
         flag_resetter.set_flag(enable_pointer_primitive_check, false);
+      else if(d.first == "disable:allocate-size-check")
+        flag_resetter.set_flag(enable_allocate_size_check, false);
     }
 
     new_code.clear();

src/analyses/goto_check.h

@@ -39,7 +39,8 @@ void goto_check(
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
-  "(pointer-primitive-check)"
+  "(pointer-primitive-check)"                                                  \
+  "(allocate-size-check)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -56,7 +57,8 @@ void goto_check(
   " --nan-check                  check floating-point for NaN\n" \
   " --no-built-in-assertions     ignore assertions in built-in library\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) */
+  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \
+  " --allocate-size-check        checks that not more memory is allocated than can be addressed by cbmc" /* NOLINT(whitespace/line_length) */
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
@@ -72,7 +74,8 @@ void goto_check(
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   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) */
+  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("allocate-size-check", cmdline.isset("allocate-size-check")) /* NOLINT(whitespace/line_length) */
 // clang-format on
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H