CBMC
statement_list_entry_point.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Statement List Language Entry Point
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/c_types.h>
15 #include <util/config.h>
16 #include <util/message.h>
17 #include <util/pointer_expr.h>
18 #include <util/std_code.h>
19 #include <util/symbol_table_base.h>
20 
23 
25 
28 #define DB_ENTRY_POINT_POSTFIX "_entry_point"
29 
31 #define CPROVER_HIDE CPROVER_PREFIX "HIDE"
32 
42  const symbol_table_baset &symbol_table,
43  message_handlert &message_handler,
44  const irep_idt &main_symbol_name)
45 {
46  bool found = false;
47 
48  for(const std::pair<const irep_idt, symbolt> &pair : symbol_table)
49  {
50  if(pair.first == main_symbol_name && pair.second.type.id() == ID_code)
51  {
52  if(found)
53  {
54  messaget message(message_handler);
55  message.error() << "main symbol `" << main_symbol_name
56  << "' is ambiguous" << messaget::eom;
57  return true;
58  }
59  else
60  found = true;
61  }
62  }
63 
64  if(found)
65  return false;
66  else
67  {
68  messaget message(message_handler);
69  message.error() << "main symbol `" << main_symbol_name << "' not found"
70  << messaget::eom;
71  return true;
72  }
73 }
74 
81 static void add_initialize_call(
82  code_blockt &function_body,
83  const symbol_table_baset &symbol_table,
84  const source_locationt &main_symbol_location)
85 {
86  symbolt init = symbol_table.lookup_ref(INITIALIZE_FUNCTION);
87  code_function_callt call_init{init.symbol_expr()};
88  call_init.add_source_location() = main_symbol_location;
89  function_body.add(call_init);
90 }
91 
98  code_blockt &function_body,
99  symbol_table_baset &symbol_table,
100  const symbolt &main_function_block)
101 {
102  const code_typet &function_type = to_code_type(main_function_block.type);
103  PRECONDITION(1u == function_type.parameters().size());
104  const code_typet::parametert &data_block_interface =
105  function_type.parameters().front();
106  symbolt instance_data_block{
107  id2string(data_block_interface.get_base_name()) + DB_ENTRY_POINT_POSTFIX,
108  to_type_with_subtype(data_block_interface.type()).subtype(),
109  ID_statement_list};
110  instance_data_block.is_static_lifetime = true;
111  symbol_table.add(instance_data_block);
112  const address_of_exprt data_block_ref{instance_data_block.symbol_expr()};
113 
114  code_function_callt::argumentst args{data_block_ref};
115  code_function_callt call_main{main_function_block.symbol_expr(), args};
116  call_main.add_source_location() = main_function_block.location;
117  function_body.add(call_main);
118 }
119 
122 static void
124 {
125  symbolt init{
126  INITIALIZE_FUNCTION, code_typet({}, empty_typet{}), ID_statement_list};
127 
128  code_blockt dest;
130 
131  for(const std::pair<const irep_idt, symbolt> &pair : symbol_table)
132  {
133  const symbolt &symbol = pair.second;
134  if(symbol.is_static_lifetime && symbol.value.is_not_nil())
135  dest.add(code_assignt{pair.second.symbol_expr(), pair.second.value});
136  }
137  init.value = std::move(dest);
138  symbol_table.add(init);
139 }
140 
143 static void generate_rounding_mode(symbol_table_baset &symbol_table)
144 {
145  symbolt rounding_mode{rounding_mode_identifier(), signed_int_type(), ID_C};
146  rounding_mode.is_thread_local = true;
147  rounding_mode.is_static_lifetime = true;
148  const constant_exprt rounding_val{
149  std::to_string(ieee_floatt::rounding_modet::ROUND_TO_EVEN),
150  signed_int_type()};
151  rounding_mode.value = rounding_val;
152  symbol_table.add(rounding_mode);
153 }
154 
161  const symbolt &main,
162  symbol_table_baset &symbol_table,
163  message_handlert &message_handler)
164 {
165  PRECONDITION(!main.value.is_nil());
166  code_blockt start_function_body;
167  start_function_body.add(code_labelt(CPROVER_HIDE, code_skipt()));
168 
169  add_initialize_call(start_function_body, symbol_table, main.location);
170  // TODO: Support calls to STL functions.
171  // Since STL function calls do not involve a data block, pass all arguments
172  // as normal parameters.
173  add_main_function_block_call(start_function_body, symbol_table, main);
174 
175  // Add the start symbol.
176  symbolt start_symbol{
178  start_symbol.base_name = goto_functionst::entry_point();
179  start_symbol.value.swap(start_function_body);
180 
181  if(!symbol_table.insert(std::move(start_symbol)).second)
182  {
183  messaget message(message_handler);
184  message.error() << "failed to insert start symbol" << messaget::eom;
185  return true;
186  }
187 
188  return false;
189 }
190 
192  symbol_table_baset &symbol_table,
193  message_handlert &message_handler)
194 {
195  // Check if the entry point is already present and return if it is.
196  if(
197  symbol_table.symbols.find(goto_functionst::entry_point()) !=
198  symbol_table.symbols.end())
199  return false;
200 
201  irep_idt main_symbol_name;
202 
203  // Find main symbol given by the user.
204  if(config.main.has_value())
205  {
207  symbol_table, message_handler, config.main.value()))
208  return true;
209  main_symbol_name = config.main.value();
210  }
211  // Fallback: Search for block with TIA main standard name.
212  // TODO: Support the standard entry point of STL (organisation blocks).
213  // This also requires to expand the grammar and typecheck.
214  else
215  {
217  symbol_table, message_handler, ID_statement_list_main_function))
218  return true;
219  main_symbol_name = ID_statement_list_main_function;
220  }
221 
222  const symbolt &main = symbol_table.lookup_ref(main_symbol_name);
223 
224  // Check if the symbol has a body.
225  if(main.value.is_nil())
226  {
227  messaget message(message_handler);
228  message.error() << "main symbol `" << id2string(main_symbol_name)
229  << "' has no body" << messaget::eom;
230  return true;
231  }
232 
233  generate_rounding_mode(symbol_table);
236  main, symbol_table, message_handler);
237 }
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
configt config
Definition: config.cpp:25
signedbv_typet signed_int_type()
Definition: c_types.cpp:22
Operator to return the address of an object.
Definition: pointer_expr.h:540
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
codet representation of a label for branch targets.
Definition: std_code.h:959
A codet representing a skip statement.
Definition: std_code.h:322
const irep_idt & get_base_name() const
Definition: std_types.h:639
Base type of functions.
Definition: std_types.h:583
const parameterst & parameters() const
Definition: std_types.h:699
std::optional< std::string > main
Definition: config.h:356
A constant literal expression.
Definition: std_expr.h:2987
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The empty type.
Definition: std_types.h:51
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool is_not_nil() const
Definition: irep.h:368
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
The symbol table base class interface.
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.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:70
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
const typet & subtype() const
Definition: type.h:187
int main(int argc, char *argv[])
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static void add_initialize_call(code_blockt &function_body, const symbol_table_baset &symbol_table, const source_locationt &main_symbol_location)
Creates a call to __CPROVER_initialize and adds it to the start function's body.
static bool is_main_symbol_invalid(const symbol_table_baset &symbol_table, message_handlert &message_handler, const irep_idt &main_symbol_name)
Searches for symbols with the given name (which is considered to be the name of the main symbol) and ...
bool statement_list_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler)
Creates a new entry point for the Statement List language.
static void add_main_function_block_call(code_blockt &function_body, symbol_table_baset &symbol_table, const symbolt &main_function_block)
Creates a call to the main function block and adds it to the start function's body.
#define CPROVER_HIDE
Name of the CPROVER-specific hide label.
#define DB_ENTRY_POINT_POSTFIX
Postfix for the artificial data block that is created when calling a main symbol that is a function b...
static void generate_rounding_mode(symbol_table_baset &symbol_table)
Creates __CPROVER_rounding_mode and adds it to the symbol table.
static void generate_statement_list_init_function(symbol_table_baset &symbol_table)
Creates __CPROVER_initialize and adds it to the symbol table.
bool generate_statement_list_start_function(const symbolt &main, symbol_table_baset &symbol_table, message_handlert &message_handler)
Creates a start function and adds it to the symbol table.
Statement List Language Entry Point.
#define INITIALIZE_FUNCTION
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Author: Diffblue Ltd.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208