23 source_locationt make_function_pointer_restriction_assertion_source_location(
29 comment <<
"dereferenced function pointer at " << restriction.first
32 if(restriction.second.size() == 1)
34 comment << *restriction.second.begin();
41 comment, restriction.second.begin(), restriction.second.end(),
", ");
49 return source_location;
52 template <
typename Handler,
typename GotoFunctionT>
53 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
55 using targett = decltype(goto_function.body.instructions.begin());
58 [](targett target) {
return target->is_function_call(); },
62 void restrict_function_pointer(
76 const auto &original_function_call = location->get_function_call();
83 auto const &called_function_pointer =
86 auto const &pointer_symbol =
to_symbol_expr(called_function_pointer);
87 auto const restriction_iterator =
88 restrictions.
restrictions.find(pointer_symbol.get_identifier());
90 if(restriction_iterator == restrictions.
restrictions.end())
93 auto const &restriction = *restriction_iterator;
99 auto const original_function_call_instruction = *location;
103 make_function_pointer_restriction_assertion_source_location(
104 original_function_call_instruction.source_location, restriction));
114 auto else_location = location;
119 for(
auto const &restriction_target : restriction.second)
121 auto new_instruction = original_function_call_instruction;
123 const symbol_exprt &function_pointer_target_symbol_expr =
126 function_pointer_target_symbol_expr;
130 end_if_location, original_function_call_instruction.source_location));
131 auto const replaced_instruction_location =
134 replaced_instruction_location,
145 : reason(std::move(reason)), correct_format(std::move(correct_format))
154 res +=
"Invalid restriction";
155 res +=
"\nReason: " + reason;
157 if(!correct_format.empty())
159 res +=
"\nFormat: " + correct_format;
171 auto const function_pointer_sym =
173 if(function_pointer_sym ==
nullptr)
176 " not found in the symbol table"};
178 auto const &function_pointer_type = function_pointer_sym->type;
179 if(function_pointer_type.id() != ID_pointer)
184 auto const &function_type =
186 if(function_type.id() != ID_code)
192 for(
auto const &function_pointer_target : restriction.second)
194 auto const function_pointer_target_sym =
196 if(function_pointer_target_sym ==
nullptr)
199 "symbol not found: " +
id2string(function_pointer_target)};
201 auto const &function_pointer_target_type =
202 function_pointer_target_sym->type;
203 if(function_type != function_pointer_target_type)
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) +
"'"};
224 restrict_function_pointer(goto_function, goto_model,
restrictions, it);
262 for(
auto const &restriction : rhs)
264 auto emplace_result = result.emplace(restriction.first, restriction.second);
265 if(!emplace_result.second)
267 for(
auto const &target : restriction.second)
269 emplace_result.first->second.insert(target);
279 const std::list<std::string> &restriction_opts,
280 const std::string &option)
282 auto function_pointer_restrictions =
285 for(
const std::string &restriction_opt : restriction_opts)
287 const auto restriction =
290 const bool inserted = function_pointer_restrictions
291 .emplace(restriction.first, restriction.second)
297 "function pointer restriction for `" +
id2string(restriction.first) +
298 "' was specified twice"};
302 return function_pointer_restrictions;
307 const std::list<std::string> &restriction_opts)
315 const std::list<std::string> &filenames,
320 for(
auto const &filename : filenames)
325 std::move(merged_restrictions),
restrictions.restrictions);
328 return merged_restrictions;
333 const std::string &restriction_opt,
334 const std::string &option)
338 auto const pointer_name_end = restriction_opt.find(
'/');
339 auto const restriction_format_message =
340 "the format for restrictions is "
341 "<pointer_name>/<target[,more_targets]*>";
343 if(pointer_name_end == std::string::npos)
346 restriction_opt +
"'",
347 restriction_format_message};
350 if(pointer_name_end == restriction_opt.size())
353 "couldn't find names of targets after '/' in `" + restriction_opt +
"'",
354 restriction_format_message};
357 if(pointer_name_end == 0)
360 "couldn't find target name before '/' in `" + restriction_opt +
"'"};
363 auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
364 auto const target_names_substring =
365 restriction_opt.substr(pointer_name_end + 1);
366 auto const target_name_strings =
split_string(target_names_substring,
',');
368 if(target_name_strings.size() == 1 && target_name_strings[0].empty())
371 "missing target list for function pointer restriction " + pointer_name,
372 restriction_format_message};
375 std::unordered_set<irep_idt> target_names;
376 target_names.insert(target_name_strings.begin(), target_name_strings.end());
378 for(
auto const &target_name : target_names)
380 if(target_name == ID_empty_string)
383 "leading or trailing comma in restrictions for `" + pointer_name +
"'",
384 restriction_format_message);
388 return std::make_pair(pointer_name, target_names);
399 const exprt &
function = location->get_function_call().function();
408 auto const &function_pointer_call_site =
417 function_pointer_call_site.get_identifier(),
418 "called function pointer must have been assigned at the previous location");
425 const auto restriction = by_name_restrictions.find(rhs.get_identifier());
427 if(restriction != by_name_restrictions.end())
431 function_pointer_call_site.get_identifier(), restriction->second));
442 auto const restriction_opts =
448 commandline_restrictions =
451 goto_model, commandline_restrictions);
462 auto const restriction_file_opts =
465 restriction_file_opts, message_handler);
476 auto const restriction_name_opts =
479 restriction_name_opts, goto_model);
489 commandline_restrictions,
498 if(!
json.is_object())
506 if(!restriction.second.is_array())
508 throw deserialization_exceptiont{
"Value of " + restriction.first +
511 auto possible_targets = std::unordered_set<irep_idt>{};
516 std::inserter(possible_targets, possible_targets.end()),
517 [&](
const jsont &array_element) {
518 if(!array_element.is_string())
520 throw deserialization_exceptiont{
521 "Value of " + restriction.first +
522 "contains a non-string array element"};
524 return irep_idt{to_json_string(array_element).value};
526 return possible_targets;
534 const std::string &filename,
537 auto inFile = std::ifstream{filename};
543 "failed to read function pointer restrictions from " + filename};
551 auto function_pointer_restrictions_json =
jsont{};
552 auto &restrictions_json_object =
557 auto &targets_array =
559 for(
auto const &target : restriction.second)
565 return function_pointer_restrictions_json;
569 const std::string &filename)
const
571 auto function_pointer_restrictions_json =
to_json();
573 auto outFile = std::ofstream{filename};
578 " for writing function pointer restrictions"};
581 function_pointer_restrictions_json.output(outFile);
588 const std::list<std::string> &restriction_name_opts,
598 for_each_function_call(
600 const auto restriction = get_by_name_restriction(
601 goto_function.second, by_name_restrictions, it);
605 restrictions.insert(*restriction);