28 template <
typename Handler,
typename GotoFunctionT>
29 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
31 using targett = decltype(goto_function.body.instructions.begin());
34 [](targett target) {
return target->is_function_call(); },
38 [[nodiscard]]
static bool restrict_function_pointer(
54 const auto &original_function = location->call_function();
61 auto const &called_function_pointer =
64 auto const &pointer_symbol =
to_symbol_expr(called_function_pointer);
65 auto const restriction_iterator =
66 restrictions.
restrictions.find(pointer_symbol.get_identifier());
68 if(restriction_iterator == restrictions.
restrictions.end())
72 std::unordered_set<symbol_exprt, irep_hash> candidates;
73 for(
const auto &candidate : restriction_iterator->second)
74 candidates.insert(ns.lookup(candidate).symbol_expr());
90 std::string correct_format)
92 correct_format(std::move(correct_format))
100 res +=
"Invalid restriction";
101 res +=
"\nReason: " +
reason;
117 auto const function_pointer_sym =
119 if(function_pointer_sym ==
nullptr)
122 " not found in the symbol table"};
124 auto const &function_pointer_type = function_pointer_sym->type;
125 if(function_pointer_type.id() != ID_pointer)
130 auto const &function_type =
132 if(function_type.id() != ID_code)
138 for(
auto const &function_pointer_target : restriction.second)
140 auto const function_pointer_target_sym =
142 if(function_pointer_target_sym ==
nullptr)
145 "symbol not found: " +
id2string(function_pointer_target)};
147 auto const &function_pointer_target_type =
148 function_pointer_target_sym->type;
149 if(function_pointer_target_type.id() != ID_code)
152 "not a function: " +
id2string(function_pointer_target)};
162 "type mismatch: `" +
id2string(restriction.first) +
"' points to `" +
163 type2c(function_type, ns) +
"', but restriction `" +
164 id2string(function_pointer_target) +
"' has type `" +
165 type2c(function_pointer_target_type, ns) +
"'"};
177 options, goto_model, message_handler);
185 bool did_something =
false;
187 did_something |= restrict_function_pointer(
234 for(
auto const &restriction : rhs)
236 auto emplace_result = result.emplace(restriction.first, restriction.second);
237 if(!emplace_result.second)
239 for(
auto const &target : restriction.second)
241 emplace_result.first->second.insert(target);
251 const std::list<std::string> &restriction_opts,
252 const std::string &option,
255 auto function_pointer_restrictions =
258 for(
const std::string &restriction_opt : restriction_opts)
260 const auto restriction =
263 const bool inserted = function_pointer_restrictions
264 .emplace(restriction.first, restriction.second)
270 "function pointer restriction for `" +
id2string(restriction.first) +
271 "' was specified twice"};
275 return function_pointer_restrictions;
280 const std::list<std::string> &restriction_opts,
289 const std::list<std::string> &filenames,
295 for(
auto const &filename : filenames)
301 std::move(merged_restrictions),
restrictions.restrictions);
304 return merged_restrictions;
312 const std::string &candidate,
315 const auto last_dot = candidate.rfind(
'.');
317 last_dot == std::string::npos || last_dot + 1 == candidate.size() ||
318 isdigit(candidate[last_dot + 1]))
323 std::string pointer_name = candidate;
325 const auto function_id = pointer_name.substr(0, last_dot);
326 const auto label = pointer_name.substr(last_dot + 1);
332 std::optional<source_locationt> location;
333 for(
const auto &instruction : it->second.body.instructions)
337 instruction.labels.begin(), instruction.labels.end(), label) !=
338 instruction.labels.end())
340 location = instruction.source_location();
344 instruction.is_function_call() &&
345 instruction.call_function().id() == ID_dereference &&
346 location.has_value() && instruction.source_location() == *location)
348 auto const &called_function_pointer =
360 "non-existent pointer name " + pointer_name,
361 "pointers should be identifiers or <function_name>.<label>"};
369 const std::string &restriction_opt,
370 const std::string &option,
375 auto const pointer_name_end = restriction_opt.find(
'/');
376 auto const restriction_format_message =
377 "the format for restrictions is "
378 "<pointer_name>/<target[,more_targets]*>";
380 if(pointer_name_end == std::string::npos)
383 restriction_opt +
"'",
384 restriction_format_message};
387 if(pointer_name_end == restriction_opt.size())
390 "couldn't find names of targets after '/' in `" + restriction_opt +
"'",
391 restriction_format_message};
394 if(pointer_name_end == 0)
397 "couldn't find target name before '/' in `" + restriction_opt +
"'"};
401 restriction_opt.substr(0, pointer_name_end), goto_model);
403 auto const target_names_substring =
404 restriction_opt.substr(pointer_name_end + 1);
405 auto const target_name_strings =
split_string(target_names_substring,
',');
407 if(target_name_strings.size() == 1 && target_name_strings[0].empty())
410 "missing target list for function pointer restriction " + pointer_name,
411 restriction_format_message};
414 std::unordered_set<irep_idt> target_names;
415 target_names.insert(target_name_strings.begin(), target_name_strings.end());
417 for(
auto const &target_name : target_names)
419 if(target_name == ID_empty_string)
422 "leading or trailing comma in restrictions for `" + pointer_name +
"'",
423 restriction_format_message);
427 return std::make_pair(pointer_name, target_names);
430 std::optional<function_pointer_restrictionst::restrictiont>
438 const exprt &
function = location->call_function();
447 auto const &function_pointer_call_site =
454 function_pointer_call_site.get_identifier(),
455 "called function pointer must have been assigned at the previous location");
462 const auto restriction = by_name_restrictions.find(rhs.get_identifier());
464 if(restriction != by_name_restrictions.end())
466 return std::optional<function_pointer_restrictionst::restrictiont>(
468 function_pointer_call_site.get_identifier(), restriction->second));
479 auto const restriction_opts =
485 commandline_restrictions =
487 restriction_opts, goto_model);
489 goto_model, commandline_restrictions);
502 auto const restriction_file_opts =
505 restriction_file_opts, goto_model, message_handler);
516 auto const restriction_name_opts =
519 restriction_name_opts, goto_model);
531 commandline_restrictions,
541 if(!
json.is_object())
548 std::string pointer_name =
551 if(!restriction.second.is_array())
553 throw deserialization_exceptiont{
"Value of " + restriction.first +
556 auto possible_targets = std::unordered_set<irep_idt>{};
561 std::inserter(possible_targets, possible_targets.end()),
562 [&](
const jsont &array_element) {
563 if(!array_element.is_string())
565 throw deserialization_exceptiont{
566 "Value of " + restriction.first +
567 "contains a non-string array element"};
569 return irep_idt{to_json_string(array_element).value};
571 return possible_targets;
579 const std::string &filename,
583 auto inFile = std::ifstream{filename};
589 "failed to read function pointer restrictions from " + filename};
597 auto function_pointer_restrictions_json =
jsont{};
598 auto &restrictions_json_object =
603 auto &targets_array =
605 for(
auto const &target : restriction.second)
611 return function_pointer_restrictions_json;
615 const std::string &filename)
const
617 auto function_pointer_restrictions_json =
to_json();
619 auto outFile = std::ofstream{filename};
624 " for writing function pointer restrictions"};
627 function_pointer_restrictions_json.output(outFile);
634 const std::list<std::string> &restriction_name_opts,
639 restriction_name_opts,
646 for_each_function_call(
648 const auto restriction = get_by_name_restriction(
649 goto_function.second, by_name_restrictions, it);
653 restrictions.insert(*restriction);
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
Base class for exceptions thrown in the cprover project.
std::string reason
The reason this exception was generated.
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
static function_pointer_restrictionst from_options(const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
Parse function pointer restrictions from command line.
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts, const goto_modelt &goto_model)
static restrictionst get_function_pointer_by_name_restrictions(const std::list< std::string > &restriction_name_opts, const goto_modelt &goto_model)
Get function pointer restrictions from restrictions with named pointers.
const restrictionst restrictions
static restrictionst parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option, const goto_modelt &goto_model)
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option, const goto_modelt &goto_model)
static function_pointer_restrictionst read_from_file(const std::string &filename, const goto_modelt &goto_model, message_handlert &message_handler)
restrictionst::value_type restrictiont
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, const goto_modelt &goto_model, message_handlert &message_handler)
void write_to_file(const std::string &filename) const
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
static function_pointer_restrictionst from_json(const jsont &json, const goto_modelt &goto_model)
static std::optional< restrictiont > get_by_name_restriction(const goto_functiont &goto_function, const function_pointer_restrictionst::restrictionst &by_name_restrictions, const goto_programt::const_targett &location)
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
void update()
Update all indices.
instructionst::iterator targett
instructionst::const_iterator const_targett
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string correct_format
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
std::string what() const override
A human readable description of what went wrong.
jsont & push_back(const jsont &json)
json_arrayt & make_array()
json_objectt & make_object()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_option(const std::string &option, const bool value)
const value_listt & get_list_option(const std::string &option) const
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Thrown when some external system fails unexpectedly.
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
const std::string & id2string(const irep_idt &d)
json_arrayt & to_json_array(jsont &json)
json_objectt & to_json_object(jsont &json)
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
API to expression classes for Pointers.
bool can_cast_expr< dereference_exprt >(const exprt &base)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
void remove_function_pointer(message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const std::unordered_set< symbol_exprt, irep_hash > &functions)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
Remove Indirect Function Calls.
static std::string resolve_pointer_name(const std::string &candidate, const goto_modelt &goto_model)
Parse candidate to distinguish whether it refers to a function pointer symbol directly (as produced b...
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void restrict_function_pointers(message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
Apply function pointer restrictions to a goto_model.
Given goto functions and a list of function parameters or globals that are function pointers with lis...
#define RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)