Skip to content

Commit 09bfc72

Browse files
author
Remi Delmas
committed
CONTRACTS: inlining_decoratort improvements
- move the class to its own file - use regexes to track all 4 types of warnings - add methods to throw errors after warnings
1 parent e448fd4 commit 09bfc72

File tree

10 files changed

+307
-120
lines changed

10 files changed

+307
-120
lines changed

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,8 @@ CORE
22
main.c
33
--enforce-contract f1 _ --unwind 20 --unwinding-assertions
44
^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$
5-
^Invariant check failed$
6-
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7-
^Reason: Recursive functions found during inlining$
8-
^EXIT=(127|134|137)$
5+
^inlining_decoratort: recursive call to 'f2' during inlining$
6+
^EXIT=6$
97
^SIGNAL=0$
108
--
119
--

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract f2 _ --unwind 20 --unwinding-assertions
4-
^file main\.c line 13 function f2: recursion is ignored on call to 'f2'$
5-
^Invariant check failed$
6-
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7-
^Reason: Recursive functions found during inlining$
8-
^EXIT=(127|134|137)$
4+
^file main.c line 13 function f2: recursion is ignored on call to 'f2'$
5+
^inlining_decoratort: recursive call to 'f2' during inlining$
6+
^EXIT=6$
97
^SIGNAL=0$
108
--
119
--

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract f1 _ --unwind 20 --unwinding-assertions
4-
^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
5-
^Invariant check failed$
6-
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7-
^Reason: Recursive functions found during inlining$
8-
^EXIT=(127|134|137)$
4+
^file main.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
5+
^inlining_decoratort: recursive call to 'f2_out' during inlining$
6+
^EXIT=6$
97
^SIGNAL=0$
108
--
119
--

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract f2_in _ --unwind 20 --unwinding-assertions
4-
^file main\.c line 13 function f2_out: recursion is ignored on call to 'f2_in'$
5-
^Invariant check failed$
6-
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7-
^Reason: Recursive functions found during inlining$
8-
^EXIT=(127|134|137)$
4+
^file main.c line 13 function f2_out: recursion is ignored on call to 'f2_in'$
5+
^inlining_decoratort: recursive call to 'f2_in' during inlining$
6+
^EXIT=6$
97
^SIGNAL=0$
108
--
119
--

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract f2_out _ --unwind 20 --unwinding-assertions
4-
^file main\.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
5-
^Invariant check failed$
6-
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7-
^Reason: Recursive functions found during inlining$
8-
^EXIT=(127|134|137)$
4+
^file main.c line 19 function f2_in: recursion is ignored on call to 'f2_out'$
5+
^inlining_decoratort: recursive call to 'f2_out' during inlining$
6+
^EXIT=6$
97
^SIGNAL=0$
108
--
119
--

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract sum _ --trace
4-
^file main\.c line 6 function sum_rec: recursion is ignored on call to 'sum_rec'$
5-
^Invariant check failed$
6-
^Condition: decorated\.get_recursive_function_warnings_count\(\) == 0$
7-
^Reason: Recursive functions found during inlining$
8-
^EXIT=(127|134|137)$
4+
^file main.c line 6 function sum_rec: recursion is ignored on call to 'sum_rec'$
5+
^inlining_decoratort: recursive call to 'sum_rec' during inlining$
6+
^EXIT=6$
97
^SIGNAL=0$
108
--
119
--

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ SRC = accelerate/accelerate.cpp \
2121
contracts/instrument_spec_assigns.cpp \
2222
contracts/memory_predicates.cpp \
2323
contracts/utils.cpp \
24+
contracts/inlining_decorator.cpp \
2425
concurrency.cpp \
2526
count_eloc.cpp \
2627
cover.cpp \

‎src/goto-instrument/contracts/contracts.cpp

Lines changed: 3 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -40,100 +40,14 @@ Date: February 2016
4040

