Library functions: mark them as compiled

When adding library functions to the goto model we no longer need their
function bodies as values in the symbol table. Marking them as
"compiled" will make sure we don't re-convert them in any subsequent run
(e.g., running cbmc after goto-instrument). Doing so would undo any
application of "drop-unused-functions." This was most notable with
contracts/dynamic frames, where we ended up reporting thousands of
properties as "SUCCESS" in library functions that were never actually
called. For some contracts examples this now reduces the number of
properties reported from over a thousand to tens of properties.

Author: tautschnig

regression/contracts-dfcc/chain.sh

@@ -58,5 +58,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}${dfcc_suffix}-mod.c"
 fi
+if ! echo "${args_cbmc}" | grep -q -- --function ; then
+  $goto_instrument --drop-unused-functions "${name}${dfcc_suffix}-mod.gb" "${name}${dfcc_suffix}-mod.gb"
+fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
 $cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}

regression/contracts/chain.sh

@@ -41,5 +41,8 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}-mod.c"
 fi
+if ! echo "${args_cbmc}" | grep -q -- --function ; then
+  $goto_instrument --drop-unused-functions "${name}-mod.gb" "${name}-mod.gb"
+fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
 $cbmc "${name}-mod.gb" ${args_cbmc}

src/ansi-c/goto-conversion/link_to_library.cpp

@@ -41,26 +41,31 @@ add_one_function(
   // convert to CFG
   if(
     library_model.symbol_table.symbols.find(missing_function) !=
-    library_model.symbol_table.symbols.end())
+      library_model.symbol_table.symbols.end() &&
+    library_model.symbol_table.lookup_ref(missing_function).value.is_not_nil())
   {
     goto_convert(
       missing_function,
       library_model.symbol_table,
       library_model.goto_functions,
       message_handler);
+    library_model.symbol_table.get_writeable_ref(missing_function)
+      .set_compiled();
   }
   // We might need a function that's outside our own library, but brought in via
   // some header file included by the library. Those functions already exist in
   // goto_model.symbol_table, but haven't been converted just yet.
   else if(
     goto_model.symbol_table.symbols.find(missing_function) !=
-    goto_model.symbol_table.symbols.end())
+      goto_model.symbol_table.symbols.end() &&
+    goto_model.symbol_table.lookup_ref(missing_function).value.is_not_nil())
   {
     goto_convert(
       missing_function,
       goto_model.symbol_table,
       library_model.goto_functions,
       message_handler);
+    goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled();
   }
 
   // check whether additional initialization may be required

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

@@ -326,6 +326,7 @@ void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
   {
     goto_convert(
       id, goto_model.symbol_table, goto_model.goto_functions, message_handler);
+    goto_model.symbol_table.get_writeable_ref(id).set_compiled();
   }
 
   // check that all symbols have a goto_implementation