Skip to content

Commit 2803ab8

Browse files
tautschnigtautschnig
committed
Basic language front end for Javascript intermediate language
1 parent 33f65e1 commit 2803ab8

20 files changed

+2468
-2
lines changed

‎src/Makefile

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
22
goto-symex langapi pointer-analysis solvers util linking xmllang \
33
assembler analyses java_bytecode aa-path-symex path-symex musketeer \
4-
json cegis goto-analyzer
4+
json cegis goto-analyzer jsil
55

66
all: cbmc.dir goto-cc.dir goto-instrument.dir path-symex.dir goto-analyzer.dir
77

@@ -18,7 +18,8 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
1818
cpp.dir: ansi-c.dir linking.dir
1919

2020
languages: util.dir langapi.dir \
21-
cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir
21+
cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
22+
jsil.dir
2223

2324
goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
2425
goto-symex.dir linking.dir analyses.dir solvers.dir \

‎src/jsil/Makefile

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
SRC = jsil_y.tab.cpp jsil_lex.yy.cpp \
2+
jsil_convert.cpp jsil_language.cpp jsil_parse_tree.cpp \
3+
jsil_parser.cpp jsil_typecheck.cpp expr2jsil.cpp \
4+
jsil_entry_point.cpp jsil_internal_additions.cpp
5+
6+
INCLUDES= -I ..
7+
8+
include ../config.inc
9+
include ../common
10+
11+
CLEANFILES = jsil$(LIBEXT) \
12+
jsil_y.tab.h jsil_y.tab.cpp jsil_lex.yy.cpp \
13+
jsil_y.tab.cpp.output jsil_y.output
14+
15+
all: jsil$(LIBEXT)
16+
17+
###############################################################################
18+
19+
jsil$(LIBEXT): $(OBJ)
20+
$(LINKLIB)
21+
22+
jsil_y.tab.cpp: parser.y
23+
$(YACC) $(YFLAGS) $$flags -pyyjsil -d parser.y -o $@
24+
25+
jsil_y.tab.h: jsil_y.tab.cpp
26+
if [ -e jsil_y.tab.hpp ] ; then mv jsil_y.tab.hpp jsil_y.tab.h ; else \
27+
mv jsil_y.tab.cpp.h jsil_y.tab.h ; fi
28+
29+
jsil_lex.yy.cpp: scanner.l
30+
$(LEX) -Pyyjsil -o$@ scanner.l
31+
32+
# extra dependencies
33+
jsil_y.tab$(OBJEXT): jsil_y.tab.cpp jsil_y.tab.h
34+
jsil_lex.yy$(OBJEXT): jsil_y.tab.cpp jsil_lex.yy.cpp jsil_y.tab.h
35+

‎src/jsil/expr2jsil.cpp

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
/*******************************************************************\
2+
3+
Module: Jsil Language
4+
5+
Author: Michael Tautschnig, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <ansi-c/expr2c_class.h>
10+
11+
#include "expr2jsil.h"
12+
13+
class expr2jsilt:public expr2ct
14+
{
15+
public:
16+
expr2jsilt(const namespacet &_ns):expr2ct(_ns) { }
17+
18+
virtual std::string convert(const exprt &src)
19+
{
20+
return expr2ct::convert(src);
21+
}
22+
23+
virtual std::string convert(const typet &src)
24+
{
25+
return expr2ct::convert(src);
26+
}
27+
28+
protected:
29+
};
30+
31+
/*******************************************************************\
32+
33+
Function: expr2jsil
34+
35+
Inputs:
36+
37+
Outputs:
38+
39+
Purpose:
40+
41+
\*******************************************************************/
42+
43+
std::string expr2jsil(const exprt &expr, const namespacet &ns)
44+
{
45+
expr2jsilt expr2jsil(ns);
46+
expr2jsil.get_shorthands(expr);
47+
return expr2jsil.convert(expr);
48+
}
49+
50+
/*******************************************************************\
51+
52+
Function: type2jsil
53+
54+
Inputs:
55+
56+
Outputs:
57+
58+
Purpose:
59+
60+
\*******************************************************************/
61+
62+
std::string type2jsil(const typet &type, const namespacet &ns)
63+
{
64+
expr2jsilt expr2jsil(ns);
65+
return expr2jsil.convert(type);
66+
}

