cprover
Loading...
Searching...
No Matches
statement_list_entry_point.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Statement List Language Entry Point
4
5Author: 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,
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"
71 return true;
72 }
73}
74
83 const symbol_tablet &symbol_table,
85{
86 symbolt init = symbol_table.lookup_ref(INITIALIZE_FUNCTION);
88 call_init.add_source_location() = main_symbol_location;
90}
91
99 symbol_tablet &symbol_table,
101{
102 const code_typet &function_type = to_code_type(main_function_block.type);
103 PRECONDITION(1u == function_type.parameters().size());
105 function_type.parameters().front();
111 instance_data_block.is_static_lifetime = true;
113 symbol_table.add(instance_data_block);
115
118 call_main.add_source_location() = main_function_block.location;
120}
121
125{
126 symbolt init;
128 init.mode = ID_statement_list;
129 init.type = code_typet({}, empty_typet{});
130
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
146static 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;
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());
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.
179
180 // Add the start symbol.
183 start_symbol.type = code_typet({}, empty_typet{});
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
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;
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
codet representation of a function call statement.
codet representation of a label for branch targets.
Definition std_code.h:959
A codet representing a skip statement.
Definition std_code.h:322
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
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
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.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
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
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()
Definition example.cpp:18
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
Author: Diffblue Ltd.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177