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 
14 
16 
18 
19 #include <util/c_types.h>
20 #include <util/config.h>
21 #include <util/pointer_expr.h>
22 #include <util/std_code.h>
23 
25 #define ROUNDING_MODE_NAME CPROVER_PREFIX "rounding_mode"
26 
29 #define DB_ENTRY_POINT_POSTFIX "_entry_point"
30 
32 #define CPROVER_HIDE CPROVER_PREFIX "HIDE"
33 
43  const symbol_tablet &symbol_table,
44  message_handlert &message_handler,
45  const irep_idt &main_symbol_name)
46 {
47  bool found = false;
48 
49  for(const std::pair<const irep_idt, symbolt> &pair : symbol_table)
50  {
51  if(pair.first == main_symbol_name && pair.second.type.id() == ID_code)
52  {
53  if(found)
54  {
55  messaget message(message_handler);
56  message.error() << "main symbol `" << main_symbol_name
57  << "' is ambiguous" << messaget::eom;
58  return true;
59  }
60  else
61  found = true;
62  }
63  }
64 
65  if(found)
66  return false;
67  else
68  {
69  messaget message(message_handler);
70  message.error() << "main symbol `" << main_symbol_name << "' not found"
71  << messaget::eom;
72  return true;
73  }
74 }
75 
82 static void add_initialize_call(
83  code_blockt &function_body,
84  const symbol_tablet &symbol_table,
85  const source_locationt &main_symbol_location)
86 {
87  symbolt init = symbol_table.lookup_ref(INITIALIZE_FUNCTION);
88  code_function_callt call_init{init.symbol_expr()};
89  call_init.add_source_location() = main_symbol_location;
90  function_body.add(call_init);
91 }
92 
99  code_blockt &function_body,
100  symbol_tablet &symbol_table,
101  const symbolt &main_function_block)
102 {
103  const code_typet &function_type = to_code_type(main_function_block.type);
104  PRECONDITION(1u == function_type.parameters().size());
105  const code_typet::parametert &data_block_interface =
106  function_type.parameters().front();
107  symbolt instance_data_block;
108  instance_data_block.name =
109  id2string(data_block_interface.get_base_name()) + DB_ENTRY_POINT_POSTFIX;
110  instance_data_block.type = 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_NAME;
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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
generate_statement_list_start_function
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.
Definition: statement_list_entry_point.cpp:165
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
statement_list_typecheck.h
Statement List Language Type Checking.
add_main_function_block_call
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.
Definition: statement_list_entry_point.cpp:98
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
configt::main
optionalt< std::string > main
Definition: config.h:261
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
generate_rounding_mode
static void generate_rounding_mode(symbol_tablet &symbol_table)
Creates __CPROVER_rounding_mode and adds it to the symbol table.
Definition: statement_list_entry_point.cpp:146
add_initialize_call
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.
Definition: statement_list_entry_point.cpp:82
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
is_main_symbol_invalid
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 ...
Definition: statement_list_entry_point.cpp:42
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:589
empty_typet
The empty type.
Definition: std_types.h:45
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
generate_statement_list_init_function
static void generate_statement_list_init_function(symbol_tablet &symbol_table)
Creates __CPROVER_initialize and adds it to the symbol table.
Definition: statement_list_entry_point.cpp:124
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
statement_list_entry_point.h
Statement List Language Entry Point.
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
irept::swap
void swap(irept &irep)
Definition: irep.h:453
code_typet
Base type of functions.
Definition: std_types.h:533
message_handlert
Definition: message.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
std_code.h
main
int main(int argc, char *argv[])
Definition: file_converter.cpp:41
DB_ENTRY_POINT_POSTFIX
#define DB_ENTRY_POINT_POSTFIX
Postfix for the artificial data block that is created when calling a main symbol that is a function b...
Definition: statement_list_entry_point.cpp:29
config
configt config
Definition: config.cpp:24
source_locationt
Definition: source_location.h:20
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:270
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
statement_list_entry_point
bool statement_list_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
Creates a new entry point for the Statement List language.
Definition: statement_list_entry_point.cpp:197
code_typet::parametert
Definition: std_types.h:550
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
config.h
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
CPROVER_HIDE
#define CPROVER_HIDE
Name of the CPROVER-specific hide label.
Definition: statement_list_entry_point.cpp:32
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
ROUNDING_MODE_NAME
#define ROUNDING_MODE_NAME
Name of the CPROVER-specific variable that specifies the rounding mode.
Definition: statement_list_entry_point.cpp:25
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40