Skip to content

Commit d2a807b

Browse files
danpoedanpoe
committed
Refactorings and cleanups for the restrict function pointer by name feature
1 parent 19040a4 commit d2a807b

File tree

3 files changed

+153
-101
lines changed

3 files changed

+153
-101
lines changed

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1038,18 +1038,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
10381038
parse_function_pointer_restriction_options_from_cmdline(cmdline, options);
10391039

10401040
if(
1041-
!options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT).empty() ||
1042-
!options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT).empty() ||
1043-
!options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT).empty())
1041+
options.is_set(RESTRICT_FUNCTION_POINTER_OPT) ||
1042+
options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
1043+
options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
10441044
{
10451045
label_function_pointer_call_sites(goto_model);
10461046

1047-
auto const by_name_restrictions =
1048-
get_function_pointer_by_name_restrictions(goto_model, options);
1049-
10501047
const auto function_pointer_restrictions =
1051-
by_name_restrictions.merge(function_pointer_restrictionst::from_options(
1052-
options, log.get_message_handler()));
1048+
function_pointer_restrictionst::from_options(
1049+
options, goto_model, log.get_message_handler());
10531050

10541051
restrict_function_pointers(goto_model, function_pointer_restrictions);
10551052
}

‎src/goto-programs/restrict_function_pointers.cpp

Lines changed: 120 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,11 @@ void typecheck_function_pointer_restrictions(
2424
const goto_modelt &goto_model,
2525
const function_pointer_restrictionst &restrictions)
2626
{
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+
2732
for(auto const &restriction : restrictions.restrictions)
2833
{
2934
auto const function_pointer_sym =
@@ -32,22 +37,22 @@ void typecheck_function_pointer_restrictions(
3237
{
3338
throw invalid_command_line_argument_exceptiont{
3439
id2string(restriction.first) + " not found in the symbol table",
35-
"--restrict-function-pointer"};
40+
options};
3641
}
3742
auto const &function_pointer_type = function_pointer_sym->type;
3843
if(function_pointer_type.id() != ID_pointer)
3944
{
4045
throw invalid_command_line_argument_exceptiont{
4146
"not a function pointer: " + id2string(restriction.first),
42-
"--restrict-function-pointer"};
47+
options};
4348
}
4449
auto const &function_type =
4550
to_pointer_type(function_pointer_type).subtype();
4651
if(function_type.id() != ID_code)
4752
{
4853
throw invalid_command_line_argument_exceptiont{
4954
"not a function pointer: " + id2string(restriction.first),
50-
"--restrict-function-pointer"};
55+
options};
5156
}
5257
auto const &ns = namespacet{goto_model.symbol_table};
5358
for(auto const &function_pointer_target : restriction.second)
@@ -58,7 +63,7 @@ void typecheck_function_pointer_restrictions(
5863
{
5964
throw invalid_command_line_argument_exceptiont{
6065
"symbol not found: " + id2string(function_pointer_target),
61-
"--restrict-function-pointer"};
66+
options};
6267
}
6368
auto const &function_pointer_target_type =
6469
function_pointer_target_sym->type;
@@ -69,7 +74,7 @@ void typecheck_function_pointer_restrictions(
6974
type2c(function_type, ns) + "', but restriction `" +
7075
id2string(function_pointer_target) + "' has type `" +
7176
type2c(function_pointer_target_type, ns) + "'",
72-
"--restrict-function-pointer"};
77+
options};
7378
}
7479
}
7580
}
@@ -114,7 +119,7 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
114119
handler);
115120
}
116121

