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.

Add `assert(false)` bodies for front-end functions
`__CPROVER_assignable`, `__CPROVER_object_whole`,
`__CPROVER_object_from`, `__CPROVER_object_upto`
to make the analysis fail when they are used
outside of contract clauses and are hence not
remapped to their library implementation.

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/cprover-assignable-fail/test.desc

@@ -5,7 +5,10 @@ CALL __CPROVER_object_whole
 CALL __CPROVER_object_upto
 CALL __CPROVER_object_from
 CALL __CPROVER_assignable
-^\[__CPROVER_object_(assignable|from|upto|whole).*.\d+\] Built-in __CPROVER_object_(assignable|from|upto|whole) should not be called after contracts transformation: FAILURE$
+^\[__CPROVER_assignable.assertion.\d+\].*undefined function should be unreachable: FAILURE$
+^\[__CPROVER_object_from.assertion.\d+\].*undefined function should be unreachable: FAILURE$
+^\[__CPROVER_object_upto.assertion.\d+\].*undefined function should be unreachable: FAILURE$
+^\[__CPROVER_object_whole.assertion.\d+\].*undefined function should be unreachable: FAILURE$
 ^\[my_write_set.assertion.\d+\] .* target null or writable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
@@ -18,5 +21,7 @@ This test checks that:
   __CPROVER_object_upto are supported;
 - GOTO conversion preserves calls to __CPROVER_object_whole,
   __CPROVER_object_upto, __CPROVER_object_from;
+- reachability assertions are inserted in front-end functions and allow to
+  detect when front-end functions are used outside of contracts clauses;
 - GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable;
 - user-defined checks embedded in `my_write_set` persist after conversion.

regression/contracts-dfcc/cprover-assignable-pass/test.desc

@@ -5,7 +5,10 @@ CALL __CPROVER_object_whole
 CALL __CPROVER_object_upto
 CALL __CPROVER_object_from
 CALL __CPROVER_assignable
-^\[__CPROVER_object_(assignable|from|upto|whole).*.\d+\] Built-in __CPROVER_object_(assignable|from|upto|whole) should not be called after contracts transformation: FAILURE$
+^\[__CPROVER_assignable.assertion.\d+\].*undefined function should be unreachable: FAILURE$
+^\[__CPROVER_object_from.assertion.\d+\].*undefined function should be unreachable: FAILURE$
+^\[__CPROVER_object_upto.assertion.\d+\].*undefined function should be unreachable: FAILURE$
+^\[__CPROVER_object_whole.assertion.\d+\].*undefined function should be unreachable: FAILURE$
 ^\[my_write_set.assertion.\d+\] .* target null or writable: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
@@ -14,8 +17,11 @@ CALL __CPROVER_assignable
 CALL __CPROVER_typed_target
 --
 This test checks that:
-- built-in __CPROVER_assignable_t functions are supported;
+- built-in __CPROVER_assignable, __CPROVER_object_from, __CPROVER_object_upto,
+  __CPROVER_object_whole functions are supported in the front-end;
 - GOTO conversion preserves calls to __CPROVER_object_whole,
   __CPROVER_object_upto, __CPROVER_object_from;
+- reachability assertions are inserted in front-end functions and allow to
+  detect when front-end functions are used outside of contracts clauses;
 - GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable;
 - user-defined checks embedded in `my_write_set` persist after conversion.

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,9 +22,11 @@ Author: Remi Delmas, delmarsd@amazon.com
 #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"
@@ -33,6 +35,8 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include "dfcc_obeys_contract.h"
 #include "dfcc_utils.h"
 
+#include <memory>
+
 std::set<irep_idt> dfcc_instrumentt::function_cache;
 
 dfcc_instrumentt::dfcc_instrumentt(
@@ -340,10 +344,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

@@ -23,7 +23,9 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include <goto-programs/goto_model.h>
 
 #include <ansi-c/c_expr.h>
+#include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
+#include <goto-instrument/generate_function_bodies.h>
 #include <goto-instrument/unwind.h>
 #include <goto-instrument/unwindset.h>
 #include <linking/static_lifetime_init.h>
@@ -488,32 +490,21 @@ void dfcc_libraryt::fix_malloc_free_calls()
 
 void dfcc_libraryt::inhibit_front_end_builtins()
 {
+  // not using assume-false in order not to hinder coverage
+  std::string options = "assert-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);
   for(const auto &it : dfcc_hook)
   {
-    const auto &fid = it.first;
-    if(goto_model.symbol_table.has_symbol(fid))
+    const auto &function_id = it.first;
+    if(goto_model.symbol_table.has_symbol(function_id))
     {
-      // make sure parameter symbols exist
-      utils.fix_parameters_symbols(fid);
-
-      // create fatal assertion code block as body
-      source_locationt sl;
-      sl.set_function(fid);
-      sl.set_file("<built-in-additions>");
-      sl.set_property_class("sanity_check");
-      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);
+      auto &goto_function =
+        goto_model.goto_functions.function_map.at(function_id);
+
+      generate_function_bodies->generate_function_body(
+        goto_function, goto_model.symbol_table, function_id);
     }
   }
 }

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

@@ -239,8 +239,9 @@ class dfcc_libraryt
   /// __CPROVER_object_from
   /// __CPROVER_assignable
   /// __CPROVER_freeable
-  /// To make sure they cannot be used in a proof unexpectedly
-  /// without causing verification errors.
+  /// An error will be triggered in case calls to these functions occur outside
+  /// of a contrat clause and were hence not mapped to their library
+  /// implementation.
   void inhibit_front_end_builtins();
 
   /// Sets the given hide flag on all instructions of all library functions