27 source_locationt make_function_pointer_restriction_assertion_source_location(
33 comment <<
"dereferenced function pointer at " << restriction.first
36 if(restriction.second.size() == 1)
38 comment << *restriction.second.begin();
45 comment, restriction.second.begin(), restriction.second.end(),
", ");
53 return source_location;
56 template <
typename Handler,
typename GotoFunctionT>
57 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
59 using targett = decltype(goto_function.body.instructions.begin());
62 [](targett target) {
return target->is_function_call(); },
66 void restrict_function_pointer(
80 const auto &original_function_call = location->get_function_call();
87 auto const &called_function_pointer =
90 auto const &pointer_symbol =
to_symbol_expr(called_function_pointer);
91 auto const restriction_iterator =
92 restrictions.
restrictions.find(pointer_symbol.get_identifier());
94 if(restriction_iterator == restrictions.
restrictions.end())
97 auto const &restriction = *restriction_iterator;
103 auto const original_function_call_instruction = *location;
107 make_function_pointer_restriction_assertion_source_location(
108 original_function_call_instruction.source_location, restriction));
118 auto else_location = location;
123 for(
auto const &restriction_target : restriction.second)
125 auto new_instruction = original_function_call_instruction;
127 const symbol_exprt &function_pointer_target_symbol_expr =
130 function_pointer_target_symbol_expr;
134 end_if_location, original_function_call_instruction.source_location));
135 auto const replaced_instruction_location =
138 replaced_instruction_location,
149 : reason(std::move(reason)), correct_format(std::move(correct_format))
158 res +=
"Invalid restriction";
159 res +=
"\nReason: " + reason;
161 if(!correct_format.empty())
163 res +=
"\nFormat: " + correct_format;
175 auto const function_pointer_sym =
177 if(function_pointer_sym ==
nullptr)
180 " not found in the symbol table"};
182 auto const &function_pointer_type = function_pointer_sym->type;
183 if(function_pointer_type.id() != ID_pointer)
188 auto const &function_type =
190 if(function_type.id() != ID_code)
196 for(
auto const &function_pointer_target : restriction.second)
198 auto const function_pointer_target_sym =
200 if(function_pointer_target_sym ==
nullptr)
203 "symbol not found: " +
id2string(function_pointer_target)};
205 auto const &function_pointer_target_type =
206 function_pointer_target_sym->type;
207 if(function_type != function_pointer_target_type)
210 "type mismatch: `" +
id2string(restriction.first) +
"' points to `" +
211 type2c(function_type, ns) +
"', but restriction `" +
212 id2string(function_pointer_target) +
"' has type `" +
213 type2c(function_pointer_target_type, ns) +
"'"};
228 restrict_function_pointer(goto_function, goto_model,
restrictions, it);
266 for(
auto const &restriction : rhs)
268 auto emplace_result = result.emplace(restriction.first, restriction.second);
269 if(!emplace_result.second)
271 for(
auto const &target : restriction.second)
273 emplace_result.first->second.insert(target);
283 const std::list<std::string> &restriction_opts,
284 const std::string &option)
286 auto function_pointer_restrictions =
289 for(
const std::string &restriction_opt : restriction_opts)
291 const auto restriction =
294 const bool inserted = function_pointer_restrictions
295 .emplace(restriction.first, restriction.second)
301 "function pointer restriction for `" +
id2string(restriction.first) +
302 "' was specified twice"};
306 return function_pointer_restrictions;
311 const std::list<std::string> &restriction_opts)
319 const std::list<std::string> &filenames,
324 for(
auto const &filename : filenames)
329 std::move(merged_restrictions),
restrictions.restrictions);
332 return merged_restrictions;
337 const std::string &restriction_opt,
338 const std::string &option)
342 auto const pointer_name_end = restriction_opt.find(
'/');
343 auto const restriction_format_message =
344 "the format for restrictions is "
345 "<pointer_name>/<target[,more_targets]*>";
347 if(pointer_name_end == std::string::npos)
350 restriction_opt +
"'",
351 restriction_format_message};
354 if(pointer_name_end == restriction_opt.size())
357 "couldn't find names of targets after '/' in `" + restriction_opt +
"'",
358 restriction_format_message};
361 if(pointer_name_end == 0)
364 "couldn't find target name before '/' in `" + restriction_opt +
"'"};
367 auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
368 auto const target_names_substring =
369 restriction_opt.substr(pointer_name_end + 1);
370 auto const target_name_strings =
split_string(target_names_substring,
',');
372 if(target_name_strings.size() == 1 && target_name_strings[0].empty())
375 "missing target list for function pointer restriction " + pointer_name,
376 restriction_format_message};
379 std::unordered_set<irep_idt> target_names;
380 target_names.insert(target_name_strings.begin(), target_name_strings.end());
382 for(
auto const &target_name : target_names)
384 if(target_name == ID_empty_string)
387 "leading or trailing comma in restrictions for `" + pointer_name +
"'",
388 restriction_format_message);
392 return std::make_pair(pointer_name, target_names);
403 const exprt &
function = location->call_function();
412 auto const &function_pointer_call_site =
419 function_pointer_call_site.get_identifier(),
420 "called function pointer must have been assigned at the previous location");
427 const auto restriction = by_name_restrictions.find(rhs.get_identifier());
429 if(restriction != by_name_restrictions.end())
433 function_pointer_call_site.get_identifier(), restriction->second));
444 auto const restriction_opts =
450 commandline_restrictions =
453 goto_model, commandline_restrictions);
464 auto const restriction_file_opts =
467 restriction_file_opts, message_handler);
478 auto const restriction_name_opts =
481 restriction_name_opts, goto_model);
491 commandline_restrictions,
500 if(!
json.is_object())
508 if(!restriction.second.is_array())
510 throw deserialization_exceptiont{
"Value of " + restriction.first +
513 auto possible_targets = std::unordered_set<irep_idt>{};
518 std::inserter(possible_targets, possible_targets.end()),
519 [&](
const jsont &array_element) {
520 if(!array_element.is_string())
522 throw deserialization_exceptiont{
523 "Value of " + restriction.first +
524 "contains a non-string array element"};
526 return irep_idt{to_json_string(array_element).value};
528 return possible_targets;
536 const std::string &filename,
539 auto inFile = std::ifstream{filename};
545 "failed to read function pointer restrictions from " + filename};
553 auto function_pointer_restrictions_json =
jsont{};
554 auto &restrictions_json_object =
559 auto &targets_array =
561 for(
auto const &target : restriction.second)
567 return function_pointer_restrictions_json;
571 const std::string &filename)
const
573 auto function_pointer_restrictions_json =
to_json();
575 auto outFile = std::ofstream{filename};
580 " for writing function pointer restrictions"};
583 function_pointer_restrictions_json.output(outFile);
590 const std::list<std::string> &restriction_name_opts,
600 for_each_function_call(
602 const auto restriction = get_by_name_restriction(
603 goto_function.second, by_name_restrictions, it);
607 restrictions.insert(*restriction);