cprover
ansi_c_entry_point.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ansi_c_entry_point.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/config.h>
14 #include <util/message.h>
15 #include <util/pointer_expr.h>
16 #include <util/range.h>
17 #include <util/symbol_table.h>
18 
20 
22 
24 #include "expr2c.h"
25 
27  const code_typet::parameterst &parameters,
28  code_blockt &init_code,
29  symbol_tablet &symbol_table,
30  const c_object_factory_parameterst &object_factory_parameters)
31 {
32  exprt::operandst main_arguments;
33  main_arguments.resize(parameters.size());
34 
35  for(std::size_t param_number=0;
36  param_number<parameters.size();
37  param_number++)
38  {
39  const code_typet::parametert &p=parameters[param_number];
40  const irep_idt base_name=p.get_base_name().empty()?
41  ("argument#"+std::to_string(param_number)):p.get_base_name();
42 
43  main_arguments[param_number] = c_nondet_symbol_factory(
44  init_code,
45  symbol_table,
46  base_name,
47  p.type(),
48  p.source_location(),
49  object_factory_parameters,
51  }
52 
53  return main_arguments;
54 }
55 
57  const symbolt &function,
58  code_blockt &init_code,
59  symbol_tablet &symbol_table)
60 {
61  bool has_return_value =
62  to_code_type(function.type).return_type() != void_type();
63 
64  if(has_return_value)
65  {
66  const symbolt &return_symbol = symbol_table.lookup_ref("return'");
67 
68  // record return value
69  init_code.add(code_outputt{
70  return_symbol.base_name, return_symbol.symbol_expr(), function.location});
71  }
72 
73  #if 0
74  std::size_t i=0;
75 
76  for(const auto &p : parameters)
77  {
78  if(p.get_identifier().empty())
79  continue;
80 
81  irep_idt identifier=p.get_identifier();
82 
83  const symbolt &symbol=symbol_table.lookup(identifier);
84 
85  if(symbol.type.id()==ID_pointer)
86  {
87  codet output(ID_output);
88  output.operands().resize(2);
89 
90  output.op0()=
94  from_integer(0, index_type())));
95  output.op1()=symbol.symbol_expr();
96  output.add_source_location()=p.source_location();
97 
98  init_code.add(std::move(output));
99  }
100 
101  i++;
102  }
103  #endif
104 }
105 
107  symbol_tablet &symbol_table,
108  message_handlert &message_handler,
109  const c_object_factory_parameterst &object_factory_parameters)
110 {
111  // check if entry point is already there
112  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
113  symbol_table.symbols.end())
114  return false; // silently ignore
115 
116  irep_idt main_symbol;
117 
118  // find main symbol, if any is given
119  if(config.main.has_value())
120  {
121  std::list<irep_idt> matches;
122 
123  for(const auto &symbol_name_entry :
124  equal_range(symbol_table.symbol_base_map, config.main.value()))
125  {
126  // look it up
127  symbol_tablet::symbolst::const_iterator s_it =
128  symbol_table.symbols.find(symbol_name_entry.second);
129 
130  if(s_it==symbol_table.symbols.end())
131  continue;
132 
133  if(s_it->second.type.id()==ID_code)
134  matches.push_back(symbol_name_entry.second);
135  }
136 
137  if(matches.empty())
138  {
139  messaget message(message_handler);
140  message.error() << "main symbol '" << config.main.value() << "' not found"
141  << messaget::eom;
142  return true; // give up
143  }
144 
145  if(matches.size()>=2)
146  {
147  messaget message(message_handler);
148  message.error() << "main symbol '" << config.main.value()
149  << "' is ambiguous" << messaget::eom;
150  return true;
151  }
152 
153  main_symbol=matches.front();
154  }
155  else
156  main_symbol=ID_main;
157 
158  // look it up
159  symbol_tablet::symbolst::const_iterator s_it=
160  symbol_table.symbols.find(main_symbol);
161 
162  if(s_it==symbol_table.symbols.end())
163  return false; // give up silently
164 
165  const symbolt &symbol=s_it->second;
166 
167  // check if it has a body
168  if(symbol.value.is_nil())
169  {
170  messaget message(message_handler);
171  message.error() << "main symbol '" << id2string(main_symbol)
172  << "' has no body" << messaget::eom;
173  return false; // give up
174  }
175 
176  static_lifetime_init(symbol_table, symbol.location);
177 
179  symbol, symbol_table, message_handler, object_factory_parameters);
180 }
181 
192  const symbolt &symbol,
193  symbol_tablet &symbol_table,
194  message_handlert &message_handler,
195  const c_object_factory_parameterst &object_factory_parameters)
196 {
197  PRECONDITION(!symbol.value.is_nil());
198  code_blockt init_code;
199 
200  // add 'HIDE' label
201  init_code.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
202 
203  // build call to initialization function
204 
205  {
206  symbol_tablet::symbolst::const_iterator init_it=
207  symbol_table.symbols.find(INITIALIZE_FUNCTION);
208 
209  if(init_it==symbol_table.symbols.end())
210  {
211  messaget message(message_handler);
212  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
213  << messaget::eom;
214  return true;
215  }
216 
217  code_function_callt call_init(init_it->second.symbol_expr());
218  call_init.add_source_location()=symbol.location;
219 
220  init_code.add(std::move(call_init));
221  }
222 
223  // build call to main function
224 
225  code_function_callt call_main(symbol.symbol_expr());
226  call_main.add_source_location()=symbol.location;
227  call_main.function().add_source_location()=symbol.location;
228 
229  if(to_code_type(symbol.type).return_type() != void_type())
230  {
231  auxiliary_symbolt return_symbol;
232  return_symbol.mode=ID_C;
233  return_symbol.is_static_lifetime=false;
234  return_symbol.name="return'";
235  return_symbol.base_name = "return'";
236  return_symbol.type=to_code_type(symbol.type).return_type();
237 
238  symbol_table.add(return_symbol);
239  call_main.lhs()=return_symbol.symbol_expr();
240  }
241 
242  const code_typet::parameterst &parameters=
243  to_code_type(symbol.type).parameters();
244 
245  if(symbol.name==ID_main)
246  {
247  if(parameters.empty())
248  {
249  // ok
250  }
251  else if(parameters.size()==2 || parameters.size()==3)
252  {
253  namespacet ns(symbol_table);
254 
255  {
256  symbolt argc_symbol;
257 
258  argc_symbol.base_name = "argc'";
259  argc_symbol.name = "argc'";
260  argc_symbol.type = signed_int_type();
261  argc_symbol.is_static_lifetime = true;
262  argc_symbol.is_lvalue = true;
263  argc_symbol.mode = ID_C;
264 
265  auto r = symbol_table.insert(argc_symbol);
266  if(!r.second && r.first != argc_symbol)
267  {
268  messaget message(message_handler);
269  message.error() << "argc already exists but is not usable"
270  << messaget::eom;
271  return true;
272  }
273  }
274 
275  const symbolt &argc_symbol = ns.lookup("argc'");
276 
277  {
278  // we make the type of this thing an array of pointers
279  // need to add one to the size -- the array is terminated
280  // with NULL
281  const exprt one_expr = from_integer(1, argc_symbol.type);
282  const plus_exprt size_expr(argc_symbol.symbol_expr(), one_expr);
283  const array_typet argv_type(pointer_type(char_type()), size_expr);
284 
285  symbolt argv_symbol;
286 
287  argv_symbol.base_name = "argv'";
288  argv_symbol.name = "argv'";
289  argv_symbol.type = argv_type;
290  argv_symbol.is_static_lifetime = true;
291  argv_symbol.is_lvalue = true;
292  argv_symbol.mode = ID_C;
293 
294  auto r = symbol_table.insert(argv_symbol);
295  if(!r.second && r.first != argv_symbol)
296  {
297  messaget message(message_handler);
298  message.error() << "argv already exists but is not usable"
299  << messaget::eom;
300  return true;
301  }
302  }
303 
304  const symbolt &argv_symbol=ns.lookup("argv'");
305 
306  {
307  // assume argc is at least one
308  exprt one=from_integer(1, argc_symbol.type);
309 
311  argc_symbol.symbol_expr(), ID_ge, std::move(one));
312 
313  init_code.add(code_assumet(std::move(ge)));
314  }
315 
316  {
317  // assume argc is at most MAX/8-1
318  mp_integer upper_bound=
320 
321  exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
322 
324  argc_symbol.symbol_expr(), ID_le, std::move(bound_expr));
325 
326  init_code.add(code_assumet(std::move(le)));
327  }
328 
329  // record argc as an input
330  init_code.add(code_inputt{"argc", argc_symbol.symbol_expr()});
331 
332  if(parameters.size()==3)
333  {
334  {
335  symbolt envp_size_symbol;
336  envp_size_symbol.base_name = "envp_size'";
337  envp_size_symbol.name = "envp_size'";
338  envp_size_symbol.type = size_type();
339  envp_size_symbol.is_static_lifetime = true;
340  envp_size_symbol.mode = ID_C;
341 
342  if(!symbol_table.insert(std::move(envp_size_symbol)).second)
343  {
344  messaget message(message_handler);
345  message.error()
346  << "failed to insert envp_size symbol" << messaget::eom;
347  return true;
348  }
349  }
350 
351  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
352 
353  {
354  symbolt envp_symbol;
355  envp_symbol.base_name = "envp'";
356  envp_symbol.name = "envp'";
357  envp_symbol.type = array_typet(
358  pointer_type(char_type()), envp_size_symbol.symbol_expr());
359  envp_symbol.is_static_lifetime = true;
360  envp_symbol.mode = ID_C;
361 
362  if(!symbol_table.insert(std::move(envp_symbol)).second)
363  {
364  messaget message(message_handler);
365  message.error() << "failed to insert envp symbol" << messaget::eom;
366  return true;
367  }
368  }
369 
370  // assume envp_size is INTMAX-1
371  const mp_integer max =
372  to_integer_bitvector_type(envp_size_symbol.type).largest();
373 
374  exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
375 
377  envp_size_symbol.symbol_expr(), ID_le, std::move(max_minus_one));
378 
379  init_code.add(code_assumet(le));
380  }
381 
382  {
383  /* zero_string doesn't work yet */
384 
385  /*
386  exprt zero_string(ID_zero_string, array_typet());
387  zero_string.type().subtype()=char_type();
388  zero_string.type().set(ID_size, "infinity");
389  const index_exprt index(zero_string, from_integer(0, uint_type()));
390  exprt address_of =
391  typecast_exprt::conditional_cast(
392  address_of_exprt(index, pointer_type(char_type())),
393  argv_symbol.type.subtype());
394 
395  // assign argv[*] to the address of a string-object
396  array_of_exprt array_of(address_of, argv_symbol.type);
397 
398  init_code.copy_to_operands(
399  code_assignt(argv_symbol.symbol_expr(), array_of));
400  */
401  }
402 
403  {
404  // assign argv[argc] to NULL
405  const null_pointer_exprt null(
406  to_pointer_type(argv_symbol.type.subtype()));
407 
408  index_exprt index_expr(
409  argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
410 
411  // disable bounds check on that one
412  index_expr.set(ID_C_bounds_check, false);
413 
414  init_code.add(code_assignt(index_expr, null));
415  }
416 
417  if(parameters.size()==3)
418  {
419  const symbolt &envp_symbol=ns.lookup("envp'");
420  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
421 
422  // assume envp[envp_size] is NULL
423  null_pointer_exprt null(to_pointer_type(envp_symbol.type.subtype()));
424 
425  index_exprt index_expr(
426  envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
427  // disable bounds check on that one
428  index_expr.set(ID_C_bounds_check, false);
429 
430  equal_exprt is_null(std::move(index_expr), std::move(null));
431 
432  init_code.add(code_assumet(is_null));
433  }
434 
435  {
436  exprt::operandst &operands=call_main.arguments();
437 
438  if(parameters.size()==3)
439  operands.resize(3);
440  else
441  operands.resize(2);
442 
443  exprt &op0=operands[0];
444  exprt &op1=operands[1];
445 
447  argc_symbol.symbol_expr(), parameters[0].type());
448 
449  {
450  index_exprt index_expr(
451  argv_symbol.symbol_expr(), from_integer(0, index_type()));
452 
453  // disable bounds check on that one
454  index_expr.set(ID_C_bounds_check, false);
455 
456  const pointer_typet &pointer_type =
457  to_pointer_type(parameters[1].type());
458 
460  address_of_exprt(index_expr), pointer_type);
461  }
462 
463  // do we need envp?
464  if(parameters.size()==3)
465  {
466  const symbolt &envp_symbol=ns.lookup("envp'");
467 
468  index_exprt index_expr(
469  envp_symbol.symbol_expr(), from_integer(0, index_type()));
470 
471  const pointer_typet &pointer_type =
472  to_pointer_type(parameters[2].type());
473 
474  operands[2] = typecast_exprt::conditional_cast(
475  address_of_exprt(index_expr), pointer_type);
476  }
477  }
478  }
479  else
480  {
481  const namespacet ns{symbol_table};
482  const std::string main_signature = type2c(symbol.type, ns);
484  "'main' with signature '" + main_signature +
485  "' found,"
486  " but expecting one of:\n"
487  " int main(void)\n"
488  " int main(int argc, char *argv[])\n"
489  " int main(int argc, char *argv[], char *envp[])\n"
490  "If this is a non-standard main entry point please provide a custom\n"
491  "entry function and point to it via cbmc --function instead"};
492  }
493  }
494  else
495  {
496  // produce nondet arguments
498  parameters, init_code, symbol_table, object_factory_parameters);
499  }
500 
501  init_code.add(std::move(call_main));
502 
503  // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
504 
505  record_function_outputs(symbol, init_code, symbol_table);
506 
507  // add the entry point symbol
508  symbolt new_symbol;
509 
510  new_symbol.name=goto_functionst::entry_point();
511  new_symbol.type = code_typet({}, void_type());
512  new_symbol.value.swap(init_code);
513  new_symbol.mode=symbol.mode;
514 
515  if(!symbol_table.insert(std::move(new_symbol)).second)
516  {
517  messaget message(message_handler);
518  message.error() << "failed to insert main symbol" << messaget::eom;
519  return true;
520  }
521 
522  return false;
523 }
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
exprt::operandst build_function_environment(const code_typet::parameterst &parameters, code_blockt &init_code, symbol_tablet &symbol_table, const c_object_factory_parameterst &object_factory_parameters)
bool generate_ansi_c_start_function(const symbolt &symbol, symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Generate a _start function for a specific function.
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
symbol_exprt c_nondet_symbol_factory(code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &loc, const c_object_factory_parameterst &object_factory_parameters, const lifetimet lifetime)
Creates a symbol and generates code so that it can vary over all possible values for its type.
C Nondet Symbol Factory.
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet size_type()
Definition: c_types.cpp:58
empty_typet void_type()
Definition: c_types.cpp:253
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bitvector_typet char_type()
Definition: c_types.cpp:114
Operator to return the address of an object.
Definition: pointer_expr.h:341
Arrays with given size.
Definition: std_types.h:763
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A codet representing an assignment in the program.
Definition: std_code.h:293
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
A codet representing sequential composition of program statements.
Definition: std_code.h:168
void add(const codet &code)
Definition: std_code.h:206
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
argumentst & arguments()
Definition: std_code.h:1258
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:675
codet representation of a label for branch targets.
Definition: std_code.h:1405
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:722
A codet representing a skip statement.
Definition: std_code.h:268
const irep_idt & get_base_name() const
Definition: std_types.h:595
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
const parameterst & parameters() const
Definition: std_types.h:655
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
optionalt< std::string > main
Definition: config.h:260
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Array index operator.
Definition: std_expr.h:1328
mp_integer largest() const
Return the largest value that can be represented using this type.
Thrown when we can't handle something in an input source file.
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
bool is_nil() const
Definition: irep.h:387
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The null pointer constant.
Definition: pointer_expr.h:703
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
const typet & subtype() const
Definition: type.h:47
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
std::string type2c(const typet &type, const namespacet &ns)
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
static int8_t r
Definition: irep_hash.h:60
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
Definition: range.h:541
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#define INITIALIZE_FUNCTION
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
Expression which is true when the string is equal to the literal "null".
std::size_t int_width
Definition: config.h:110
Author: Diffblue Ltd.