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

goto-instrument now errors out when attempting to enforce or replace
the contract of an unknown function. Added missing error checking in
`goto_instrument_parse_optionst::doit()` on return of `replace_calls`
and `enforce_contracts`.

Author: Remi Delmas

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

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

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

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract goo
+^Invariant check failed$
+^Condition: Precondition$
+^Reason: all_functions_found\(to_enforce\)$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+Checks that attempting to enforce the contract of an unknown function creates
+an error.

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

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

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

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-call-with-contract goo
+^Invariant check failed$
+^Condition: Precondition$
+^Reason: all_functions_found\(to_replace\)$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+Checks that attempting call replacement with an unknown function creates an
+error.

src/goto-instrument/contracts/contracts.cpp

@@ -1536,8 +1536,29 @@ void code_contractst::add_contract_check(
   dest.destructive_insert(dest.instructions.begin(), check);
 }
 
+bool code_contractst::all_functions_found(
+  const std::set<std::string> &functions) const
+{
+  bool all_found = true;
+  for(const auto &function : functions)
+  {
+    if(
+      goto_functions.function_map.find(function) ==
+      goto_functions.function_map.end())
+    {
+      all_found = false;
+      log.error() << "Function '" << function << "' not found" << messaget::eom;
+    }
+  }
+  return all_found;
+}
+
 bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
 {
+  PRECONDITION_WITH_DIAGNOSTICS(
+    all_functions_found(to_replace),
+    "Functions to replace with contracts must exist in the GOTO program");
+
   if(to_replace.empty())
     return false;
 
@@ -1587,25 +1608,17 @@ void code_contractst::apply_loop_contracts()
 
 bool code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
 {
+  PRECONDITION_WITH_DIAGNOSTICS(
+    all_functions_found(to_enforce),
+    "Functions to enforce contracts for must exist in the GOTO program");
+
   if(to_enforce.empty())
     return false;
 
   bool fail = false;
 
   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;
-    }
+    fail |= enforce_contract(function);
 
-    if(!fail)
-      fail = enforce_contract(function);
-  }
   return fail;
 }

src/goto-instrument/contracts/contracts.h

@@ -62,8 +62,14 @@ class code_contractst
   {
   }
 
-  /// \brief Replace all calls to each function in the list with that function's
-  ///        contract
+  /// True iff all functions in `functions` are found in the GOTO program or
+  // `functions` is empty.
+  bool 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
+  ///
+  /// All functions in `to_replace` must be found in the GOTO programs.
   ///
   /// Use this function when proving code that calls into an expensive function,
   /// `F`. You can write a contract for F using __CPROVER_requires and
@@ -75,11 +81,13 @@ class code_contractst
   /// it using `cbmc --function F`.
   ///
   /// \return `true` on failure, `false` otherwise
-  bool replace_calls(const std::set<std::string> &);
+  bool replace_calls(const std::set<std::string> &to_replace);
 
   /// \brief Turn requires & ensures into assumptions and assertions for each of
   ///        the named functions
   ///
+  /// All functions in `to_enforce` must be found in the GOTO programs.
+  ///
   /// 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
@@ -93,7 +101,7 @@ class code_contractst
   /// then asserts `CF`'s `ensures` clause.
   ///
   /// \return `true` on failure, `false` otherwise
-  bool enforce_contracts(const std::set<std::string> &functions);
+  bool enforce_contracts(const std::set<std::string> &to_enforce);
 
   void apply_loop_contracts();
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1150,8 +1150,18 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     // first replacement then enforcement. We rely on contract replacement
     // and inlining of sub-function calls to properly annotate all
     // assignments.
-    contracts.replace_calls(to_replace);
-    contracts.enforce_contracts(to_enforce);
+    if(contracts.replace_calls(to_replace))
+    {
+      log.error() << FLAG_REPLACE_CALL << " failed, aborting." << messaget::eom;
+      throw 0;
+    }
+
+    if(contracts.enforce_contracts(to_enforce))
+    {
+      log.error() << FLAG_ENFORCE_CONTRACT << " failed, aborting."
+                  << messaget::eom;
+      throw 0;
+    }
 
     if(cmdline.isset(FLAG_LOOP_CONTRACTS))
       contracts.apply_loop_contracts();