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/expr_iterator.h>
16 #include <util/pointer_expr.h>
17 #include <util/string_utils.h>
18 
19 #include <algorithm>
20 #include <fstream>
21 #include <functional>
22 #include <iostream>
23 
24 namespace
25 {
26 source_locationt make_function_pointer_restriction_assertion_source_location(
27  source_locationt source_location,
29 {
30  std::stringstream comment;
31 
32  comment << "dereferenced function pointer at " << restriction.first
33  << " must be ";
34 
35  if(restriction.second.size() == 1)
36  {
37  comment << *restriction.second.begin();
38  }
39  else
40  {
41  comment << "one of [";
42 
44  comment, restriction.second.begin(), restriction.second.end(), ", ");
45 
46  comment << ']';
47  }
48 
49  source_location.set_comment(comment.str());
50  source_location.set_property_class(ID_assertion);
51 
52  return source_location;
53 }
54 
55 template <typename Handler, typename GotoFunctionT>
56 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
57 {
58  using targett = decltype(goto_function.body.instructions.begin());
60  goto_function,
61  [](targett target) { return target->is_function_call(); },
62  handler);
63 }
64 
65 void restrict_function_pointer(
66  goto_functiont &goto_function,
67  goto_modelt &goto_model,
68  const function_pointer_restrictionst &restrictions,
69  const goto_programt::targett &location)
70 {
71  PRECONDITION(location->is_function_call());
72 
73  // for each function call, we check if it is using a symbol we have
74  // restrictions for, and if so branch on its value and insert concrete calls
75  // to the restriction functions
76 
77  // Check if this is calling a function pointer, and if so if it is one
78  // we have a restriction for
79  const auto &original_function_call = location->get_function_call();
80 
81  if(!can_cast_expr<dereference_exprt>(original_function_call.function()))
82  return;
83 
84  // because we run the label function pointer calls transformation pass before
85  // this stage a dereference can only dereference a symbol expression
86  auto const &called_function_pointer =
87  to_dereference_expr(original_function_call.function()).pointer();
88  PRECONDITION(can_cast_expr<symbol_exprt>(called_function_pointer));
89  auto const &pointer_symbol = to_symbol_expr(called_function_pointer);
90  auto const restriction_iterator =
91  restrictions.restrictions.find(pointer_symbol.get_identifier());
92 
93  if(restriction_iterator == restrictions.restrictions.end())
94  return;
95 
96  auto const &restriction = *restriction_iterator;
97 
98  // this is intentionally a copy because we're about to change the
99  // instruction this iterator points to
100  // if we can, we will replace uses of it by a case distinction over
101  // given functions the function pointer can point to
102  auto const original_function_call_instruction = *location;
103 
104  *location = goto_programt::make_assertion(
105  false_exprt{},
106  make_function_pointer_restriction_assertion_source_location(
107  original_function_call_instruction.source_location, restriction));
108 
109  auto const assume_false_location = goto_function.body.insert_after(
110  location,
112  false_exprt{}, original_function_call_instruction.source_location));
113 
114  // this is mutable because we'll update this at the end of each
115  // loop iteration to always point at the start of the branch
116  // we created
117  auto else_location = location;
118 
119  auto const end_if_location = goto_function.body.insert_after(
120  assume_false_location, goto_programt::make_skip());
121 
122  for(auto const &restriction_target : restriction.second)
123  {
124  auto new_instruction = original_function_call_instruction;
125  // can't use get_function_call because that'll return a const ref
126  const symbol_exprt &function_pointer_target_symbol_expr =
127  goto_model.symbol_table.lookup_ref(restriction_target).symbol_expr();
128  to_code_function_call(new_instruction.code).function() =
129  function_pointer_target_symbol_expr;
130  auto const goto_end_if_location = goto_function.body.insert_before(
131  else_location,
133  end_if_location, original_function_call_instruction.source_location));
134  auto const replaced_instruction_location =
135  goto_function.body.insert_before(goto_end_if_location, new_instruction);
136  else_location = goto_function.body.insert_before(
137  replaced_instruction_location,
139  else_location,
140  notequal_exprt{pointer_symbol,
141  address_of_exprt{function_pointer_target_symbol_expr}}));
142  }
143 }
144 } // namespace
145 
147  invalid_restriction_exceptiont(std::string reason, std::string correct_format)
148  : reason(std::move(reason)), correct_format(std::move(correct_format))
149 {
150 }
151 
152 std::string
154 {
155  std::string res;
156 
157  res += "Invalid restriction";
158  res += "\nReason: " + reason;
159 
160  if(!correct_format.empty())
161  {
162  res += "\nFormat: " + correct_format;
163  }
164 
165  return res;
166 }
167 
169  const goto_modelt &goto_model,
171 {
172  for(auto const &restriction : restrictions)
173  {
174  auto const function_pointer_sym =
175  goto_model.symbol_table.lookup(restriction.first);
176  if(function_pointer_sym == nullptr)
177  {
178  throw invalid_restriction_exceptiont{id2string(restriction.first) +
179  " not found in the symbol table"};
180  }
181  auto const &function_pointer_type = function_pointer_sym->type;
182  if(function_pointer_type.id() != ID_pointer)
183  {
184  throw invalid_restriction_exceptiont{"not a function pointer: " +
185  id2string(restriction.first)};
186  }
187  auto const &function_type =
188  to_pointer_type(function_pointer_type).subtype();
189  if(function_type.id() != ID_code)
190  {
191  throw invalid_restriction_exceptiont{"not a function pointer: " +
192  id2string(restriction.first)};
193  }
194  auto const &ns = namespacet{goto_model.symbol_table};
195  for(auto const &function_pointer_target : restriction.second)
196  {
197  auto const function_pointer_target_sym =
198  goto_model.symbol_table.lookup(function_pointer_target);
199  if(function_pointer_target_sym == nullptr)
200  {
202  "symbol not found: " + id2string(function_pointer_target)};
203  }
204  auto const &function_pointer_target_type =
205  function_pointer_target_sym->type;
206  if(function_type != function_pointer_target_type)
207  {
209  "type mismatch: `" + id2string(restriction.first) + "' points to `" +
210  type2c(function_type, ns) + "', but restriction `" +
211  id2string(function_pointer_target) + "' has type `" +
212  type2c(function_pointer_target_type, ns) + "'"};
213  }
214  }
215  }
216 }
217 
219  goto_modelt &goto_model,
221 {
222  for(auto &function_item : goto_model.goto_functions.function_map)
223  {
224  goto_functiont &goto_function = function_item.second;
225 
226  for_each_function_call(goto_function, [&](const goto_programt::targett it) {
227  restrict_function_pointer(goto_function, goto_model, restrictions, it);
228  });
229  }
230 }
231 
233  const cmdlinet &cmdline,
234  optionst &options)
235 {
237  {
238  options.set_option(
241  }
242 
244  {
245  options.set_option(
248  }
249 
251  {
252  options.set_option(
255  }
256 }
257 
262 {
263  auto &result = lhs;
264 
265  for(auto const &restriction : rhs)
266  {
267  auto emplace_result = result.emplace(restriction.first, restriction.second);
268  if(!emplace_result.second)
269  {
270  for(auto const &target : restriction.second)
271  {
272  emplace_result.first->second.insert(target);
273  }
274  }
275  }
276 
277  return result;
278 }
279 
282  const std::list<std::string> &restriction_opts,
283  const std::string &option)
284 {
285  auto function_pointer_restrictions =
287 
288  for(const std::string &restriction_opt : restriction_opts)
289  {
290  const auto restriction =
291  parse_function_pointer_restriction(restriction_opt, option);
292 
293  const bool inserted = function_pointer_restrictions
294  .emplace(restriction.first, restriction.second)
295  .second;
296 
297  if(!inserted)
298  {
300  "function pointer restriction for `" + id2string(restriction.first) +
301  "' was specified twice"};
302  }
303  }
304 
305  return function_pointer_restrictions;
306 }
307 
310  const std::list<std::string> &restriction_opts)
311 {
313  restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT);
314 }
315 
318  const std::list<std::string> &filenames,
319  message_handlert &message_handler)
320 {
321  auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
322 
323  for(auto const &filename : filenames)
324  {
325  auto const restrictions = read_from_file(filename, message_handler);
326 
327  merged_restrictions = merge_function_pointer_restrictions(
328  std::move(merged_restrictions), restrictions.restrictions);
329  }
330 
331  return merged_restrictions;
332 }
333 
336  const std::string &restriction_opt,
337  const std::string &option)
338 {
339  // the format for restrictions is <pointer_name>/<target[,more_targets]*>
340  // exactly one pointer and at least one target
341  auto const pointer_name_end = restriction_opt.find('/');
342  auto const restriction_format_message =
343  "the format for restrictions is "
344  "<pointer_name>/<target[,more_targets]*>";
345 
346  if(pointer_name_end == std::string::npos)
347  {
348  throw invalid_restriction_exceptiont{"couldn't find '/' in `" +
349  restriction_opt + "'",
350  restriction_format_message};
351  }
352 
353  if(pointer_name_end == restriction_opt.size())
354  {
356  "couldn't find names of targets after '/' in `" + restriction_opt + "'",
357  restriction_format_message};
358  }
359 
360  if(pointer_name_end == 0)
361  {
363  "couldn't find target name before '/' in `" + restriction_opt + "'"};
364  }
365 
366  auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
367  auto const target_names_substring =
368  restriction_opt.substr(pointer_name_end + 1);
369  auto const target_name_strings = split_string(target_names_substring, ',');
370 
371  if(target_name_strings.size() == 1 && target_name_strings[0].empty())
372  {
374  "missing target list for function pointer restriction " + pointer_name,
375  restriction_format_message};
376  }
377 
378  std::unordered_set<irep_idt> target_names;
379  target_names.insert(target_name_strings.begin(), target_name_strings.end());
380 
381  for(auto const &target_name : target_names)
382  {
383  if(target_name == ID_empty_string)
384  {
386  "leading or trailing comma in restrictions for `" + pointer_name + "'",
387  restriction_format_message);
388  }
389  }
390 
391  return std::make_pair(pointer_name, target_names);
392 }
393 
396  const goto_functiont &goto_function,
397  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
398  const goto_programt::const_targett &location)
399 {
400  PRECONDITION(location->is_function_call());
401 
402  const exprt &function = location->get_function_call().function();
403 
404  if(!can_cast_expr<dereference_exprt>(function))
405  return {};
406 
407  // the function pointer is guaranteed to be a symbol expression, as the
408  // label_function_pointer_call_sites() pass (which must be run before the
409  // function pointer restriction) replaces calls via complex pointer
410  // expressions by calls to a function pointer variable
411  auto const &function_pointer_call_site =
412  to_symbol_expr(to_dereference_expr(function).pointer());
413 
414  const goto_programt::const_targett it = std::prev(location);
415 
416  const code_assignt &assign = it->get_assign();
417 
418  INVARIANT(
419  to_symbol_expr(assign.lhs()).get_identifier() ==
420  function_pointer_call_site.get_identifier(),
421  "called function pointer must have been assigned at the previous location");
422 
423  if(!can_cast_expr<symbol_exprt>(assign.rhs()))
424  return {};
425 
426  const auto &rhs = to_symbol_expr(assign.rhs());
427 
428  const auto restriction = by_name_restrictions.find(rhs.get_identifier());
429 
430  if(restriction != by_name_restrictions.end())
431  {
433  std::make_pair(
434  function_pointer_call_site.get_identifier(), restriction->second));
435  }
436 
437  return {};
438 }
439 
441  const optionst &options,
442  const goto_modelt &goto_model,
443  message_handlert &message_handler)
444 {
445  auto const restriction_opts =
447 
448  restrictionst commandline_restrictions;
449  try
450  {
451  commandline_restrictions =
454  goto_model, commandline_restrictions);
455  }
456  catch(const invalid_restriction_exceptiont &e)
457  {
460  }
461 
462  restrictionst file_restrictions;
463  try
464  {
465  auto const restriction_file_opts =
468  restriction_file_opts, message_handler);
469  typecheck_function_pointer_restrictions(goto_model, file_restrictions);
470  }
471  catch(const invalid_restriction_exceptiont &e)
472  {
473  throw deserialization_exceptiont{e.what()};
474  }
475 
476  restrictionst name_restrictions;
477  try
478  {
479  auto const restriction_name_opts =
481  name_restrictions = get_function_pointer_by_name_restrictions(
482  restriction_name_opts, goto_model);
483  typecheck_function_pointer_restrictions(goto_model, name_restrictions);
484  }
485  catch(const invalid_restriction_exceptiont &e)
486  {
489  }
490 
492  commandline_restrictions,
493  merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
494 }
495 
498 {
500 
501  if(!json.is_object())
502  {
503  throw deserialization_exceptiont{"top level item is not an object"};
504  }
505 
506  for(auto const &restriction : to_json_object(json))
507  {
508  restrictions.emplace(irep_idt{restriction.first}, [&] {
509  if(!restriction.second.is_array())
510  {
511  throw deserialization_exceptiont{"Value of " + restriction.first +
512  " is not an array"};
513  }
514  auto possible_targets = std::unordered_set<irep_idt>{};
515  auto const &array = to_json_array(restriction.second);
516  std::transform(
517  array.begin(),
518  array.end(),
519  std::inserter(possible_targets, possible_targets.end()),
520  [&](const jsont &array_element) {
521  if(!array_element.is_string())
522  {
523  throw deserialization_exceptiont{
524  "Value of " + restriction.first +
525  "contains a non-string array element"};
526  }
527  return irep_idt{to_json_string(array_element).value};
528  });
529  return possible_targets;
530  }());
531  }
532 
534 }
535 
537  const std::string &filename,
538  message_handlert &message_handler)
539 {
540  auto inFile = std::ifstream{filename};
541  jsont json;
542 
543  if(parse_json(inFile, filename, message_handler, json))
544  {
546  "failed to read function pointer restrictions from " + filename};
547  }
548 
549  return from_json(json);
550 }
551 
553 {
554  auto function_pointer_restrictions_json = jsont{};
555  auto &restrictions_json_object =
556  function_pointer_restrictions_json.make_object();
557 
558  for(auto const &restriction : restrictions)
559  {
560  auto &targets_array =
561  restrictions_json_object[id2string(restriction.first)].make_array();
562  for(auto const &target : restriction.second)
563  {
564  targets_array.push_back(json_stringt{target});
565  }
566  }
567 
568  return function_pointer_restrictions_json;
569 }
570 
572  const std::string &filename) const
573 {
574  auto function_pointer_restrictions_json = to_json();
575 
576  auto outFile = std::ofstream{filename};
577 
578  if(!outFile)
579  {
580  throw system_exceptiont{"cannot open " + filename +
581  " for writing function pointer restrictions"};
582  }
583 
584  function_pointer_restrictions_json.output(outFile);
585  // Ensure output file ends with a newline character.
586  outFile << '\n';
587 }
588 
591  const std::list<std::string> &restriction_name_opts,
592  const goto_modelt &goto_model)
593 {
594  function_pointer_restrictionst::restrictionst by_name_restrictions =
596  restriction_name_opts, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
597 
599  for(auto const &goto_function : goto_model.goto_functions.function_map)
600  {
601  for_each_function_call(
602  goto_function.second, [&](const goto_programt::const_targett it) {
603  const auto restriction = get_by_name_restriction(
604  goto_function.second, by_name_restrictions, it);
605 
606  if(restriction)
607  {
608  restrictions.insert(*restriction);
609  }
610  });
611  }
612 
613  return restrictions;
614 }
Operator to return the address of an object.
Definition: pointer_expr.h:200
virtual bool isset(char option) const
Definition: cmdline.cpp:29
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
exprt & function()
Definition: std_code.h:1250
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
const source_locationt & source_location() const
Definition: expr.h:234
The Boolean constant false.
Definition: std_expr.h:2726
std::string what() const override
A human readable description of what went wrong.
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
static function_pointer_restrictionst from_options(const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
Parse function pointer restrictions from command line.
static restrictionst get_function_pointer_by_name_restrictions(const std::list< std::string > &restriction_name_opts, const goto_modelt &goto_model)
Get function pointer restrictions from restrictions with named pointers.
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
static optionalt< restrictiont > get_by_name_restriction(const goto_functiont &goto_function, const function_pointer_restrictionst::restrictionst &by_name_restrictions, const goto_programt::const_targett &location)
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts)
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option)
static restrictionst parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option)
restrictionst::value_type restrictiont
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, message_handlert &message_handler)
void write_to_file(const std::string &filename) const
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
static function_pointer_restrictionst read_from_file(const std::string &filename, message_handlert &message_handler)
static function_pointer_restrictionst from_json(const jsont &json)
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
goto_programt body
Definition: goto_function.h:29
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
instructionst::iterator targett
Definition: goto_program.h:550
instructionst::const_iterator const_targett
Definition: goto_program.h:551
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:626
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:969
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:610
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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:92
Disequality.
Definition: std_expr.h:1198
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
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
Thrown when some external system fails unexpectedly.
const typet & subtype() const
Definition: type.h:47
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3937
Forward depth-first search iterators These iterators' copy operations are expensive,...
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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
API to expression classes for Pointers.
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:296
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
Given goto functions and a list of function parameters or globals that are function pointers with lis...
#define RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:174
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62