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 
19 class jsil_convertt:public messaget
20 {
21 public:
23  symbol_tablet &_symbol_table,
24  message_handlert &_message_handler):
25  messaget(_message_handler),
26  symbol_table(_symbol_table)
27  {
28  }
29 
30  bool operator()(const jsil_parse_treet &parse_tree);
31 
32 protected:
34 
35  bool convert_code(const symbolt &symbol, codet &code);
36 };
37 
39 {
40  for(jsil_parse_treet::itemst::const_iterator
41  it=parse_tree.items.begin();
42  it!=parse_tree.items.end();
43  ++it)
44  {
45  symbolt new_symbol;
46  it->to_symbol(new_symbol);
47 
48  if(convert_code(new_symbol, to_code(new_symbol.value)))
49  return true;
50 
51  if(const auto maybe_symbol=symbol_table.lookup(new_symbol.name))
52  {
53  const symbolt &s=*maybe_symbol;
54  if(s.value.id()=="no-body-just-yet")
55  {
57  }
58  }
59  if(symbol_table.add(new_symbol))
60  {
61  error() << "duplicate symbol " << new_symbol.name << eom;
62  throw 0;
63  }
64  }
65 
66  return false;
67 }
68 
69 bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
70 {
71  if(code.get_statement()==ID_block)
72  {
73  Forall_operands(it, code)
74  if(convert_code(symbol, to_code(*it)))
75  return true;
76  }
77  else if(code.get_statement()==ID_assign)
78  {
80 
81  if(a.rhs().id()==ID_with)
82  {
83  exprt to_try = to_with_expr(a.rhs()).old();
84  codet t(code_assignt(a.lhs(), to_try));
85  if(convert_code(symbol, t))
86  return true;
87 
88  irep_idt c_target =
90  code_gotot g(c_target);
91 
92  code_try_catcht t_c(std::move(t));
93  // Adding empty symbol to catch decl
94  code_declt d(symbol_exprt::typeless("decl_symbol"));
95  t_c.add_catch(d, g);
97 
98  code.swap(t_c);
99  }
100  else if(a.rhs().id()==ID_side_effect &&
101  to_side_effect_expr(a.rhs()).get_statement()== ID_function_call)
102  {
105 
106  code_function_callt f(a.lhs(), f_expr.function(), f_expr.arguments());
108 
109  code.swap(f);
110  }
111  }
112 
113  return false;
114 }
115 
117  const jsil_parse_treet &parse_tree,
118  symbol_tablet &symbol_table,
119  message_handlert &message_handler)
120 {
121  jsil_convertt jsil_convert(symbol_table, message_handler);
122 
123  try
124  {
125  return jsil_convert(parse_tree);
126  }
127 
128  catch(int)
129  {
130  }
131 
132  catch(const char *e)
133  {
134  jsil_convert.error() << e << messaget::eom;
135  }
136 
137  catch(const std::string &e)
138  {
139  jsil_convert.error() << e << messaget::eom;
140  }
141 
142  return true;
143 }
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:2471
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:2182
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_try_catcht
codet representation of a try/catch block.
Definition: std_code.h:2429
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2117
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
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:53
jsil_convertt::jsil_convertt
jsil_convertt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
Definition: jsil_convert.cpp:22
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:1931
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:1183
with_exprt::old
exprt & old()
Definition: std_expr.h:3060
jsil_parse_treet
Definition: jsil_parse_tree.h:102
messaget::error
mstreamt & error() const
Definition: message.h:399
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1127
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:3112
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
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:33
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:2161
jsil_parse_tree.h
Jsil Language.
jsil_convertt::convert_code
bool convert_code(const symbolt &symbol, codet &code)
Definition: jsil_convert.cpp:69
jsil_convert
bool jsil_convert(const jsil_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: jsil_convert.cpp:116
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
jsil_convertt::operator()
bool operator()(const jsil_parse_treet &parse_tree)
Definition: jsil_convert.cpp:38
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:2151
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
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:254
with_exprt::where
exprt & where()
Definition: std_expr.h:3070
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