CONTRACTS: insert reachability canary asssertions

When a GOTO function has no body, insert a canary assertion
to make the analysis fail in case the function is reachable.

Author: Remi Delmas

regression/contracts-dfcc/assigns_replace_02/main.c

@@ -1,6 +1,6 @@
 #include <assert.h>
 
-void foo(int *x, int *y) __CPROVER_assigns(*x)
+void foo(int *x) __CPROVER_assigns(*x)
 {
   *x = 7;
 }
@@ -9,7 +9,7 @@ int main()
 {
   int n;
   int m = 4;
-  bar(&n);
+  foo(&n);
   assert(m == 4);
 
   return 0;

regression/contracts-dfcc/missing-function-body/main.c

@@ -0,0 +1,13 @@
+int foo(int);
+
+int bar(int i) __CPROVER_requires(i > 0)
+  __CPROVER_ensures(__CPROVER_return_value > 0)
+{
+  return foo(i);
+}
+
+int main()
+{
+  int i;
+  bar(i);
+}

regression/contracts-dfcc/missing-function-body/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract bar
+^\[foo.assertion.\d+\] line 1 undefined function should be unreachable: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks that functions without bodies result in analysis failures.

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

@@ -22,16 +22,20 @@ Author: Remi Delmas, [email protected]
 #include <goto-programs/remove_skip.h>
 
 #include <ansi-c/c_expr.h>
+#include <ansi-c/c_object_factory_parameters.h>
 #include <goto-instrument/contracts/cfg_info.h>
 #include <goto-instrument/contracts/contracts.h>
 #include <goto-instrument/contracts/utils.h>
+#include <goto-instrument/generate_function_bodies.h>
 #include <langapi/language_util.h>
 
 #include "dfcc_is_freeable.h"
 #include "dfcc_is_fresh.h"
 #include "dfcc_library.h"
 #include "dfcc_utils.h"
 
+#include <memory>
+
 std::set<irep_idt> dfcc_instrumentt::function_cache;
 
 dfcc_instrumentt::dfcc_instrumentt(
@@ -323,10 +327,13 @@ 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;
+    // generate a default body `assert(false);assume(false);`
+    std::string options = "assert-false-assume-false";
+    c_object_factory_parameterst object_factory_params;
+    auto generate_function_bodies = generate_function_bodies_factory(
+      options, object_factory_params, goto_model.symbol_table, message_handler);
+    generate_function_bodies->generate_function_body(
+      goto_function, goto_model.symbol_table, function_id);
     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,