‎src/jsil/expr2jsil.h

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
/*******************************************************************\
2+
3+
Module: Jsil Language
4+
5+
Author: Michael Tautschnig, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_EXPR2JSIL_H
10+
#define CPROVER_EXPR2JSIL_H
11+
12+
#include <string>
13+
14+
class exprt;
15+
class namespacet;
16+
class typet;
17+
18+
std::string expr2jsil(const exprt &expr, const namespacet &ns);
19+
std::string type2jsil(const typet &type, const namespacet &ns);
20+
21+
#endif

‎src/jsil/jsil_convert.cpp

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
/*******************************************************************\
2+
3+
Module: Jsil Language Conversion
4+
5+
Author: Michael Tautschnig, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <util/message.h>
10+
#include <util/symbol_table.h>
11+
12+
#include "jsil_parse_tree.h"
13+
#include "jsil_convert.h"
14+
15+
class jsil_convertt:public messaget
16+
{
17+
public:
18+
jsil_convertt(
19+
symbol_tablet &_symbol_table,
20+
message_handlert &_message_handler):
21+
messaget(_message_handler),
22+
symbol_table(_symbol_table)
23+
{
24+
}
25+
26+
bool operator()(const jsil_parse_treet &parse_tree);
27+
28+
protected:
29+
symbol_tablet &symbol_table;
30+
31+
bool convert_code(const symbolt &symbol, codet &code);
32+
};
33+
34+
/*******************************************************************\
35+
36+
Function: jsil_convertt::operator()
37+
38+
Inputs:
39+
40+
Outputs:
41+
42+
Purpose:
43+
44+
\*******************************************************************/
45+
46+
bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree)
47+
{
48+
for(jsil_parse_treet::itemst::const_iterator
49+
it=parse_tree.items.begin();
50+
it!=parse_tree.items.end();
51+
++it)
52+
{
53+
symbolt new_symbol;
54+
it->to_symbol(new_symbol);
55+
56+
if(convert_code(new_symbol, to_code(new_symbol.value)))
57+
return true;
58+
59+
if(symbol_table.add(new_symbol))
60+
{
61+
throw "duplicate symbol "+id2string(new_symbol.name);
62+
63+
return true;
64+
}
65+
}
66+
67+
return false;
68+
}
69+
70+
/*******************************************************************\
71+
72+
Function: jsil_convertt::convert_code
73+
74+
Inputs:
75+
76+
Outputs:
77+
78+
Purpose:
79+
80+
\*******************************************************************/
81+
82+
bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
83+
{
84+
if(code.get_statement()==ID_block)
85+
{
86+
Forall_operands(it, code)
87+
if(convert_code(symbol, to_code(*it)))
88+
return true;
89+
}
90+
else if(code.get_statement()==ID_assign)
91+
{
92+
code_assignt &a=to_code_assign(code);
93+
94+
if(a.rhs().id()==ID_with)
95+
{
96+
exprt to_try=a.rhs().op0();
97+
codet t(code_assignt(a.lhs(), to_try));
98+
if(convert_code(symbol, t))
99+
return true;
100+
101+
irep_idt c_target=
102+
to_symbol_expr(a.rhs().op1()).get_identifier();
103+
code_gotot g(c_target);
104+
105+
code_try_catcht t_c;
106+
t_c.try_code().swap(t);
107+
code_declt d(symbol.symbol_expr());
108+
t_c.add_catch(d, g);
109+
t_c.add_source_location()=code.source_location();
110+
111+
code.swap(t_c);
112+
}
113+
else if(a.rhs().id()==ID_side_effect &&
114+
to_side_effect_expr(a.rhs()).get_statement()== ID_function_call)
115+
{
116+
side_effect_expr_function_callt f_expr=
117+
to_side_effect_expr_function_call(a.rhs());
118+
119+
code_function_callt f;
120+
f.lhs().swap(a.lhs());
121+
f.function().swap(f_expr.function());
122+
f.arguments().swap(f_expr.arguments());
123+
f.add_source_location()=code.source_location();
124+
125+
code.swap(f);
126+
}
127+
}
128+
129+
return false;
130+
}
131+
132+
/*******************************************************************\
133+
134+
Function: jsil_convert
135+
136+
Inputs:
137+
138+
Outputs:
139+
140+
Purpose:
141+
142+
\*******************************************************************/
143+
144+
bool jsil_convert(
145+
const jsil_parse_treet &parse_tree,
146+
symbol_tablet &symbol_table,
147+
message_handlert &message_handler)
148+
{
149+
jsil_convertt jsil_convert(symbol_table, message_handler);
150+
151+
try
152+
{
153+
return jsil_convert(parse_tree);
154+
}
155+
156+
catch(int)
157+
{
158+
}
159+
160+
catch(const char *e)
161+
{
162+
jsil_convert.error() << e << messaget::eom;
163+
}
164+
165+
catch(const std::string &e)
166+
{
167+
jsil_convert.error() << e << messaget::eom;
168+
}
169+
170+
return true;
171+
}

‎src/jsil/jsil_convert.h

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/*******************************************************************\
2+
3+
Module: Jsil Language Conversion
4+
5+
Author: Michael Tautschnig, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_JSIL_CONVERT_H
10+
#define CPROVER_JSIL_CONVERT_H
11+
12+
class jsil_parse_treet;
13+
class message_handlert;
14+
class symbol_tablet;
15+
16+
bool jsil_convert(
17+
const jsil_parse_treet &parse_tree,
18+
symbol_tablet &symbol_table,
19+
message_handlert &message_handler);
20+
21+
#endif
22+

0 commit comments

Comments
 (0)