Skip to content

Commit bcd2929

Browse files
author
Daniel Kroening
committed
Merge pull request #51 from tautschnig/jsil
JSIL (Javscript Intermediate Language) front-end
2 parents 33f65e1 + a656f27 commit bcd2929

27 files changed

+2521
-3
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/cbmc/Makefile

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,11 @@ ifneq ($(wildcard ../java_bytecode/Makefile),)
5555
endif
5656
endif
5757

58+
ifneq ($(wildcard ../jsil/Makefile),)
59+
OBJ += ../jsil/jsil$(LIBEXT)
60+
CP_CXXFLAGS += -DHAVE_JSIL
61+
endif
62+
5863
ifneq ($(wildcard ../specc/Makefile),)
5964
OBJ += ../specc/specc$(LIBEXT)
6065
CP_CXXFLAGS += -DHAVE_SPECC

‎src/cbmc/cbmc_languages.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,10 @@ Author: Daniel Kroening, [email protected]
1919
#include <java_bytecode/java_bytecode_language.h>
2020
#endif
2121

22+
#ifdef HAVE_JSIL
23+
#include <jsil/jsil_language.h>
24+
#endif
25+
2226
#include "cbmc_parse_options.h"
2327

2428
/*******************************************************************\
@@ -45,5 +49,9 @@ void cbmc_parse_optionst::register_languages()
4549
#ifdef HAVE_JAVA_BYTECODE
4650
register_language(new_java_bytecode_language);
4751
#endif
52+
53+
#ifdef HAVE_JSIL
54+
register_language(new_jsil_language);
55+
#endif
4856
}
4957

‎src/goto-analyzer/Makefile

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,11 @@ ifneq ($(wildcard ../java_bytecode/Makefile),)
3535
endif
3636
endif
3737

38+
ifneq ($(wildcard ../jsil/Makefile),)
39+
OBJ += ../jsil/jsil$(LIBEXT)
40+
CP_CXXFLAGS += -DHAVE_JSIL
41+
endif
42+
3843
ifneq ($(wildcard ../specc/Makefile),)
3944
OBJ += ../specc/specc$(LIBEXT)
4045
CP_CXXFLAGS += -DHAVE_SPECC

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <ansi-c/ansi_c_language.h>
1515
#include <cpp/cpp_language.h>
1616
#include <java_bytecode/java_bytecode_language.h>
17+
#include <jsil/jsil_language.h>
1718

1819
#include <goto-programs/set_properties.h>
1920
#include <goto-programs/remove_function_pointers.h>
@@ -79,6 +80,7 @@ void goto_analyzer_parse_optionst::register_languages()
7980
register_language(new_ansi_c_language);
8081
register_language(new_cpp_language);
8182
register_language(new_java_bytecode_language);
83+
register_language(new_jsil_language);
8284
}
8385

8486
/*******************************************************************\

‎src/goto-cc/Makefile

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,11 @@ ifneq ($(wildcard ../java_bytecode/Makefile),)
4040
endif
4141
endif
4242

43+
ifneq ($(wildcard ../jsil/Makefile),)
44+
OBJ += ../jsil/jsil$(LIBEXT)
45+
CP_CXXFLAGS += -DHAVE_JSIL
46+
endif
47+
4348
###############################################################################
4449

4550
goto-cc$(EXEEXT): $(OBJ)

‎src/goto-cc/compile.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,8 @@ bool compilet::add_input_file(const std::string &file_name)
179179
ext=="i" ||
180180
ext=="ii" ||
181181
ext=="class" ||
182-
ext=="jar")
182+
ext=="jar" ||
183+
ext=="jsil")
183184
{
184185
source_files.push_back(file_name);
185186
}

‎src/goto-cc/goto_cc_languages.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: CM Wintersteiger
1111
#include <ansi-c/ansi_c_language.h>
1212
#include <cpp/cpp_language.h>
1313
#include <java_bytecode/java_bytecode_language.h>
14+
#include <jsil/jsil_language.h>
1415

1516
#ifdef HAVE_SPECC
1617
#include <specc/specc_language.h>
@@ -35,6 +36,7 @@ void goto_cc_modet::register_languages()
3536
register_language(new_ansi_c_language);
3637
register_language(new_cpp_language);
3738
register_language(new_java_bytecode_language);
39+
register_language(new_jsil_language);
3840

3941
#ifdef HAVE_SPECC
4042
register_language(new_specc_language);

‎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

0 commit comments

Comments
 (0)