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  const c_object_factory_parameterst &object_factory_parameters)
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] = c_nondet_symbol_factory(
40  init_code,
41  symbol_table,
42  base_name,
43  p.type(),
44  p.source_location(),
45  object_factory_parameters);
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.add(std::move(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.add(std::move(output));
105  }
106 
107  i++;
108  }
109  #endif
110 }
111 
113  symbol_tablet &symbol_table,
114  message_handlert &message_handler,
115  const c_object_factory_parameterst &object_factory_parameters)
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  static_lifetime_init(symbol_table, symbol.location);
182 
184  symbol, symbol_table, message_handler, object_factory_parameters);
185 }
186 
197  const symbolt &symbol,
198  symbol_tablet &symbol_table,
199  message_handlert &message_handler,
200  const c_object_factory_parameterst &object_factory_parameters)
201 {
202  PRECONDITION(!symbol.value.is_nil());
203  code_blockt init_code;
204 
205  // add 'HIDE' label
206  init_code.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
207 
208  // build call to initialization function
209 
210  {
211  symbol_tablet::symbolst::const_iterator init_it=
212  symbol_table.symbols.find(INITIALIZE_FUNCTION);
213 
214  if(init_it==symbol_table.symbols.end())
215  {
216  messaget message(message_handler);
217  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
218  << messaget::eom;
219  return true;
220  }
221 
222  code_function_callt call_init(init_it->second.symbol_expr());
223  call_init.add_source_location()=symbol.location;
224 
225  init_code.add(std::move(call_init));
226  }
227 
228  // build call to main function
229 
230  code_function_callt call_main(symbol.symbol_expr());
231  call_main.add_source_location()=symbol.location;
232  call_main.function().add_source_location()=symbol.location;
233 
234  if(to_code_type(symbol.type).return_type()!=empty_typet())
235  {
236  auxiliary_symbolt return_symbol;
237  return_symbol.mode=ID_C;
238  return_symbol.is_static_lifetime=false;
239  return_symbol.name="return'";
240  return_symbol.base_name="return";
241  return_symbol.type=to_code_type(symbol.type).return_type();
242 
243  symbol_table.add(return_symbol);
244  call_main.lhs()=return_symbol.symbol_expr();
245  }
246 
247  const code_typet::parameterst &parameters=
248  to_code_type(symbol.type).parameters();
249 
250  if(symbol.name==ID_main)
251  {
252  if(parameters.empty())
253  {
254  // ok
255  }
256  else if(parameters.size()==2 || parameters.size()==3)
257  {
258  namespacet ns(symbol_table);
259 
260  const symbolt &argc_symbol=ns.lookup("argc'");
261  const symbolt &argv_symbol=ns.lookup("argv'");
262 
263  {
264  // assume argc is at least one
265  exprt one=from_integer(1, argc_symbol.type);
266 
267  const binary_relation_exprt ge(argc_symbol.symbol_expr(), ID_ge, one);
268 
269  code_assumet assumption(ge);
270  init_code.add(std::move(assumption));
271  }
272 
273  {
274  // assume argc is at most MAX/8-1
275  mp_integer upper_bound=
277 
278  exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
279 
280  const binary_relation_exprt le(
281  argc_symbol.symbol_expr(), ID_le, bound_expr);
282 
283  code_assumet assumption(le);
284  init_code.add(std::move(assumption));
285  }
286 
287  {
288  // record argc as an input
289  codet input(ID_input);
290  input.operands().resize(2);
291  input.op0()=address_of_exprt(
293  input.op1()=argc_symbol.symbol_expr();
294  init_code.add(std::move(input));
295  }
296 
297  if(parameters.size()==3)
298  {
299  const symbolt &envp_size_symbol=ns.lookup("envp_size'");
300 
301  // assume envp_size is INTMAX-1
302  mp_integer max;
303 
304  if(envp_size_symbol.type.id()==ID_signedbv)
305  {
306  max=to_signedbv_type(envp_size_symbol.type).largest();
307  }
308  else if(envp_size_symbol.type.id()==ID_unsignedbv)
309  {
310  max=to_unsignedbv_type(envp_size_symbol.type).largest();
311  }
312  else
313  UNREACHABLE;
314 
315  exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
316 
317  const binary_relation_exprt le(
318  envp_size_symbol.symbol_expr(), ID_le, max_minus_one);
319 
320  code_assumet assumption(le);
321  init_code.add(std::move(assumption));
322  }
323 
324  {
325  /* zero_string doesn't work yet */
326 
327  /*
328  exprt zero_string(ID_zero_string, array_typet());
329  zero_string.type().subtype()=char_type();
330  zero_string.type().set(ID_size, "infinity");
331  const index_exprt index(zero_string, from_integer(0, uint_type()));
332  exprt address_of=address_of_exprt(index, pointer_type(char_type()));
333 
334  if(argv_symbol.type.subtype()!=address_of.type())
335  address_of.make_typecast(argv_symbol.type.subtype());
336 
337  // assign argv[*] to the address of a string-object
338  array_of_exprt array_of(address_of, argv_symbol.type);
339 
340  init_code.copy_to_operands(
341  code_assignt(argv_symbol.symbol_expr(), array_of));
342  */
343  }
344 
345  {
346  // assign argv[argc] to NULL
347  const null_pointer_exprt null(
348  to_pointer_type(argv_symbol.type.subtype()));
349 
350  index_exprt index_expr(
351  argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
352 
353  // disable bounds check on that one
354  index_expr.set("bounds_check", false);
355 
356  init_code.add(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  const null_pointer_exprt null(
366  to_pointer_type(envp_symbol.type.subtype()));
367 
368  index_exprt index_expr(
369  envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());
370  // disable bounds check on that one
371  index_expr.set("bounds_check", false);
372 
373  const equal_exprt is_null(index_expr, null);
374 
375  code_assumet assumption2(is_null);
376  init_code.add(std::move(assumption2));
377  }
378 
379  {
380  exprt::operandst &operands=call_main.arguments();
381 
382  if(parameters.size()==3)
383  operands.resize(3);
384  else
385  operands.resize(2);
386 
387  exprt &op0=operands[0];
388  exprt &op1=operands[1];
389 
390  op0=argc_symbol.symbol_expr();
391 
392  {
393  const exprt &arg1=parameters[1];
395  to_pointer_type(arg1.type());
396 
397  index_exprt index_expr(
398  argv_symbol.symbol_expr(),
399  from_integer(0, index_type()),
401 
402  // disable bounds check on that one
403  index_expr.set("bounds_check", false);
404 
405  op1=address_of_exprt(index_expr, pointer_type);
406  }
407 
408  // do we need envp?
409  if(parameters.size()==3)
410  {
411  const symbolt &envp_symbol=ns.lookup("envp'");
412  exprt &op2=operands[2];
413 
414  const exprt &arg2=parameters[2];
416  to_pointer_type(arg2.type());
417 
418  index_exprt index_expr(
419  envp_symbol.symbol_expr(),
420  from_integer(0, index_type()),
422 
423  op2=address_of_exprt(index_expr, pointer_type);
424  }
425  }
426  }
427  else
428  UNREACHABLE;
429  }
430  else
431  {
432  // produce nondet arguments
434  parameters, init_code, symbol_table, object_factory_parameters);
435  }
436 
437  init_code.add(std::move(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;
454  message.set_message_handler(message_handler);
455  message.error() << "failed to insert main symbol" << messaget::eom;
456  return true;
457  }
458 
459  return false;
460 }
c_nondet_symbol_factory.h
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
typet::subtype
const typet & subtype() const
Definition: type.h:38
arith_tools.h
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Definition: symbol_table_base.h:28
ansi_c_entry_point.h
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
configt::main
std::string main
Definition: config.h:172
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
exprt::op0
exprt & op0()
Definition: expr.h:84
build_function_environment
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)
Definition: ansi_c_entry_point.cpp:22
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
auxiliary_symbolt
Internally generated symbol table entry.
Definition: symbol.h:148
configt::ansi_c
struct configt::ansi_ct ansi_c
string_constantt
Definition: string_constant.h:15
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
record_function_outputs
void record_function_outputs(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table)
Definition: ansi_c_entry_point.cpp:51
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:386
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:833
empty_typet
The empty type.
Definition: std_types.h:48
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:14
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
static_lifetime_init
void static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location)
Definition: static_lifetime_init.cpp:25
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4471
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1256
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
exprt::op1
exprt & op1()
Definition: expr.h:87
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:17
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::swap
void swap(irept &irep)
Definition: irep.h:303
code_typet
Base type of functions.
Definition: std_types.h:751
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
message_handlert
Definition: message.h:24
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
dstringt::empty
bool empty() const
Definition: dstring.h:75
code_blockt::add
void add(const codet &code)
Definition: std_code.h:189
generate_ansi_c_start_function
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.
Definition: ansi_c_entry_point.cpp:196
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
unsignedbv_typet::largest
mp_integer largest() const
Definition: std_types.cpp:195
ansi_c_entry_point
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Definition: ansi_c_entry_point.cpp:112
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
config
configt config
Definition: config.cpp:24
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
code_skipt
A codet representing a skip statement.
Definition: std_code.h:237
c_nondet_symbol_factory
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)
Creates a symbol and generates code so that it can vary over all possible values for its type.
Definition: c_nondet_symbol_factory.cpp:266
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
forall_symbol_base_map
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:218
code_typet::parametert
Definition: std_types.h:788
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
signedbv_typet::largest
mp_integer largest() const
Definition: std_types.cpp:170
goto_functions.h
config.h
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
exprt::operands
operandst & operands()
Definition: expr.h:78
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
index_exprt
Array index operator.
Definition: std_expr.h:1595
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34