Add memory leak instrumentation to abort and exit

SV-COMP (also) requires that all dynamically allocated memory is freed
via `free` before terminating the program.

Author: peterschrammel

doc/man/cbmc.1

@@ -178,6 +178,9 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+enable memory cleanup checks
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

doc/man/goto-analyzer.1

@@ -506,6 +506,9 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+enable memory cleanup checks
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

doc/man/goto-diff.1

@@ -47,6 +47,9 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+enable memory cleanup checks
+.TP
 \fB\-\-div\-by\-zero\-check\fR
 enable division by zero checks
 .TP

doc/man/goto-instrument.1

@@ -187,6 +187,9 @@ enable pointer checks
 \fB\-\-memory\-leak\-check\fR
 enable memory leak checks
 .TP
+\fB\-\-memory\-cleanup\-check\fR
+enable memory cleanup checks
+.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() __attribute__((__noreturn__));
+
+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 =
@@ -257,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;
@@ -276,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},
@@ -2219,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)

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" &&