cprover
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 static 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 
305 static 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 
434  if(!can_cast_expr<dereference_exprt>(function))
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  {
502  throw deserialization_exceptiont{e.what()};
503  }
504 
505  restrictionst name_restrictions;
506  try
507  {
508  auto const restriction_name_opts =
510  name_restrictions = get_function_pointer_by_name_restrictions(
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);
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 {
627  function_pointer_restrictionst::restrictionst by_name_restrictions =
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 }
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
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_arrayt & to_json_array(jsont &json)
Definition: json.h:426
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
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)