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 true);
84}
85} // namespace
86
88 std::string reason,
89 std::string correct_format)
90 : reason(std::move(reason)), 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
196 const cmdlinet &cmdline,
197 optionst &options)
198{
200 {
201 options.set_option(
204 }
205
207 {
208 options.set_option(
211 }
212
214 {
215 options.set_option(
218 }
219}
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 {
489 }
490
491 restrictionst file_restrictions;
492 try
493 {
494 auto const restriction_file_opts =
497 restriction_file_opts, goto_model, message_handler);
498 typecheck_function_pointer_restrictions(goto_model, file_restrictions);
499 }
500 catch(const invalid_restriction_exceptiont &e)
501 {
503 }
504
505 restrictionst name_restrictions;
506 try
507 {
508 auto const restriction_name_opts =
511 restriction_name_opts, goto_model);
512 typecheck_function_pointer_restrictions(goto_model, name_restrictions);
513 }
514 catch(const invalid_restriction_exceptiont &e)
515 {
518 }
519
521 commandline_restrictions,
522 merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
523}
524
526 const jsont &json,
527 const goto_modelt &goto_model)
528{
530
531 if(!json.is_object())
532 {
533 throw deserialization_exceptiont{"top level item is not an object"};
534 }
535
536 for(auto const &restriction : to_json_object(json))
537 {
538 std::string pointer_name =
539 resolve_pointer_name(restriction.first, goto_model);
540 restrictions.emplace(irep_idt{pointer_name}, [&] {
541 if(!restriction.second.is_array())
542 {
543 throw deserialization_exceptiont{"Value of " + restriction.first +
544 " is not an array"};
545 }
546 auto possible_targets = std::unordered_set<irep_idt>{};
547 auto const &array = to_json_array(restriction.second);
548 std::transform(
549 array.begin(),
550 array.end(),
551 std::inserter(possible_targets, possible_targets.end()),
552 [&](const jsont &array_element) {
553 if(!array_element.is_string())
554 {
555 throw deserialization_exceptiont{
556 "Value of " + restriction.first +
557 "contains a non-string array element"};
558 }
559 return irep_idt{to_json_string(array_element).value};
560 });
561 return possible_targets;
562 }());
563 }
564
565 return function_pointer_restrictionst{restrictions};
566}
567
569 const std::string &filename,
570 const goto_modelt &goto_model,
571 message_handlert &message_handler)
572{
573 auto inFile = std::ifstream{filename};
574 jsont json;
575
576 if(parse_json(inFile, filename, message_handler, json))
577 {
579 "failed to read function pointer restrictions from " + filename};
580 }
581
582 return from_json(json, goto_model);
583}
584
586{
587 auto function_pointer_restrictions_json = jsont{};
588 auto &restrictions_json_object =
589 function_pointer_restrictions_json.make_object();
590
591 for(auto const &restriction : restrictions)
592 {
593 auto &targets_array =
594 restrictions_json_object[id2string(restriction.first)].make_array();
595 for(auto const &target : restriction.second)
596 {
597 targets_array.push_back(json_stringt{target});
598 }
599 }
600
601 return function_pointer_restrictions_json;
602}
603
605 const std::string &filename) const
606{
607 auto function_pointer_restrictions_json = to_json();
608
609 auto outFile = std::ofstream{filename};
610
611 if(!outFile)
612 {
613 throw system_exceptiont{"cannot open " + filename +
614 " for writing function pointer restrictions"};
615 }
616
617 function_pointer_restrictions_json.output(outFile);
618 // Ensure output file ends with a newline character.
619 outFile << '\n';
620}
621
624 const std::list<std::string> &restriction_name_opts,
625 const goto_modelt &goto_model)
626{
629 restriction_name_opts,
631 goto_model);
632
634 for(auto const &goto_function : goto_model.goto_functions.function_map)
635 {
636 for_each_function_call(
637 goto_function.second, [&](const goto_programt::const_targett it) {
638 const auto restriction = get_by_name_restriction(
639 goto_function.second, by_name_restrictions, it);
640
641 if(restriction)
642 {
643 restrictions.insert(*restriction);
644 }
645 });
646 }
647
648 return restrictions;
649}
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
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:37
Base class for all expressions.
Definition: expr.h:54
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)
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)
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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.
Definition: pointer_expr.h:35
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
Thrown when some external system fails unexpectedly.
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4027
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)
Definition: json_parser.cpp:16
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)
Definition: pointer_expr.h:688
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
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
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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:173
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
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)
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target, const std::set< symbol_exprt > &functions, goto_modelt &goto_model)