cprover
jsil_convert.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language Conversion
4 
5 Author: Michael Tautschnig, tautschn@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #include "jsil_convert.h"
13 
14 #include <util/message.h>
15 #include <util/symbol_table.h>
16 
17 #include "jsil_parse_tree.h"
18 
20 {
21 public:
22  jsil_convertt(symbol_tablet &_symbol_table) : symbol_table(_symbol_table)
23  {
24  }
25 
26  bool operator()(const jsil_parse_treet &parse_tree, message_handlert &);
27 
28 protected:
30 
31  bool convert_code(const symbolt &symbol, codet &code);
32 };
33 
35  const jsil_parse_treet &parse_tree,
36  message_handlert &message_handler)
37 {
38  for(jsil_parse_treet::itemst::const_iterator
39  it=parse_tree.items.begin();
40  it!=parse_tree.items.end();
41  ++it)
42  {
43  symbolt new_symbol;
44  it->to_symbol(new_symbol);
45 
46  if(convert_code(new_symbol, to_code(new_symbol.value)))
47  return true;
48 
49  if(const auto maybe_symbol=symbol_table.lookup(new_symbol.name))
50  {
51  const symbolt &s=*maybe_symbol;
52  if(s.value.id()=="no-body-just-yet")
53  {
55  }
56  }
57  if(symbol_table.add(new_symbol))
58  {
59  messaget log{message_handler};
60  log.error() << "duplicate symbol " << new_symbol.name << messaget::eom;
61  throw 0;
62  }
63  }
64 
65  return false;
66 }
67 
68 bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
69 {
70  if(code.get_statement()==ID_block)
71  {
72  Forall_operands(it, code)
73  if(convert_code(symbol, to_code(*it)))
74  return true;
75  }
76  else if(code.get_statement()==ID_assign)
77  {
79 
80  if(a.rhs().id()==ID_with)
81  {
82  exprt to_try = to_with_expr(a.rhs()).old();
83  codet t(code_assignt(a.lhs(), to_try));
84  if(convert_code(symbol, t))
85  return true;
86 
87  irep_idt c_target =
89  code_gotot g(c_target);
90 
91  code_try_catcht t_c(std::move(t));
92  // Adding empty symbol to catch decl
93  code_declt d(symbol_exprt::typeless("decl_symbol"));
94  t_c.add_catch(d, g);
96 
97  code.swap(t_c);
98  }
99  else if(a.rhs().id()==ID_side_effect &&
100  to_side_effect_expr(a.rhs()).get_statement()== ID_function_call)
101  {
104 
105  code_function_callt f(a.lhs(), f_expr.function(), f_expr.arguments());
107 
108  code.swap(f);
109  }
110  }
111 
112  return false;
113 }
114 
116  const jsil_parse_treet &parse_tree,
117  symbol_tablet &symbol_table,
118  message_handlert &message_handler)
119 {
120  jsil_convertt jsil_convert{symbol_table};
121 
122  try
123  {
124  return jsil_convert(parse_tree, message_handler);
125  }
126 
127  catch(int)
128  {
129  }
130 
131  catch(const char *e)
132  {
133  messaget log{message_handler};
134  log.error() << e << messaget::eom;
135  }
136 
137  catch(const std::string &e)
138  {
139  messaget log{message_handler};
140  log.error() << e << messaget::eom;
141  }
142 
143  return true;
144 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
jsil_parse_treet::items
itemst items
Definition: jsil_parse_tree.h:105
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_try_catcht::add_catch
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:2476
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2187
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_try_catcht
codet representation of a try/catch block.
Definition: std_code.h:2434
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:100
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
exprt
Base class for all expressions.
Definition: expr.h:54
messaget::eom
static eomt eom
Definition: message.h:297
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
with_exprt::old
exprt & old()
Definition: std_expr.h:2183
jsil_parse_treet
Definition: jsil_parse_tree.h:102
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
jsil_convertt::operator()
bool operator()(const jsil_parse_treet &parse_tree, message_handlert &)
Definition: jsil_convert.cpp:34
jsil_convertt::jsil_convertt
jsil_convertt(symbol_tablet &_symbol_table)
Definition: jsil_convert.cpp:22
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
jsil_convert.h
Jsil Language Conversion.
irept::swap
void swap(irept &irep)
Definition: irep.h:452
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition: symbol_table_base.cpp:27
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1920
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_convertt::symbol_table
symbol_tablet & symbol_table
Definition: jsil_convert.cpp:29
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
symbolt
Symbol table entry.
Definition: symbol.h:28
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2166
jsil_parse_tree.h
Jsil Language.
jsil_convertt::convert_code
bool convert_code(const symbolt &symbol, codet &code)
Definition: jsil_convert.cpp:68
jsil_convert
bool jsil_convert(const jsil_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: jsil_convert.cpp:115
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:2156
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
symbol_table.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
with_exprt::where
exprt & where()
Definition: std_expr.h:2193
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
jsil_convertt
Definition: jsil_convert.cpp:20
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35