Skip to content

Commit 8154f23

Browse files
danpoedanpoe
committed
Refactor error handling of function pointer restriction
1 parent 9917b20 commit 8154f23

File tree

3 files changed

+152
-103
lines changed

3 files changed

+152
-103
lines changed

‎src/goto-programs/restrict_function_pointers.cpp‎

Lines changed: 129 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -20,66 +20,6 @@ Author: Diffblue Ltd.
2020

2121
namespace
2222
{
23-
void typecheck_function_pointer_restrictions(
24-
const goto_modelt &goto_model,
25-
const function_pointer_restrictionst &restrictions)
26-
{
27-
const std::string options =
28-
"--" RESTRICT_FUNCTION_POINTER_OPT "/"
29-
"--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "/"
30-
"--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT;
31-
32-
for(auto const &restriction : restrictions.restrictions)
33-
{
34-
auto const function_pointer_sym =
35-
goto_model.symbol_table.lookup(restriction.first);
36-
if(function_pointer_sym == nullptr)
37-
{
38-
throw invalid_command_line_argument_exceptiont{
39-
id2string(restriction.first) + " not found in the symbol table",
40-
options};
41-
}
42-
auto const &function_pointer_type = function_pointer_sym->type;
43-
if(function_pointer_type.id() != ID_pointer)
44-
{
45-
throw invalid_command_line_argument_exceptiont{
46-
"not a function pointer: " + id2string(restriction.first),
47-
options};
48-
}
49-
auto const &function_type =
50-
to_pointer_type(function_pointer_type).subtype();
51-
if(function_type.id() != ID_code)
52-
{
53-
throw invalid_command_line_argument_exceptiont{
54-
"not a function pointer: " + id2string(restriction.first),
55-
options};
56-
}
57-
auto const &ns = namespacet{goto_model.symbol_table};
58-
for(auto const &function_pointer_target : restriction.second)
59-
{
60-
auto const function_pointer_target_sym =
61-
goto_model.symbol_table.lookup(function_pointer_target);
62-
if(function_pointer_target_sym == nullptr)
63-
{
64-
throw invalid_command_line_argument_exceptiont{
65-
"symbol not found: " + id2string(function_pointer_target),
66-
options};
67-
}
68-
auto const &function_pointer_target_type =
69-
function_pointer_target_sym->type;
70-
if(function_type != function_pointer_target_type)
71-
{
72-
throw invalid_command_line_argument_exceptiont{
73-
"type mismatch: `" + id2string(restriction.first) + "' points to `" +
74-
type2c(function_type, ns) + "', but restriction `" +
75-
id2string(function_pointer_target) + "' has type `" +
76-
type2c(function_pointer_target_type, ns) + "'",
77-
options};
78-
}
79-
}
80-
}
81-
}
82-
8323
source_locationt make_function_pointer_restriction_assertion_source_location(
8424
source_locationt source_location,
8525
const function_pointer_restrictionst::restrictiont restriction)
@@ -200,12 +140,82 @@ void restrict_function_pointer(
200140
}
201141
} // namespace
202142

