C library: atexit

atexit introduces function calls that may affect the verification
outcome.

Author: tautschnig

regression/cbmc-library/atexit-01/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void cleanup()
+{
+  assert(0);
+}
+
+int main()
+{
+  atexit(cleanup);
+}

regression/cbmc-library/atexit-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-library/atexit-02/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void cleanup()
+{
+  assert(0);
+}
+
+int main()
+{
+  atexit(cleanup);
+  exit(0);
+}

regression/cbmc-library/atexit-02/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-library/posix_memalign-02/test.desc

@@ -6,5 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 \[main.precondition_instance.1\] .* memcpy src/dst overlap: FAILURE
 \[main.precondition_instance.3\] .* memcpy destination region writeable: FAILURE
+\*\* 2 of 24 failed
 --
 ^warning: ignoring

regression/cbmc-library/pthread_cond_wait-01/test.desc

@@ -3,7 +3,7 @@ main.c
 --bounds-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\*\* 1 of 2 failed
+^\*\* 1 of 4 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed
+\*\* 1 of 18 failed
 --
 ^warning: ignoring
 --

regression/cbmc/array-cell-sensitivity2/test.desc

@@ -6,7 +6,7 @@ main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-\[\[[0-9]+\]\]
+array.*\[\[[0-9]+\]\]
 --
 This checks that arrays of uncertain size are always treated as aggregates and
 are not expanded into individual cell symbols (which use the [[index]] notation

regression/cbmc/array_constraints1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 2 of 14
+^\*\* 2 of 24
 --
 ^warning: ignoring

regression/cbmc/memory_allocation2/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$
 ^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
-^\*\* 1 of 6 failed
+^\*\* 2 of 9 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/multiple-goto-traces/test.desc

@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-Trace for main\.assertion\.1:(\n.*){22}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50}  assertion argc \+ 1 != 5
+Trace for main\.assertion\.1:(\n.*){150}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){164}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){178}  assertion argc \+ 1 != 5
 \*\* 3 of 4 failed
 --
 ^warning: ignoring

regression/cbmc/pragma_cprover1/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --signed-overflow-check --bounds-check
 line 14 array 'y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$
-^\*\* 1 of 1 failed
+^\*\* 1 of 4 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/pragma_cprover2/test.desc

@@ -3,7 +3,7 @@ main.c
 --signed-overflow-check
 ^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$
 ^\[main.overflow\.2\] line 22 arithmetic overflow on signed \+ in x \+ n: FAILURE$
-^\*\* 2 of 2 failed
+^\*\* 2 of 3 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/switch8/test.desc

@@ -13,7 +13,7 @@ main.c
 ^\[main\.pointer_dereference\.4\] line 42 dereference failure: dead object in \*p: FAILURE$
 ^\[main\.assertion\.4\] line 49 assertion e == 42: FAILURE$
 ^\[main\.assertion\.5\] line 51 assertion f == 42: FAILURE$
-^\*\* 4 of 10 failed
+^\*\* 4 of 18 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/union12/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] line 20 should fail: FAILURE$
-^\*\* 1 of 15 failed
+^\*\* 1 of 25 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/analyses/goto_check_c.cpp

@@ -2213,6 +2213,28 @@ void goto_check_ct::goto_check(
         i.turn_into_skip();
         did_something = true;
       }
+
+      if(enable_memory_leak_check && function_identifier == "exit")
+      {
+        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);
+      }
     }
     else if(i.is_dead())
     {
@@ -2262,29 +2284,6 @@ void goto_check_ct::goto_check(
     }
     else if(i.is_end_function())
     {
-      if(
-        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);
-      }
     }
 
     for(auto &instruction : new_code.instructions)

src/ansi-c/ansi_c_entry_point.cpp

