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,
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
59  if(config.main!="")
60  {
61  std::list<irep_idt> matches;
62 
64  {
65  // look it up
66  symbol_tablet::symbolst::const_iterator s_it=
67  symbol_table.symbols.find(it->second);
68 
69  if(s_it==symbol_table.symbols.end())
70  continue;
71 
72  if(s_it->second.type.id()==ID_code)
73  matches.push_back(it->second);
74  }
75 
76  if(matches.empty())
77  {
78  messaget message(message_handler);
79  message.error() << "main symbol `" << config.main
80  << "' not found" << messaget::eom;
81  return true; // give up
82  }
83 
84  if(matches.size()>=2)
85  {
86  messaget message(message_handler);
87  message.error() << "main symbol `" << config.main
88  << "' is ambiguous" << messaget::eom;
89  return true;
90  }
91 
92  main_symbol=matches.front();
93  }
94  else
95  main_symbol=ID_main;
96 
97  // look it up
98  symbol_tablet::symbolst::const_iterator s_it=
99  symbol_table.symbols.find(main_symbol);
100 
101  if(s_it==symbol_table.symbols.end())
102  {
103  messaget message(message_handler);
104  message.error() << "main symbol `" << id2string(main_symbol)
105  << "' not in symbol table" << messaget::eom;
106  return true; // give up, no main
107  }
108 
109  const symbolt &symbol=s_it->second;
110 
111  // check if it has a body
112  if(symbol.value.is_nil())
113  {
114  messaget message(message_handler);
115  message.error() << "main symbol `" << main_symbol
116  << "' has no body" << messaget::eom;
117  return false; // give up
118  }
119 
120  create_initialize(symbol_table);
121 
122  code_blockt init_code;
123 
124  // build call to initialization function
125 
126  {
127  symbol_tablet::symbolst::const_iterator init_it=
128  symbol_table.symbols.find(INITIALIZE_FUNCTION);
129 
130  if(init_it==symbol_table.symbols.end())
131  throw "failed to find " INITIALIZE_FUNCTION " symbol";
132 
133  code_function_callt call_init;
134  call_init.lhs().make_nil();
135  call_init.add_source_location()=symbol.location;
136  call_init.function()=init_it->second.symbol_expr();
137 
138  init_code.move_to_operands(call_init);
139  }
140 
141  // build call to main function
142 
143  code_function_callt call_main;
144  call_main.add_source_location()=symbol.location;
145  call_main.function()=symbol.symbol_expr();
146  call_main.function().add_source_location()=symbol.location;
147 
148  init_code.move_to_operands(call_main);
149 
150  // add "main"
151  symbolt new_symbol;
152 
153  new_symbol.name=goto_functionst::entry_point();
154  new_symbol.type = code_typet({}, empty_typet());
155  new_symbol.value.swap(init_code);
156 
157  if(!symbol_table.insert(std::move(new_symbol)).second)
158  {
159  messaget message;
161  message.error() << "failed to move main symbol" << messaget::eom;
162  return true;
163  }
164 
165  return false;
166 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:52
const symbol_base_mapt & symbol_base_map
Goto Programs with Functions.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
exprt value
Initial value of symbol.
Definition: symbol.h:37
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
static void create_initialize(symbol_tablet &symbol_table)
The empty type.
Definition: std_types.h:54
std::string main
Definition: config.h:163
#define INITIALIZE_FUNCTION
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A function call.
Definition: std_code.h:828
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
const symbolst & symbols
bool jsil_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
static irep_idt entry_point()
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
exprt & function()
Definition: std_code.h:848
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Jsil Language.
Assignment.
Definition: std_code.h:195
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.