143+
function_pointer_restrictionst::invalid_restriction_exceptiont::
144+
invalid_restriction_exceptiont(std::string reason, std::string correct_format)
145+
: reason(std::move(reason)), correct_format(std::move(correct_format))
146+
{
147+
}
148+
149+
std::string
150+
function_pointer_restrictionst::invalid_restriction_exceptiont::what() const
151+
{
152+
std::string res;
153+
154+
res += "Invalid restriction";
155+
res += "\nReason: " + reason;
156+
157+
if(!correct_format.empty())
158+
{
159+
res += "\nFormat: " + correct_format;
160+
}
161+
162+
return res;
163+
}
164+
165+
void function_pointer_restrictionst::typecheck_function_pointer_restrictions(
166+
const goto_modelt &goto_model,
167+
const function_pointer_restrictionst::restrictionst &restrictions)
168+
{
169+
for(auto const &restriction : restrictions)
170+
{
171+
auto const function_pointer_sym =
172+
goto_model.symbol_table.lookup(restriction.first);
173+
if(function_pointer_sym == nullptr)
174+
{
175+
throw invalid_restriction_exceptiont{id2string(restriction.first) +
176+
" not found in the symbol table"};
177+
}
178+
auto const &function_pointer_type = function_pointer_sym->type;
179+
if(function_pointer_type.id() != ID_pointer)
180+
{
181+
throw invalid_restriction_exceptiont{"not a function pointer: " +
182+
id2string(restriction.first)};
183+
}
184+
auto const &function_type =
185+
to_pointer_type(function_pointer_type).subtype();
186+
if(function_type.id() != ID_code)
187+
{
188+
throw invalid_restriction_exceptiont{"not a function pointer: " +
189+
id2string(restriction.first)};
190+
}
191+
auto const &ns = namespacet{goto_model.symbol_table};
192+
for(auto const &function_pointer_target : restriction.second)
193+
{
194+
auto const function_pointer_target_sym =
195+
goto_model.symbol_table.lookup(function_pointer_target);
196+
if(function_pointer_target_sym == nullptr)
197+
{
198+
throw invalid_restriction_exceptiont{
199+
"symbol not found: " + id2string(function_pointer_target)};
200+
}
201+
auto const &function_pointer_target_type =
202+
function_pointer_target_sym->type;
203+
if(function_type != function_pointer_target_type)
204+
{
205+
throw invalid_restriction_exceptiont{
206+
"type mismatch: `" + id2string(restriction.first) + "' points to `" +
207+
type2c(function_type, ns) + "', but restriction `" +
208+
id2string(function_pointer_target) + "' has type `" +
209+
type2c(function_pointer_target_type, ns) + "'"};
210+
}
211+
}
212+
}
213+
}
214+
203215
void restrict_function_pointers(
204216
goto_modelt &goto_model,
205217
const function_pointer_restrictionst &restrictions)
206218
{
207-
typecheck_function_pointer_restrictions(goto_model, restrictions);
208-
209219
for(auto &function_item : goto_model.goto_functions.function_map)
210220
{
211221
goto_functiont &goto_function = function_item.second;
@@ -283,24 +293,21 @@ function_pointer_restrictionst::parse_function_pointer_restrictions(
283293

284294
if(!inserted)
285295
{
286-
throw invalid_command_line_argument_exceptiont{
296+
throw invalid_restriction_exceptiont{
287297
"function pointer restriction for `" + id2string(restriction.first) +
288-
"' was specified twice",
289-
option};
298+
"' was specified twice"};
290299
}
291300
}
292301

293302
return function_pointer_restrictions;
294303
}
295304

296-
function_pointer_restrictionst::restrictionst
297-
function_pointer_restrictionst::
298-
parse_function_pointer_restrictions_from_command_line(
299-
const std::list<std::string> &restriction_opts)
305+
function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
306+
parse_function_pointer_restrictions_from_command_line(
307+
const std::list<std::string> &restriction_opts)
300308
{
301309
return parse_function_pointer_restrictions(
302-
restriction_opts,
303-
"--" RESTRICT_FUNCTION_POINTER_OPT);
310+
restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT);
304311
}
305312

306313
function_pointer_restrictionst::restrictionst
@@ -335,25 +342,22 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
335342

336343
if(pointer_name_end == std::string::npos)
337344
{
338-
throw invalid_command_line_argument_exceptiont{
339-
"couldn't find '/' in `" + restriction_opt + "'",
340-
option,
341-
restriction_format_message};
345+
throw invalid_restriction_exceptiont{"couldn't find '/' in `" +
346+
restriction_opt + "'",
347+
restriction_format_message};
342348
}
343349

344350
if(pointer_name_end == restriction_opt.size())
345351
{
346-
throw invalid_command_line_argument_exceptiont{
352+
throw invalid_restriction_exceptiont{
347353
"couldn't find names of targets after '/' in `" + restriction_opt + "'",
348-
option,
349354
restriction_format_message};
350355
}
351356

352357
if(pointer_name_end == 0)
353358
{
354-
throw invalid_command_line_argument_exceptiont{
355-
"couldn't find target name before '/' in `" + restriction_opt + "'",
356-
option};
359+
throw invalid_restriction_exceptiont{
360+
"couldn't find target name before '/' in `" + restriction_opt + "'"};
357361
}
358362

359363
auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
@@ -363,9 +367,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
363367

364368
if(target_name_strings.size() == 1 && target_name_strings[0].empty())
365369
{
366-
throw invalid_command_line_argument_exceptiont{
370+
throw invalid_restriction_exceptiont{
367371
"missing target list for function pointer restriction " + pointer_name,
368-
option,
369372
restriction_format_message};
370373
}
371374

@@ -376,9 +379,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
376379
{
377380
if(target_name == ID_empty_string)
378381
{
379-
throw invalid_command_line_argument_exceptiont(
382+
throw invalid_restriction_exceptiont(
380383
"leading or trailing comma in restrictions for `" + pointer_name + "'",
381-
option,
382384
restriction_format_message);
383385
}
384386
}
@@ -426,7 +428,7 @@ function_pointer_restrictionst::get_by_name_restriction(
426428
{
427429
return optionalt<function_pointer_restrictionst::restrictiont>(
428430
std::make_pair(
429-
function_pointer_call_site.get_identifier(), restriction->second));
431+
function_pointer_call_site.get_identifier(), restriction->second));
430432
}
431433

432434
return {};
@@ -439,18 +441,49 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
439441
{
440442
auto const restriction_opts =
441443
options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT);
442-
auto const commandline_restrictions =
443-
parse_function_pointer_restrictions_from_command_line(restriction_opts);
444444

445-
auto const restriction_file_opts =
446-
options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT);
447-
auto const file_restrictions = parse_function_pointer_restrictions_from_file(
448-
restriction_file_opts, message_handler);
445+
restrictionst commandline_restrictions;
446+
try
447+
{
448+
commandline_restrictions =
449+
parse_function_pointer_restrictions_from_command_line(restriction_opts);
450+
typecheck_function_pointer_restrictions(
451+
goto_model, commandline_restrictions);
452+
}
453+
catch(const invalid_restriction_exceptiont &e)
454+
{
455+
throw invalid_command_line_argument_exceptiont{
456+
e.reason, "--" RESTRICT_FUNCTION_POINTER_OPT, e.correct_format};
457+
}
458+
459+
restrictionst file_restrictions;
460+
try
461+
{
462+
auto const restriction_file_opts =
463+
options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT);
464+
file_restrictions = parse_function_pointer_restrictions_from_file(
465+
restriction_file_opts, message_handler);
466+
typecheck_function_pointer_restrictions(goto_model, file_restrictions);
467+
}
468+
catch(const invalid_restriction_exceptiont &e)
469+
{
470+
throw deserialization_exceptiont{e.what()};
471+
}
449472

