DFCC instrumentation: skip unused functions

regression/contracts-dfcc/skip_unused_instrumentation/main.c

@@ -0,0 +1,10 @@
+// Using a forward declaration rather than including netdb.h to make sure we do
+// not have the compiled body of functions from header files available right
+// away.
+struct hostent;
+struct hostent *gethostbyname(const char *name);
+
+int main()
+{
+  (void)gethostbyname("x");
+}

regression/contracts-dfcc/skip_unused_instrumentation/test.desc

@@ -0,0 +1,31 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that functions brought in from header files when loading
+entries from the model library are not subject to instrumentation (when those
+functions are never used). Else we end up with invariant failures like:
+[...]
+Instrumenting '__bswap_16'
+--- begin invariant violation report ---
+Invariant check failed
+File: /src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp:329 function: instrument_function
+Condition: Precondition
+Reason: found != goto_model.goto_functions.function_map.end()
+Backtrace:
+build/bin/goto-instrument(+0xbfe182) [0x649c3d22b182]
+[...]
+/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x78dc2f029d90]
+/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x78dc2f029e40]
+build/bin/goto-instrument(+0x363cb5) [0x649c3c990cb5]
+
+Diagnostics:
+<< EXTRA DIAGNOSTICS >>
+Function '__bswap_16' must exist in the model.
+<< END EXTRA DIAGNOSTICS >>
+
+--- end invariant violation report ---

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -38,6 +38,7 @@
 #include <ansi-c/goto-conversion/link_to_library.h>
 #include <goto-instrument/contracts/cfg_info.h>
 #include <goto-instrument/contracts/utils.h>
+#include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/nondet_static.h>
 #include <langapi/language.h>
 #include <langapi/language_file.h>
@@ -257,6 +258,12 @@
   std::set<irep_idt> &contract_symbols,
   std::set<irep_idt> &other_symbols)
 {
+  std::set<irep_idt> called_functions;
+  find_used_functions(
+    goto_functionst::entry_point(),
+    goto_model.goto_functions,
+    called_functions);
+
   // collect contract and other symbols
   for(auto &entry : goto_model.symbol_table)
   {
@@ -272,7 +279,7 @@
     {
       contract_symbols.insert(sym_name);
     }
-    else
+    else if(called_functions.find(sym_name) != called_functions.end())
     {
       // it is not a contract
       other_symbols.insert(sym_name);
@@ -486,21 +493,6 @@
 
   library.inhibit_front_end_builtins();
 
-  // TODO implement a means to inhibit unreachable functions (possibly via the
-  // code that implements drop-unused-functions followed by
-  // generate-function-bodies):
-  // Traverse the call tree from the given entry point to identify
-  // functions symbols that are effectively called in the model,
-  // Then goes over all functions of the model and turns the bodies of all
-  // functions that are not in the used function set into:
-  //  ```c
-  //  assert(false, "function identified as unreachable");
-  //  assume(false);
-  //  ```
-  // That way, if the analysis mistakenly pruned some functions, assertions
-  // will be violated and the analysis will fail.
-  // TODO: add a command line flag to tell the instrumentation to not prune
-  // a function.
   goto_model.goto_functions.update();
 
   remove_skip(goto_model);
@@ -510,11 +502,25 @@
 
   // This can prune too many functions if function pointers have not been
   // yet been removed or if the entry point is not defined.
-  // Another solution would be to rewrite the bodies of functions that seem to
-  // be unreachable into assert(false);assume(false)
+  // TODO: add a command line flag to tell the instrumentation to not prune
+  // a function.
   remove_unused_functions(goto_model, message_handler);
   goto_model.goto_functions.update();
 
+  // generate assert(0); assume(0); function bodies for all functions missing an
+  // implementation (other than ones containing __CPROVER in their name)
+  auto generate_implementation = generate_function_bodies_factory(
+    "assert-false-assume-false",
+    c_object_factory_parameterst{},
+    goto_model.symbol_table,
+    message_handler);
+  generate_function_bodies(
+    std::regex("(?!" CPROVER_PREFIX ").*"),
+    *generate_implementation,
+    goto_model,
+    message_handler);
+  goto_model.goto_functions.update();
+
   reinitialize_model();
 }