@@ -242,6 +242,8 @@ bool generate_ansi_c_start_function(
   const code_typet::parameterst &parameters=
     to_code_type(symbol.type).parameters();
 
+  const namespacet ns(symbol_table);
+
   if(symbol.name==ID_main)
   {
     if(parameters.empty())
@@ -250,8 +252,6 @@ bool generate_ansi_c_start_function(
     }
     else if(parameters.size()==2 || parameters.size()==3)
     {
-      namespacet ns(symbol_table);
-
       {
         symbolt argc_symbol;
 
@@ -498,8 +498,23 @@ bool generate_ansi_c_start_function(
       parameters, init_code, symbol_table, object_factory_parameters);
   }
 
+  exprt return_value = call_main.lhs();
   init_code.add(std::move(call_main));
 
+  const symbolt &exit_symbol = ns.lookup("exit");
+  const typet &arg_type = to_code_type(exit_symbol.type).parameters()[0].type();
+  code_function_callt call_exit{exit_symbol.symbol_expr()};
+  if(return_value.is_not_nil())
+  {
+    call_exit.arguments().push_back(
+      typecast_exprt::conditional_cast(return_value, arg_type));
+  }
+  else
+    call_exit.arguments().push_back(from_integer(0, arg_type));
+  call_exit.add_source_location() = symbol.location;
+  call_exit.function().add_source_location() = symbol.location;
+  init_code.add(std::move(call_exit));
+
   // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
 
   record_function_outputs(symbol, init_code, symbol_table);

src/ansi-c/ansi_c_internal_additions.cpp

@@ -186,6 +186,9 @@ void ansi_c_internal_additions(std::string &code)
       id2string(rounding_mode_identifier()) + '='+
       std::to_string(config.ansi_c.rounding_mode)+";\n"
 
+    // atexit
+    "void exit(int);\n"
+
     // pipes, write, read, close
     "struct " CPROVER_PREFIX "pipet {\n"
     "  _Bool widowed;\n"

src/ansi-c/library/stdlib.c

@@ -32,9 +32,20 @@ inline long long int __builtin_llabs(long long int i) { return __CPROVER_llabs(i
 
 #undef exit
 
+__CPROVER_thread_local void (*__CPROVER_atexit_table[32])(void);
+__CPROVER_thread_local int __CPROVER_atexit_table_use = 0;
+
 inline void exit(int status)
 {
+__CPROVER_HIDE:;
   (void)status;
+
+  while(__CPROVER_atexit_table_use > 0)
+  {
+    --__CPROVER_atexit_table_use;
+    __CPROVER_atexit_table[__CPROVER_atexit_table_use]();
+  }
+
   __CPROVER_assume(0);
 #ifdef LIBRARY_CHECK
   __builtin_unreachable();
@@ -604,3 +615,28 @@ __CPROVER_HIDE:;
   __CPROVER_assume(result >= 0);
   return result;
 }
+
+/* FUNCTION: atexit */
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+#ifndef LIBRARY_CHECK
+__CPROVER_thread_local void (*__CPROVER_atexit_table[32])(void);
+__CPROVER_thread_local int __CPROVER_atexit_table_use = 0;
+#endif
+
+int atexit(void (*function)(void))
+{
+__CPROVER_HIDE:;
+  if(__CPROVER_atexit_table_use >= 32)
+  {
+    errno = ENOMEM;
+    return -1;
+  }
+
+  __CPROVER_atexit_table[__CPROVER_atexit_table_use++] = function;
+  return 0;
+}

src/cpp/cpp_internal_additions.cpp

@@ -89,6 +89,9 @@ void cpp_internal_additions(std::ostream &out)
   out << "int " << rounding_mode_identifier() << " = "
       << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
 
+  // atexit
+  out << "void exit(int);" << '\n';
+
   // pipes, write, read, close
   out << "struct " CPROVER_PREFIX "pipet {\n"
       << "  bool widowed;\n"

src/linking/remove_internal_symbols.cpp

@@ -127,6 +127,7 @@ void remove_internal_symbols(
   special.insert("__placement_new_array");
   special.insert("__delete");
   special.insert("__delete_array");
+  special.insert("exit");
 
   for(symbol_tablet::symbolst::const_iterator
       it=symbol_table.symbols.begin();