CBMC
restrict_function_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Restrict function pointers
4 
5 Author: 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 
26 namespace
27 {
28 template <typename Handler, typename GotoFunctionT>
29 void 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 
38 [[nodiscard]] static bool 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 false;
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 false;
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  return true;
85 }
86 } // namespace
87 
89  std::string reason,
90  std::string correct_format)
91  : cprover_exception_baset(std::move(reason)),
92  correct_format(std::move(correct_format))
93 {
94 }
95 
97 {
98  std::string res;
99 
100  res += "Invalid restriction";
101  res += "\nReason: " + reason;
102 
103  if(!correct_format.empty())
104  {
105  res += "\nFormat: " + correct_format;
106  }
107 
108  return res;
109 }
110 
112  const goto_modelt &goto_model,
114 {
115  for(auto const &restriction : restrictions)
116  {
117  auto const function_pointer_sym =
118  goto_model.symbol_table.lookup(restriction.first);
119  if(function_pointer_sym == nullptr)
120  {
121  throw invalid_restriction_exceptiont{id2string(restriction.first) +
122  " not found in the symbol table"};
123  }
124  auto const &function_pointer_type = function_pointer_sym->type;
125  if(function_pointer_type.id() != ID_pointer)
126  {
127  throw invalid_restriction_exceptiont{"not a function pointer: " +
128  id2string(restriction.first)};
129  }
130  auto const &function_type =
131  to_pointer_type(function_pointer_type).base_type();
132  if(function_type.id() != ID_code)
133  {
134  throw invalid_restriction_exceptiont{"not a function pointer: " +
135  id2string(restriction.first)};
136  }
137  auto const &ns = namespacet{goto_model.symbol_table};
138  for(auto const &function_pointer_target : restriction.second)
139  {
140  auto const function_pointer_target_sym =
141  goto_model.symbol_table.lookup(function_pointer_target);
142  if(function_pointer_target_sym == nullptr)
143  {
145  "symbol not found: " + id2string(function_pointer_target)};
146  }
147  auto const &function_pointer_target_type =
148  function_pointer_target_sym->type;
149  if(function_pointer_target_type.id() != ID_code)
150  {
152  "not a function: " + id2string(function_pointer_target)};
153  }
154 
156  true,
157  to_code_type(function_type),
158  to_code_type(function_pointer_target_type),
159  ns))
160  {
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) + "'"};
166  }
167  }
168  }
169 }
170 
172  message_handlert &message_handler,
173  goto_modelt &goto_model,
174  const optionst &options)
175 {
176  const auto restrictions = function_pointer_restrictionst::from_options(
177  options, goto_model, message_handler);
178  if(restrictions.restrictions.empty())
179  return;
180 
181  for(auto &function_item : goto_model.goto_functions.function_map)
182  {
183  goto_functiont &goto_function = function_item.second;
184 
185  bool did_something = false;
186  for_each_function_call(goto_function, [&](const goto_programt::targett it) {
187  did_something |= restrict_function_pointer(
188  message_handler,
189  goto_model.symbol_table,
190  goto_function.body,
191  function_item.first,
192  restrictions,
193  it);
194  });
195 
196  if(did_something)
197  goto_function.body.update();
198  }
199 }
200 
202  const cmdlinet &cmdline,
203  optionst &options)
204 {
206  {
207  options.set_option(
210  }
211 
213  {
214  options.set_option(
217  }
218 
220  {
221  options.set_option(
224  }
225 }
226 
231 {
232  auto &result = lhs;
233 
234  for(auto const &restriction : rhs)
235  {
236  auto emplace_result = result.emplace(restriction.first, restriction.second);
237  if(!emplace_result.second)
238  {
239  for(auto const &target : restriction.second)
240  {
241  emplace_result.first->second.insert(target);
242  }
243  }
244  }
245 
246  return result;
247 }
248 
251  const std::list<std::string> &restriction_opts,
252  const std::string &option,
253  const goto_modelt &goto_model)
254 {
255  auto function_pointer_restrictions =
257 
258  for(const std::string &restriction_opt : restriction_opts)
259  {
260  const auto restriction =
261  parse_function_pointer_restriction(restriction_opt, option, goto_model);
262 
263  const bool inserted = function_pointer_restrictions
264  .emplace(restriction.first, restriction.second)
265  .second;
266 
267  if(!inserted)
268  {
270  "function pointer restriction for `" + id2string(restriction.first) +
271  "' was specified twice"};
272  }
273  }
274 
275  return function_pointer_restrictions;
276 }
277 
280  const std::list<std::string> &restriction_opts,
281  const goto_modelt &goto_model)
282 {
284  restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT, goto_model);
285 }
286 
289  const std::list<std::string> &filenames,
290  const goto_modelt &goto_model,
291  message_handlert &message_handler)
292 {
293  auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
294 
295  for(auto const &filename : filenames)
296  {
297  auto const restrictions =
298  read_from_file(filename, goto_model, message_handler);
299 
300  merged_restrictions = merge_function_pointer_restrictions(
301  std::move(merged_restrictions), restrictions.restrictions);
302  }
303 
304  return merged_restrictions;
305 }
306 
311 static std::string resolve_pointer_name(
312  const std::string &candidate,
313  const goto_modelt &goto_model)
314 {
315  const auto last_dot = candidate.rfind('.');
316  if(
317  last_dot == std::string::npos || last_dot + 1 == candidate.size() ||
318  isdigit(candidate[last_dot + 1]))
319  {
320  return candidate;
321  }
322 
323  std::string pointer_name = candidate;
324 
325  const auto function_id = pointer_name.substr(0, last_dot);
326  const auto label = pointer_name.substr(last_dot + 1);
327 
328  bool found = false;
329  const auto it = goto_model.goto_functions.function_map.find(function_id);
330  if(it != goto_model.goto_functions.function_map.end())
331  {
332  std::optional<source_locationt> location;
333  for(const auto &instruction : it->second.body.instructions)
334  {
335  if(
336  std::find(
337  instruction.labels.begin(), instruction.labels.end(), label) !=
338  instruction.labels.end())
339  {
340  location = instruction.source_location();
341  }
342 
343  if(
344  instruction.is_function_call() &&
345  instruction.call_function().id() == ID_dereference &&
346  location.has_value() && instruction.source_location() == *location)
347  {
348  auto const &called_function_pointer =
349  to_dereference_expr(instruction.call_function()).pointer();
350  pointer_name =
351  id2string(to_symbol_expr(called_function_pointer).get_identifier());
352  found = true;
353  break;
354  }
355  }
356  }
357  if(!found)
358  {
360  "non-existent pointer name " + pointer_name,
361  "pointers should be identifiers or <function_name>.<label>"};
362  }
363 
364  return pointer_name;
365 }
366 
369  const std::string &restriction_opt,
370  const std::string &option,
371  const goto_modelt &goto_model)
372 {
373  // the format for restrictions is <pointer_name>/<target[,more_targets]*>
374  // exactly one pointer and at least one target
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]*>";
379 
380  if(pointer_name_end == std::string::npos)
381  {
382  throw invalid_restriction_exceptiont{"couldn't find '/' in `" +
383  restriction_opt + "'",
384  restriction_format_message};
385  }
386 
387  if(pointer_name_end == restriction_opt.size())
388  {
390  "couldn't find names of targets after '/' in `" + restriction_opt + "'",
391  restriction_format_message};
392  }
393 
394  if(pointer_name_end == 0)
395  {
397  "couldn't find target name before '/' in `" + restriction_opt + "'"};
398  }
399 
400  std::string pointer_name = resolve_pointer_name(
401  restriction_opt.substr(0, pointer_name_end), goto_model);
402 
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, ',');
406 
407  if(target_name_strings.size() == 1 && target_name_strings[0].empty())
408  {
410  "missing target list for function pointer restriction " + pointer_name,
411  restriction_format_message};
412  }
413 
414  std::unordered_set<irep_idt> target_names;
415  target_names.insert(target_name_strings.begin(), target_name_strings.end());
416 
417  for(auto const &target_name : target_names)
418  {
419  if(target_name == ID_empty_string)
420  {
422  "leading or trailing comma in restrictions for `" + pointer_name + "'",
423  restriction_format_message);
424  }
425  }
426 
427  return std::make_pair(pointer_name, target_names);
428 }
429 
430 std::optional<function_pointer_restrictionst::restrictiont>
432  const goto_functiont &goto_function,
433  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
434  const goto_programt::const_targett &location)
435 {
436  PRECONDITION(location->is_function_call());
437 
438  const exprt &function = location->call_function();
439 
440  if(!can_cast_expr<dereference_exprt>(function))
441  return {};
442 
443  // the function pointer is guaranteed to be a symbol expression, as the
444  // label_function_pointer_call_sites() pass (which must be run before the
445  // function pointer restriction) replaces calls via complex pointer
446  // expressions by calls to a function pointer variable
447  auto const &function_pointer_call_site =
448  to_symbol_expr(to_dereference_expr(function).pointer());
449 
450  const goto_programt::const_targett it = std::prev(location);
451 
452  INVARIANT(
453  to_symbol_expr(it->assign_lhs()).get_identifier() ==
454  function_pointer_call_site.get_identifier(),
455  "called function pointer must have been assigned at the previous location");
456 
457  if(!can_cast_expr<symbol_exprt>(it->assign_rhs()))
458  return {};
459 
460  const auto &rhs = to_symbol_expr(it->assign_rhs());
461 
462  const auto restriction = by_name_restrictions.find(rhs.get_identifier());
463 
464  if(restriction != by_name_restrictions.end())
465  {
466  return std::optional<function_pointer_restrictionst::restrictiont>(
467  std::make_pair(
468  function_pointer_call_site.get_identifier(), restriction->second));
469  }
470 
471  return {};
472 }
473 
475  const optionst &options,
476  const goto_modelt &goto_model,
477  message_handlert &message_handler)
478 {
479  auto const restriction_opts =
481 
482  restrictionst commandline_restrictions;
483  try
484  {
485  commandline_restrictions =
487  restriction_opts, goto_model);
489  goto_model, commandline_restrictions);
490  }
491  catch(const invalid_restriction_exceptiont &e)
492  {
494  static_cast<cprover_exception_baset>(e).what(),
496  e.correct_format};
497  }
498 
499  restrictionst file_restrictions;
500  try
501  {
502  auto const restriction_file_opts =
505  restriction_file_opts, goto_model, message_handler);
506  typecheck_function_pointer_restrictions(goto_model, file_restrictions);
507  }
508  catch(const invalid_restriction_exceptiont &e)
509  {
510  throw deserialization_exceptiont{e.what()};
511  }
512 
513  restrictionst name_restrictions;
514  try
515  {
516  auto const restriction_name_opts =
518  name_restrictions = get_function_pointer_by_name_restrictions(
519  restriction_name_opts, goto_model);
520  typecheck_function_pointer_restrictions(goto_model, name_restrictions);
521  }
522  catch(const invalid_restriction_exceptiont &e)
523  {
525  static_cast<cprover_exception_baset>(e).what(),
527  e.correct_format};
528  }
529 
531  commandline_restrictions,
532  merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
533 }
534 
536  const jsont &json,
537  const goto_modelt &goto_model)
538 {
540 
541  if(!json.is_object())
542  {
543  throw deserialization_exceptiont{"top level item is not an object"};
544  }
545 
546  for(auto const &restriction : to_json_object(json))
547  {
548  std::string pointer_name =
549  resolve_pointer_name(restriction.first, goto_model);
550  restrictions.emplace(irep_idt{pointer_name}, [&] {
551  if(!restriction.second.is_array())
552  {
553  throw deserialization_exceptiont{"Value of " + restriction.first +
554  " is not an array"};
555  }
556  auto possible_targets = std::unordered_set<irep_idt>{};
557  auto const &array = to_json_array(restriction.second);
559  array.begin(),
560  array.end(),
561  std::inserter(possible_targets, possible_targets.end()),
562  [&](const jsont &array_element) {
563  if(!array_element.is_string())
564  {
565  throw deserialization_exceptiont{
566  "Value of " + restriction.first +
567  "contains a non-string array element"};
568  }
569  return irep_idt{to_json_string(array_element).value};
570  });
571  return possible_targets;
572  }());
573  }
574 
575  return function_pointer_restrictionst{restrictions};
576 }
577 
579  const std::string &filename,
580  const goto_modelt &goto_model,
581  message_handlert &message_handler)
582 {
583  auto inFile = std::ifstream{filename};
584  jsont json;
585 
586  if(parse_json(inFile, filename, message_handler, json))
587  {
589  "failed to read function pointer restrictions from " + filename};
590  }
591 
592  return from_json(json, goto_model);
593 }
594 
596 {
597  auto function_pointer_restrictions_json = jsont{};
598  auto &restrictions_json_object =
599  function_pointer_restrictions_json.make_object();
600 
601  for(auto const &restriction : restrictions)
602  {
603  auto &targets_array =
604  restrictions_json_object[id2string(restriction.first)].make_array();
605  for(auto const &target : restriction.second)
606  {
607  targets_array.push_back(json_stringt{target});
608  }
609  }
610 
611  return function_pointer_restrictions_json;
612 }
613 
615  const std::string &filename) const
616 {
617  auto function_pointer_restrictions_json = to_json();
618 
619  auto outFile = std::ofstream{filename};
620 
621  if(!outFile)
622  {
623  throw system_exceptiont{"cannot open " + filename +
624  " for writing function pointer restrictions"};
625  }
626 
627  function_pointer_restrictions_json.output(outFile);
628  // Ensure output file ends with a newline character.
629  outFile << '\n';
630 }
631 
634  const std::list<std::string> &restriction_name_opts,
635  const goto_modelt &goto_model)
636 {
637  function_pointer_restrictionst::restrictionst by_name_restrictions =
639  restriction_name_opts,
641  goto_model);
642 
644  for(auto const &goto_function : goto_model.goto_functions.function_map)
645  {
646  for_each_function_call(
647  goto_function.second, [&](const goto_programt::const_targett it) {
648  const auto restriction = get_by_name_restriction(
649  goto_function.second, by_name_restrictions, it);
650 
651  if(restriction)
652  {
653  restrictions.insert(*restriction);
654  }
655  });
656  }
657 
658  return restrictions;
659 }
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
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:38
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)
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...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
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.
Definition: goto_program.h:73
void update()
Update all indices.
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
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:418
json_objectt & make_object()
Definition: json.h:436
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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:160
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.
int isdigit(int c)
Definition: ctype.c:24
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4171
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:44
json_arrayt & to_json_array(jsont &json)
Definition: json.h:424
json_objectt & to_json_object(jsont &json)
Definition: json.h:442
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:27
Options.
API to expression classes for Pointers.
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:874
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
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
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:256
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)