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 <cassert>
12 #include <cstdlib>
13 
14 #include <util/namespace.h>
15 #include <util/std_expr.h>
16 #include <util/arith_tools.h>
17 #include <util/std_code.h>
18 #include <util/config.h>
19 #include <util/cprover_prefix.h>
20 #include <util/prefix.h>
21 
22 #include <util/c_types.h>
23 #include <ansi-c/string_constant.h>
24 
27 
29 
31  const code_typet::parameterst &parameters,
32  code_blockt &init_code,
33  symbol_tablet &symbol_table,
34  message_handlert &message_handler)
35 {
36  exprt::operandst main_arguments;
37  main_arguments.resize(parameters.size());
38 
39  for(std::size_t param_number=0;
40  param_number<parameters.size();
41  param_number++)
42  {
43  const code_typet::parametert &p=parameters[param_number];
44  const irep_idt base_name=p.get_base_name().empty()?
45  ("argument#"+std::to_string(param_number)):p.get_base_name();
46 
47  main_arguments[param_number]=
49  init_code,
50  symbol_table,
51  base_name,
52  p.type(),
53  p.source_location(),
54  true);
55  }
56 
57  return main_arguments;
58 }
59 
61  const symbolt &function,
62  code_blockt &init_code,
63  symbol_tablet &symbol_table)
64 {
65  bool has_return_value=
66  to_code_type(function.type).return_type()!=empty_typet();
67 
68  if(has_return_value)
69  {
70  // record return value
71  codet output(ID_output);
72  output.operands().resize(2);
73 
74  const symbolt &return_symbol=symbol_table.lookup("return'");
75 
76  output.op0()=
79  string_constantt(return_symbol.base_name),
80  from_integer(0, index_type())));
81 
82  output.op1()=return_symbol.symbol_expr();
83  output.add_source_location()=function.location;
84 
85  init_code.move_to_operands(output);
86  }
87 
88  #if 0
89  std::size_t i=0;
90 
91  for(const auto &p : parameters)
92  {
93  if(p.get_identifier().empty())
94  continue;
95 
96  irep_idt identifier=p.get_identifier();
97 
98  const symbolt &symbol=symbol_table.lookup(identifier);
99 
100  if(symbol.type.id()==ID_pointer)
101  {
102  codet output(ID_output);
103  output.operands().resize(2);
104 
105  output.op0()=
107  index_exprt(
108  string_constantt(symbol.base_name),
109  from_integer(0, index_type())));
110  output.op1()=symbol.symbol_expr();
111  output.add_source_location()=p.source_location();
112 
113  init_code.move_to_operands(output);
114  }
115 
116  i++;
117  }
118  #endif
119 }
120 
122  symbol_tablet &symbol_table,
123  const std::string &standard_main,
124  message_handlert &message_handler)
125 {
126  // check if entry point is already there
127  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
128  symbol_table.symbols.end())
129  return false; // silently ignore
130 
131  irep_idt main_symbol;
132 
133  // find main symbol
134  if(config.main!="")
135  {
136  std::list<irep_idt> matches;
137 
139  {
140  // look it up
141  symbol_tablet::symbolst::const_iterator s_it=
142  symbol_table.symbols.find(it->second);
143 
144  if(s_it==symbol_table.symbols.end())
145  continue;
146 
147  if(s_it->second.type.id()==ID_code)
148  matches.push_back(it->second);
149  }
150 
151  if(matches.empty())
152  {
153  messaget message(message_handler);
154  message.error() << "main symbol `" << config.main
155  << "' not found" << messaget::eom;
156  return true; // give up
157  }
158 
159  if(matches.size()>=2)
160  {
161  messaget message(message_handler);
162  message.error() << "main symbol `" << config.main
163  << "' is ambiguous" << messaget::eom;
164  return true;
165  }
166 
167  main_symbol=matches.front();
168  }
169  else
170  main_symbol=standard_main;
171 
172  // look it up
173  symbol_tablet::symbolst::const_iterator s_it=
174  symbol_table.symbols.find(main_symbol);
175 
176  if(s_it==symbol_table.symbols.end())
177  return false; // give up silently
178 
179  const symbolt &symbol=s_it->second;
180 
181  // check if it has a body
182  if(symbol.value.is_nil())
183  {
184  messaget message(message_handler);
185  message.error() << "main symbol `" << id2string(main_symbol)
186  << "' has no body" << messaget::eom;
187  return false; // give up
188  }
189 
190  if(static_lifetime_init(symbol_table, symbol.location, message_handler))
191  return true;
192 
193  code_blockt init_code;
194 
195  // build call to initialization function
196 
197  {
198  symbol_tablet::symbolst::iterator init_it=
199  symbol_table.symbols.find(INITIALIZE_FUNCTION);
200 
201  if(init_it==symbol_table.symbols.end())
202  {
203  messaget message(message_handler);
204  message.error() << "failed to find " CPROVER_PREFIX "initialize symbol"
205  << messaget::eom;
206  return true;
207  }
208 
209  code_function_callt call_init;
210  call_init.lhs().make_nil();
211  call_init.add_source_location()=symbol.location;
212  call_init.function()=init_it->second.symbol_expr();
213 
214  init_code.move_to_operands(call_init);
215  }
216 
217  // build call to main function
218 
219  code_function_callt call_main;
220  call_main.add_source_location()=symbol.location;
221  call_main.function()=symbol.symbol_expr();
222  call_main.function().add_source_location()=symbol.location;
223 
224  if(to_code_type(symbol.type).return_type()!=empty_typet())
225  {
226  auxiliary_symbolt return_symbol;
227  return_symbol.mode=ID_C;
228  return_symbol.is_static_lifetime=false;
229  return_symbol.name="return'";
230  return_symbol.base_name="return";
231  return_symbol.type=to_code_type(symbol.type).return_type();
232 
233  symbol_table.add(return_symbol);
234  call_main.lhs()=return_symbol.symbol_expr();
235  }
236 
237  const code_typet::parameterst &parameters=
238  to_code_type(symbol.type).parameters();
239 
240  if(symbol.name==standard_main)
241  {
242  if(parameters.empty())
243  {
244  // ok
245  }
246  else if(parameters.size()==2 || parameters.size()==3)
247  {
248  namespacet ns(symbol_table);
249 
250  const symbolt &argc_symbol=ns.lookup("argc'");
251  const symbolt &argv_symbol=ns.lookup("argv'");
252 
253  {
254  // assume argc is at least one
255  exprt one=from_integer(1, argc_symbol.type);
256 
257  exprt ge(ID_ge, typet(ID_bool));
258  ge.copy_to_operands(argc_symbol.symbol_expr(), one);
259 
260  codet assumption;
261  assumption.set_statement(ID_assume);
262  assumption.move_to_operands(ge);
263  init_code.move_to_operands(assumption);
264  }
265 
266  {
267  // assume argc is at most MAX/8-1
268  mp_integer upper_bound=
270 
271  exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
272 
273  exprt le(ID_le, typet(ID_bool));
274  le.copy_to_operands(argc_symbol.symbol_expr(), bound_expr);
275 
276  codet assumption;
277  assumption.set_statement(ID_assume);
278  assumption.move_to_operands(le);
279  init_code.move_to_operands(assumption);
280  }
281 
282  {
283  // record argc as an input
284  codet input(ID_input);
285  input.operands().resize(2);
286  input.op0()=address_of_exprt(
288  input.op1()=argc_symbol.symbol_expr();
289  init_code.move_to_operands(input);
290  }
291 
292  if(parameters.size()==3)
293  {
294  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
295 
296  // assume envp_size is INTMAX-1
297  mp_integer max;
298 
299  if(envp_size_symbol.type.id()==ID_signedbv)
300  {
301  max=to_signedbv_type(envp_size_symbol.type).largest();
302  }
303  else if(envp_size_symbol.type.id()==ID_unsignedbv)
304  {
305  max=to_unsignedbv_type(envp_size_symbol.type).largest();
306  }
307  else
308  assert(false);
309 
310  exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
311 
312  exprt le(ID_le, bool_typet());
313  le.copy_to_operands(envp_size_symbol.symbol_expr(), max_minus_one);
314 
315  codet assumption;
316  assumption.set_statement(ID_assume);
317  assumption.move_to_operands(le);
318  init_code.move_to_operands(assumption);
319  }
320 
321  {
322  /* zero_string doesn't work yet */
323 
324  /*
325  exprt zero_string(ID_zero_string, array_typet());
326  zero_string.type().subtype()=char_type();
327  zero_string.type().set(ID_size, "infinity");
328  exprt index(ID_index, char_type());
329  index.copy_to_operands(zero_string, from_integer(0, uint_type()));
330  exprt address_of=address_of_exprt(index, pointer_type(char_type()));
331 
332  if(argv_symbol.type.subtype()!=address_of.type())
333  address_of.make_typecast(argv_symbol.type.subtype());
334 
335  // assign argv[*] to the address of a string-object
336  array_of_exprt array_of(address_of, argv_symbol.type);
337 
338  init_code.copy_to_operands(
339  code_assignt(argv_symbol.symbol_expr(), array_of));
340  */
341  }
342 
343  {
344  // assign argv[argc] to NULL
345  exprt null(ID_constant, argv_symbol.type.subtype());
346  null.set(ID_value, ID_NULL);
347 
348  exprt index_expr(ID_index, argv_symbol.type.subtype());
349  index_expr.copy_to_operands(
350  argv_symbol.symbol_expr(),
351  argc_symbol.symbol_expr());
352 
353  // disable bounds check on that one
354  index_expr.set("bounds_check", false);
355 
356  init_code.copy_to_operands(code_assignt(index_expr, null));
357  }
358 
359  if(parameters.size()==3)
360  {
361  const symbolt &envp_symbol=ns.lookup("envp'");
362  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
363 
364  // assume envp[envp_size] is NULL
365  exprt null(ID_constant, envp_symbol.type.subtype());
366  null.set(ID_value, ID_NULL);
367 
368  exprt index_expr(ID_index, envp_symbol.type.subtype());
369  index_expr.copy_to_operands(
370  envp_symbol.symbol_expr(),
371  envp_size_symbol.symbol_expr());
372 
373  // disable bounds check on that one
374  index_expr.set("bounds_check", false);
375 
376  exprt is_null(ID_equal, typet(ID_bool));
377  is_null.copy_to_operands(index_expr, null);
378 
379  codet assumption2;
380  assumption2.set_statement(ID_assume);
381  assumption2.move_to_operands(is_null);
382  init_code.move_to_operands(assumption2);
383  }
384 
385  {
386  exprt::operandst &operands=call_main.arguments();
387 
388  if(parameters.size()==3)
389  operands.resize(3);
390  else
391  operands.resize(2);
392 
393  exprt &op0=operands[0];
394  exprt &op1=operands[1];
395 
396  op0=argc_symbol.symbol_expr();
397 
398  {
399  const exprt &arg1=parameters[1];
401  to_pointer_type(arg1.type());
402 
403  index_exprt index_expr(
404  argv_symbol.symbol_expr(),
405  from_integer(0, index_type()),
407 
408  // disable bounds check on that one
409  index_expr.set("bounds_check", false);
410 
411  op1=address_of_exprt(index_expr, pointer_type);
412  }
413 
414  // do we need envp?
415  if(parameters.size()==3)
416  {
417  const symbolt &envp_symbol=ns.lookup("envp'");
418  exprt &op2=operands[2];
419 
420  const exprt &arg2=parameters[2];
422  to_pointer_type(arg2.type());
423 
424  index_exprt index_expr(
425  envp_symbol.symbol_expr(),
426  from_integer(0, index_type()),
428 
429  op2=address_of_exprt(index_expr, pointer_type);
430  }
431  }
432  }
433  else
434  assert(false);
435  }
436  else
437  {
438  // produce nondet arguments
439  call_main.arguments()=
441  parameters,
442  init_code,
443  symbol_table,
444  message_handler);
445  }
446 
447  init_code.move_to_operands(call_main);
448 
449  // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
450 
451  record_function_outputs(symbol, init_code, symbol_table);
452 
453  // add the entry point symbol
454  symbolt new_symbol;
455 
456  code_typet main_type;
457  main_type.return_type()=empty_typet();
458 
459  new_symbol.name=goto_functionst::entry_point();
460  new_symbol.type.swap(main_type);
461  new_symbol.value.swap(init_code);
462  new_symbol.mode=symbol.mode;
463 
464  if(symbol_table.move(new_symbol))
465  {
466  messaget message;
467  message.set_message_handler(message_handler);
468  message.error() << "failed to move main symbol" << messaget::eom;
469  return true;
470  }
471 
472  return false;
473 }
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
struct configt::ansi_ct ansi_c
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
BigInt mp_integer
Definition: mp_arith.h:19
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
unsigned int_width
Definition: config.h:30
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
C Nondet Symbol Factory.
irep_idt mode
Language mode.
Definition: symbol.h:55
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
Goto Programs with Functions.
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
std::vector< parametert > parameterst
Definition: std_types.h:829
exprt value
Initial value of symbol.
Definition: symbol.h:40
bool static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location, message_handlert &message_handler)
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
symbol_base_mapt symbol_base_map
Definition: symbol_table.h:58
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
bool is_static_lifetime
Definition: symbol.h:70
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, bool allow_null)
Creates a symbol and generates code so that it can vary over all possible values for its type...
const irep_idt & id() const
Definition: irep.h:189
const irep_idt & get_base_name() const
Definition: std_types.h:787
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
exprt::operandst build_function_environment(const code_typet::parameterst &parameters, code_blockt &init_code, symbol_tablet &symbol_table, message_handlert &message_handler)
The pointer type.
Definition: std_types.h:1343
The empty type.
Definition: std_types.h:53
std::string main
Definition: config.h:147
#define INITIALIZE_FUNCTION
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
mp_integer largest() const
Definition: std_types.cpp:167
bitvector_typet index_type()
Definition: c_types.cpp:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
Operator to return the address of an object.
Definition: std_expr.h:2593
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
std::vector< exprt > operandst
Definition: expr.h:49
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
mp_integer largest() const
Definition: std_types.cpp:142
bool ansi_c_entry_point(symbol_tablet &symbol_table, const std::string &standard_main, message_handlert &message_handler)
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:39
exprt & function()
Definition: std_code.h:677
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
const source_locationt & source_location() const
Definition: expr.h:142
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
A statement in a programming language.
Definition: std_code.h:19
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool empty() const
Definition: dstring.h:61
const typet & return_type() const
Definition: std_types.h:831
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
array index operator
Definition: std_expr.h:1170