117-
void handle_call(
122+
void restrict_function_pointer(
118123
goto_functiont &goto_function,
119124
goto_modelt &goto_model,
120125
const function_pointer_restrictionst &restrictions,
@@ -193,6 +198,51 @@ void handle_call(
193198
address_of_exprt{function_pointer_target_symbol_expr}}));
194199
}
195200
}
201+
202+
void get_by_name_restriction(
203+
const goto_functiont &goto_function,
204+
const function_pointer_restrictionst::restrictionst &by_name_restrictions,
205+
function_pointer_restrictionst::restrictionst &restrictions,
206+
const goto_programt::const_targett &location)
207+
{
208+
PRECONDITION(location->is_function_call());
209+
210+
const exprt &function = location->get_function_call().function();
211+
212+
if(!can_cast_expr<dereference_exprt>(function))
213+
return;
214+
215+
auto const &function_pointer_call_site = to_symbol_expr(
216+
to_dereference_expr(function)
217+
.pointer());
218+
219+
for(auto it = std::prev(location);
220+
it != goto_function.body.instructions.end();
221+
++it)
222+
{
223+
if(!it->is_assign())
224+
continue;
225+
226+
if(it->get_assign().lhs() != function_pointer_call_site)
227+
continue;
228+
229+
if(!can_cast_expr<symbol_exprt>(it->get_assign().rhs()))
230+
continue;
231+
232+
auto const &rhs = to_symbol_expr(it->get_assign().rhs());
233+
auto const restriction =
234+
by_name_restrictions.find(rhs.get_identifier());
235+
236+
if(
237+
restriction != by_name_restrictions.end() &&
238+
restriction->first == rhs.get_identifier())
239+
{
240+
restrictions.emplace(
241+
function_pointer_call_site.get_identifier(),
242+
restriction->second);
243+
}
244+
}
245+
}
196246
} // namespace
197247

198248
void restrict_function_pointers(
@@ -206,7 +256,7 @@ void restrict_function_pointers(
206256
goto_functiont &goto_function = function_item.second;
207257

208258
for_each_function_call(goto_function, [&](const goto_programt::targett it) {
209-
handle_call(goto_function, goto_model, restrictions, it);
259+
restrict_function_pointer(goto_function, goto_model, restrictions, it);
210260
});
211261
}
212262
}
@@ -215,15 +265,26 @@ void parse_function_pointer_restriction_options_from_cmdline(
215265
const cmdlinet &cmdline,
216266
optionst &options)
217267
{
218-
options.set_option(
219-
RESTRICT_FUNCTION_POINTER_OPT,
220-
cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT));
221-
options.set_option(
222-
RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT,
223-
cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT));
224-
options.set_option(
225-
RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
226-
cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT));
268+
if(cmdline.isset(RESTRICT_FUNCTION_POINTER_OPT))
269+
{
270+
options.set_option(
271+
RESTRICT_FUNCTION_POINTER_OPT,
272+
cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT));
273+
}
274+
275+
if(cmdline.isset(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
276+
{
277+
options.set_option(
278+
RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT,
279+
cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT));
280+
}
281+
282+
if(cmdline.isset(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT))
283+
{
284+
options.set_option(
285+
RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
286+
cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT));
287+
}
227288
}
228289

229290
function_pointer_restrictionst::restrictionst
@@ -249,18 +310,17 @@ function_pointer_restrictionst::merge_function_pointer_restrictions(
249310
}
250311

251312
function_pointer_restrictionst::restrictionst
252-
function_pointer_restrictionst::
253-
parse_function_pointer_restrictions_from_command_line(
313+
function_pointer_restrictionst::parse_function_pointer_restrictions(
254314
const std::list<std::string> &restriction_opts,
255-
const std::string &option_name)
315+
const std::string &option)
256316
{
257317
auto function_pointer_restrictions =
258318
function_pointer_restrictionst::restrictionst{};
259319

260320
for(const std::string &restriction_opt : restriction_opts)
261321
{
262322
const auto restriction =
263-
parse_function_pointer_restriction(restriction_opt, "--" + option_name);
323+
parse_function_pointer_restriction(restriction_opt, option);
264324

265325
const bool inserted = function_pointer_restrictions
266326
.emplace(restriction.first, restriction.second)
@@ -271,23 +331,33 @@ parse_function_pointer_restrictions_from_command_line(
271331
throw invalid_command_line_argument_exceptiont{
272332
"function pointer restriction for `" + id2string(restriction.first) +
273333
"' was specified twice",
274-
"--" RESTRICT_FUNCTION_POINTER_OPT};
334+
option};
275335
}
276336
}
277337

278338
return function_pointer_restrictions;
279339
}
280340

