CONTRACTS: Handle all 4 inlining warning types in inlining_decoratort

regression/contracts/function-calls-03-1/test-enf-f1.desc

@@ -2,10 +2,8 @@ CORE
 main.c
 --enforce-contract f1 _ --unwind 20 --unwinding-assertions
 ^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$
-^Invariant check failed$
-^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
-^Reason: Recursive functions found during inlining$
-^EXIT=(127|134|137)$
+^Recursive call to 'f2' during inlining$
+^EXIT=6$
 ^SIGNAL=0$
 --
 --

regression/contracts/function-calls-03-1/test-enf-f2.desc

@@ -1,11 +1,9 @@
 CORE
 main.c
 --enforce-contract f2 _ --unwind 20 --unwinding-assertions
-^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$
-^Invariant check failed$
-^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
-^Reason: Recursive functions found during inlining$
-^EXIT=(127|134|137)$
+^file main.c line 13 function f2: recursion is ignored on call to 'f2'$
+^Recursive call to 'f2' during inlining$
+^EXIT=6$
 ^SIGNAL=0$
 --
 --

regression/contracts/function-calls-04-1/test-enf-f1.desc

@@ -1,11 +1,9 @@
 CORE
 main.c
 --enforce-contract f1 _ --unwind 20 --unwinding-assertions
-^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
-^Invariant check failed$
-^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
-^Reason: Recursive functions found during inlining$
-^EXIT=(127|134|137)$
+^file main.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
+^Recursive call to 'f2_out' during inlining$
+^EXIT=6$
 ^SIGNAL=0$
 --
 --

regression/contracts/function-calls-04-1/test-enf-f2_in.desc

@@ -1,11 +1,9 @@
 CORE
 main.c
 --enforce-contract f2_in _ --unwind 20 --unwinding-assertions
-^file main\.c line 13 function f2_out: recursion is ignored on call to 'f2_in'$
-^Invariant check failed$
-^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
-^Reason: Recursive functions found during inlining$
-^EXIT=(127|134|137)$
+^file main.c line 13 function f2_out: recursion is ignored on call to 'f2_in'$
+^Recursive call to 'f2_in' during inlining$
+^EXIT=6$
 ^SIGNAL=0$
 --
 --

regression/contracts/function-calls-04-1/test-enf-f2_out.desc

@@ -1,11 +1,9 @@
 CORE
 main.c
 --enforce-contract f2_out _ --unwind 20 --unwinding-assertions
-^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
-^Invariant check failed$
-^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
-^Reason: Recursive functions found during inlining$
-^EXIT=(127|134|137)$
+^file main.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
+^Recursive call to 'f2_out' during inlining$
+^EXIT=6$
 ^SIGNAL=0$
 --
 --

regression/contracts/function-calls-recursive-01/test.desc

@@ -1,11 +1,9 @@
 CORE
 main.c
 --enforce-contract sum _ --trace
-^file main\.c line 6 function sum_rec: recursion is ignored on call to 'sum_rec'$
-^Invariant check failed$
-^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
-^Reason: Recursive functions found during inlining$
-^EXIT=(127|134|137)$
+^file main.c line 6 function sum_rec: recursion is ignored on call to 'sum_rec'$
+^Recursive call to 'sum_rec' during inlining$
+^EXIT=6$
 ^SIGNAL=0$
 --
 --

src/goto-instrument/Makefile

@@ -21,6 +21,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/instrument_spec_assigns.cpp \
       contracts/memory_predicates.cpp \
       contracts/utils.cpp \
+      contracts/inlining_decorator.cpp \
       concurrency.cpp \
       count_eloc.cpp \
       cover.cpp \

src/goto-instrument/contracts/contracts.cpp

@@ -40,100 +40,14 @@ Date: February 2016
 
 #include "cfg_info.h"
 #include "havoc_assigns_clause_targets.h"
