cprover
Loading...
Searching...
No Matches
jsil_convert.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language Conversion
4
5Author: 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{
23public:
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
30protected:
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
70bool 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.
const irep_idt & get_statement() const
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
const source_locationt & source_location() const
Definition expr.h:230
source_locationt & add_source_location()
Definition expr.h:235
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
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.
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 & where()
Definition std_expr.h:2332
exprt & old()
Definition std_expr.h:2322
#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.