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/symbol_table.h>
17 #include <util/message.h>
18 #include <util/std_types.h>
19 #include <util/cprover_prefix.h>
20 
22 
23 #define INITIALIZE CPROVER_PREFIX "initialize"
24 
25 static void create_initialize(symbol_tablet &symbol_table)
26 {
27  symbolt initialize;
28  initialize.name=CPROVER_PREFIX "initialize";
29  initialize.base_name=CPROVER_PREFIX "initialize";
30  initialize.mode="jsil";
31 
32  code_typet type;
33  type.return_type()=empty_typet();
34  initialize.type=type;
35 
36  code_blockt init_code;
37 
38  namespacet ns(symbol_table);
39 
40  symbol_exprt rounding_mode=
41  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
42 
43  code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
44  init_code.add(a);
45 
46  initialize.value=init_code;
47 
48  if(symbol_table.add(initialize))
49  throw "failed to add " CPROVER_PREFIX "initialize";
50 }
51 
53  symbol_tablet &symbol_table,
54  message_handlert &message_handler)
55 {
56  // check if main is already there
57  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
58  symbol_table.symbols.end())
59  return false; // silently ignore
60 
61  irep_idt main_symbol;
62 
63  // find main symbol
64  if(config.main!="")
65  {
66  std::list<irep_idt> matches;
67 
69  {
70  // look it up
71  symbol_tablet::symbolst::const_iterator s_it=
72  symbol_table.symbols.find(it->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(it->second);
79  }
80 
81  if(matches.empty())
82  {
83  messaget message(message_handler);
84  message.error() << "main symbol `" << config.main
85  << "' not found" << messaget::eom;
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
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
121  << "' has no body" << 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::iterator init_it=
133  symbol_table.symbols.find(CPROVER_PREFIX "initialize");
134 
135  if(init_it==symbol_table.symbols.end())
136  throw "failed to find " CPROVER_PREFIX "initialize symbol";
137 
138  code_function_callt call_init;
139  call_init.lhs().make_nil();
140  call_init.add_source_location()=symbol.location;
141  call_init.function()=init_it->second.symbol_expr();
142 
143  init_code.move_to_operands(call_init);
144  }
145 
146  // build call to main function
147 
148  code_function_callt call_main;
149  call_main.add_source_location()=symbol.location;
150  call_main.function()=symbol.symbol_expr();
151  call_main.function().add_source_location()=symbol.location;
152 
153  init_code.move_to_operands(call_main);
154 
155  // add "main"
156  symbolt new_symbol;
157 
158  code_typet main_type;
159  main_type.return_type()=empty_typet();
160 
161  new_symbol.name=goto_functionst::entry_point();
162  new_symbol.type.swap(main_type);
163  new_symbol.value.swap(init_code);
164 
165  if(symbol_table.move(new_symbol))
166  {
167  messaget message;
168  message.set_message_handler(message_handler);
169  message.error() << "failed to move main symbol" << messaget::eom;
170  return true;
171  }
172 
173  return false;
174 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:55
Goto Programs with Functions.
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
exprt value
Initial value of symbol.
Definition: symbol.h:40
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
symbol_base_mapt symbol_base_map
Definition: symbol_table.h:58
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
void add(const codet &code)
Definition: std_code.h:81
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
symbolst symbols
Definition: symbol_table.h:57
static void create_initialize(symbol_tablet &symbol_table)
The empty type.
Definition: std_types.h:53
std::string main
Definition: config.h:147
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
bool jsil_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
API to type classes.
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:39
exprt & function()
Definition: std_code.h:677
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
Expression to hold a symbol (variable)
Definition: std_expr.h:82
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const typet & return_type() const
Definition: std_types.h:831
Jsil Language.
Assignment.
Definition: std_code.h:144