cprover
jsil_entry_point.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: 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 
19 
21 
22 static void create_initialize(symbol_tablet &symbol_table)
23 {
24  symbolt initialize;
25  initialize.name = INITIALIZE_FUNCTION;
26  initialize.base_name = INITIALIZE_FUNCTION;
27  initialize.mode="jsil";
28 
29  initialize.type = code_typet({}, empty_typet());
30 
31  code_blockt init_code;
32 
33  namespacet ns(symbol_table);
34 
35  symbol_exprt rounding_mode=
36  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
37 
38  code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
39  init_code.add(a);
40 
41  initialize.value=init_code;
42 
43  if(symbol_table.add(initialize))
44  throw "failed to add " INITIALIZE_FUNCTION;
45 }
46 
48  symbol_tablet &symbol_table,
49  message_handlert &message_handler)
50 {
51  // check if main is already there
52  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
53  symbol_table.symbols.end())
54  return false; // silently ignore
55 
56  irep_idt main_symbol;
57 
58  // find main symbol, if any is given
59  if(config.main.has_value())
60  {
61  std::list<irep_idt> matches;
62 
64  it, symbol_table.symbol_base_map, config.main.value())
65  {
66  // look it up
67  symbol_tablet::symbolst::const_iterator s_it=
68  symbol_table.symbols.find(it->second);
69 
70  if(s_it==symbol_table.symbols.end())
71  continue;
72 
73  if(s_it->second.type.id()==ID_code)
74  matches.push_back(it->second);
75  }
76 
77  if(matches.empty())
78  {
79  messaget message(message_handler);
80  message.error() << "main symbol '" << config.main.value() << "' not found"
81  << messaget::eom;
82  return true; // give up
83  }
84 
85  if(matches.size()>=2)
86  {
87  messaget message(message_handler);
88  message.error() << "main symbol '" << config.main.value()
89  << "' is ambiguous" << messaget::eom;
90  return true;
91  }
92 
93  main_symbol=matches.front();
94  }
95  else
96  main_symbol=ID_main;
97 
98  // look it up
99  symbol_tablet::symbolst::const_iterator s_it=
100  symbol_table.symbols.find(main_symbol);
101 
102  if(s_it==symbol_table.symbols.end())
103  {
104  messaget message(message_handler);
105  message.error() << "main symbol '" << id2string(main_symbol)
106  << "' not in symbol table" << messaget::eom;
107  return true; // give up, no main
108  }
109 
110  const symbolt &symbol=s_it->second;
111 
112  // check if it has a body
113  if(symbol.value.is_nil())
114  {
115  messaget message(message_handler);
116  message.error() << "main symbol '" << main_symbol << "' has no body"
117  << messaget::eom;
118  return false; // give up
119  }
120 
121  create_initialize(symbol_table);
122 
123  code_blockt init_code;
124 
125  // build call to initialization function
126 
127  {
128  symbol_tablet::symbolst::const_iterator init_it=
129  symbol_table.symbols.find(INITIALIZE_FUNCTION);
130 
131  if(init_it==symbol_table.symbols.end())
132  throw "failed to find " INITIALIZE_FUNCTION " symbol";
133 
134  code_function_callt call_init(init_it->second.symbol_expr());
135  call_init.add_source_location()=symbol.location;
136  init_code.add(call_init);
137  }
138 
139  // build call to main function
140 
141  code_function_callt call_main(symbol.symbol_expr());
142  call_main.add_source_location()=symbol.location;
143  call_main.function().add_source_location()=symbol.location;
144 
145  init_code.add(call_main);
146 
147  // add "main"
148  symbolt new_symbol;
149 
150  new_symbol.name=goto_functionst::entry_point();
151  new_symbol.type = code_typet({}, empty_typet());
152  new_symbol.value.swap(init_code);
153 
154  if(!symbol_table.insert(std::move(new_symbol)).second)
155  {
157  message.set_message_handler(message_handler);
158  message.error() << "failed to move main symbol" << messaget::eom;
159  return true;
160  }
161 
162  return false;
163 }
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
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
arith_tools.h
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
Definition: symbol_table_base.h:33
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
configt::main
optionalt< std::string > main
Definition: config.h:181
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
jsil_entry_point.h
Jsil Language.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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:463
code_typet
Base type of functions.
Definition: std_types.h:736
irept::is_nil
bool is_nil() const
Definition: irep.h:398
message_handlert
Definition: message.h:28
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
config
configt config
Definition: config.cpp:24
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
jsil_entry_point
bool jsil_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: jsil_entry_point.cpp:47
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
forall_symbol_base_map
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
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
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
create_initialize
static void create_initialize(symbol_tablet &symbol_table)
Definition: jsil_entry_point.cpp:22