450-
auto const restriction_name_opts =
451-
options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
452-
auto const name_restrictions = get_function_pointer_by_name_restrictions(
453-
restriction_name_opts, goto_model);
473+
restrictionst name_restrictions;
474+
try
475+
{
476+
auto const restriction_name_opts =
477+
options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
478+
name_restrictions = get_function_pointer_by_name_restrictions(
479+
restriction_name_opts, goto_model);
480+
typecheck_function_pointer_restrictions(goto_model, name_restrictions);
481+
}
482+
catch(const invalid_restriction_exceptiont &e)
483+
{
484+
throw invalid_command_line_argument_exceptiont{
485+
e.reason, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT, e.correct_format};
486+
}
454487

455488
return {merge_function_pointer_restrictions(
456489
commandline_restrictions,
@@ -561,8 +594,7 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
561594
for(auto const &goto_function : goto_model.goto_functions.function_map)
562595
{
563596
for_each_function_call(
564-
goto_function.second,
565-
[&](const goto_programt::const_targett it) {
597+
goto_function.second, [&](const goto_programt::const_targett it) {
566598
const auto restriction = get_by_name_restriction(
567599
goto_function.second, by_name_restrictions, it);
568600

‎src/goto-programs/restrict_function_pointers.h‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,23 @@ class function_pointer_restrictionst
8282
void write_to_file(const std::string &filename) const;
8383

8484
protected:
85+
class invalid_restriction_exceptiont : public cprover_exception_baset
86+
{
87+
public:
88+
explicit invalid_restriction_exceptiont(
89+
std::string reason,
90+
std::string correct_format = "");
91+
92+
std::string what() const override;
93+
94+
std::string reason;
95+
std::string correct_format;
96+
};
97+
98+
static void typecheck_function_pointer_restrictions(
99+
const goto_modelt &goto_model,
100+
const restrictionst &restrictions);
101+
85102
static restrictionst merge_function_pointer_restrictions(
86103
restrictionst lhs,
87104
const restrictionst &rhs);

‎unit/goto-programs/restrict_function_pointers.cpp‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -43,29 +43,29 @@ void restriction_parsing_test()
4343

4444
REQUIRE_THROWS_AS(
4545
fp_restrictionst::parse_function_pointer_restriction("func", "test"),
46-
invalid_command_line_argument_exceptiont);
46+
fp_restrictionst::invalid_restriction_exceptiont);
4747

4848
REQUIRE_THROWS_AS(
4949
fp_restrictionst::parse_function_pointer_restriction("/func", "test"),
50-
invalid_command_line_argument_exceptiont);
50+
fp_restrictionst::invalid_restriction_exceptiont);
5151

5252
REQUIRE_THROWS_AS(
5353
fp_restrictionst::parse_function_pointer_restriction("func/", "test"),
54-
invalid_command_line_argument_exceptiont);
54+
fp_restrictionst::invalid_restriction_exceptiont);
5555

5656
REQUIRE_THROWS_AS(
5757
fp_restrictionst::parse_function_pointer_restriction("func/,", "test"),
58-
invalid_command_line_argument_exceptiont);
58+
fp_restrictionst::invalid_restriction_exceptiont);
5959

6060
REQUIRE_THROWS_AS(
6161
fp_restrictionst::parse_function_pointer_restriction(
6262
"func1/func2,", "test"),
63-
invalid_command_line_argument_exceptiont);
63+
fp_restrictionst::invalid_restriction_exceptiont);
6464

6565
REQUIRE_THROWS_AS(
6666
fp_restrictionst::parse_function_pointer_restriction(
6767
"func1/,func2", "test"),
68-
invalid_command_line_argument_exceptiont);
68+
fp_restrictionst::invalid_restriction_exceptiont);
6969
}
7070

7171
void merge_restrictions_test()

0 commit comments

Comments
 (0)