cprover
generate_function_bodies.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Replace bodies of goto functions
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
11 #include <util/arith_tools.h>
12 #include <util/format_expr.h>
13 #include <util/make_unique.h>
14 #include <util/string_utils.h>
15 
16 #include "remove_skip.h"
17 
19  goto_functiont &function,
20  symbol_tablet &symbol_table,
21  const irep_idt &function_name) const
22 {
23  PRECONDITION(!function.body_available());
24  generate_parameter_names(function, symbol_table, function_name);
25  generate_function_body_impl(function, symbol_table, function_name);
26 }
27 
29  goto_functiont &function,
30  symbol_tablet &symbol_table,
31  const irep_idt &function_name) const
32 {
33  const namespacet ns(symbol_table);
34  int param_counter = 0;
35  for(auto &parameter : function.type.parameters())
36  {
37  if(parameter.get_identifier().empty())
38  {
39  const std::string param_base_name =
40  parameter.get_base_name().empty()
41  ? "__param$" + std::to_string(param_counter++)
42  : id2string(parameter.get_base_name());
43  irep_idt new_param_identifier =
44  id2string(function_name) + "::" + param_base_name;
45  parameter.set_base_name(param_base_name);
46  parameter.set_identifier(new_param_identifier);
47  parameter_symbolt new_param_sym;
48  new_param_sym.name = new_param_identifier;
49  new_param_sym.type = parameter.type();
50  new_param_sym.base_name = param_base_name;
51  auto const &function_symbol = symbol_table.lookup_ref(function_name);
52  new_param_sym.mode = function_symbol.mode;
53  new_param_sym.module = function_symbol.module;
54  new_param_sym.location = function_symbol.location;
55  symbol_table.add(new_param_sym);
56  }
57  }
58  auto &function_symbol = symbol_table.get_writeable_ref(function_name);
59  function_symbol.type = function.type;
60 }
61 
63 {
64 protected:
66  goto_functiont &function,
67  const symbol_tablet &symbol_table,
68  const irep_idt &function_name) const override
69  {
70  auto const &function_symbol = symbol_table.lookup_ref(function_name);
71  // NOLINTNEXTLINE
72  auto add_instruction = [&]() {
73  auto instruction = function.body.add_instruction();
74  instruction->function = function_name;
75  instruction->source_location = function_symbol.location;
76  return instruction;
77  };
78  auto assume_instruction = add_instruction();
79  assume_instruction->make_assumption(false_exprt());
80  auto end_instruction = add_instruction();
81  end_instruction->make_end_function();
82  }
83 };
84 
86 {
87 protected:
89  goto_functiont &function,
90  const symbol_tablet &symbol_table,
91  const irep_idt &function_name) const override
92  {
93  auto const &function_symbol = symbol_table.lookup_ref(function_name);
94  // NOLINTNEXTLINE
95  auto add_instruction = [&]() {
96  auto instruction = function.body.add_instruction();
97  instruction->function = function_name;
98  instruction->source_location = function_symbol.location;
99  instruction->source_location.set_function(function_name);
100  return instruction;
101  };
102  auto assert_instruction = add_instruction();
103  assert_instruction->make_assertion(false_exprt());
104  const namespacet ns(symbol_table);
105  std::ostringstream comment_stream;
106  comment_stream << id2string(ID_assertion) << " "
107  << format(assert_instruction->guard);
108  assert_instruction->source_location.set_comment(comment_stream.str());
109  assert_instruction->source_location.set_property_class(ID_assertion);
110  auto end_instruction = add_instruction();
111  end_instruction->make_end_function();
112  }
113 };
114 
117 {
118 protected:
120  goto_functiont &function,
121  const symbol_tablet &symbol_table,
122  const irep_idt &function_name) const override
123  {
124  auto const &function_symbol = symbol_table.lookup_ref(function_name);
125  // NOLINTNEXTLINE
126  auto add_instruction = [&]() {
127  auto instruction = function.body.add_instruction();
128  instruction->function = function_name;
129  instruction->source_location = function_symbol.location;
130  instruction->source_location.set_function(function_name);
131  return instruction;
132  };
133  auto assert_instruction = add_instruction();
134  assert_instruction->make_assertion(false_exprt());
135  assert_instruction->source_location.set_function(function_name);
136  const namespacet ns(symbol_table);
137  std::ostringstream comment_stream;
138  comment_stream << id2string(ID_assertion) << " "
139  << format(assert_instruction->guard);
140  assert_instruction->source_location.set_comment(comment_stream.str());
141  assert_instruction->source_location.set_property_class(ID_assertion);
142  auto assume_instruction = add_instruction();
143  assume_instruction->make_assumption(false_exprt());
144  auto end_instruction = add_instruction();
145  end_instruction->make_end_function();
146  }
147 };
148 
150  private messaget
151 {
152 public:
154  std::vector<irep_idt> globals_to_havoc,
155  std::regex parameters_to_havoc,
161  {
162  }
163 
164 private:
166  const exprt &lhs,
167  const namespacet &ns,
168  const std::function<goto_programt::targett(void)> &add_instruction,
169  const irep_idt &function_name) const
170  {
171  // resolve type symbols
172  auto const lhs_type = ns.follow(lhs.type());
173  // skip constants
174  if(!lhs_type.get_bool(ID_C_constant))
175  {
176  // expand arrays, structs and union, everything else gets
177  // assigned nondet
178  if(lhs_type.id() == ID_struct || lhs_type.id() == ID_union)
179  {
180  // Note: In the case of unions it's often enough to assign
181  // just one member; However consider a case like
182  // union { struct { const int x; int y; } a;
183  // struct { int x; const int y; } b;};
184  // in this case both a.y and b.x must be assigned
185  // otherwise these parts stay constant even though
186  // they could've changed (note that type punning through
187  // unions is allowed in the C standard but forbidden in C++)
188  // so we're assigning all members even in the case of
189  // unions just to be safe
190  auto const lhs_struct_type = to_struct_union_type(lhs_type);
191  for(auto const &component : lhs_struct_type.components())
192  {
194  member_exprt(lhs, component.get_name(), component.type()),
195  ns,
196  add_instruction,
197  function_name);
198  }
199  }
200  else if(lhs_type.id() == ID_array)
201  {
202  auto const lhs_array_type = to_array_type(lhs_type);
203  if(!lhs_array_type.subtype().get_bool(ID_C_constant))
204  {
205  bool constant_known_array_size = lhs_array_type.size().is_constant();
206  if(!constant_known_array_size)
207  {
208  warning() << "Cannot havoc non-const array " << format(lhs)
209  << " in function " << function_name
210  << ": Unknown array size" << eom;
211  }
212  else
213  {
214  auto const array_size =
215  numeric_cast<mp_integer>(lhs_array_type.size());
216  INVARIANT(
217  array_size.has_value(),
218  "Array size should be known constant integer");
219  if(array_size.value() == 0)
220  {
221  // Pretty much the same thing as a unknown size array
222  // Technically not allowed by the C standard, but we model
223  // unknown size arrays in structs this way
224  warning() << "Cannot havoc non-const array " << format(lhs)
225  << " in function " << function_name << ": Array size 0"
226  << eom;
227  }
228  else
229  {
230  for(mp_integer i = 0; i < array_size.value(); ++i)
231  {
232  auto const index =
233  from_integer(i, lhs_array_type.size().type());
235  index_exprt(lhs, index, lhs_array_type.subtype()),
236  ns,
237  add_instruction,
238  function_name);
239  }
240  }
241  }
242  }
243  }
244  else
245  {
246  auto assign_instruction = add_instruction();
247  assign_instruction->make_assignment(
248  code_assignt(
249  lhs, side_effect_expr_nondett(lhs_type, lhs.source_location())));
250  }
251  }
252  }
253 
254 protected:
256  goto_functiont &function,
257  const symbol_tablet &symbol_table,
258  const irep_idt &function_name) const override
259  {
260  auto const &function_symbol = symbol_table.lookup_ref(function_name);
261  // NOLINTNEXTLINE
262  auto add_instruction = [&]() {
263  auto instruction = function.body.add_instruction();
264  instruction->function = function_name;
265  instruction->source_location = function_symbol.location;
266  return instruction;
267  };
268  const namespacet ns(symbol_table);
269  for(auto const &parameter : function.type.parameters())
270  {
271  if(
272  parameter.type().id() == ID_pointer &&
273  std::regex_match(
274  id2string(parameter.get_base_name()), parameters_to_havoc))
275  {
276  // if (param != nullptr) { *param = nondet(); }
277  auto goto_instruction = add_instruction();
280  symbol_exprt(parameter.get_identifier(), parameter.type()),
281  parameter.type().subtype()),
282  ns,
283  add_instruction,
284  function_name);
285  auto label_instruction = add_instruction();
286  goto_instruction->make_goto(
287  label_instruction,
288  equal_exprt(
289  symbol_exprt(parameter.get_identifier(), parameter.type()),
290  null_pointer_exprt(to_pointer_type(parameter.type()))));
291  label_instruction->make_skip();
292  }
293  }
294 
295  for(auto const &global_id : globals_to_havoc)
296  {
297  auto const &global_sym = symbol_table.lookup_ref(global_id);
299  symbol_exprt(global_sym.name, global_sym.type),
300  ns,
301  add_instruction,
302  function_name);
303  }
304  if(function.type.return_type() != void_typet())
305  {
306  auto return_instruction = add_instruction();
307  return_instruction->make_return();
308  return_instruction->code = code_returnt(
310  function.type.return_type(), function_symbol.location));
311  }
312  auto end_function_instruction = add_instruction();
313  end_function_instruction->make_end_function();
314 
315  remove_skip(function.body);
316  }
317 
318 private:
319  const std::vector<irep_idt> globals_to_havoc;
321 };
322 
323 class generate_function_bodies_errort : public std::runtime_error
324 {
325 public:
326  explicit generate_function_bodies_errort(const std::string &reason)
327  : runtime_error(reason)
328  {
329  }
330 };
331 
335 std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
336  const std::string &options,
337  const symbol_tablet &symbol_table,
338  message_handlert &message_handler)
339 {
340  if(options.empty() || options == "nondet-return")
341  {
342  return util_make_unique<havoc_generate_function_bodiest>(
343  std::vector<irep_idt>{}, std::regex{}, message_handler);
344  }
345 
346  if(options == "assume-false")
347  {
348  return util_make_unique<assume_false_generate_function_bodiest>();
349  }
350 
351  if(options == "assert-false")
352  {
353  return util_make_unique<assert_false_generate_function_bodiest>();
354  }
355 
356  if(options == "assert-false-assume-false")
357  {
358  return util_make_unique<
360  }
361 
362  const std::vector<std::string> option_components = split_string(options, ',');
363  if(!option_components.empty() && option_components[0] == "havoc")
364  {
365  std::regex globals_regex;
366  std::regex params_regex;
367  for(std::size_t i = 1; i < option_components.size(); ++i)
368  {
369  const std::vector<std::string> key_value_pair =
370  split_string(option_components[i], ':');
371  if(key_value_pair.size() != 2)
372  {
374  "Expected key_value_pair of form argument:value");
375  }
376  if(key_value_pair[0] == "globals")
377  {
378  globals_regex = key_value_pair[1];
379  }
380  else if(key_value_pair[0] == "params")
381  {
382  params_regex = key_value_pair[1];
383  }
384  else
385  {
387  "Unknown option \"" + key_value_pair[0] + "\"");
388  }
389  }
390  std::vector<irep_idt> globals_to_havoc;
391  namespacet ns(symbol_table);
392  messaget messages(message_handler);
393  const std::regex cprover_prefix = std::regex("__CPROVER.*");
394  for(auto const &symbol : symbol_table.symbols)
395  {
396  if(
397  symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
398  std::regex_match(id2string(symbol.first), globals_regex))
399  {
400  if(std::regex_match(id2string(symbol.first), cprover_prefix))
401  {
402  messages.warning() << "generate function bodies: "
403  << "matched global '" << id2string(symbol.first)
404  << "' begins with __CPROVER, "
405  << "havoc-ing this global may interfere"
406  << " with analysis" << messaget::eom;
407  }
408  globals_to_havoc.push_back(symbol.first);
409  }
410  }
411  return util_make_unique<havoc_generate_function_bodiest>(
412  std::move(globals_to_havoc), std::move(params_regex), message_handler);
413  }
414  throw generate_function_bodies_errort("Can't parse \"" + options + "\"");
415 }
416 
455  const std::regex &functions_regex,
456  const generate_function_bodiest &generate_function_body,
457  goto_modelt &model,
458  message_handlert &message_handler)
459 {
460  messaget messages(message_handler);
461  const std::regex cprover_prefix = std::regex("__CPROVER.*");
462  bool did_generate_body = false;
463  for(auto &function : model.goto_functions.function_map)
464  {
465  if(
466  !function.second.body_available() &&
467  std::regex_match(id2string(function.first), functions_regex))
468  {
469  if(std::regex_match(id2string(function.first), cprover_prefix))
470  {
471  messages.warning() << "generate function bodies: matched function '"
472  << id2string(function.first)
473  << "' begins with __CPROVER "
474  << "the generated body for this function "
475  << "may interfere with analysis" << messaget::eom;
476  }
477  did_generate_body = true;
478  generate_function_body.generate_function_body(
479  function.second, model.symbol_table, function.first);
480  }
481  }
482  if(!did_generate_body)
483  {
484  messages.warning()
485  << "generate function bodies: No function name matched regex"
486  << messaget::eom;
487  }
488 }
The void type, the same as empty_typet.
Definition: std_types.h:57
irep_idt name
The unique identifier.
Definition: symbol.h:40
virtual void generate_function_body_impl(goto_functiont &function, const symbol_tablet &symbol_table, const irep_idt &function_name) const =0
Produce a body for the passed function At this point the body of function is always empty,...
BigInt mp_integer
Definition: mp_arith.h:22
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, message_handlert &message_handler)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:172
irep_idt mode
Language mode.
Definition: symbol.h:49
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
The null pointer constant.
Definition: std_expr.h:4471
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Base class for replace_function_body implementations.
Extract member of struct or union.
Definition: std_expr.h:3890
mstreamt & warning() const
Definition: message.h:391
Equality.
Definition: std_expr.h:1484
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
instructionst::iterator targett
Definition: goto_program.h:414
Operator to dereference a pointer.
Definition: std_expr.h:3355
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
const symbolst & symbols
void generate_function_body_impl(goto_functiont &function, const symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
The Boolean constant false.
Definition: std_expr.h:4452
void generate_function_body_impl(goto_functiont &function, const symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
const std::vector< irep_idt > globals_to_havoc
void havoc_expr_rec(const exprt &lhs, const namespacet &ns, const std::function< goto_programt::targett(void)> &add_instruction, const irep_idt &function_name) const
static eomt eom
Definition: message.h:284
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior A list of currently accepted command line argumen...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
void generate_function_body_impl(goto_functiont &function, const symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Replace the function body with one based on the replace_function_body class being used.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
const source_locationt & source_location() const
Definition: expr.h:228
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
generate_function_bodies_errort(const std::string &reason)
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
const typet & subtype() const
Definition: type.h:38
Program Transformation.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
message_handlert * message_handler
Definition: message.h:426
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
A codet representing an assignment in the program.
Definition: std_code.h:256
Array index operator.
Definition: std_expr.h:1595
static format_containert< T > format(const T &o)
Definition: format.h:35
void generate_function_body_impl(goto_functiont &function, const symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...