cprover
Loading...
Searching...
No Matches
restrict_function_pointers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Restrict function pointers
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
11#include <ansi-c/expr2c.h>
12
13#include <json/json_parser.h>
14
15#include <util/cmdline.h>
16#include <util/options.h>
17#include <util/pointer_expr.h>
18#include <util/string_utils.h>
19
20#include "goto_model.h"
22
23#include <algorithm>
24#include <fstream>
25
26namespace
27{
28template <typename Handler, typename GotoFunctionT>
29void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
30{
31 using targett = decltype(goto_function.body.instructions.begin());
33 goto_function,
34 [](targett target) { return target->is_function_call(); },
35 handler);
36}
37
38static void restrict_function_pointer(
39 message_handlert &message_handler,
40 symbol_tablet &symbol_table,
41 goto_programt &goto_program,
42 const irep_idt &function_id,
43 const function_pointer_restrictionst &restrictions,
44 const goto_programt::targett &location)
45{
46 PRECONDITION(location->is_function_call());
47
48 // for each function call, we check if it is using a symbol we have
49 // restrictions for, and if so branch on its value and insert concrete calls
50 // to the restriction functions
51
52 // Check if this is calling a function pointer, and if so if it is one
53 // we have a restriction for
54 const auto &original_function = location->call_function();
55
56 if(!can_cast_expr<dereference_exprt>(original_function))
57 return;
58
59 // because we run the label function pointer calls transformation pass before
60 // this stage a dereference can only dereference a symbol expression
61 auto const &called_function_pointer =
62 to_dereference_expr(original_function).pointer();
63 PRECONDITION(can_cast_expr<symbol_exprt>(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());
67
68 if(restriction_iterator == restrictions.restrictions.end())
69 return;
70
71 const namespacet ns(symbol_table);
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());
75
77 message_handler,
78 symbol_table,
79 goto_program,
80 function_id,
81 location,
82 candidates);
83}
84} // namespace
85
87 std::string reason,
88 std::string correct_format)
89 : cprover_exception_baset(std::move(reason)),
90 correct_format(std::move(correct_format))
91{
92}
93
95{
96 std::string res;
97
98 res += "Invalid restriction";
99 res += "\nReason: " + reason;
100
101 if(!correct_format.empty())
102 {
103 res += "\nFormat: " + correct_format;
104 }
105
106 return res;
107}
108
110 const goto_modelt &goto_model,
112{
113 for(auto const &restriction : restrictions)
114 {
115 auto const function_pointer_sym =
116 goto_model.symbol_table.lookup(restriction.first);
117 if(function_pointer_sym == nullptr)
118 {
119 throw invalid_restriction_exceptiont{id2string(restriction.first) +
120 " not found in the symbol table"};
121 }
122 auto const &function_pointer_type = function_pointer_sym->type;
123 if(function_pointer_type.id() != ID_pointer)
124 {
125 throw invalid_restriction_exceptiont{"not a function pointer: " +
126 id2string(restriction.first)};
127 }
128 auto const &function_type =
129 to_pointer_type(function_pointer_type).base_type();
130 if(function_type.id() != ID_code)
131 {
132 throw invalid_restriction_exceptiont{"not a function pointer: " +
133 id2string(restriction.first)};
134 }
135 auto const &ns = namespacet{goto_model.symbol_table};
136 for(auto const &function_pointer_target : restriction.second)
137 {
138 auto const function_pointer_target_sym =
139 goto_model.symbol_table.lookup(function_pointer_target);
140 if(function_pointer_target_sym == nullptr)
141 {
143 "symbol not found: " + id2string(function_pointer_target)};
144 }
145 auto const &function_pointer_target_type =
146 function_pointer_target_sym->type;
147 if(function_pointer_target_type.id() != ID_code)
148 {
150 "not a function: " + id2string(function_pointer_target)};
151 }
152
154 true,
155 to_code_type(function_type),
156 to_code_type(function_pointer_target_type),
157 ns))
158 {
160 "type mismatch: `" + id2string(restriction.first) + "' points to `" +
161 type2c(function_type, ns) + "', but restriction `" +
162 id2string(function_pointer_target) + "' has type `" +
163 type2c(function_pointer_target_type, ns) + "'"};
164 }
165 }
166 }
167}
168
170 message_handlert &message_handler,
171 goto_modelt &goto_model,
172 const optionst &options)
173{
174 const auto restrictions = function_pointer_restrictionst::from_options(
175 options, goto_model, message_handler);
176 if(restrictions.restrictions.empty())
177 return;
178
179 for(auto &function_item : goto_model.goto_functions.function_map)
180 {
181 goto_functiont &goto_function = function_item.second;
182
183 for_each_function_call(goto_function, [&](const goto_programt::targett it) {
184 restrict_function_pointer(
185 message_handler,
186 goto_model.symbol_table,
187 goto_function.body,
188 function_item.first,
189 restrictions,
190 it);
191 });
192 }
193}
194
220
225{
226 auto &result = lhs;
227
228 for(auto const &restriction : rhs)
229 {
230 auto emplace_result = result.emplace(restriction.first, restriction.second);
231 if(!emplace_result.second)
232 {
233 for(auto const &target : restriction.second)
234 {
235 emplace_result.first->second.insert(target);
236 }
237 }
238 }
239
240 return result;
241}
242
245 const std::list<std::string> &restriction_opts,
246 const std::string &option,
247 const goto_modelt &goto_model)
248{
249 auto function_pointer_restrictions =
251
252 for(const std::string &restriction_opt : restriction_opts)
253 {
254 const auto restriction =
255 parse_function_pointer_restriction(restriction_opt, option, goto_model);
256
257 const bool inserted = function_pointer_restrictions
258 .emplace(restriction.first, restriction.second)
259 .second;
260
261 if(!inserted)
262 {
264 "function pointer restriction for `" + id2string(restriction.first) +
265 "' was specified twice"};
266 }
267 }
268
269 return function_pointer_restrictions;
270}
271
274 const std::list<std::string> &restriction_opts,
275 const goto_modelt &goto_model)
276{
278 restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT, goto_model);
279}
280
283 const std::list<std::string> &filenames,
284 const goto_modelt &goto_model,
285 message_handlert &message_handler)
286{
287 auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
288
289 for(auto const &filename : filenames)
290 {
291 auto const restrictions =
292 read_from_file(filename, goto_model, message_handler);
293
294 merged_restrictions = merge_function_pointer_restrictions(
295 std::move(merged_restrictions), restrictions.restrictions);
296 }
297
298 return merged_restrictions;
299}
300
305static std::string resolve_pointer_name(
306 const std::string &candidate,
307 const goto_modelt &goto_model)
308{
309 const auto last_dot = candidate.rfind('.');
310 if(
311 last_dot == std::string::npos || last_dot + 1 == candidate.size() ||
312 isdigit(candidate[last_dot + 1]))
313 {
314 return candidate;
315 }
316
317 std::string pointer_name = candidate;
318
319 const auto function_id = pointer_name.substr(0, last_dot);
320 const auto label = pointer_name.substr(last_dot + 1);
321
322 bool found = false;
323 const auto it = goto_model.goto_functions.function_map.find(function_id);
324 if(it != goto_model.goto_functions.function_map.end())
325 {
327 for(const auto &instruction : it->second.body.instructions)
328 {
329 if(
330 std::find(
331 instruction.labels.begin(), instruction.labels.end(), label) !=
332 instruction.labels.end())
333 {
334 location = instruction.source_location();
335 }
336
337 if(
338 instruction.is_function_call() &&
339 instruction.call_function().id() == ID_dereference &&
340 location.has_value() && instruction.source_location() == *location)
341 {
342 auto const &called_function_pointer =
343 to_dereference_expr(instruction.call_function()).pointer();
344 pointer_name =
345 id2string(to_symbol_expr(called_function_pointer).get_identifier());
346 found = true;
347 break;
348 }
349 }
350 }
351 if(!found)
352 {
354 "non-existent pointer name " + pointer_name,
355 "pointers should be identifiers or <function_name>.<label>"};
356 }
357
358 return pointer_name;
359}
360
363 const std::string &restriction_opt,
364 const std::string &option,
365 const goto_modelt &goto_model)
366{
367 // the format for restrictions is <pointer_name>/<target[,more_targets]*>
368 // exactly one pointer and at least one target
369 auto const pointer_name_end = restriction_opt.find('/');
370 auto const restriction_format_message =
371 "the format for restrictions is "
372 "<pointer_name>/<target[,more_targets]*>";
373
374 if(pointer_name_end == std::string::npos)
375 {
376 throw invalid_restriction_exceptiont{"couldn't find '/' in `" +
377 restriction_opt + "'",
378 restriction_format_message};
379 }
380
381 if(pointer_name_end == restriction_opt.size())
382 {
384 "couldn't find names of targets after '/' in `" + restriction_opt + "'",
385 restriction_format_message};
386 }
387
388 if(pointer_name_end == 0)
389 {
391 "couldn't find target name before '/' in `" + restriction_opt + "'"};
392 }
393
394 std::string pointer_name = resolve_pointer_name(
395 restriction_opt.substr(0, pointer_name_end), goto_model);
396
397 auto const target_names_substring =
398 restriction_opt.substr(pointer_name_end + 1);
399 auto const target_name_strings = split_string(target_names_substring, ',');
400
401 if(target_name_strings.size() == 1 && target_name_strings[0].empty())
402 {
404 "missing target list for function pointer restriction " + pointer_name,
405 restriction_format_message};
406 }
407
408 std::unordered_set<irep_idt> target_names;
409 target_names.insert(target_name_strings.begin(), target_name_strings.end());
410
411 for(auto const &target_name : target_names)
412 {
413 if(target_name == ID_empty_string)
414 {
416 "leading or trailing comma in restrictions for `" + pointer_name + "'",
417 restriction_format_message);
418 }
419 }
420
421 return std::make_pair(pointer_name, target_names);
422}
423
426 const goto_functiont &goto_function,
427 const function_pointer_restrictionst::restrictionst &by_name_restrictions,
428 const goto_programt::const_targett &location)
429{
430 PRECONDITION(location->is_function_call());
431
432 const exprt &function = location->call_function();
433
435 return {};
436
437 // the function pointer is guaranteed to be a symbol expression, as the
438 // label_function_pointer_call_sites() pass (which must be run before the
439 // function pointer restriction) replaces calls via complex pointer
440 // expressions by calls to a function pointer variable
441 auto const &function_pointer_call_site =
442 to_symbol_expr(to_dereference_expr(function).pointer());
443
444 const goto_programt::const_targett it = std::prev(location);
445
446 INVARIANT(
447 to_symbol_expr(it->assign_lhs()).get_identifier() ==
448 function_pointer_call_site.get_identifier(),
449 "called function pointer must have been assigned at the previous location");
450
451 if(!can_cast_expr<symbol_exprt>(it->assign_rhs()))
452 return {};
453
454 const auto &rhs = to_symbol_expr(it->assign_rhs());
455
456 const auto restriction = by_name_restrictions.find(rhs.get_identifier());
457
458 if(restriction != by_name_restrictions.end())
459 {
461 std::make_pair(
462 function_pointer_call_site.get_identifier(), restriction->second));
463 }
464
465 return {};
466}
467
469 const optionst &options,
470 const goto_modelt &goto_model,
471 message_handlert &message_handler)
472{
473 auto const restriction_opts =
475
476 restrictionst commandline_restrictions;
477 try
478 {
479 commandline_restrictions =
481 restriction_opts, goto_model);
483 goto_model, commandline_restrictions);
484 }
485 catch(const invalid_restriction_exceptiont &e)
486 {
488 static_cast<cprover_exception_baset>(e).what(),
491 }
492
493 restrictionst file_restrictions;
494 try
495 {
496 auto const restriction_file_opts =
499 restriction_file_opts, goto_model, message_handler);
500 typecheck_function_pointer_restrictions(goto_model, file_restrictions);
501 }
502 catch(const invalid_restriction_exceptiont &e)
503 {
505 }
506
507 restrictionst name_restrictions;
508 try
509 {
510 auto const restriction_name_opts =
513 restriction_name_opts, goto_model);
514 typecheck_function_pointer_restrictions(goto_model, name_restrictions);
515 }
516 catch(const invalid_restriction_exceptiont &e)
517 {
519 static_cast<cprover_exception_baset>(e).what(),
522 }
523
525 commandline_restrictions,
526 merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
527}
528
530 const jsont &json,
531 const goto_modelt &goto_model)
532{
534
535 if(!json.is_object())
536 {
537 throw deserialization_exceptiont{"top level item is not an object"};
538 }
539
540 for(auto const &restriction : to_json_object(json))
541 {
542 std::string pointer_name =
543 resolve_pointer_name(restriction.first, goto_model);
544 restrictions.emplace(irep_idt{pointer_name}, [&] {
545 if(!restriction.second.is_array())
546 {
547 throw deserialization_exceptiont{"Value of " + restriction.first +
548 " is not an array"};
549 }
550 auto possible_targets = std::unordered_set<irep_idt>{};
551 auto const &array = to_json_array(restriction.second);
552 std::transform(
553 array.begin(),
554 array.end(),
555 std::inserter(possible_targets, possible_targets.end()),
556 [&](const jsont &array_element) {
557 if(!array_element.is_string())
558 {
559 throw deserialization_exceptiont{
560 "Value of " + restriction.first +
561 "contains a non-string array element"};
562 }
563 return irep_idt{to_json_string(array_element).value};
564 });
565 return possible_targets;
566 }());
567 }
568
569 return function_pointer_restrictionst{restrictions};
570}
571
573 const std::string &filename,
574 const goto_modelt &goto_model,
575 message_handlert &message_handler)
576{
577 auto inFile = std::ifstream{filename};
578 jsont json;
579
580 if(parse_json(inFile, filename, message_handler, json))
581 {
583 "failed to read function pointer restrictions from " + filename};
584 }
585
586 return from_json(json, goto_model);
587}
588
590{
591 auto function_pointer_restrictions_json = jsont{};
592 auto &restrictions_json_object =
593 function_pointer_restrictions_json.make_object();
594
595 for(auto const &restriction : restrictions)
596 {
597 auto &targets_array =
598 restrictions_json_object[id2string(restriction.first)].make_array();
599 for(auto const &target : restriction.second)
600 {
601 targets_array.push_back(json_stringt{target});
602 }
603 }
604
605 return function_pointer_restrictions_json;
606}
607
609 const std::string &filename) const
610{
611 auto function_pointer_restrictions_json = to_json();
612
613 auto outFile = std::ofstream{filename};
614
615 if(!outFile)
616 {
617 throw system_exceptiont{"cannot open " + filename +
618 " for writing function pointer restrictions"};
619 }
620
621 function_pointer_restrictions_json.output(outFile);
622 // Ensure output file ends with a newline character.
623 outFile << '\n';
624}
625
628 const std::list<std::string> &restriction_name_opts,
629 const goto_modelt &goto_model)
630{
633 restriction_name_opts,
635 goto_model);
636
638 for(auto const &goto_function : goto_model.goto_functions.function_map)
639 {
640 for_each_function_call(
641 goto_function.second, [&](const goto_programt::const_targett it) {
642 const auto restriction = get_by_name_restriction(
643 goto_function.second, by_name_restrictions, it);
644
645 if(restriction)
646 {
647 restrictions.insert(*restriction);
648 }
649 });
650 }
651
652 return restrictions;
653}
virtual bool isset(char option) const
Definition cmdline.cpp:30
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
std::string reason
The reason this exception was generated.
Definition c_errors.h:83
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.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
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.
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)
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)
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)
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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)
Definition json.h:212
Definition json.h:27
json_arrayt & make_array()
Definition json.h:420
json_objectt & make_object()
Definition json.h:438
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
const value_listt & get_list_option(const std::string &option) const
Definition options.cpp:80
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
Definition std_expr.h:142
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Thrown when some external system fails unexpectedly.
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4160
Symbol Table + CFG.
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
json_objectt & to_json_object(jsont &json)
Definition json.h:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
STL namespace.
nonstd::optional< T > optionalt
Definition optional.h:35
Options.
API to expression classes for Pointers.
bool can_cast_expr< dereference_exprt >(const exprt &base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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)
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)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)