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)
26 {
27  exprt::operandst main_arguments;
28  main_arguments.resize(parameters.size());
29 
30  for(std::size_t param_number=0;
31  param_number<parameters.size();
32  param_number++)
33  {
34  const code_typet::parametert &p=parameters[param_number];
35  const irep_idt base_name=p.get_base_name().empty()?
36  ("argument#"+std::to_string(param_number)):p.get_base_name();
37 
38  main_arguments[param_number]=
40  init_code,
41  symbol_table,
42  base_name,
43  p.type(),
44  p.source_location(),
45  true);
46  }
47 
48  return main_arguments;
49 }
50 
52  const symbolt &function,
53  code_blockt &init_code,
54  symbol_tablet &symbol_table)
55 {
56  bool has_return_value=
57  to_code_type(function.type).return_type()!=empty_typet();
58 
59  if(has_return_value)
60  {
61  // record return value
62  codet output(ID_output);
63  output.operands().resize(2);
64 
65  const symbolt &return_symbol=*symbol_table.lookup("return'");
66 
67  output.op0()=
70  string_constantt(return_symbol.base_name),
71  from_integer(0, index_type())));
72 
73  output.op1()=return_symbol.symbol_expr();
74  output.add_source_location()=function.location;
75 
76  init_code.move_to_operands(output);
77  }
78 
79  #if 0
80  std::size_t i=0;
81 
82  for(const auto &p : parameters)
83  {
84  if(p.get_identifier().empty())
85  continue;
86 
87  irep_idt identifier=p.get_identifier();
88 
89  const symbolt &symbol=symbol_table.lookup(identifier);
90 
91  if(symbol.type.id()==ID_pointer)
92  {
93  codet output(ID_output);
94  output.operands().resize(2);
95 
96  output.op0()=
100  from_integer(0, index_type())));
101  output.op1()=symbol.symbol_expr();
102  output.add_source_location()=p.source_location();
103 
104  init_code.move_to_operands(output);
105  }
106 
107  i++;
108  }
109  #endif
110 }
111 
113  symbol_tablet &symbol_table,
115 {
116  // check if entry point is already there
117  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
118  symbol_table.symbols.end())
119  return false; // silently ignore
120 
121  irep_idt main_symbol;
122 
123  // find main symbol
124  if(config.main!="")
125  {
126  std::list<irep_idt> matches;
127 
129  {
130  // look it up
131  symbol_tablet::symbolst::const_iterator s_it=
132  symbol_table.symbols.find(it->second);
133 
134  if(s_it==symbol_table.symbols.end())
135  continue;
136 
137  if(s_it->second.type.id()==ID_code)
138  matches.push_back(it->second);
139  }
140 
141  if(matches.empty())
142  {
143  messaget message(message_handler);
144  message.error() << "main symbol `" << config.main
145  << "' not found" << messaget::eom;
146  return true; // give up
147  }
148 
149  if(matches.size()>=2)
150  {
151  messaget message(message_handler);
152  message.error() << "main symbol `" << config.main
153  << "' is ambiguous" << messaget::eom;
154  return true;
155  }
156 
157  main_symbol=matches.front();
158  }
159  else
160  main_symbol=ID_main;
161 
162  // look it up
163  symbol_tablet::symbolst::const_iterator s_it=
164  symbol_table.symbols.find(main_symbol);
165 
166  if(s_it==symbol_table.symbols.end())
167  return false; // give up silently
168 
169  const symbolt &symbol=s_it->second;
170 
171  // check if it has a body
172  if(symbol.value.is_nil())
173  {
174  messaget message(message_handler);
175  message.error() << "main symbol `" << id2string(main_symbol)
176  << "' has no body" << messaget::eom;
177  return false; // give up
178  }
179 
180  if(static_lifetime_init(symbol_table, symbol.location, message_handler))
181  return true;
182 
183  return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
184 }
185 
186 
195  const symbolt &symbol,
196  symbol_tablet &symbol_table,
198 {
199  PRECONDITION(!symbol.value.is_nil());
200  code_blockt init_code;
201 
202  // build call to initialization function
203 
204  {
205  symbol_tablet::symbolst::const_iterator init_it=
206  symbol_table.symbols.find(INITIALIZE_FUNCTION);
207 
208  if(init_it==symbol_table.symbols.end())
209  {
210  messaget message(message_handler);
211  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
212  << messaget::eom;
213  return true;
214  }
215 
216  code_function_callt call_init;
217  call_init.lhs().make_nil();
218  call_init.add_source_location()=symbol.location;
219  call_init.function()=init_it->second.symbol_expr();
220 
221  init_code.move_to_operands(call_init);
222  }
223 
224  // build call to main function
225 
226  code_function_callt call_main;
227  call_main.add_source_location()=symbol.location;
228  call_main.function()=symbol.symbol_expr();
229  call_main.function().add_source_location()=symbol.location;
230 
231  if(to_code_type(symbol.type).return_type()!=empty_typet())
232  {
233  auxiliary_symbolt return_symbol;
234  return_symbol.mode=ID_C;
235  return_symbol.is_static_lifetime=false;
236  return_symbol.name="return'";
237  return_symbol.base_name="return";
238  return_symbol.type=to_code_type(symbol.type).return_type();
239 
240  symbol_table.add(return_symbol);
241  call_main.lhs()=return_symbol.symbol_expr();
242  }
243 
244  const code_typet::parameterst &parameters=
245  to_code_type(symbol.type).parameters();
246 
247  if(symbol.name==ID_main)
248  {
249  if(parameters.empty())
250  {
251  // ok
252  }
253  else if(parameters.size()==2 || parameters.size()==3)
254  {
255  namespacet ns(symbol_table);
256 
257  const symbolt &argc_symbol=ns.lookup("argc'");
258  const symbolt &argv_symbol=ns.lookup("argv'");
259 
260  {
261  // assume argc is at least one
262  exprt one=from_integer(1, argc_symbol.type);
263 
264  const binary_relation_exprt ge(argc_symbol.symbol_expr(), ID_ge, one);
265 
266  code_assumet assumption(ge);
267  init_code.move_to_operands(assumption);
268  }
269 
270  {
271  // assume argc is at most MAX/8-1
272  mp_integer upper_bound=
274 
275  exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
276 
277  const binary_relation_exprt le(
278  argc_symbol.symbol_expr(), ID_le, bound_expr);
279 
280  code_assumet assumption(le);
281  init_code.move_to_operands(assumption);
282  }
283 
284  {
285  // record argc as an input
286  codet input(ID_input);
287  input.operands().resize(2);
288  input.op0()=address_of_exprt(
290  input.op1()=argc_symbol.symbol_expr();
291  init_code.move_to_operands(input);
292  }
293 
294  if(parameters.size()==3)
295  {
296  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
297 
298  // assume envp_size is INTMAX-1
299  mp_integer max;
300 
301  if(envp_size_symbol.type.id()==ID_signedbv)
302  {
303  max=to_signedbv_type(envp_size_symbol.type).largest();
304  }
305  else if(envp_size_symbol.type.id()==ID_unsignedbv)
306  {
307  max=to_unsignedbv_type(envp_size_symbol.type).largest();
308  }
309  else
310  UNREACHABLE;
311 
312  exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
313 
314  const binary_relation_exprt le(
315  envp_size_symbol.symbol_expr(), ID_le, max_minus_one);
316 
317  code_assumet assumption(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  const index_exprt index(zero_string, from_integer(0, uint_type()));
329  exprt address_of=address_of_exprt(index, pointer_type(char_type()));
330 
331  if(argv_symbol.type.subtype()!=address_of.type())
332  address_of.make_typecast(argv_symbol.type.subtype());
333 
334  // assign argv[*] to the address of a string-object
335  array_of_exprt array_of(address_of, argv_symbol.type);
336 
337  init_code.copy_to_operands(
338  code_assignt(argv_symbol.symbol_expr(), array_of));
339  */
340  }
341 
342  {
343  // assign argv[argc] to NULL
344  const null_pointer_exprt null(
345  to_pointer_type(argv_symbol.type.subtype()));
346 
347  index_exprt index_expr(
348  argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
349 
350  // disable bounds check on that one
351  index_expr.set("bounds_check", false);
352 
353  init_code.copy_to_operands(code_assignt(index_expr, null));
354  }
355 
356  if(parameters.size()==3)
357  {
358  const symbolt &envp_symbol=ns.lookup("envp'");
359  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
360 
361  // assume envp[envp_size] is NULL
362  const null_pointer_exprt null(
363  to_pointer_type(envp_symbol.type.subtype()));
364 
365  index_exprt index_expr(
366  envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
367  // disable bounds check on that one
368  index_expr.set("bounds_check", false);
369 
370  const equal_exprt is_null(index_expr, null);
371 
372  code_assumet assumption2(is_null);
373  init_code.move_to_operands(assumption2);
374  }
375 
376  {
377  exprt::operandst &operands=call_main.arguments();
378 
379  if(parameters.size()==3)
380  operands.resize(3);
381  else
382  operands.resize(2);
383 
384  exprt &op0=operands[0];
385  exprt &op1=operands[1];
386 
387  op0=argc_symbol.symbol_expr();
388 
389  {
390  const exprt &arg1=parameters[1];
392  to_pointer_type(arg1.type());
393 
394  index_exprt index_expr(
395  argv_symbol.symbol_expr(),
396  from_integer(0, index_type()),
398 
399  // disable bounds check on that one
400  index_expr.set("bounds_check", false);
401 
402  op1=address_of_exprt(index_expr, pointer_type);
403  }
404 
405  // do we need envp?
406  if(parameters.size()==3)
407  {
408  const symbolt &envp_symbol=ns.lookup("envp'");
409  exprt &op2=operands[2];
410 
411  const exprt &arg2=parameters[2];
413  to_pointer_type(arg2.type());
414 
415  index_exprt index_expr(
416  envp_symbol.symbol_expr(),
417  from_integer(0, index_type()),
419 
420  op2=address_of_exprt(index_expr, pointer_type);
421  }
422  }
423  }
424  else
425  UNREACHABLE;
426  }
427  else
428  {
429  // produce nondet arguments
430  call_main.arguments()=
432  parameters,
433  init_code,
434  symbol_table);
435  }
436 
437  init_code.move_to_operands(call_main);
438 
439  // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
440 
441  record_function_outputs(symbol, init_code, symbol_table);
442 
443  // add the entry point symbol
444  symbolt new_symbol;
445 
446  new_symbol.name=goto_functionst::entry_point();
447  new_symbol.type = code_typet({}, empty_typet());
448  new_symbol.value.swap(init_code);
449  new_symbol.mode=symbol.mode;
450 
451  if(!symbol_table.insert(std::move(new_symbol)).second)
452  {
453  messaget message;
455  message.error() << "failed to insert main symbol" << messaget::eom;
456  return true;
457  }
458 
459  return false;
460 }
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:172
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:44
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:1296
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:993
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:4518
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:259
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:890
exprt::operandst build_function_environment(const code_typet::parameterst &parameters, code_blockt &init_code, symbol_tablet &symbol_table)
The pointer type.
Definition: std_types.h:1435
The empty type.
Definition: std_types.h:54
std::string main
Definition: config.h:171
#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:242
std::size_t int_width
Definition: config.h:30
A function call.
Definition: std_code.h:858
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
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:1254
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
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:878
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:271
void make_nil()
Definition: irep.h:315
void swap(irept &irep)
Definition: irep.h:303
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
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:1459
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:73
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:136
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
array index operator
Definition: std_expr.h:1462