From 664a7acd19d08d3c71a037867e293f191f650c37 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 22 Aug 2022 12:52:14 -0400 Subject: [PATCH] CONTRACTS: Handle all 4 inlining warning types in `inlining_decoratort` Modifications: - move the class from contracts.cpp to its own file - use regexes to track all 4 types of warnings - add getter methods to inspect functions involved in warnings - add methods to throw errors after warnings --- .../function-calls-03-1/test-enf-f1.desc | 6 +- .../function-calls-03-1/test-enf-f2.desc | 8 +- .../function-calls-04-1/test-enf-f1.desc | 8 +- .../function-calls-04-1/test-enf-f2_in.desc | 8 +- .../function-calls-04-1/test-enf-f2_out.desc | 8 +- .../function-calls-recursive-01/test.desc | 8 +- src/goto-instrument/Makefile | 1 + src/goto-instrument/contracts/contracts.cpp | 94 +--------- .../contracts/inlining_decorator.cpp | 124 +++++++++++++ .../contracts/inlining_decorator.h | 165 ++++++++++++++++++ 10 files changed, 310 insertions(+), 120 deletions(-) create mode 100644 src/goto-instrument/contracts/inlining_decorator.cpp create mode 100644 src/goto-instrument/contracts/inlining_decorator.h diff --git a/regression/contracts/function-calls-03-1/test-enf-f1.desc b/regression/contracts/function-calls-03-1/test-enf-f1.desc index b4074b3fae9..2f7263a73dd 100644 --- a/regression/contracts/function-calls-03-1/test-enf-f1.desc +++ b/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$ -- -- diff --git a/regression/contracts/function-calls-03-1/test-enf-f2.desc b/regression/contracts/function-calls-03-1/test-enf-f2.desc index 8adfa3f0afd..3aab71fcd8c 100644 --- a/regression/contracts/function-calls-03-1/test-enf-f2.desc +++ b/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$ -- -- diff --git a/regression/contracts/function-calls-04-1/test-enf-f1.desc b/regression/contracts/function-calls-04-1/test-enf-f1.desc index 05550b8a420..87fce4d250e 100644 --- a/regression/contracts/function-calls-04-1/test-enf-f1.desc +++ b/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$ -- -- diff --git a/regression/contracts/function-calls-04-1/test-enf-f2_in.desc b/regression/contracts/function-calls-04-1/test-enf-f2_in.desc index 21bafb9a4ef..88486870350 100644 --- a/regression/contracts/function-calls-04-1/test-enf-f2_in.desc +++ b/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$ -- -- diff --git a/regression/contracts/function-calls-04-1/test-enf-f2_out.desc b/regression/contracts/function-calls-04-1/test-enf-f2_out.desc index 2d5c000f3b3..be908344748 100644 --- a/regression/contracts/function-calls-04-1/test-enf-f2_out.desc +++ b/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$ -- -- diff --git a/regression/contracts/function-calls-recursive-01/test.desc b/regression/contracts/function-calls-recursive-01/test.desc index ef1a4b1df44..d834d5dafd7 100644 --- a/regression/contracts/function-calls-recursive-01/test.desc +++ b/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$ -- -- diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 3d658b52529..1e73214a8b2 100644 --- a/src/goto-instrument/Makefile +++ b/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 \ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index a08d2b764ae..29a861cad02 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -40,6 +40,7 @@ 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" @@ -47,93 +48,6 @@ Date: February 2016 #include #include -/// 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); diff --git a/src/goto-instrument/contracts/inlining_decorator.cpp b/src/goto-instrument/contracts/inlining_decorator.cpp new file mode 100644 index 00000000000..a7e776fff94 --- /dev/null +++ b/src/goto-instrument/contracts/inlining_decorator.cpp @@ -0,0 +1,124 @@ +/*******************************************************************\ + +Module: Utility functions for code contracts. + +Author: Remi Delmas, delmasrd@amazon.com + +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; + } +} diff --git a/src/goto-instrument/contracts/inlining_decorator.h b/src/goto-instrument/contracts/inlining_decorator.h new file mode 100644 index 00000000000..098e0331b29 --- /dev/null +++ b/src/goto-instrument/contracts/inlining_decorator.h @@ -0,0 +1,165 @@ +/*******************************************************************\ + +Module: Utility functions for code contracts. + +Author: Remi Delmas, delmasrd@amazon.com + +Date: August 2022 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INLINING_DECORATOR_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INLINING_DECORATOR_H + +#include +#include + +#include +#include +#include + +/// Decorator for a \ref message_handlert used during function inlining that +/// collect names of GOTO functions creating warnings and allows to turn +/// inlining warnings into hard errors. +/// +/// The decorator intercepts and parses messages sent to the decorated +/// message handler and collects the names of GOTO functions involved in these +/// 4 types warnings: +/// - `recursive call` warnings, +/// - `missing function` warnings, +/// - `not enough arguments` warnings, +/// - `no body for function` warnings. +/// +/// For each warning type, the decorator offers: +/// - a method that returns the set of function names that caused the warnings +/// - a method that throws an error in case that set is not empty +/// +/// So this decorator allows to inspect the sets of functions involved in +/// warnings to check if the warnings are expected or not, and to turn warnings +/// into hard errors if desired. +/// +/// Decorator pattern info: https://en.wikipedia.org/wiki/Decorator_pattern +class inlining_decoratort : public message_handlert +{ +private: + message_handlert &wrapped; + + std::regex no_body_regex; + std::set no_body_set; + + void match_no_body_warning(const std::string &message); + + std::regex missing_function_regex; + std::set missing_function_set; + + void match_missing_function_warning(const std::string &message); + + std::regex recursive_call_regex; + std::set recursive_call_set; + + void match_recursive_call_warning(const std::string &message); + + std::regex not_enough_arguments_regex; + std::set not_enough_arguments_set; + + void match_not_enough_arguments_warning(const std::string &message); + + void parse_message(const std::string &message); + +public: + explicit inlining_decoratort(message_handlert &_wrapped); + + /// Throws the given error code if `no body for function` + /// warnings happend during inlining + void throw_on_no_body(messaget &log, const int error_code); + + /// Throws the given error code if `recursive call` + /// warnings happend during inlining + void throw_on_recursive_calls(messaget &log, const int error_code); + + /// Throws the given error code if `missing function` + /// warnings happend during inlining + void throw_on_missing_function(messaget &log, const int error_code); + + /// Throws the given error code if `not enough arguments` + /// warnings happend during inlining + void throw_on_not_enough_arguments(messaget &log, const int error_code); + + const std::set &get_no_body_set() const + { + return no_body_set; + } + + const std::set &get_missing_function_set() const + { + return missing_function_set; + } + + const std::set &get_recursive_call_set() const + { + return recursive_call_set; + } + + const std::set &get_not_enough_arguments_set() const + { + return not_enough_arguments_set; + } + + 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); + } +}; + +#endif