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(symbol_table.has_symbol(new_symbol.name))
52  {
53  symbolt &s=symbol_table.lookup(new_symbol.name);
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=a.rhs().op0();
84  codet t(code_assignt(a.lhs(), to_try));
85  if(convert_code(symbol, t))
86  return true;
87 
88  irep_idt c_target=
89  to_symbol_expr(a.rhs().op1()).get_identifier();
90  code_gotot g(c_target);
91 
92  code_try_catcht t_c;
93  t_c.try_code().swap(t);
94  // Adding empty symbol to catch decl
95  code_declt d(symbol_exprt("decl_symbol"));
96  t_c.add_catch(d, g);
98 
99  code.swap(t_c);
100  }
101  else if(a.rhs().id()==ID_side_effect &&
102  to_side_effect_expr(a.rhs()).get_statement()== ID_function_call)
103  {
106 
108  f.lhs().swap(a.lhs());
109  f.function().swap(f_expr.function());
110  f.arguments().swap(f_expr.arguments());
111  f.add_source_location()=code.source_location();
112 
113  code.swap(f);
114  }
115  }
116 
117  return false;
118 }
119 
121  const jsil_parse_treet &parse_tree,
124 {
125  jsil_convertt jsil_convert(symbol_table, message_handler);
126 
127  try
128  {
129  return jsil_convert(parse_tree);
130  }
131 
132  catch(int)
133  {
134  }
135 
136  catch(const char *e)
137  {
138  jsil_convert.error() << e << messaget::eom;
139  }
140 
141  catch(const std::string &e)
142  {
143  jsil_convert.error() << e << messaget::eom;
144  }
145 
146  return true;
147 }
const irep_idt & get_statement() const
Definition: std_code.h:37
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1083
irep_idt name
The unique identifier.
Definition: symbol.h:46
bool operator()(const jsil_parse_treet &parse_tree)
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
A try/catch block.
Definition: std_code.h:1160
exprt & op0()
Definition: expr.h:84
exprt value
Initial value of symbol.
Definition: symbol.h:40
A `goto&#39; instruction.
Definition: std_code.h:613
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
A declaration of a local variable.
Definition: std_code.h:192
exprt & rhs()
Definition: std_code.h:162
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
A function call.
Definition: std_code.h:657
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
A function call side effect.
Definition: std_code.h:1052
Jsil Language.
bool convert_code(const symbolt &symbol, codet &code)
symbol_tablet & symbol_table
codet & try_code()
Definition: std_code.h:1168
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const source_locationt & source_location() const
Definition: expr.h:142
Jsil Language Conversion.
bool jsil_convert(const jsil_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler)
exprt::operandst & arguments()
Definition: std_code.h:1071
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
jsil_convertt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
A statement in a programming language.
Definition: std_code.h:19
message_handlert * message_handler
Definition: message.h:259
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:1202
Assignment.
Definition: std_code.h:144