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/range.h>
18#include <util/std_code.h>
19#include <util/symbol_table.h>
20
23
25
26static void create_initialize(symbol_tablet &symbol_table)
27{
28 symbolt initialize;
29 initialize.name = INITIALIZE_FUNCTION;
30 initialize.base_name = INITIALIZE_FUNCTION;
31 initialize.mode="jsil";
32
33 initialize.type = code_typet({}, empty_typet());
34
35 code_blockt init_code;
36
37 namespacet ns(symbol_table);
38
39 symbol_exprt rounding_mode =
40 ns.lookup(rounding_mode_identifier()).symbol_expr();
41
42 code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
43 init_code.add(a);
44
45 initialize.value=init_code;
46
47 if(symbol_table.add(initialize))
48 throw "failed to add " INITIALIZE_FUNCTION;
49}
50
52 symbol_tablet &symbol_table,
53 message_handlert &message_handler)
54{
55 // check if main is already there
56 if(symbol_table.symbols.find(goto_functionst::entry_point())!=
57 symbol_table.symbols.end())
58 return false; // silently ignore
59
60 irep_idt main_symbol;
61
62 // find main symbol, if any is given
63 if(config.main.has_value())
64 {
65 std::list<irep_idt> matches;
66
67 for(const auto &symbol_name_entry :
68 equal_range(symbol_table.symbol_base_map, config.main.value()))
69 {
70 // look it up
71 symbol_tablet::symbolst::const_iterator s_it =
72 symbol_table.symbols.find(symbol_name_entry.second);
73
74 if(s_it==symbol_table.symbols.end())
75 continue;
76
77 if(s_it->second.type.id()==ID_code)
78 matches.push_back(symbol_name_entry.second);
79 }
80
81 if(matches.empty())
82 {
83 messaget message(message_handler);
84 message.error() << "main symbol '" << config.main.value() << "' not found"
86 return true; // give up
87 }
88
89 if(matches.size()>=2)
90 {
91 messaget message(message_handler);
92 message.error() << "main symbol '" << config.main.value()
93 << "' is ambiguous" << messaget::eom;
94 return true;
95 }
96
97 main_symbol=matches.front();
98 }
99 else
100 main_symbol=ID_main;
101
102 // look it up
103 symbol_tablet::symbolst::const_iterator s_it=
104 symbol_table.symbols.find(main_symbol);
105
106 if(s_it==symbol_table.symbols.end())
107 {
108 messaget message(message_handler);
109 message.error() << "main symbol '" << id2string(main_symbol)
110 << "' not in symbol table" << messaget::eom;
111 return true; // give up, no main
112 }
113
114 const symbolt &symbol=s_it->second;
115
116 // check if it has a body
117 if(symbol.value.is_nil())
118 {
119 messaget message(message_handler);
120 message.error() << "main symbol '" << main_symbol << "' has no body"
121 << messaget::eom;
122 return false; // give up
123 }
124
125 create_initialize(symbol_table);
126
127 code_blockt init_code;
128
129 // build call to initialization function
130
131 {
132 symbol_tablet::symbolst::const_iterator init_it=
133 symbol_table.symbols.find(INITIALIZE_FUNCTION);
134
135 if(init_it==symbol_table.symbols.end())
136 throw "failed to find " INITIALIZE_FUNCTION " symbol";
137
138 code_function_callt call_init(init_it->second.symbol_expr());
139 call_init.add_source_location()=symbol.location;
140 init_code.add(call_init);
141 }
142
143 // build call to main function
144
145 code_function_callt call_main(symbol.symbol_expr());
146 call_main.add_source_location()=symbol.location;
147 call_main.function().add_source_location()=symbol.location;
148
149 init_code.add(call_main);
150
151 // add "main"
152 symbolt new_symbol;
153
155 new_symbol.type = code_typet({}, empty_typet());
156 new_symbol.value.swap(init_code);
157
158 if(!symbol_table.insert(std::move(new_symbol)).second)
159 {
160 messaget message;
161 message.set_message_handler(message_handler);
162 message.error() << "failed to move main symbol" << messaget::eom;
163 return true;
164 }
165
166 return false;
167}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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.
Base type of functions.
Definition: std_types.h:539
optionalt< std::string > main
Definition: config.h:326
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
source_locationt & add_source_location()
Definition: expr.h:235
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void swap(irept &irep)
Definition: irep.h:442
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().
Definition: namespace.cpp:138
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
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.
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
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
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
configt config
Definition: config.cpp:25
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
bool jsil_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
static void create_initialize(symbol_tablet &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.