Merge pull request #6733 from remi-delmas-3000/contracts-replace-unknown-fix

CONTRACTS: Error-out on unknown functions (replace/enforce).

Author: remi-delmas-3000

regression/contracts/enforce-replace-unknown-function/enforce.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract goo
+^Function 'goo' was not found in the GOTO program.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+Checks that attempting to enforce the contract of an unknown function creates
+an error.

regression/contracts/enforce-replace-unknown-function/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/contracts/enforce-replace-unknown-function/replace.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--replace-call-with-contract goo
+^Function 'goo' was not found in the GOTO program.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+Checks that attempting call replacement with an unknown function creates an
+error.

src/goto-instrument/contracts/contracts.cpp

@@ -13,23 +13,8 @@ Date: February 2016
 
 #include "contracts.h"
 
-#include <algorithm>
-#include <map>
-
-#include <analyses/local_bitvector_analysis.h>
-#include <analyses/local_may_alias.h>
-
-#include <ansi-c/c_expr.h>
-
-#include <goto-instrument/havoc_utils.h>
-
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/goto_program.h>
-#include <goto-programs/remove_skip.h>
-
-#include <langapi/language_util.h>
-
 #include <util/c_types.h>
+#include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
 #include <util/format_expr.h>
@@ -43,11 +28,24 @@ Date: February 2016
 #include <util/replace_symbol.h>
 #include <util/std_code.h>
 
+#include <goto-programs/goto_inline.h>
+#include <goto-programs/goto_program.h>
+#include <goto-programs/remove_skip.h>
+
+#include <analyses/local_bitvector_analysis.h>
+#include <analyses/local_may_alias.h>
+#include <ansi-c/c_expr.h>
+#include <goto-instrument/havoc_utils.h>
+#include <langapi/language_util.h>
+
 #include "havoc_assigns_clause_targets.h"
 #include "instrument_spec_assigns.h"
 #include "memory_predicates.h"
 #include "utils.h"
 
+#include <algorithm>
+#include <map>
+
 /// Decorator for \ref message_handlert that keeps track of warnings
 /// occuring when inlining a function.
 ///
@@ -729,7 +727,7 @@ code_contractst::create_ensures_instruction(
   return std::make_pair(std::move(ensures_program), std::move(history));
 }
 
