CONTRACTS: insert reachability canary asssertions

When a GOTO function has no body, insert a canary assertion
to make sure the function is indeed unreachable.

Author: Remi Delmas

regression/contracts-dfcc/assigns_replace_02/main.c

@@ -9,7 +9,7 @@ int main()
 {
   int n;
   int m = 4;
-  bar(&n);
+  foo(&n);
   assert(m == 4);
 
   return 0;

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

@@ -323,10 +323,20 @@ void dfcc_instrumentt::instrument_function_body(
 
   if(!goto_function.body_available())
   {
-    log.warning() << "DFCC instrumentation: '" << function_id
-                  << "' body is not available. Results may be unsound if the "
-                     "actual function has side effects."
-                  << messaget::eom;
+    // we interpret this as "the function should be unreachable"
+    // create fatal assertion code block as body
+    const auto &function_location =
+      utils.get_function_symbol(function_id).location;
+    source_locationt sl;
+    sl.set_property_class("reachability");
+    sl.set_function(function_id);
+    sl.set_line(0);
+    sl.set_column(0);
+    sl.set_file(function_location.get_file());
+    sl.set_working_directory(function_location.get_working_directory());
+    sl.set_comment(
+      "Function " + id2string(function_id) + " should not be reachable");
+    utils.gen_fatal_assertion_body(function_id, sl);
     return;
   }
 

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

@@ -469,9 +469,6 @@ void dfcc_libraryt::inhibit_front_end_builtins()
     const auto &fid = it.first;
     if(goto_model.symbol_table.has_symbol(fid))
     {
-      // make sure parameter symbols exist
-      utils.fix_parameters_symbols(fid);
-
       // create fatal assertion code block as body
       source_locationt sl;
       sl.set_function(fid);
@@ -480,16 +477,7 @@ void dfcc_libraryt::inhibit_front_end_builtins()
       sl.set_comment(
         "Built-in " + id2string(fid) +
         " should not be called after contracts transformation");
-      auto block = create_fatal_assertion(false_exprt(), sl);
-      auto &symbol = goto_model.symbol_table.get_writeable_ref(fid);
-      symbol.value = block;
-
-      // convert the function
-      goto_convert(
-        fid,
-        goto_model.symbol_table,
-        goto_model.goto_functions,
-        message_handler);
+      utils.gen_fatal_assertion_body(fid, sl);
     }
   }
 }

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

@@ -42,6 +42,28 @@ dfcc_utilst::dfcc_utilst(
 {
 }
 
+void dfcc_utilst::gen_fatal_assertion_body(
+  const irep_idt &function_id,
+  const source_locationt &source_location)
+{
+  PRECONDITION(goto_model.symbol_table.has_symbol(function_id));
+
+  // make sure parameter symbols exist
+  fix_parameters_symbols(function_id);
+
+  // create fatal assertion code block as body
+  auto block = create_fatal_assertion(false_exprt(), source_location);
+  auto &symbol = goto_model.symbol_table.get_writeable_ref(function_id);
+  symbol.value = block;
+
+  // convert the function
+  goto_convert(
+    function_id,
+    goto_model.symbol_table,
+    goto_model.goto_functions,
+    message_handler);
+}
+
 const bool dfcc_utilst::symbol_exists(
   const irep_idt &name,
   const bool require_has_code_type,

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h

@@ -35,6 +35,15 @@ class dfcc_utilst
   namespacet ns;
 
 public:
+  /// \brief Genrate a body `assert(false); assume(false);`
+  /// for the given \p function_id.
+  /// \param function_id function to generate the body for
+  /// \param source_location source location to use for the assertion.
+  /// Must define the property class, comment for the assertion, etc.
+  void gen_fatal_assertion_body(
+    const irep_idt &function_id,
+    const source_locationt &source_location);
+
   /// Returns true iff the given symbol exists and satisfies requirements.
   const bool symbol_exists(
     const irep_idt &function_id,