341+
function_pointer_restrictionst::restrictionst
342+
function_pointer_restrictionst::
343+
parse_function_pointer_restrictions_from_command_line(
344+
const std::list<std::string> &restriction_opts)
345+
{
346+
return parse_function_pointer_restrictions(
347+
restriction_opts,
348+
"--" RESTRICT_FUNCTION_POINTER_OPT);
349+
}
350+
281351
function_pointer_restrictionst::restrictionst
282352
function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
283353
const std::list<std::string> &filenames,
284354
message_handlert &message_handler)
285355
{
286356
auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
357+
287358
for(auto const &filename : filenames)
288359
{
289-
auto const restrictions =
290-
function_pointer_restrictionst::read_from_file(filename, message_handler);
360+
auto const restrictions = read_from_file(filename, message_handler);
291361

292362
merged_restrictions = merge_function_pointer_restrictions(
293363
std::move(merged_restrictions), restrictions.restrictions);
@@ -363,18 +433,27 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
363433

364434
function_pointer_restrictionst function_pointer_restrictionst::from_options(
365435
const optionst &options,
436+
const goto_modelt &goto_model,
366437
message_handlert &message_handler)
367438
{
368439
auto const restriction_opts =
369440
options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT);
370441
auto const commandline_restrictions =
371-
parse_function_pointer_restrictions_from_command_line(
372-
restriction_opts, RESTRICT_FUNCTION_POINTER_OPT);
442+
parse_function_pointer_restrictions_from_command_line(restriction_opts);
443+
444+
auto const restriction_file_opts =
445+
options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT);
373446
auto const file_restrictions = parse_function_pointer_restrictions_from_file(
374-
options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT),
375-
message_handler);
447+
restriction_file_opts, message_handler);
448+
449+
auto const restriction_name_opts =
450+
options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
451+
auto const name_restrictions = get_function_pointer_by_name_restrictions(
452+
restriction_name_opts, goto_model);
453+
376454
return {merge_function_pointer_restrictions(
377-
std::move(file_restrictions), commandline_restrictions)};
455+
commandline_restrictions,
456+
merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
378457
}
379458

380459
function_pointer_restrictionst
@@ -467,61 +546,26 @@ void function_pointer_restrictionst::write_to_file(
467546

468547
function_pointer_restrictions_json.output(outFile);
469548
}
470-
function_pointer_restrictionst function_pointer_restrictionst::merge(
471-
const function_pointer_restrictionst &other) const
472-
{
473-
return function_pointer_restrictionst{
474-
merge_function_pointer_restrictions(restrictions, other.restrictions)};
475-
}
476549

477-
function_pointer_restrictionst get_function_pointer_by_name_restrictions(
478-
const goto_modelt &goto_model,
479-
const optionst &options)
550+
function_pointer_restrictionst::restrictionst
551+
function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
552+
const std::list<std::string> &restriction_name_opts,
553+
const goto_modelt &goto_model)
480554
{
481555
function_pointer_restrictionst::restrictionst by_name_restrictions =
482-
function_pointer_restrictionst::
483-
parse_function_pointer_restrictions_from_command_line(
484-
options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT),
485-
RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
556+
parse_function_pointer_restrictions(
557+
restriction_name_opts, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
558+
486559
function_pointer_restrictionst::restrictionst restrictions;
487560
for(auto const &goto_function : goto_model.goto_functions.function_map)
488561
{
489562
for_each_function_call(
490-
goto_function.second, [&](goto_programt::const_targett location) {
491-
PRECONDITION(location->is_function_call());
492-
if(can_cast_expr<dereference_exprt>(
493-
location->get_function_call().function()))
494-
{
495-
PRECONDITION(can_cast_expr<symbol_exprt>(
496-
to_dereference_expr(location->get_function_call().function())
497-
.pointer()));
498-
auto const &function_pointer_call_site = to_symbol_expr(
499-
to_dereference_expr(location->get_function_call().function())
500-
.pointer());
501-
auto const &body = goto_function.second.body;
502-
for(auto it = std::prev(location); it != body.instructions.end();
503-
++it)
504-
{
505-
if(
506-
it->is_assign() &&
507-
it->get_assign().lhs() == function_pointer_call_site &&
508-
can_cast_expr<symbol_exprt>(it->get_assign().rhs()))
509-
{
510-
auto const &assign_rhs = to_symbol_expr(it->get_assign().rhs());
511-
auto const restriction =
512-
by_name_restrictions.find(assign_rhs.get_identifier());
513-
if(
514-
restriction != by_name_restrictions.end() &&
515-
restriction->first == assign_rhs.get_identifier())
516-
{
517-
restrictions.emplace(
518-
function_pointer_call_site.get_identifier(),
519-
restriction->second);
520-
}
521-
}
522-
}
523-
}
563+
goto_function.second,
564+
[&](const goto_programt::const_targett it) {
565+
get_by_name_restriction(
566+
goto_function.second, by_name_restrictions, restrictions, it);
524567
});
525568
}
526-
return function_pointer_restrictionst{restrictions};
569+
570+
return restrictions;
527571
}

0 commit comments

Comments
 (0)