26 source_locationt make_function_pointer_restriction_assertion_source_location(
32 comment <<
"dereferenced function pointer at " << restriction.first
35 if(restriction.second.size() == 1)
37 comment << *restriction.second.begin();
44 comment, restriction.second.begin(), restriction.second.end(),
", ");
52 return source_location;
55 template <
typename Handler,
typename GotoFunctionT>
56 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
58 using targett = decltype(goto_function.body.instructions.begin());
61 [](targett target) {
return target->is_function_call(); },
65 void restrict_function_pointer(
79 const auto &original_function_call = location->get_function_call();
86 auto const &called_function_pointer =
89 auto const &pointer_symbol =
to_symbol_expr(called_function_pointer);
90 auto const restriction_iterator =
91 restrictions.
restrictions.find(pointer_symbol.get_identifier());
93 if(restriction_iterator == restrictions.
restrictions.end())
96 auto const &restriction = *restriction_iterator;
102 auto const original_function_call_instruction = *location;
106 make_function_pointer_restriction_assertion_source_location(
107 original_function_call_instruction.source_location, restriction));
117 auto else_location = location;
122 for(
auto const &restriction_target : restriction.second)
124 auto new_instruction = original_function_call_instruction;
126 const symbol_exprt &function_pointer_target_symbol_expr =
129 function_pointer_target_symbol_expr;
133 end_if_location, original_function_call_instruction.source_location));
134 auto const replaced_instruction_location =
137 replaced_instruction_location,
148 : reason(std::move(reason)), correct_format(std::move(correct_format))
157 res +=
"Invalid restriction";
158 res +=
"\nReason: " + reason;
160 if(!correct_format.empty())
162 res +=
"\nFormat: " + correct_format;
174 auto const function_pointer_sym =
176 if(function_pointer_sym ==
nullptr)
179 " not found in the symbol table"};
181 auto const &function_pointer_type = function_pointer_sym->type;
182 if(function_pointer_type.id() != ID_pointer)
187 auto const &function_type =
189 if(function_type.id() != ID_code)
195 for(
auto const &function_pointer_target : restriction.second)
197 auto const function_pointer_target_sym =
199 if(function_pointer_target_sym ==
nullptr)
202 "symbol not found: " +
id2string(function_pointer_target)};
204 auto const &function_pointer_target_type =
205 function_pointer_target_sym->type;
206 if(function_type != function_pointer_target_type)
209 "type mismatch: `" +
id2string(restriction.first) +
"' points to `" +
210 type2c(function_type, ns) +
"', but restriction `" +
211 id2string(function_pointer_target) +
"' has type `" +
212 type2c(function_pointer_target_type, ns) +
"'"};
227 restrict_function_pointer(goto_function, goto_model,
restrictions, it);
265 for(
auto const &restriction : rhs)
267 auto emplace_result = result.emplace(restriction.first, restriction.second);
268 if(!emplace_result.second)
270 for(
auto const &target : restriction.second)
272 emplace_result.first->second.insert(target);
282 const std::list<std::string> &restriction_opts,
283 const std::string &option)
285 auto function_pointer_restrictions =
288 for(
const std::string &restriction_opt : restriction_opts)
290 const auto restriction =
293 const bool inserted = function_pointer_restrictions
294 .emplace(restriction.first, restriction.second)
300 "function pointer restriction for `" +
id2string(restriction.first) +
301 "' was specified twice"};
305 return function_pointer_restrictions;
310 const std::list<std::string> &restriction_opts)
318 const std::list<std::string> &filenames,
323 for(
auto const &filename : filenames)
328 std::move(merged_restrictions),
restrictions.restrictions);
331 return merged_restrictions;
336 const std::string &restriction_opt,
337 const std::string &option)
341 auto const pointer_name_end = restriction_opt.find(
'/');
342 auto const restriction_format_message =
343 "the format for restrictions is "
344 "<pointer_name>/<target[,more_targets]*>";
346 if(pointer_name_end == std::string::npos)
349 restriction_opt +
"'",
350 restriction_format_message};
353 if(pointer_name_end == restriction_opt.size())
356 "couldn't find names of targets after '/' in `" + restriction_opt +
"'",
357 restriction_format_message};
360 if(pointer_name_end == 0)
363 "couldn't find target name before '/' in `" + restriction_opt +
"'"};
366 auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
367 auto const target_names_substring =
368 restriction_opt.substr(pointer_name_end + 1);
369 auto const target_name_strings =
split_string(target_names_substring,
',');
371 if(target_name_strings.size() == 1 && target_name_strings[0].empty())
374 "missing target list for function pointer restriction " + pointer_name,
375 restriction_format_message};
378 std::unordered_set<irep_idt> target_names;
379 target_names.insert(target_name_strings.begin(), target_name_strings.end());
381 for(
auto const &target_name : target_names)
383 if(target_name == ID_empty_string)
386 "leading or trailing comma in restrictions for `" + pointer_name +
"'",
387 restriction_format_message);
391 return std::make_pair(pointer_name, target_names);
402 const exprt &
function = location->get_function_call().function();
411 auto const &function_pointer_call_site =
420 function_pointer_call_site.get_identifier(),
421 "called function pointer must have been assigned at the previous location");
428 const auto restriction = by_name_restrictions.find(rhs.get_identifier());
430 if(restriction != by_name_restrictions.end())
434 function_pointer_call_site.get_identifier(), restriction->second));
445 auto const restriction_opts =
451 commandline_restrictions =
454 goto_model, commandline_restrictions);
465 auto const restriction_file_opts =
468 restriction_file_opts, message_handler);
479 auto const restriction_name_opts =
482 restriction_name_opts, goto_model);
492 commandline_restrictions,
501 if(!
json.is_object())
509 if(!restriction.second.is_array())
511 throw deserialization_exceptiont{
"Value of " + restriction.first +
514 auto possible_targets = std::unordered_set<irep_idt>{};
519 std::inserter(possible_targets, possible_targets.end()),
520 [&](
const jsont &array_element) {
521 if(!array_element.is_string())
523 throw deserialization_exceptiont{
524 "Value of " + restriction.first +
525 "contains a non-string array element"};
527 return irep_idt{to_json_string(array_element).value};
529 return possible_targets;
537 const std::string &filename,
540 auto inFile = std::ifstream{filename};
546 "failed to read function pointer restrictions from " + filename};
554 auto function_pointer_restrictions_json =
jsont{};
555 auto &restrictions_json_object =
560 auto &targets_array =
562 for(
auto const &target : restriction.second)
568 return function_pointer_restrictions_json;
572 const std::string &filename)
const
574 auto function_pointer_restrictions_json =
to_json();
576 auto outFile = std::ofstream{filename};
581 " for writing function pointer restrictions"};
584 function_pointer_restrictions_json.output(outFile);
591 const std::list<std::string> &restriction_name_opts,
601 for_each_function_call(
603 const auto restriction = get_by_name_restriction(
604 goto_function.second, by_name_restrictions, it);
608 restrictions.insert(*restriction);
Operator to return the address of an object.
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
A codet representing an assignment in the program.
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.
const source_locationt & source_location() const
The Boolean constant false.
std::string what() const override
A human readable description of what went wrong.
std::string correct_format
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
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 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 merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
static optionalt< restrictiont > get_by_name_restriction(const goto_functiont &goto_function, const function_pointer_restrictionst::restrictionst &by_name_restrictions, const goto_programt::const_targett &location)
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts)
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option)
static restrictionst parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option)
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, 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 read_from_file(const std::string &filename, message_handlert &message_handler)
static function_pointer_restrictionst from_json(const jsont &json)
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.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Thrown when some external system fails unexpectedly.
const typet & subtype() const
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Forward depth-first search iterators These iterators' copy operations are expensive,...
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)
nonstd::optional< T > optionalt
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.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
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 code_function_callt & to_code_function_call(const codet &code)
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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.