cprover
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 
16 
18 
19 #include <util/c_types.h>
20 #include <util/config.h>
21 #include <util/message.h>
22 #include <util/pointer_expr.h>
23 #include <util/std_code.h>
24 #include <util/symbol_table.h>
25 
28 #define DB_ENTRY_POINT_POSTFIX "_entry_point"
29 
31 #define CPROVER_HIDE CPROVER_PREFIX "HIDE"
32 
42  const symbol_tablet &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_tablet &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_tablet &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  instance_data_block.name =
108  id2string(data_block_interface.get_base_name()) + DB_ENTRY_POINT_POSTFIX;
109  instance_data_block.type =
110  to_type_with_subtype(data_block_interface.type()).subtype();
111  instance_data_block.is_static_lifetime = true;
112  instance_data_block.mode = ID_statement_list;
113  symbol_table.add(instance_data_block);
114  const address_of_exprt data_block_ref{instance_data_block.symbol_expr()};
115 
116  code_function_callt::argumentst args{data_block_ref};
117  code_function_callt call_main{main_function_block.symbol_expr(), args};
118  call_main.add_source_location() = main_function_block.location;
119  function_body.add(call_main);
120 }
121 
125 {
126  symbolt init;
127  init.name = INITIALIZE_FUNCTION;
128  init.mode = ID_statement_list;
129  init.type = code_typet({}, empty_typet{});
130 
131  code_blockt dest;
133 
134  for(const std::pair<const irep_idt, symbolt> &pair : symbol_table)
135  {
136  const symbolt &symbol = pair.second;
137  if(symbol.is_static_lifetime && symbol.value.is_not_nil())
138  dest.add(code_assignt{pair.second.symbol_expr(), pair.second.value});
139  }
140  init.value = std::move(dest);
141  symbol_table.add(init);
142 }
143 
146 static void generate_rounding_mode(symbol_tablet &symbol_table)
147 {
148  symbolt rounding_mode;
149  rounding_mode.name = rounding_mode_identifier();
150  rounding_mode.type = signed_int_type();
151  rounding_mode.is_thread_local = true;
152  rounding_mode.is_static_lifetime = true;
153  const constant_exprt rounding_val{
154  std::to_string(ieee_floatt::rounding_modet::ROUND_TO_EVEN),
155  signed_int_type()};
156  rounding_mode.value = rounding_val;
157  symbol_table.add(rounding_mode);
158 }
159 
166  const symbolt &main,
167  symbol_tablet &symbol_table,
168  message_handlert &message_handler)
169 {
170  PRECONDITION(!main.value.is_nil());
171  code_blockt start_function_body;
172  start_function_body.add(code_labelt(CPROVER_HIDE, code_skipt()));
173 
174  add_initialize_call(start_function_body, symbol_table, main.location);
175  // TODO: Support calls to STL functions.
176  // Since STL function calls do not involve a data block, pass all arguments
177  // as normal parameters.
178  add_main_function_block_call(start_function_body, symbol_table, main);
179 
180  // Add the start symbol.
181  symbolt start_symbol;
182  start_symbol.name = goto_functionst::entry_point();
183  start_symbol.type = code_typet({}, empty_typet{});
184  start_symbol.value.swap(start_function_body);
185  start_symbol.mode = main.mode;
186 
187  if(!symbol_table.insert(std::move(start_symbol)).second)
188  {
189  messaget message(message_handler);
190  message.error() << "failed to insert start symbol" << messaget::eom;
191  return true;
192  }
193 
194  return false;
195 }
196 
198  symbol_tablet &symbol_table,
199  message_handlert &message_handler)
200 {
201  // Check if the entry point is already present and return if it is.
202  if(
203  symbol_table.symbols.find(goto_functionst::entry_point()) !=
204  symbol_table.symbols.end())
205  return false;
206 
207  irep_idt main_symbol_name;
208 
209  // Find main symbol given by the user.
210  if(config.main.has_value())
211  {
213  symbol_table, message_handler, config.main.value()))
214  return true;
215  main_symbol_name = config.main.value();
216  }
217  // Fallback: Search for block with TIA main standard name.
218  // TODO: Support the standard entry point of STL (organisation blocks).
219  // This also requires to expand the grammar and typecheck.
220  else
221  {
223  symbol_table, message_handler, ID_statement_list_main_function))
224  return true;
225  main_symbol_name = ID_statement_list_main_function;
226  }
227 
228  const symbolt &main = symbol_table.lookup_ref(main_symbol_name);
229 
230  // Check if the symbol has a body.
231  if(main.value.is_nil())
232  {
233  messaget message(message_handler);
234  message.error() << "main symbol `" << id2string(main_symbol_name)
235  << "' has no body" << messaget::eom;
236  return true;
237  }
238 
239  generate_rounding_mode(symbol_table);
242  main, symbol_table, message_handler);
243 }
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
Operator to return the address of an object.
Definition: pointer_expr.h:361
A 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
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:595
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
optionalt< std::string > main
Definition: config.h:326
A constant literal expression.
Definition: std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
source_locationt & add_source_location()
Definition: expr.h:235
typet & type()
Return the type of the expression.
Definition: expr.h:82
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool is_not_nil() const
Definition: irep.h:380
void swap(irept &irep)
Definition: irep.h:442
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
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.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
bool is_thread_local
Definition: symbol.h:65
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
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
const typet & subtype() const
Definition: type.h:156
configt config
Definition: config.cpp:25
int main(int argc, char *argv[])
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static bool is_main_symbol_invalid(const symbol_tablet &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 ...
static void generate_rounding_mode(symbol_tablet &symbol_table)
Creates __CPROVER_rounding_mode and adds it to the symbol table.
static void add_main_function_block_call(code_blockt &function_body, symbol_tablet &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.
static void generate_statement_list_init_function(symbol_tablet &symbol_table)
Creates __CPROVER_initialize and adds it to the symbol table.
#define DB_ENTRY_POINT_POSTFIX
Postfix for the artificial data block that is created when calling a main symbol that is a function b...
bool generate_statement_list_start_function(const symbolt &main, symbol_tablet &symbol_table, message_handlert &message_handler)
Creates a start function and adds it to the symbol table.
static void add_initialize_call(code_blockt &function_body, const symbol_tablet &symbol_table, const source_locationt &main_symbol_location)
Creates a call to __CPROVER_initialize and adds it to the start function's body.
bool statement_list_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
Creates a new entry point for the Statement List language.
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:744
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:177