+#include "inlining_decorator.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.
-///
-/// It counts the number of :
-/// - recursive functions warnings
-/// - missing functions warnings
-/// - missing function body warnings
-/// - missing function arguments warnings
-class inlining_decoratort : public message_handlert
-{
-private:
-  message_handlert &wrapped;
-  unsigned int recursive_function_warnings_count = 0;
-
-  void parse_message(const std::string &message)
-  {
-    if(message.find("recursion is ignored on call") != std::string::npos)
-      recursive_function_warnings_count++;
-  }
-
-public:
-  explicit inlining_decoratort(message_handlert &_wrapped) : wrapped(_wrapped)
-  {
-  }
-
-  unsigned int get_recursive_function_warnings_count()
-  {
-    return recursive_function_warnings_count;
-  }
-
-  void print(unsigned level, const std::string &message) override
-  {
-    parse_message(message);
-    wrapped.print(level, message);
-  }
-
-  void print(unsigned level, const xmlt &xml) override
-  {
-    wrapped.print(level, xml);
-  }
-
-  void print(unsigned level, const jsont &json) override
-  {
-    wrapped.print(level, json);
-  }
-
-  void print(unsigned level, const structured_datat &data) override
-  {
-    wrapped.print(level, data);
-  }
-
-  void print(
-    unsigned level,
-    const std::string &message,
-    const source_locationt &location) override
-  {
-    parse_message(message);
-    wrapped.print(level, message, location);
-    return;
-  }
-
-  void flush(unsigned i) override
-  {
-    return wrapped.flush(i);
-  }
-
-  void set_verbosity(unsigned _verbosity)
-  {
-    wrapped.set_verbosity(_verbosity);
-  }
-
-  unsigned get_verbosity() const
-  {
-    return wrapped.get_verbosity();
-  }
-
-  std::size_t get_message_count(unsigned level) const
-  {
-    return wrapped.get_message_count(level);
-  }
-
-  std::string command(unsigned i) const override
-  {
-    return wrapped.command(i);
-  }
-};
-
 void code_contractst::check_apply_loop_contracts(
   const irep_idt &function_name,
   goto_functionst::goto_functiont &goto_function,
@@ -1031,7 +945,7 @@ void code_contractst::apply_loop_contract(
     goto_functions, function_name, ns, log.get_message_handler());
 
   INVARIANT(
-    decorated.get_recursive_function_warnings_count() == 0,
+    decorated.get_recursive_call_set().size() == 0,
     "Recursive functions found during inlining");
 
   // restore internal invariants
@@ -1301,9 +1215,7 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
   inlining_decoratort decorated(log.get_message_handler());
   goto_function_inline(goto_functions, function, ns, decorated);
 
-  INVARIANT(
-    decorated.get_recursive_function_warnings_count() == 0,
-    "Recursive functions found during inlining");
+  decorated.throw_on_recursive_calls(log, 0);
 
   // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
   simplify_gotos(function_body, ns);

src/goto-instrument/contracts/inlining_decorator.cpp

@@ -0,0 +1,124 @@
+/*******************************************************************\
+
+Module: Utility functions for code contracts.
+
+Author: Remi Delmas, [email protected]
+
+Date: August 2022
+
+\*******************************************************************/
+
+#include "inlining_decorator.h"
+
+inlining_decoratort::inlining_decoratort(message_handlert &_wrapped)
+  : wrapped(_wrapped),
+    no_body_regex(std::regex(".*no body for function '(.*)'.*")),
+    missing_function_regex(
+      std::regex(".*missing function '(.*)' is ignored.*")),
+    recursive_call_regex(
+      std::regex(".*recursion is ignored on call to '(.*)'.*")),
+    not_enough_arguments_regex(
+      std::regex(".*call to '(.*)': not enough arguments.*"))
+{
+}
+
+void inlining_decoratort::match_no_body_warning(const std::string &message)
+{
+  std::smatch sm;
+  std::regex_match(message, sm, no_body_regex);
+  if(sm.size() == 2)
+    no_body_set.insert(sm.str(1));
+}
+
+void inlining_decoratort::match_missing_function_warning(
+  const std::string &message)
+{
+  std::smatch sm;
+  std::regex_match(message, sm, missing_function_regex);
+  if(sm.size() == 2)
+    missing_function_set.insert(sm.str(1));
+}
+
+void inlining_decoratort::match_recursive_call_warning(
+  const std::string &message)
+{
+  std::smatch sm;
+  std::regex_match(message, sm, recursive_call_regex);
+  if(sm.size() == 2)
+    recursive_call_set.insert(sm.str(1));
+}
+
+void inlining_decoratort::match_not_enough_arguments_warning(
+  const std::string &message)
+{
+  std::smatch sm;
+  std::regex_match(message, sm, not_enough_arguments_regex);
+  if(sm.size() == 2)
+    not_enough_arguments_set.insert(sm.str(1));
+}
+
+void inlining_decoratort::parse_message(const std::string &message)
+{
+  match_no_body_warning(message);
+  match_missing_function_warning(message);
+  match_recursive_call_warning(message);
+  match_not_enough_arguments_warning(message);
+}
+
+void inlining_decoratort::throw_on_no_body(messaget &log, const int error_code)
+{
+  if(no_body_set.size() != 0)
+  {
+    for(auto it : no_body_set)
+    {
+      log.error() << "No body for '" << it << "' during inlining"
+                  << messaget::eom;
+    }
+    throw error_code;
+  }
+}
+
+void inlining_decoratort::throw_on_recursive_calls(
+  messaget &log,
+  const int error_code)
+{
+  if(recursive_call_set.size() != 0)
+  {
+    for(auto it : recursive_call_set)
+    {
+      log.error() << "Recursive call to '" << it << "' during inlining"
+                  << messaget::eom;
+    }
+    throw error_code;
+  }
+}
+
+void inlining_decoratort::throw_on_missing_function(
+  messaget &log,
+  const int error_code)
+{
+  if(missing_function_set.size() != 0)
+  {
+    for(auto it : missing_function_set)
+    {
+      log.error() << "Missing function '" << it << "' during inlining"
+                  << messaget::eom;
+    }
+    throw error_code;
+  }
+}
+
+void inlining_decoratort::throw_on_not_enough_arguments(
+  messaget &log,
+  const int error_code)
+{
+  if(not_enough_arguments_set.size() != 0)
+  {
+    for(auto it : not_enough_arguments_set)
+    {
+      log.error() << "Not enough arguments for '" << it << "' during inlining"
+                  << messaget::eom;
+    }
+    throw error_code;
+  }
+}