Check for memory leaks on exit and abort

doc/man/cbmc.1

@@ -178,6 +178,10 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+Enable memory cleanup checks: assert that all dynamically allocated memory is
+explicitly freed before terminating the program.
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

doc/man/goto-analyzer.1

@@ -506,6 +506,10 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+Enable memory cleanup checks: assert that all dynamically allocated memory is
+explicitly freed before terminating the program.
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

doc/man/goto-diff.1

@@ -47,6 +47,10 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+Enable memory cleanup checks: assert that all dynamically allocated memory is
+explicitly freed before terminating the program.
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

doc/man/goto-instrument.1

@@ -187,6 +187,10 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+Enable memory cleanup checks: assert that all dynamically allocated memory is
+explicitly freed before terminating the program.
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

regression/cbmc/Memory_leak_abort/main.c

@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+extern void __VERIFIER_error();
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  if(*p == 0)
+    abort();
+  if(*p == 1)
+    exit(1);
+  if(*p == 2)
+    _Exit(1);
+  if(*p == 3)
+    __VERIFIER_error();
+  free(p);
+  return 0;
+}

regression/cbmc/Memory_leak_abort/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--memory-leak-check --memory-cleanup-check --no-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+_Exit\.memory-leak\.1.*FAILURE
+__CPROVER__start\.memory-leak\.1.*SUCCESS
+abort\.memory-leak\.1.*FAILURE
+exit\.memory-leak\.1.*FAILURE
+main\.memory-leak\.1.*FAILURE
+--
+main\.assertion\.1.*FAILURE
+^warning: ignoring

src/ansi-c/goto_check_c.cpp

@@ -55,6 +55,8 @@ class goto_check_ct
     enable_bounds_check = _options.get_bool_option("bounds-check");
     enable_pointer_check = _options.get_bool_option("pointer-check");
     enable_memory_leak_check = _options.get_bool_option("memory-leak-check");
+    enable_memory_cleanup_check =
+      _options.get_bool_option("memory-cleanup-check");
     enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
     enable_enum_range_check = _options.get_bool_option("enum-range-check");
     enable_signed_overflow_check =
@@ -181,6 +183,7 @@ class goto_check_ct
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const binary_exprt &, const guardt &);
   void pointer_overflow_check(const exprt &, const guardt &);
+  void memory_leak_check(const irep_idt &function_id);
 
   /// Generates VCCs for the validity of the given dereferencing operation.
   /// \param expr the expression to be checked
@@ -256,6 +259,7 @@ class goto_check_ct
   bool enable_bounds_check;
   bool enable_pointer_check;
   bool enable_memory_leak_check;
+  bool enable_memory_cleanup_check;
   bool enable_div_by_zero_check;
   bool enable_enum_range_check;
   bool enable_signed_overflow_check;
@@ -275,6 +279,7 @@ class goto_check_ct
     {"bounds-check", &enable_bounds_check},
     {"pointer-check", &enable_pointer_check},
     {"memory-leak-check", &enable_memory_leak_check},
+    {"memory-cleanup-check", &enable_memory_cleanup_check},
     {"div-by-zero-check", &enable_div_by_zero_check},
     {"enum-range-check", &enable_enum_range_check},
     {"signed-overflow-check", &enable_signed_overflow_check},
@@ -2045,6 +2050,28 @@ optionalt<exprt> goto_check_ct::expand_pointer_checks(exprt expr)
     return {};
 }
 
+void goto_check_ct::memory_leak_check(const irep_idt &function_id)
+{
+  const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
+  const symbol_exprt leak_expr = leak.symbol_expr();
+
+  // add self-assignment to get helpful counterexample output
+  new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
+
+  source_locationt source_location;
+  source_location.set_function(function_id);
+
+  equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
+
+  add_guarded_property(
+    eq,
+    "dynamically allocated memory never freed",
+    "memory-leak",
+    source_location,
+    eq,
+    identity);
+}
+
 void goto_check_ct::goto_check(
   const irep_idt &function_identifier,
   goto_functiont &goto_function)
@@ -2196,6 +2223,19 @@ void goto_check_ct::goto_check(
       // this has no successor
       assertions.clear();
     }
+    else if(i.is_assume())
+    {
+      // These are further 'exit points' of the program
+      const exprt simplified_guard = simplify_expr(i.condition(), ns);
+      if(
+        enable_memory_cleanup_check && simplified_guard.is_false() &&
+        (function_identifier == "abort" || function_identifier == "exit" ||
+         function_identifier == "_Exit" ||
+         (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
+      {
+        memory_leak_check(function_identifier);
+      }
+    }
     else if(i.is_dead())
     {
       if(enable_pointer_check || enable_pointer_primitive_check)
@@ -2225,24 +2265,7 @@ void goto_check_ct::goto_check(
         function_identifier == goto_functionst::entry_point() &&
         enable_memory_leak_check)
       {
-        const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
-        const symbol_exprt leak_expr = leak.symbol_expr();
-
-        // add self-assignment to get helpful counterexample output
-        new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
-
-        source_locationt source_location;
-        source_location.set_function(function_identifier);
-
-        equal_exprt eq(
-          leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
-        add_guarded_property(
-          eq,
-          "dynamically allocated memory never freed",
-          "memory-leak",
-          source_location,
-          eq,
-          identity);
+        memory_leak_check(function_identifier);
       }
     }
 

src/ansi-c/goto_check_c.h

@@ -38,7 +38,7 @@ void goto_check_c(
   message_handlert &message_handler);
 
 #define OPT_GOTO_CHECK                                                         \
-  "(bounds-check)(pointer-check)(memory-leak-check)"                           \
+  "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
   "(div-by-zero-check)(enum-range-check)"                                      \
   "(signed-overflow-check)(unsigned-overflow-check)"                           \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
@@ -54,6 +54,7 @@ void goto_check_c(
   " --bounds-check               enable array bounds checks\n" \
   " --pointer-check              enable pointer checks\n" /* NOLINT(whitespace/line_length) */ \
   " --memory-leak-check          enable memory leak checks\n" \
+  " --memory-cleanup-check       enable memory cleanup checks\n" \
   " --div-by-zero-check          enable division by zero checks\n" \
   " --signed-overflow-check      enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
   " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */  \
@@ -75,6 +76,7 @@ void goto_check_c(
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
   options.set_option("pointer-check", cmdline.isset("pointer-check")); \
   options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
+  options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
   options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
   options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */  \

src/goto-programs/builtin_functions.cpp

@@ -831,6 +831,7 @@ void goto_convertt::do_function_call_symbol(
     annotated_location = function.source_location();
     annotated_location.set("user-provided", true);
     dest.add(goto_programt::make_assumption(false_exprt(), annotated_location));
+    dest.instructions.back().labels.push_back("__VERIFIER_abort");
   }
   else if(
     identifier == "assert" &&