Skip to content

Commit 14a0433

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 585039a commit 14a0433

File tree

10 files changed

+315
-120
lines changed

10 files changed

+315
-120
lines changed

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,9 @@ 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+
^Numeric exception : 0$
7+
^EXIT=6$
98
^SIGNAL=0$
109
--
1110
--

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
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+
^Numeric exception : 0$
7+
^EXIT=6$
98
^SIGNAL=0$
109
--
1110
--

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
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+
^Numeric exception : 0$
7+
^EXIT=6$
98
^SIGNAL=0$
109
--
1110
--

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
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+
^Numeric exception : 0$
7+
^EXIT=6$
98
^SIGNAL=0$
109
--
1110
--

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
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+
^Numeric exception : 0$
7+
^EXIT=6$
98
^SIGNAL=0$
109
--
1110
--

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
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+
^Numeric exception : 0$
7+
^EXIT=6$
98
^SIGNAL=0$
109
--
1110
--

‎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: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
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+
{
31+
std::stringstream ss;
32+
ss << sm[1];
33+
no_body_set.insert(ss.str());
34+
}
35+
}
36+
37+
void inlining_decoratort::match_missing_function_warning(
38+
const std::string &message)
39+
{
40+
std::smatch sm;
41+
std::regex_match(message, sm, missing_function_regex);
42+
if(sm.size() == 2)
43+
{
44+
std::stringstream ss;
45+
ss << sm[1];
46+
missing_function_set.insert(ss.str());
47+
}
48+
}
49+
50+
void inlining_decoratort::match_recursive_call_warning(
51+
const std::string &message)
52+
{
53+
std::smatch sm;
54+
std::regex_match(message, sm, recursive_call_regex);
55+
if(sm.size() == 2)
56+
{
57+
std::stringstream ss;
58+
ss << sm[1];
59+
recursive_call_set.insert(ss.str());
60+
}
61+
}
62+
63+
void inlining_decoratort::match_not_enough_arguments_warning(
64+
const std::string &message)
65+
{
66+
std::smatch sm;
67+
std::regex_match(message, sm, not_enough_arguments_regex);
68+
if(sm.size() == 2)
69+
{
70+
std::stringstream ss;
71+
ss << sm[1];
72+
not_enough_arguments_set.insert(ss.str());
73+
}
74+
}
75+
76+
void inlining_decoratort::parse_message(const std::string &message)
77+
{
78+
match_no_body_warning(message);
79+
match_missing_function_warning(message);
80+
match_recursive_call_warning(message);
81+
match_not_enough_arguments_warning(message);
82+
}
83+
84+
void inlining_decoratort::throw_on_no_body(messaget &log, const int error_code)
85+
{
86+
if(no_body_set.size() != 0)
87+
{
88+
for(auto it : no_body_set)
89+
{
90+
log.error() << "inlining_decoratort: no body for '" << it
91+
<< "' during inlining" << messaget::eom;
92+
}
93+
throw error_code;
94+
}
95+
}
96+
97+
void inlining_decoratort::throw_on_recursive_calls(
98+
messaget &log,
99+
const int error_code)
100+
{
101+
if(recursive_call_set.size() != 0)
102+
{
103+
for(auto it : recursive_call_set)
104+
{
105+
log.error() << "inlining_decoratort: recursive call to '" << it
106+
<< "' during inlining" << messaget::eom;
107+
}
108+
throw error_code;
109+
}
110+
}
111+
112+
void inlining_decoratort::throw_on_missing_function(
113+
messaget &log,
114+
const int error_code)
115+
{
116+
if(missing_function_set.size() != 0)
117+
{
118+
for(auto it : missing_function_set)
119+
{
120+
log.error() << "inlining_decoratort: missing function '" << it
121+
<< "' during inlining" << messaget::eom;
122+
}
123+
throw error_code;
124+
}
125+
}
126+
127+
/// Throws the given error code if `not enough arguments`
128+
/// warnings happend during inlining
129+
void inlining_decoratort::throw_on_not_enough_arguments(
130+
messaget &log,
131+
const int error_code)
132+
{
133+
if(not_enough_arguments_set.size() != 0)
134+
{
135+
for(auto it : not_enough_arguments_set)
136+
{
137+
log.error() << "inlining_decoratort: not enough arguments for '" << it
138+
<< "' during inlining" << messaget::eom;
139+
}
140+
throw error_code;
141+
}
142+
}

0 commit comments

Comments
 (0)