4141
#include "cfg_info.h"
4242
#include "havoc_assigns_clause_targets.h"
43+
#include "inlining_decorator.h"
4344
#include "instrument_spec_assigns.h"
4445
#include "memory_predicates.h"
4546
#include "utils.h"
4647

4748
#include <algorithm>
4849
#include <map>
4950

50-
/// Decorator for \ref message_handlert that keeps track of warnings
51-
/// occuring when inlining a function.
52-
///
53-
/// It counts the number of :
54-
/// - recursive functions warnings
55-
/// - missing functions warnings
56-
/// - missing function body warnings
57-
/// - missing function arguments warnings
58-
class inlining_decoratort : public message_handlert
59-
{
60-
private:
61-
message_handlert &wrapped;
62-
unsigned int recursive_function_warnings_count = 0;
63-
64-
void parse_message(const std::string &message)
65-
{
66-
if(message.find("recursion is ignored on call") != std::string::npos)
67-
recursive_function_warnings_count++;
68-
}
69-
70-
public:
71-
explicit inlining_decoratort(message_handlert &_wrapped) : wrapped(_wrapped)
72-
{
73-
}
74-
75-
unsigned int get_recursive_function_warnings_count()
76-
{
77-
return recursive_function_warnings_count;
78-
}
79-
80-
void print(unsigned level, const std::string &message) override
81-
{
82-
parse_message(message);
83-
wrapped.print(level, message);
84-
}
85-
86-
void print(unsigned level, const xmlt &xml) override
87-
{
88-
wrapped.print(level, xml);
89-
}
90-
91-
void print(unsigned level, const jsont &json) override
92-
{
93-
wrapped.print(level, json);
94-
}
95-
96-
void print(unsigned level, const structured_datat &data) override
97-
{
98-
wrapped.print(level, data);
99-
}
100-
101-
void print(
102-
unsigned level,
103-
const std::string &message,
104-
const source_locationt &location) override
105-
{
106-
parse_message(message);
107-
wrapped.print(level, message, location);
108-
return;
109-
}
110-
111-
void flush(unsigned i) override
112-
{
113-
return wrapped.flush(i);
114-
}
115-
116-
void set_verbosity(unsigned _verbosity)
117-
{
118-
wrapped.set_verbosity(_verbosity);
119-
}
120-
121-
unsigned get_verbosity() const
122-
{
123-
return wrapped.get_verbosity();
124-
}
125-
126-
std::size_t get_message_count(unsigned level) const
127-
{
128-
return wrapped.get_message_count(level);
129-
}
130-
131-
std::string command(unsigned i) const override
132-
{
133-
return wrapped.command(i);
134-
}
135-
};
136-
13751
void code_contractst::check_apply_loop_contracts(
13852
const irep_idt &function_name,
13953
goto_functionst::goto_functiont &goto_function,
@@ -1031,7 +945,7 @@ void code_contractst::apply_loop_contract(
1031945
goto_functions, function_name, ns, log.get_message_handler());
1032946

1033947
INVARIANT(
1034-
decorated.get_recursive_function_warnings_count() == 0,
948+
decorated.get_recursive_call_set().size() == 0,
1035949
"Recursive functions found during inlining");
1036950

1037951
// restore internal invariants
@@ -1301,9 +1215,7 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
13011215
inlining_decoratort decorated(log.get_message_handler());
13021216
goto_function_inline(goto_functions, function, ns, decorated);
13031217

1304-
INVARIANT(
1305-
decorated.get_recursive_function_warnings_count() == 0,
1306-
"Recursive functions found during inlining");
1218+
decorated.throw_on_recursive_calls(log, 0);
13071219

13081220
// Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
13091221
simplify_gotos(function_body, ns);

‎src/goto-instrument/contracts/inlining_decorator.cpp

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
/*******************************************************************\
2+
3+
Module: Utility functions for code contracts.
4+
5+
Author: Remi Delmas, [email protected]
6+
7+
Date: August 2022
8+
9+
\*******************************************************************/
10+
11+
#include "inlining_decorator.h"
12+
13+
inlining_decoratort::inlining_decoratort(message_handlert &_wrapped)
14+
: wrapped(_wrapped),
15+
no_body_regex(std::regex(".*no body for function '(.*)'.*")),
16+
missing_function_regex(
17+
std::regex(".*missing function '(.*)' is ignored.*")),
18+
recursive_call_regex(
19+
std::regex(".*recursion is ignored on call to '(.*)'.*")),
20+
not_enough_arguments_regex(
21+
std::regex(".*call to '(.*)': not enough arguments.*"))
22+
{
23+
}
24+
25+
void inlining_decoratort::match_no_body_warning(const std::string &message)
26+
{
27+
std::smatch sm;
28+
std::regex_match(message, sm, no_body_regex);
29+
if(sm.size() == 2)
30+
no_body_set.insert(sm.str(1));
31+
}
32+
33+
void inlining_decoratort::match_missing_function_warning(
34+
const std::string &message)
35+
{
36+
std::smatch sm;
37+
std::regex_match(message, sm, missing_function_regex);
38+
if(sm.size() == 2)
39+
missing_function_set.insert(sm.str(1));
40+
}
41+
42+
void inlining_decoratort::match_recursive_call_warning(
43+
const std::string &message)
44+
{
45+
std::smatch sm;
46+
std::regex_match(message, sm, recursive_call_regex);
47+
if(sm.size() == 2)
48+
recursive_call_set.insert(sm.str(1));
49+
}
50+
51+
void inlining_decoratort::match_not_enough_arguments_warning(
52+
const std::string &message)
53+
{
54+
std::smatch sm;
55+
std::regex_match(message, sm, not_enough_arguments_regex);
56+
if(sm.size() == 2)
57+
not_enough_arguments_set.insert(sm.str(1));
58+
}
59+
60+
void inlining_decoratort::parse_message(const std::string &message)
61+
{
62+
match_no_body_warning(message);
63+
match_missing_function_warning(message);
64+
match_recursive_call_warning(message);
65+
match_not_enough_arguments_warning(message);
66+
}
67+
68+
void inlining_decoratort::throw_on_no_body(messaget &log, const int error_code)
69+
{
70+
if(no_body_set.size() != 0)
71+
{
72+
for(auto it : no_body_set)
73+
{
74+
log.error() << "inlining_decoratort: no body for '" << it
75+
<< "' during inlining" << messaget::eom;
76+
}
77+
throw error_code;
78+
}
79+
}
80+
81+
void inlining_decoratort::throw_on_recursive_calls(
82+
messaget &log,
83+
const int error_code)
84+
{
85+
if(recursive_call_set.size() != 0)
86+
{
87+
for(auto it : recursive_call_set)
88+
{
89+
log.error() << "inlining_decoratort: recursive call to '" << it
90+
<< "' during inlining" << messaget::eom;
91+
}
92+
throw error_code;
93+
}
94+
}
95+
96+
void inlining_decoratort::throw_on_missing_function(
97+
messaget &log,
98+
const int error_code)
99+
{
100+
if(missing_function_set.size() != 0)
101+
{
102+
for(auto it : missing_function_set)
103+
{
104+
log.error() << "inlining_decoratort: missing function '" << it
105+
<< "' during inlining" << messaget::eom;
106+
}
107+
throw error_code;
108+
}
109+
}
110+
111+
void inlining_decoratort::throw_on_not_enough_arguments(
112+
messaget &log,
113+
const int error_code)
114+
{
115+
if(not_enough_arguments_set.size() != 0)
116+
{
117+
for(auto it : not_enough_arguments_set)
118+
{
119+
log.error() << "inlining_decoratort: not enough arguments for '" << it
120+
<< "' during inlining" << messaget::eom;
121+
}
122+
throw error_code;
123+
}
124+
}

0 commit comments

Comments
 (0)