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(lhs, side_effect_expr_nondett(lhs_type)));
249  }
250  }
251  }
252 
253 protected:
255  goto_functiont &function,
256  const symbol_tablet &symbol_table,
257  const irep_idt &function_name) const override
258  {
259  auto const &function_symbol = symbol_table.lookup_ref(function_name);
260  // NOLINTNEXTLINE
261  auto add_instruction = [&]() {
262  auto instruction = function.body.add_instruction();
263  instruction->function = function_name;
264  instruction->source_location = function_symbol.location;
265  return instruction;
266  };
267  const namespacet ns(symbol_table);
268  for(auto const &parameter : function.type.parameters())
269  {
270  if(
271  parameter.type().id() == ID_pointer &&
272  std::regex_match(
273  id2string(parameter.get_base_name()), parameters_to_havoc))
274  {
275  // if (param != nullptr) { *param = nondet(); }
276  auto goto_instruction = add_instruction();
279  symbol_exprt(parameter.get_identifier(), parameter.type()),
280  parameter.type().subtype()),
281  ns,
282  add_instruction,
283  function_name);
284  auto label_instruction = add_instruction();
285  goto_instruction->make_goto(
286  label_instruction,
287  equal_exprt(
288  symbol_exprt(parameter.get_identifier(), parameter.type()),
289  null_pointer_exprt(to_pointer_type(parameter.type()))));
290  label_instruction->make_skip();
291  }
292  }
293 
294  for(auto const &global_id : globals_to_havoc)
295  {
296  auto const &global_sym = symbol_table.lookup_ref(global_id);
298  symbol_exprt(global_sym.name, global_sym.type),
299  ns,
300  add_instruction,
301  function_name);
302  }
303  if(function.type.return_type() != void_typet())
304  {
305  auto return_instruction = add_instruction();
306  return_instruction->make_return();
307  return_instruction->code =
308  code_returnt(side_effect_expr_nondett(function.type.return_type()));
309  }
310  auto end_function_instruction = add_instruction();
311  end_function_instruction->make_end_function();
312 
313  remove_skip(function.body);
314  }
315 
316 private:
317  const std::vector<irep_idt> globals_to_havoc;
319 };
320 
321 class generate_function_bodies_errort : public std::runtime_error
322 {
323 public:
324  explicit generate_function_bodies_errort(const std::string &reason)
325  : runtime_error(reason)
326  {
327  }
328 };
329 
333 std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
334  const std::string &options,
335  const symbol_tablet &symbol_table,
337 {
338  if(options.empty() || options == "nondet-return")
339  {
340  return util_make_unique<havoc_generate_function_bodiest>(
341  std::vector<irep_idt>{}, std::regex{}, message_handler);
342  }
343 
344  if(options == "assume-false")
345  {
346  return util_make_unique<assume_false_generate_function_bodiest>();
347  }
348 
349  if(options == "assert-false")
350  {
351  return util_make_unique<assert_false_generate_function_bodiest>();
352  }
353 
354  if(options == "assert-false-assume-false")
355  {
356  return util_make_unique<
358  }
359 
360  const std::vector<std::string> option_components = split_string(options, ',');
361  if(!option_components.empty() && option_components[0] == "havoc")
362  {
363  std::regex globals_regex;
364  std::regex params_regex;
365  for(std::size_t i = 1; i < option_components.size(); ++i)
366  {
367  const std::vector<std::string> key_value_pair =
368  split_string(option_components[i], ':');
369  if(key_value_pair.size() != 2)
370  {
372  "Expected key_value_pair of form argument:value");
373  }
374  if(key_value_pair[0] == "globals")
375  {
376  globals_regex = key_value_pair[1];
377  }
378  else if(key_value_pair[0] == "params")
379  {
380  params_regex = key_value_pair[1];
381  }
382  else
383  {
385  "Unknown option \"" + key_value_pair[0] + "\"");
386  }
387  }
388  std::vector<irep_idt> globals_to_havoc;
389  namespacet ns(symbol_table);
390  messaget messages(message_handler);
391  const std::regex cprover_prefix = std::regex("__CPROVER.*");
392  for(auto const &symbol : symbol_table.symbols)
393  {
394  if(
395  symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
396  std::regex_match(id2string(symbol.first), globals_regex))
397  {
398  if(std::regex_match(id2string(symbol.first), cprover_prefix))
399  {
400  messages.warning() << "generate function bodies: "
401  << "matched global '" << id2string(symbol.first)
402  << "' begins with __CPROVER, "
403  << "havoc-ing this global may interfere"
404  << " with analysis" << messaget::eom;
405  }
406  globals_to_havoc.push_back(symbol.first);
407  }
408  }
409  return util_make_unique<havoc_generate_function_bodiest>(
410  std::move(globals_to_havoc), std::move(params_regex), message_handler);
411  }
412  throw generate_function_bodies_errort("Can't parse \"" + options + "\"");
413 }
414 
453  const std::regex &functions_regex,
454  const generate_function_bodiest &generate_function_body,
455  goto_modelt &model,
457 {
458  messaget messages(message_handler);
459  const std::regex cprover_prefix = std::regex("__CPROVER.*");
460  bool did_generate_body = false;
461  for(auto &function : model.goto_functions.function_map)
462  {
463  if(
464  !function.second.body_available() &&
465  std::regex_match(id2string(function.first), functions_regex))
466  {
467  if(std::regex_match(id2string(function.first), cprover_prefix))
468  {
469  messages.warning() << "generate function bodies: matched function '"
470  << id2string(function.first)
471  << "' begins with __CPROVER "
472  << "the generated body for this function "
473  << "may interfere with analysis" << messaget::eom;
474  }
475  did_generate_body = true;
476  generate_function_body.generate_function_body(
477  function.second, model.symbol_table, function.first);
478  }
479  }
480  if(!did_generate_body)
481  {
482  messages.warning()
483  << "generate function bodies: No function name matched regex"
484  << messaget::eom;
485  }
486 }
The void type.
Definition: std_types.h:64
irep_idt name
The unique identifier.
Definition: symbol.h:43
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:43
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:161
irep_idt mode
Language mode.
Definition: symbol.h:52
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:4520
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
function_mapt function_map
typet & type()
Definition: expr.h:56
STL namespace.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
Base class for replace_function_body implementations.
Extract member of struct or union.
Definition: std_expr.h:3871
mstreamt & warning() const
Definition: message.h:307
equality
Definition: std_expr.h:1354
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:397
Operator to dereference a pointer.
Definition: std_expr.h:3284
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:122
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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:4499
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...
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
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:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
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 generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
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 generic typet to a struct_union_typet.
Definition: std_types.h:280
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
generate_function_bodies_errort(const std::string &reason)
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Return from a function.
Definition: std_code.h:893
const typet & subtype() const
Definition: type.h:33
Program Transformation.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
message_handlert * message_handler
Definition: message.h:342
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Assignment.
Definition: std_code.h:195
array index operator
Definition: std_expr.h:1462
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...