cprover
Loading...
Searching...
No Matches
jsil_entry_point.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: Michael Tautschnig, tautschn@amazon.com
6
7\*******************************************************************/
8
11
12#include "jsil_entry_point.h"
13
14#include <util/arith_tools.h>
15#include <util/config.h>
16#include <util/message.h>
17#include <util/namespace.h>
18#include <util/range.h>
19#include <util/std_code.h>
21
24
26
27static void create_initialize(symbol_table_baset &symbol_table)
28{
29 symbolt initialize{
31 initialize.base_name = INITIALIZE_FUNCTION;
32
34
35 namespacet ns(symbol_table);
36
37 symbol_exprt rounding_mode =
38 ns.lookup(rounding_mode_identifier()).symbol_expr();
39
40 code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
41 init_code.add(a);
42
43 initialize.value=init_code;
44
45 if(symbol_table.add(initialize))
46 throw "failed to add " INITIALIZE_FUNCTION;
47}
48
50 symbol_table_baset &symbol_table,
51 message_handlert &message_handler)
52{
53 // check if main is already there
54 if(symbol_table.symbols.find(goto_functionst::entry_point())!=
55 symbol_table.symbols.end())
56 return false; // silently ignore
57
58 irep_idt main_symbol;
59
60 // find main symbol, if any is given
61 if(config.main.has_value())
62 {
63 std::list<irep_idt> matches;
64
65 for(const auto &symbol_name_entry :
66 equal_range(symbol_table.symbol_base_map, config.main.value()))
67 {
68 // look it up
69 symbol_table_baset::symbolst::const_iterator s_it =
70 symbol_table.symbols.find(symbol_name_entry.second);
71
72 if(s_it==symbol_table.symbols.end())
73 continue;
74
75 if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
76 matches.push_back(symbol_name_entry.second);
77 }
78
79 if(matches.empty())
80 {
81 messaget message(message_handler);
82 message.error() << "main symbol '" << config.main.value() << "' not found"
84 return true; // give up
85 }
86
87 if(matches.size()>=2)
88 {
89 messaget message(message_handler);
90 message.error() << "main symbol '" << config.main.value()
91 << "' is ambiguous" << messaget::eom;
92 return true;
93 }
94
95 main_symbol=matches.front();
96 }
97 else
98 main_symbol=ID_main;
99
100 // look it up
101 symbol_table_baset::symbolst::const_iterator s_it =
102 symbol_table.symbols.find(main_symbol);
103
104 if(s_it==symbol_table.symbols.end())
105 {
106 messaget message(message_handler);
107 message.error() << "main symbol '" << id2string(main_symbol)
108 << "' not in symbol table" << messaget::eom;
109 return true; // give up, no main
110 }
111
112 const symbolt &symbol=s_it->second;
113
114 // check if it has a body
115 if(symbol.value.is_nil())
116 {
117 messaget message(message_handler);
118 message.error() << "main symbol '" << main_symbol << "' has no body"
119 << messaget::eom;
120 return false; // give up
121 }
122
123 create_initialize(symbol_table);
124
126
127 // build call to initialization function
128
129 {
130 symbol_table_baset::symbolst::const_iterator init_it =
131 symbol_table.symbols.find(INITIALIZE_FUNCTION);
132
133 if(init_it==symbol_table.symbols.end())
134 throw "failed to find " INITIALIZE_FUNCTION " symbol";
135
136 code_function_callt call_init(init_it->second.symbol_expr());
137 call_init.add_source_location()=symbol.location;
138 init_code.add(call_init);
139 }
140
141 // build call to main function
142
144 call_main.add_source_location()=symbol.location;
145 call_main.function().add_source_location()=symbol.location;
146
147 init_code.add(call_main);
148
149 // add "main"
150 symbolt new_symbol{
152 new_symbol.base_name = goto_functionst::entry_point();
153 new_symbol.value.swap(init_code);
154
155 if(!symbol_table.insert(std::move(new_symbol)).second)
156 {
157 messaget message;
158 message.set_message_handler(message_handler);
159 message.error() << "failed to move main symbol" << messaget::eom;
160 return true;
161 }
162
163 return false;
164}
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
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
optionalt< std::string > main
Definition config.h:353
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
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_nil() const
Definition irep.h:376
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
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.
Symbol table entry.
Definition symbol.h:28
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
exprt value
Initial value of symbol.
Definition symbol.h:34
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
bool jsil_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler)
static void create_initialize(symbol_table_baset &symbol_table)
Jsil Language.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
Definition range.h:541
#define INITIALIZE_FUNCTION
Author: Diffblue Ltd.