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 
15 
16 #include <util/message.h>
17 #include <util/symbol_table.h>
18 
19 #include "jsil_parse_tree.h"
20 
22 {
23 public:
24  jsil_convertt(symbol_tablet &_symbol_table) : symbol_table(_symbol_table)
25  {
26  }
27 
28  bool operator()(const jsil_parse_treet &parse_tree, message_handlert &);
29 
30 protected:
32 
33  bool convert_code(const symbolt &symbol, codet &code);
34 };
35 
37  const jsil_parse_treet &parse_tree,
38  message_handlert &message_handler)
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  messaget log{message_handler};
62  log.error() << "duplicate symbol " << new_symbol.name << messaget::eom;
63  throw 0;
64  }
65  }
66 
67  return false;
68 }
69 
70 bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
71 {
72  if(code.get_statement()==ID_block)
73  {
74  Forall_operands(it, code)
75  if(convert_code(symbol, to_code(*it)))
76  return true;
77  }
78  else if(code.get_statement()==ID_assign)
79  {
81 
82  if(a.rhs().id()==ID_with)
83  {
84  exprt to_try = to_with_expr(a.rhs()).old();
85  codet t(code_assignt(a.lhs(), to_try));
86  if(convert_code(symbol, t))
87  return true;
88 
89  irep_idt c_target =
91  code_gotot g(c_target);
92 
93  code_try_catcht t_c(std::move(t));
94  // Adding empty symbol to catch decl
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 
107  code_function_callt f(a.lhs(), f_expr.function(), f_expr.arguments());
109 
110  code.swap(f);
111  }
112  }
113 
114  return false;
115 }
116 
118  const jsil_parse_treet &parse_tree,
119  symbol_tablet &symbol_table,
120  message_handlert &message_handler)
121 {
122  jsil_convertt jsil_convert{symbol_table};
123 
124  try
125  {
126  return jsil_convert(parse_tree, message_handler);
127  }
128 
129  catch(int)
130  {
131  }
132 
133  catch(const char *e)
134  {
135  messaget log{message_handler};
136  log.error() << e << messaget::eom;
137  }
138 
139  catch(const std::string &e)
140  {
141  messaget log{message_handler};
142  log.error() << e << messaget::eom;
143  }
144 
145  return true;
146 }
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
Definition: std_code.h:347
codet representation of a function call statement.
codet representation of a goto statement.
Definition: std_code.h:841
codet representation of a try/catch block.
Definition: std_code.h:1986
void add_catch(const code_frontend_declt &to_catch, const codet &code_catch)
Definition: std_code.h:2028
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
const irep_idt & get_statement() const
Definition: std_code_base.h:65
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
bool convert_code(const symbolt &symbol, codet &code)
bool operator()(const jsil_parse_treet &parse_tree, message_handlert &)
symbol_tablet & symbol_table
jsil_convertt(symbol_tablet &_symbol_table)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
exprt::operandst & arguments()
Definition: std_code.h:1718
const irep_idt & get_statement() const
Definition: std_code.h:1472
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
const irep_idt & get_identifier() const
Definition: std_expr.h:109
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
exprt & old()
Definition: std_expr.h:2322
exprt & where()
Definition: std_expr.h:2332
#define Forall_operands(it, expr)
Definition: expr.h:25
const code_assignt & to_code_assign(const codet &code)
bool jsil_convert(const jsil_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler)
Jsil Language Conversion.
Jsil Language.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
Author: Diffblue Ltd.