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/string_constant.h>
15 
17 
19 
21 
23  const code_typet::parameterst &parameters,
24  code_blockt &init_code,
25  symbol_tablet &symbol_table,
27 {
28  exprt::operandst main_arguments;
29  main_arguments.resize(parameters.size());
30 
31  for(std::size_t param_number=0;
32  param_number<parameters.size();
33  param_number++)
34  {
35  const code_typet::parametert &p=parameters[param_number];
36  const irep_idt base_name=p.get_base_name().empty()?
37  ("argument#"+std::to_string(param_number)):p.get_base_name();
38 
39  main_arguments[param_number]=
41  init_code,
42  symbol_table,
43  base_name,
44  p.type(),
45  p.source_location(),
46  true);
47  }
48 
49  return main_arguments;
50 }
51 
53  const symbolt &function,
54  code_blockt &init_code,
55  symbol_tablet &symbol_table)
56 {
57  bool has_return_value=
58  to_code_type(function.type).return_type()!=empty_typet();
59 
60  if(has_return_value)
61  {
62  // record return value
63  codet output(ID_output);
64  output.operands().resize(2);
65 
66  const symbolt &return_symbol=*symbol_table.lookup("return'");
67 
68  output.op0()=
71  string_constantt(return_symbol.base_name),
72  from_integer(0, index_type())));
73 
74  output.op1()=return_symbol.symbol_expr();
75  output.add_source_location()=function.location;
76 
77  init_code.move_to_operands(output);
78  }
79 
80  #if 0
81  std::size_t i=0;
82 
83  for(const auto &p : parameters)
84  {
85  if(p.get_identifier().empty())
86  continue;
87 
88  irep_idt identifier=p.get_identifier();
89 
90  const symbolt &symbol=symbol_table.lookup(identifier);
91 
92  if(symbol.type.id()==ID_pointer)
93  {
94  codet output(ID_output);
95  output.operands().resize(2);
96 
97  output.op0()=
100  string_constantt(symbol.base_name),
101  from_integer(0, index_type())));
102  output.op1()=symbol.symbol_expr();
103  output.add_source_location()=p.source_location();
104 
105  init_code.move_to_operands(output);
106  }
107 
108  i++;
109  }
110  #endif
111 }
112 
114  symbol_tablet &symbol_table,
116 {
117  // check if entry point is already there
118  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
119  symbol_table.symbols.end())
120  return false; // silently ignore
121 
122  irep_idt main_symbol;
123 
124  // find main symbol
125  if(config.main!="")
126  {
127  std::list<irep_idt> matches;
128 
130  {
131  // look it up
132  symbol_tablet::symbolst::const_iterator s_it=
133  symbol_table.symbols.find(it->second);
134 
135  if(s_it==symbol_table.symbols.end())
136  continue;
137 
138  if(s_it->second.type.id()==ID_code)
139  matches.push_back(it->second);
140  }
141 
142  if(matches.empty())
143  {
144  messaget message(message_handler);
145  message.error() << "main symbol `" << config.main
146  << "' not found" << messaget::eom;
147  return true; // give up
148  }
149 
150  if(matches.size()>=2)
151  {
152  messaget message(message_handler);
153  message.error() << "main symbol `" << config.main
154  << "' is ambiguous" << messaget::eom;
155  return true;
156  }
157 
158  main_symbol=matches.front();
159  }
160  else
161  main_symbol=ID_main;
162 
163  // look it up
164  symbol_tablet::symbolst::const_iterator s_it=
165  symbol_table.symbols.find(main_symbol);
166 
167  if(s_it==symbol_table.symbols.end())
168  return false; // give up silently
169 
170  const symbolt &symbol=s_it->second;
171 
172  // check if it has a body
173  if(symbol.value.is_nil())
174  {
175  messaget message(message_handler);
176  message.error() << "main symbol `" << id2string(main_symbol)
177  << "' has no body" << messaget::eom;
178  return false; // give up
179  }
180 
181  if(static_lifetime_init(symbol_table, symbol.location, message_handler))
182  return true;
183 
184  return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
185 }
186 
187 
196  const symbolt &symbol,
197  symbol_tablet &symbol_table,
199 {
200  PRECONDITION(!symbol.value.is_nil());
201  code_blockt init_code;
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;
218  call_init.lhs().make_nil();
219  call_init.add_source_location()=symbol.location;
220  call_init.function()=init_it->second.symbol_expr();
221 
222  init_code.move_to_operands(call_init);
223  }
224 
225  // build call to main function
226 
227  code_function_callt call_main;
228  call_main.add_source_location()=symbol.location;
229  call_main.function()=symbol.symbol_expr();
230  call_main.function().add_source_location()=symbol.location;
231 
232  if(to_code_type(symbol.type).return_type()!=empty_typet())
233  {
234  auxiliary_symbolt return_symbol;
235  return_symbol.mode=ID_C;
236  return_symbol.is_static_lifetime=false;
237  return_symbol.name="return'";
238  return_symbol.base_name="return";
239  return_symbol.type=to_code_type(symbol.type).return_type();
240 
241  symbol_table.add(return_symbol);
242  call_main.lhs()=return_symbol.symbol_expr();
243  }
244 
245  const code_typet::parameterst &parameters=
246  to_code_type(symbol.type).parameters();
247 
248  if(symbol.name==ID_main)
249  {
250  if(parameters.empty())
251  {
252  // ok
253  }
254  else if(parameters.size()==2 || parameters.size()==3)
255  {
256  namespacet ns(symbol_table);
257 
258  const symbolt &argc_symbol=ns.lookup("argc'");
259  const symbolt &argv_symbol=ns.lookup("argv'");
260 
261  {
262  // assume argc is at least one
263  exprt one=from_integer(1, argc_symbol.type);
264 
265  const binary_relation_exprt ge(argc_symbol.symbol_expr(), ID_ge, one);
266 
267  code_assumet assumption(ge);
268  init_code.move_to_operands(assumption);
269  }
270 
271  {
272  // assume argc is at most MAX/8-1
273  mp_integer upper_bound=
275 
276  exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
277 
278  const binary_relation_exprt le(
279  argc_symbol.symbol_expr(), ID_le, bound_expr);
280 
281  code_assumet assumption(le);
282  init_code.move_to_operands(assumption);
283  }
284 
285  {
286  // record argc as an input
287  codet input(ID_input);
288  input.operands().resize(2);
289  input.op0()=address_of_exprt(
291  input.op1()=argc_symbol.symbol_expr();
292  init_code.move_to_operands(input);
293  }
294 
295  if(parameters.size()==3)
296  {
297  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
298 
299  // assume envp_size is INTMAX-1
300  mp_integer max;
301 
302  if(envp_size_symbol.type.id()==ID_signedbv)
303  {
304  max=to_signedbv_type(envp_size_symbol.type).largest();
305  }
306  else if(envp_size_symbol.type.id()==ID_unsignedbv)
307  {
308  max=to_unsignedbv_type(envp_size_symbol.type).largest();
309  }
310  else
311  UNREACHABLE;
312 
313  exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
314 
315  const binary_relation_exprt le(
316  envp_size_symbol.symbol_expr(), ID_le, max_minus_one);
317 
318  code_assumet assumption(le);
319  init_code.move_to_operands(assumption);
320  }
321 
322  {
323  /* zero_string doesn't work yet */
324 
325  /*
326  exprt zero_string(ID_zero_string, array_typet());
327  zero_string.type().subtype()=char_type();
328  zero_string.type().set(ID_size, "infinity");
329  const index_exprt index(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  const null_pointer_exprt null(
346  to_pointer_type(argv_symbol.type.subtype()));
347 
348  index_exprt index_expr(
349  argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
350 
351  // disable bounds check on that one
352  index_expr.set("bounds_check", false);
353 
354  init_code.copy_to_operands(code_assignt(index_expr, null));
355  }
356 
357  if(parameters.size()==3)
358  {
359  const symbolt &envp_symbol=ns.lookup("envp'");
360  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
361 
362  // assume envp[envp_size] is NULL
363  const null_pointer_exprt null(
364  to_pointer_type(envp_symbol.type.subtype()));
365 
366  index_exprt index_expr(
367  envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
368  // disable bounds check on that one
369  index_expr.set("bounds_check", false);
370 
371  const equal_exprt is_null(index_expr, null);
372 
373  code_assumet assumption2(is_null);
374  init_code.move_to_operands(assumption2);
375  }
376 
377  {
378  exprt::operandst &operands=call_main.arguments();
379 
380  if(parameters.size()==3)
381  operands.resize(3);
382  else
383  operands.resize(2);
384 
385  exprt &op0=operands[0];
386  exprt &op1=operands[1];
387 
388  op0=argc_symbol.symbol_expr();
389 
390  {
391  const exprt &arg1=parameters[1];
393  to_pointer_type(arg1.type());
394 
395  index_exprt index_expr(
396  argv_symbol.symbol_expr(),
397  from_integer(0, index_type()),
399 
400  // disable bounds check on that one
401  index_expr.set("bounds_check", false);
402 
403  op1=address_of_exprt(index_expr, pointer_type);
404  }
405 
406  // do we need envp?
407  if(parameters.size()==3)
408  {
409  const symbolt &envp_symbol=ns.lookup("envp'");
410  exprt &op2=operands[2];
411 
412  const exprt &arg2=parameters[2];
414  to_pointer_type(arg2.type());
415 
416  index_exprt index_expr(
417  envp_symbol.symbol_expr(),
418  from_integer(0, index_type()),
420 
421  op2=address_of_exprt(index_expr, pointer_type);
422  }
423  }
424  }
425  else
426  UNREACHABLE;
427  }
428  else
429  {
430  // produce nondet arguments
431  call_main.arguments()=
433  parameters,
434  init_code,
435  symbol_table,
437  }
438 
439  init_code.move_to_operands(call_main);
440 
441  // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
442 
443  record_function_outputs(symbol, init_code, symbol_table);
444 
445  // add the entry point symbol
446  symbolt new_symbol;
447 
448  new_symbol.name=goto_functionst::entry_point();
449  new_symbol.type = code_typet({}, empty_typet());
450  new_symbol.value.swap(init_code);
451  new_symbol.mode=symbol.mode;
452 
453  if(!symbol_table.insert(std::move(new_symbol)).second)
454  {
455  messaget message;
457  message.error() << "failed to insert main symbol" << messaget::eom;
458  return true;
459  }
460 
461  return false;
462 }
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
irep_idt name
The unique identifier.
Definition: symbol.h:43
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
exprt & op0()
Definition: expr.h:72
C Nondet Symbol Factory.
irep_idt mode
Language mode.
Definition: symbol.h:52
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const symbol_base_mapt & symbol_base_map
Goto Programs with Functions.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
The null pointer constant.
Definition: std_expr.h:4520
std::vector< parametert > parameterst
Definition: std_types.h:767
exprt value
Initial value of symbol.
Definition: symbol.h:37
bool static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location, message_handlert &message_handler)
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
bool is_static_lifetime
Definition: symbol.h:67
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...
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
const irep_idt & get_base_name() const
Definition: std_types.h:845
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:860
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:1426
The empty type.
Definition: std_types.h:54
std::string main
Definition: config.h:163
#define INITIALIZE_FUNCTION
exprt & op1()
Definition: expr.h:75
bool generate_ansi_c_start_function(const symbolt &symbol, symbol_tablet &symbol_table, message_handlert &message_handler)
Generate a _start function for a specific function.
The symbol table.
Definition: symbol_table.h:19
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
std::size_t int_width
Definition: config.h:30
A function call.
Definition: std_code.h:828
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
mp_integer largest() const
Definition: std_types.cpp:167
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: std_expr.h:3170
const symbolst & symbols
std::vector< exprt > operandst
Definition: expr.h:45
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
An assumption, which must hold in subsequent code.
Definition: std_code.h:354
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
mp_integer largest() const
Definition: std_types.cpp:142
static irep_idt entry_point()
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
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
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
A statement in a programming language.
Definition: std_code.h:21
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
array index operator
Definition: std_expr.h:1462