-bool code_contractst::apply_function_contract(
+void code_contractst::apply_function_contract(
   const irep_idt &function,
   const source_locationt &location,
   goto_programt &function_body,
@@ -932,7 +930,6 @@ bool code_contractst::apply_function_contract(
 
   // Add this function to the set of replaced functions.
   summarized.insert(target_function);
-  return false;
 }
 
 void code_contractst::apply_loop_contract(
@@ -1225,17 +1222,14 @@ goto_functionst &code_contractst::get_goto_functions()
   return goto_functions;
 }
 
-bool code_contractst::check_frame_conditions_function(const irep_idt &function)
+void code_contractst::check_frame_conditions_function(const irep_idt &function)
 {
   // Get the function object before instrumentation.
   auto function_obj = goto_functions.function_map.find(function);
-  if(function_obj == goto_functions.function_map.end())
-  {
-    log.error() << "Could not find function '" << function
-                << "' in goto-program; not enforcing contracts."
-                << messaget::eom;
-    return true;
-  }
+
+  INVARIANT(
+    function_obj != goto_functions.function_map.end(),
+    "Function '" + id2string(function) + "'must exist in the goto program");
 
   const auto &goto_function = function_obj->second;
   auto &function_body = function_obj->second.body;
@@ -1316,11 +1310,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     function_body.instructions.end(),
     skip_function_paramst::YES,
     cfg_info_opt);
-
-  return false;
 }
 
-bool code_contractst::enforce_contract(const irep_idt &function)
+void code_contractst::enforce_contract(const irep_idt &function)
 {
   // Add statements to the source function
   // to ensure assigns clause is respected.
@@ -1333,13 +1325,9 @@ bool code_contractst::enforce_contract(const irep_idt &function)
   const irep_idt original(function);
 
   auto old_function = goto_functions.function_map.find(original);
-  if(old_function == goto_functions.function_map.end())
-  {
-    log.error() << "Could not find function '" << function
-                << "' in goto-program; not enforcing contracts."
-                << messaget::eom;
-    return true;
-  }
+  INVARIANT(
+    old_function != goto_functions.function_map.end(),
+    "Function to replace must exist in the program.");
 
   std::swap(goto_functions.function_map[mangled], old_function->second);
   goto_functions.function_map.erase(old_function);
@@ -1379,8 +1367,6 @@ bool code_contractst::enforce_contract(const irep_idt &function)
   wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
   wrapper.body.add(goto_programt::make_end_function(sl));
   add_contract_check(original, mangled, wrapper.body);
-
-  return false;
 }
 
 void code_contractst::add_contract_check(
@@ -1536,12 +1522,29 @@ void code_contractst::add_contract_check(
   dest.destructive_insert(dest.instructions.begin(), check);
 }
 
-bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
+void code_contractst::check_all_functions_found(
+  const std::set<std::string> &functions) const
+{
+  for(const auto &function : functions)
+  {
+    if(
+      goto_functions.function_map.find(function) ==
+      goto_functions.function_map.end())
+    {
+      throw invalid_input_exceptiont(
+        "Function '" + function + "' was not found in the GOTO program.");
+    }
+  }
+}
+
+void code_contractst::replace_calls(const std::set<std::string> &to_replace)
 {
   if(to_replace.empty())
-    return false;
+    return;
 
-  bool fail = false;
+  log.status() << "Replacing function calls with contracts" << messaget::eom;
+
+  check_all_functions_found(to_replace);
 
   for(auto &goto_function : goto_functions.function_map)
   {
@@ -1559,7 +1562,7 @@ bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
         if(found == to_replace.end())
           continue;
 
-        fail |= apply_function_contract(
+        apply_function_contract(
           goto_function.first,
           ins->source_location(),
           goto_function.second.body,
@@ -1568,15 +1571,10 @@ bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
     }
   }
 
-  if(fail)
-    return true;
-
   for(auto &goto_function : goto_functions.function_map)
     remove_skip(goto_function.second.body);
 
   goto_functions.update();
-
-  return false;
 }
 
 void code_contractst::apply_loop_contracts()
@@ -1585,27 +1583,15 @@ void code_contractst::apply_loop_contracts()
     apply_loop_contract(goto_function.first, goto_function.second);
 }
 
-bool code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
+void code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
 {
   if(to_enforce.empty())
-    return false;
+    return;
 
-  bool fail = false;
+  log.status() << "Enforcing contracts" << messaget ::eom;
 
-  for(const auto &function : to_enforce)
-  {
-    auto goto_function = goto_functions.function_map.find(function);
-    if(goto_function == goto_functions.function_map.end())
-    {
-      fail = true;
-      log.error() << "Could not find function '" << function
-                  << "' in goto-program; not enforcing contracts."
-                  << messaget::eom;
-      continue;
-    }
+  check_all_functions_found(to_enforce);
 
-    if(!fail)
-      fail = enforce_contract(function);
-  }
-  return fail;
+  for(const auto &function : to_enforce)
+    enforce_contract(function);
 }

src/goto-instrument/contracts/contracts.h

@@ -62,8 +62,13 @@ class code_contractst
   {
   }
 
-  /// \brief Replace all calls to each function in the list with that function's
-  ///        contract
+  /// Throws an exception if some function `functions` is found in the program.
+  void check_all_functions_found(const std::set<std::string> &functions) const;
+
+  /// \brief Replace all calls to each function in the `to_replace` set
+  /// with that function's contract
+  ///
+  /// Throws an exception if some `to_replace` functions are not found.
   ///
   /// Use this function when proving code that calls into an expensive function,
   /// `F`. You can write a contract for F using __CPROVER_requires and
@@ -73,13 +78,13 @@ class code_contractst
   /// actually abides by its `ensures` and `requires` clauses, you should
   /// separately call `code_constractst::enforce_contracts()` on `F` and verify
   /// it using `cbmc --function F`.
-  ///
-  /// \return `true` on failure, `false` otherwise
-  bool replace_calls(const std::set<std::string> &);
+  void replace_calls(const std::set<std::string> &to_replace);
 
   /// \brief Turn requires & ensures into assumptions and assertions for each of
   ///        the named functions
   ///
+  /// Throws an exception if some `to_enforce` functions are not found.
+  ///
   /// Use this function to prove the correctness of a function F independently
   /// of its calling context. If you have proved that F is correct, then you can
   /// soundly replace all calls to F with F's contract using the
@@ -92,8 +97,7 @@ class code_contractst
   /// function called `F` that assumes `CF`'s `requires` clause, calls `CF`, and
   /// then asserts `CF`'s `ensures` clause.
   ///
-  /// \return `true` on failure, `false` otherwise
-  bool enforce_contracts(const std::set<std::string> &functions);
+  void enforce_contracts(const std::set<std::string> &to_enforce);
 
   void apply_loop_contracts();
 
@@ -125,10 +129,10 @@ class code_contractst
   std::unordered_set<irep_idt> summarized;
 
   /// \brief Enforce contract of a single function
-  bool enforce_contract(const irep_idt &function);
+  void enforce_contract(const irep_idt &function);
 
   /// Instrument functions to check frame conditions.
-  bool check_frame_conditions_function(const irep_idt &function);
+  void check_frame_conditions_function(const irep_idt &function);
 
   /// Apply loop contracts, whenever available, to all loops in `function`.
   /// Loop invariants, loop variants, and loop assigns clauses.
@@ -139,7 +143,7 @@ class code_contractst
   /// Replaces function calls with assertions based on requires clauses,
   /// non-deterministic assignments for the write set, and assumptions
   /// based on ensures clauses.
-  bool apply_function_contract(
+  void apply_function_contract(
     const irep_idt &function,
     const source_locationt &location,
     goto_programt &function_body,