diff --git a/.gitignore b/.gitignore index cc109ddc3d2..cc8c048280b 100644 --- a/.gitignore +++ b/.gitignore @@ -91,10 +91,6 @@ src/ansi-c/ansi_c_y.tab.cpp src/ansi-c/ansi_c_y.tab.h src/assembler/assembler_lex.yy.cpp src/crangler/c_lex.yy.cpp -src/jsil/jsil_lex.yy.cpp -src/jsil/jsil_y.output -src/jsil/jsil_y.tab.cpp -src/jsil/jsil_y.tab.h src/json/json_lex.yy.cpp src/json/json_y.output src/json/json_y.tab.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 540f840f247..2c1289a121e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -256,7 +256,6 @@ cprover_default_properties( goto-symex goto-synthesizer goto-synthesizer-lib - jsil json json-symtab-language langapi diff --git a/CODEOWNERS b/CODEOWNERS index 9b5fdd7532d..dfbe48cbfb0 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -56,7 +56,6 @@ /src/goto-inspect/ @diffblue/diffblue-opensource /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000 /src/goto-diff/ @tautschnig @peterschrammel -/src/jsil/ @kroening @tautschnig /src/memory-analyzer/ @tautschnig @kroening /jbmc/src/jbmc/ @peterschrammel @TGWDB /jbmc/src/janalyzer/ @peterschrammel @TGWDB diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md index 5d5643d804c..395c42519fe 100644 --- a/doc/architectural/folder-walkthrough.md +++ b/doc/architectural/folder-walkthrough.md @@ -32,7 +32,6 @@ containing the code for a different part of the system. * C: \ref ansi-c * C++: \ref cpp * Java: \ref java_bytecode - * JavaScript: \ref jsil - Tools @@ -155,7 +154,6 @@ digraph directory_dependencies { ansi_c [label = "ansi-c", URL = "\ref ansi-c"]; langapi [URL = "\ref langapi"]; cpp [URL = "\ref cpp"]; - jsil [URL = "\ref jsil"]; java_bytecode [URL = "\ref java_bytecode"]; } @@ -174,15 +172,14 @@ digraph directory_dependencies { JBMC -> { CBMC, java_bytecode }; jdiff -> { goto_diff, java_bytecode }; janalyzer -> { goto_analyzer, java_bytecode }; - CBMC -> { goto_instrument, jsil }; + CBMC -> { goto_instrument }; goto_diff -> { goto_instrument }; - goto_analyzer -> { analyses, jsil, cpp }; + goto_analyzer -> { analyses, cpp }; goto_instrument -> { goto_symex, cpp }; - goto_cc -> { cpp, jsil }; + goto_cc -> { cpp }; smt2_solver -> solvers; java_bytecode -> { analyses, miniz }; - jsil -> linking; cpp -> ansi_c; ansi_c -> langapi; langapi -> goto_programs; diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile index f1fc8fcf0fa..1f309b491af 100644 --- a/jbmc/src/janalyzer/Makefile +++ b/jbmc/src/janalyzer/Makefile @@ -34,11 +34,6 @@ CLEANFILES = janalyzer$(EXEEXT) all: janalyzer$(EXEEXT) -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - ############################################################################### janalyzer$(EXEEXT): $(OBJ) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c5cf6eb697a..c7fb54d4e46 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -99,7 +99,6 @@ add_subdirectory(goto-checker) add_subdirectory(goto-programs) add_subdirectory(goto-symex) add_subdirectory(goto-inspect) -add_subdirectory(jsil) add_subdirectory(json) add_subdirectory(json-symtab-language) add_subdirectory(langapi) diff --git a/src/Makefile b/src/Makefile index 50c5e8c7e97..e9181a2e039 100644 --- a/src/Makefile +++ b/src/Makefile @@ -17,7 +17,6 @@ DIRS = analyses \ goto-programs \ goto-symex \ goto-synthesizer \ - jsil \ json \ json-symtab-language \ langapi \ @@ -82,7 +81,7 @@ crangler.dir: util.dir json.dir languages: util.dir langapi.dir \ cpp.dir ansi-c.dir xmllang.dir assembler.dir \ - jsil.dir json.dir json-symtab-language.dir statement-list.dir + json.dir json-symtab-language.dir statement-list.dir solvers.dir: util.dir diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index 97560d70b57..14ab91958a0 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -29,7 +29,6 @@ target_link_libraries(cbmc-lib ) add_if_library(cbmc-lib bv_refinement) -add_if_library(cbmc-lib jsil) # Executable add_executable(cbmc cbmc_main.cpp) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index da45aec1695..d78b9221461 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -60,11 +60,6 @@ ifneq ($(wildcard ../bv_refinement/Makefile),) CP_CXXFLAGS += -DHAVE_BV_REFINEMENT endif -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - ############################################################################### cbmc$(EXEEXT): $(OBJ) diff --git a/src/cbmc/cbmc_languages.cpp b/src/cbmc/cbmc_languages.cpp index cbf142cf017..ea406f5c485 100644 --- a/src/cbmc/cbmc_languages.cpp +++ b/src/cbmc/cbmc_languages.cpp @@ -18,18 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#ifdef HAVE_JSIL -# include -#endif - void cbmc_parse_optionst::register_languages() { register_language(new_ansi_c_language); register_language(new_statement_list_language); register_language(new_cpp_language); register_language(new_json_symtab_language); - -#ifdef HAVE_JSIL - register_language(new_jsil_language); -#endif } diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt index 9c9fd45de75..0325edd3c2e 100644 --- a/src/cbmc/module_dependencies.txt +++ b/src/cbmc/module_dependencies.txt @@ -6,7 +6,6 @@ goto-checker goto-instrument goto-programs goto-symex -jsil json json-symtab-language langapi # should go away diff --git a/src/cprover/CMakeLists.txt b/src/cprover/CMakeLists.txt index efc757bd34a..8383b5d1af8 100644 --- a/src/cprover/CMakeLists.txt +++ b/src/cprover/CMakeLists.txt @@ -29,7 +29,6 @@ target_link_libraries(cprover-lib ) add_if_library(cprover-lib bv_refinement) -add_if_library(cprover-lib jsil) # Executable add_executable(cprover cprover_main.cpp) diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt index 8486733a795..20cc1f44d49 100644 --- a/src/goto-analyzer/CMakeLists.txt +++ b/src/goto-analyzer/CMakeLists.txt @@ -22,8 +22,6 @@ target_link_libraries(goto-analyzer-lib util ) -add_if_library(goto-analyzer-lib jsil) - # Executable add_executable(goto-analyzer goto_analyzer_main.cpp) target_link_libraries(goto-analyzer goto-analyzer-lib) diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index f5bc1488934..d3cc012ca02 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -36,11 +36,6 @@ CLEANFILES = goto-analyzer$(EXEEXT) all: goto-analyzer$(EXEEXT) -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - ############################################################################### goto-analyzer$(EXEEXT): $(OBJ) diff --git a/src/goto-analyzer/goto_analyzer_languages.cpp b/src/goto-analyzer/goto_analyzer_languages.cpp index 2227340fe8e..11c8018df59 100644 --- a/src/goto-analyzer/goto_analyzer_languages.cpp +++ b/src/goto-analyzer/goto_analyzer_languages.cpp @@ -16,16 +16,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include -#ifdef HAVE_JSIL -# include -#endif - void goto_analyzer_parse_optionst::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); - -#ifdef HAVE_JSIL - register_language(new_jsil_language); -#endif } diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt index df25ebdf0ed..c224d97fef9 100644 --- a/src/goto-analyzer/module_dependencies.txt +++ b/src/goto-analyzer/module_dependencies.txt @@ -7,6 +7,5 @@ goto-checker goto-programs java_bytecode # will go away langapi # should go away -jsil json util diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt index 3547589b683..cd259bbb960 100644 --- a/src/goto-cc/CMakeLists.txt +++ b/src/goto-cc/CMakeLists.txt @@ -20,8 +20,6 @@ target_link_libraries(goto-cc-lib langapi ) -add_if_library(goto-cc-lib jsil) - # Executable add_executable(goto-cc goto_cc_main.cpp) target_link_libraries(goto-cc goto-cc-lib) diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 8a70a3f6705..64d5ba774d8 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -51,11 +51,6 @@ else all: goto-gcc$(EXEEXT) endif -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - ############################################################################### goto-gcc$(EXEEXT): goto-cc$(EXEEXT) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3d83ea42659..25119867bb7 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -141,7 +141,7 @@ static file_typet detect_file_type( if( ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" || ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" || - ext == "jar" || ext == "jsil") + ext == "jar") { return file_typet::SOURCE_FILE; } diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp index 7c3e06e5630..5e7d4a98307 100644 --- a/src/goto-cc/goto_cc_languages.cpp +++ b/src/goto-cc/goto_cc_languages.cpp @@ -16,16 +16,8 @@ Author: CM Wintersteiger #include #include -#ifdef HAVE_JSIL -# include -#endif - void goto_cc_modet::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); - -#ifdef HAVE_JSIL - register_language(new_jsil_language); -#endif } diff --git a/src/goto-cc/module_dependencies.txt b/src/goto-cc/module_dependencies.txt index 43aa9ecd738..10b5d7bf0c8 100644 --- a/src/goto-cc/module_dependencies.txt +++ b/src/goto-cc/module_dependencies.txt @@ -2,7 +2,6 @@ ansi-c cpp goto-cc goto-programs -jsil json langapi # should go away linking diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 20e656c69ff..9c4607be813 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -23,8 +23,6 @@ target_link_libraries(goto-diff-lib solvers ) -add_if_library(goto-diff-lib jsil) - # Executable add_executable(goto-diff goto_diff_main.cpp) target_link_libraries(goto-diff goto-diff-lib) diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 2401c7046bb..41727b37aac 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -43,7 +43,6 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions) symbol_pair.second.type.id() == ID_code && (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp || symbol_pair.second.mode == ID_java || - symbol_pair.second.mode == "jsil" || symbol_pair.second.mode == ID_statement_list)) { symbol_list.push_back(symbol_pair.first); diff --git a/src/jsil/CMakeLists.txt b/src/jsil/CMakeLists.txt deleted file mode 100644 index e3ebea25d35..00000000000 --- a/src/jsil/CMakeLists.txt +++ /dev/null @@ -1,13 +0,0 @@ -generic_bison(jsil) -generic_flex(jsil) - -file(GLOB_RECURSE sources "*.cpp" "*.h") -add_library(jsil - ${sources} - ${BISON_parser_OUTPUTS} - ${FLEX_scanner_OUTPUTS} -) - -generic_includes(jsil) - -target_link_libraries(jsil util) diff --git a/src/jsil/Makefile b/src/jsil/Makefile deleted file mode 100644 index b45d2c43ae9..00000000000 --- a/src/jsil/Makefile +++ /dev/null @@ -1,42 +0,0 @@ -SRC = expr2jsil.cpp \ - jsil_convert.cpp \ - jsil_entry_point.cpp \ - jsil_internal_additions.cpp \ - jsil_language.cpp \ - jsil_lex.yy.cpp \ - jsil_parse_tree.cpp \ - jsil_parser.cpp \ - jsil_typecheck.cpp \ - jsil_types.cpp \ - jsil_y.tab.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = jsil$(LIBEXT) \ - jsil_y.tab.h jsil_y.tab.cpp jsil_lex.yy.cpp \ - jsil_y.tab.cpp.output jsil_y.output - -all: jsil$(LIBEXT) - -############################################################################### - -jsil$(LIBEXT): $(OBJ) - $(LINKLIB) - -jsil_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) -pyyjsil parser.y --defines=jsil_y.tab.h -o $@ - -jsil_y.tab.h: jsil_y.tab.cpp - -jsil_lex.yy.cpp: scanner.l - $(LEX) -Pyyjsil -o$@ scanner.l - -generated_files: jsil_lex.yy.cpp jsil_y.tab.cpp jsil_y.tab.h - -# extra dependencies -jsil_y.tab$(OBJEXT): jsil_y.tab.cpp jsil_y.tab.h -jsil_lex.yy$(OBJEXT): jsil_y.tab.cpp jsil_lex.yy.cpp jsil_y.tab.h diff --git a/src/jsil/README.md b/src/jsil/README.md deleted file mode 100644 index 3f77753cbfc..00000000000 --- a/src/jsil/README.md +++ /dev/null @@ -1,6 +0,0 @@ -\ingroup module_hidden -\defgroup jsil jsil - -# Folder jsil - -`jsil/` contains a JavaScript front end. diff --git a/src/jsil/expr2jsil.cpp b/src/jsil/expr2jsil.cpp deleted file mode 100644 index 5f88416b2ca..00000000000 --- a/src/jsil/expr2jsil.cpp +++ /dev/null @@ -1,35 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "expr2jsil.h" - -#include - -class expr2jsilt:public expr2ct -{ -public: - explicit expr2jsilt(const namespacet &_ns):expr2ct(_ns) { } - -protected: -}; - -std::string expr2jsil(const exprt &expr, const namespacet &ns) -{ - expr2jsilt expr2jsil(ns); - expr2jsil.get_shorthands(expr); - return expr2jsil.convert(expr); -} - -std::string type2jsil(const typet &type, const namespacet &ns) -{ - expr2jsilt expr2jsil(ns); - return expr2jsil.convert(type); -} diff --git a/src/jsil/expr2jsil.h b/src/jsil/expr2jsil.h deleted file mode 100644 index f8f99620380..00000000000 --- a/src/jsil/expr2jsil.h +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_EXPR2JSIL_H -#define CPROVER_JSIL_EXPR2JSIL_H - -#include - -class exprt; -class namespacet; -class typet; - -std::string expr2jsil(const exprt &expr, const namespacet &ns); -std::string type2jsil(const typet &type, const namespacet &ns); - -#endif // CPROVER_JSIL_EXPR2JSIL_H diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp deleted file mode 100644 index 8344603bf14..00000000000 --- a/src/jsil/jsil_convert.cpp +++ /dev/null @@ -1,146 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language Conversion - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language Conversion - -#include "jsil_convert.h" - -#include -#include - -#include - -#include "jsil_parse_tree.h" - -class jsil_convertt -{ -public: - explicit jsil_convertt(symbol_table_baset &_symbol_table) - : symbol_table(_symbol_table) - { - } - - bool operator()(const jsil_parse_treet &parse_tree, message_handlert &); - -protected: - symbol_table_baset &symbol_table; - - bool convert_code(const symbolt &symbol, codet &code); -}; - -bool jsil_convertt::operator()( - const jsil_parse_treet &parse_tree, - message_handlert &message_handler) -{ - for(jsil_parse_treet::itemst::const_iterator - it=parse_tree.items.begin(); - it!=parse_tree.items.end(); - ++it) - { - symbolt new_symbol = it->to_symbol(); - - if(convert_code(new_symbol, to_code(new_symbol.value))) - return true; - - if(const auto maybe_symbol=symbol_table.lookup(new_symbol.name)) - { - const symbolt &s=*maybe_symbol; - if(s.value.id()=="no-body-just-yet") - { - symbol_table.remove(s.name); - } - } - if(symbol_table.add(new_symbol)) - { - messaget log{message_handler}; - log.error() << "duplicate symbol " << new_symbol.name << messaget::eom; - throw 0; - } - } - - return false; -} - -bool jsil_convertt::convert_code(const symbolt &symbol, codet &code) -{ - if(code.get_statement()==ID_block) - { - Forall_operands(it, code) - if(convert_code(symbol, to_code(*it))) - return true; - } - else if(code.get_statement()==ID_assign) - { - code_assignt &a=to_code_assign(code); - - if(a.rhs().id()==ID_with) - { - exprt to_try = to_with_expr(a.rhs()).old(); - codet t(code_assignt(a.lhs(), to_try)); - if(convert_code(symbol, t)) - return true; - - irep_idt c_target = - to_symbol_expr(to_with_expr(a.rhs()).where()).get_identifier(); - code_gotot g(c_target); - - code_try_catcht t_c(std::move(t)); - // Adding empty symbol to catch decl - code_frontend_declt d(symbol_exprt::typeless("decl_symbol")); - t_c.add_catch(std::move(d), std::move(g)); - t_c.add_source_location()=code.source_location(); - - code.swap(t_c); - } - else if(a.rhs().id()==ID_side_effect && - to_side_effect_expr(a.rhs()).get_statement()== ID_function_call) - { - side_effect_expr_function_callt f_expr= - to_side_effect_expr_function_call(a.rhs()); - - code_function_callt f(a.lhs(), f_expr.function(), f_expr.arguments()); - f.add_source_location()=code.source_location(); - - code.swap(f); - } - } - - return false; -} - -bool jsil_convert( - const jsil_parse_treet &parse_tree, - symbol_table_baset &symbol_table, - message_handlert &message_handler) -{ - jsil_convertt jsil_convert{symbol_table}; - - try - { - return jsil_convert(parse_tree, message_handler); - } - - catch(int) - { - } - - catch(const char *e) - { - messaget log{message_handler}; - log.error() << e << messaget::eom; - } - - catch(const std::string &e) - { - messaget log{message_handler}; - log.error() << e << messaget::eom; - } - - return true; -} diff --git a/src/jsil/jsil_convert.h b/src/jsil/jsil_convert.h deleted file mode 100644 index 96ca67858fc..00000000000 --- a/src/jsil/jsil_convert.h +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language Conversion - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language Conversion - -#ifndef CPROVER_JSIL_JSIL_CONVERT_H -#define CPROVER_JSIL_JSIL_CONVERT_H - -class jsil_parse_treet; -class message_handlert; -class symbol_table_baset; - -bool jsil_convert( - const jsil_parse_treet &parse_tree, - symbol_table_baset &symbol_table, - message_handlert &message_handler); - -#endif // CPROVER_JSIL_JSIL_CONVERT_H diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp deleted file mode 100644 index 8e5364d31a4..00000000000 --- a/src/jsil/jsil_entry_point.cpp +++ /dev/null @@ -1,163 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_entry_point.h" - -#include -#include -#include -#include -#include -#include -#include - -#include -#include - -#include - -static void create_initialize(symbol_table_baset &symbol_table) -{ - symbolt initialize{ - INITIALIZE_FUNCTION, code_typet({}, empty_typet()), "jsil"}; - initialize.base_name = INITIALIZE_FUNCTION; - - code_blockt init_code; - - namespacet ns(symbol_table); - - symbol_exprt rounding_mode = - ns.lookup(rounding_mode_identifier()).symbol_expr(); - - code_assignt a(rounding_mode, from_integer(0, rounding_mode.type())); - init_code.add(a); - - initialize.value=init_code; - - if(symbol_table.add(initialize)) - throw "failed to add " INITIALIZE_FUNCTION; -} - -bool jsil_entry_point( - symbol_table_baset &symbol_table, - message_handlert &message_handler) -{ - // check if main is already there - if(symbol_table.symbols.find(goto_functionst::entry_point())!= - symbol_table.symbols.end()) - return false; // silently ignore - - irep_idt main_symbol; - - // find main symbol, if any is given - if(config.main.has_value()) - { - std::list matches; - - for(const auto &symbol_name_entry : - equal_range(symbol_table.symbol_base_map, config.main.value())) - { - // look it up - symbol_table_baset::symbolst::const_iterator s_it = - symbol_table.symbols.find(symbol_name_entry.second); - - if(s_it==symbol_table.symbols.end()) - continue; - - if(s_it->second.type.id() == ID_code && !s_it->second.is_property) - matches.push_back(symbol_name_entry.second); - } - - if(matches.empty()) - { - messaget message(message_handler); - message.error() << "main symbol '" << config.main.value() << "' not found" - << messaget::eom; - return true; // give up - } - - if(matches.size()>=2) - { - messaget message(message_handler); - message.error() << "main symbol '" << config.main.value() - << "' is ambiguous" << messaget::eom; - return true; - } - - main_symbol=matches.front(); - } - else - main_symbol=ID_main; - - // look it up - symbol_table_baset::symbolst::const_iterator s_it = - symbol_table.symbols.find(main_symbol); - - if(s_it==symbol_table.symbols.end()) - { - messaget message(message_handler); - message.error() << "main symbol '" << id2string(main_symbol) - << "' not in symbol table" << messaget::eom; - return true; // give up, no main - } - - const symbolt &symbol=s_it->second; - - // check if it has a body - if(symbol.value.is_nil()) - { - messaget message(message_handler); - message.error() << "main symbol '" << main_symbol << "' has no body" - << messaget::eom; - return false; // give up - } - - create_initialize(symbol_table); - - code_blockt init_code; - - // build call to initialization function - - { - symbol_table_baset::symbolst::const_iterator init_it = - symbol_table.symbols.find(INITIALIZE_FUNCTION); - - if(init_it==symbol_table.symbols.end()) - throw "failed to find " INITIALIZE_FUNCTION " symbol"; - - code_function_callt call_init(init_it->second.symbol_expr()); - call_init.add_source_location()=symbol.location; - init_code.add(call_init); - } - - // build call to main function - - code_function_callt call_main(symbol.symbol_expr()); - call_main.add_source_location()=symbol.location; - call_main.function().add_source_location()=symbol.location; - - init_code.add(call_main); - - // add "main" - symbolt new_symbol{ - goto_functionst::entry_point(), code_typet{{}, empty_typet{}}, "jsil"}; - new_symbol.base_name = goto_functionst::entry_point(); - new_symbol.value.swap(init_code); - - if(!symbol_table.insert(std::move(new_symbol)).second) - { - messaget message{message_handler}; - message.error() << "failed to move main symbol" << messaget::eom; - return true; - } - - return false; -} diff --git a/src/jsil/jsil_entry_point.h b/src/jsil/jsil_entry_point.h deleted file mode 100644 index 6dfd4b9c57d..00000000000 --- a/src/jsil/jsil_entry_point.h +++ /dev/null @@ -1,19 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_ENTRY_POINT_H -#define CPROVER_JSIL_JSIL_ENTRY_POINT_H - -bool jsil_entry_point( - class symbol_table_baset &symbol_table, - class message_handlert &message_handler); - -#endif // CPROVER_JSIL_JSIL_ENTRY_POINT_H diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp deleted file mode 100644 index d46ea056ea9..00000000000 --- a/src/jsil/jsil_internal_additions.cpp +++ /dev/null @@ -1,89 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_internal_additions.h" - -#include -#include -#include - -#include - -#include "jsil_types.h" - -void jsil_internal_additions(symbol_table_baset &dest) -{ - // add __CPROVER_rounding_mode - - { - symbolt symbol{rounding_mode_identifier(), signed_int_type(), ID_C}; - symbol.base_name = symbol.name; - symbol.is_lvalue=true; - symbol.is_state_var=true; - symbol.is_thread_local=true; - // mark as already typechecked - symbol.is_extern=true; - dest.add(symbol); - } - - // add eval - - { - code_typet eval_type({code_typet::parametert(typet())}, empty_typet()); - - symbolt symbol{"eval", eval_type, "jsil"}; - symbol.base_name="eval"; - dest.add(symbol); - } - - // add nan - - { - symbolt symbol{"nan", floatbv_typet(), "jsil"}; - symbol.base_name="nan"; - // mark as already typechecked - symbol.is_extern=true; - dest.add(symbol); - } - - // add empty symbol used for decl statements - - { - symbolt symbol{"decl_symbol", empty_typet(), "jsil"}; - symbol.base_name="decl_symbol"; - // mark as already typechecked - symbol.is_extern=true; - dest.add(symbol); - } - - // add builtin objects - const std::vector builtin_objects= - { - "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString", - "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp", - "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror", - "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp", - "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp", - "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp", - "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp", - "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp", - "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson" - }; - - for(const auto &identifier : builtin_objects) - { - symbolt new_symbol{identifier, jsil_builtin_object_type(), "jsil"}; - new_symbol.base_name=identifier; - // mark as already typechecked - new_symbol.is_extern=true; - dest.add(new_symbol); - } -} diff --git a/src/jsil/jsil_internal_additions.h b/src/jsil/jsil_internal_additions.h deleted file mode 100644 index c85f8905c3c..00000000000 --- a/src/jsil/jsil_internal_additions.h +++ /dev/null @@ -1,19 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_INTERNAL_ADDITIONS_H -#define CPROVER_JSIL_JSIL_INTERNAL_ADDITIONS_H - -class symbol_table_baset; - -void jsil_internal_additions(symbol_table_baset &dest); - -#endif // CPROVER_JSIL_JSIL_INTERNAL_ADDITIONS_H diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp deleted file mode 100644 index 8b0d543c949..00000000000 --- a/src/jsil/jsil_language.cpp +++ /dev/null @@ -1,172 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_language.h" - -#include -#include - -#include "expr2jsil.h" -#include "jsil_convert.h" -#include "jsil_entry_point.h" -#include "jsil_internal_additions.h" -#include "jsil_parser.h" -#include "jsil_typecheck.h" - -std::set jsil_languaget::extensions() const -{ - return { "jsil" }; -} - -void jsil_languaget::modules_provided(std::set &modules) -{ - modules.insert(get_base_name(parse_path, true)); -} - -/// Adding symbols for all procedure declarations -bool jsil_languaget::interfaces( - symbol_table_baset &symbol_table, - message_handlert &message_handler) -{ - if(jsil_convert(parse_tree, symbol_table, message_handler)) - return true; - - jsil_internal_additions(symbol_table); - return false; -} - -bool jsil_languaget::preprocess( - std::istream &, - const std::string &, - std::ostream &, - message_handlert &) -{ - // there is no preprocessing! - return true; -} - -bool jsil_languaget::parse( - std::istream &instream, - const std::string &path, - message_handlert &message_handler) -{ - // store the path - parse_path=path; - - // parsing - jsil_parsert jsil_parser{message_handler}; - jsil_parser.clear(); - jsil_parser.set_file(path); - jsil_parser.in=&instream; - - bool result=jsil_parser.parse(); - - // save result - parse_tree.swap(jsil_parser.parse_tree); - - // save some memory - jsil_parser.clear(); - - return result; -} - -/// Converting from parse tree and type checking. -bool jsil_languaget::typecheck( - symbol_table_baset &symbol_table, - const std::string &, - message_handlert &message_handler) -{ - if(jsil_typecheck(symbol_table, message_handler)) - return true; - - return false; -} - -bool jsil_languaget::generate_support_functions( - symbol_table_baset &symbol_table, - message_handlert &message_handler) -{ - return jsil_entry_point(symbol_table, message_handler); -} - -void jsil_languaget::show_parse(std::ostream &out, message_handlert &) -{ - parse_tree.output(out); -} - -std::unique_ptr new_jsil_language() -{ - return std::make_unique(); -} - -bool jsil_languaget::from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) -{ - code=expr2jsil(expr, ns); - return false; -} - -bool jsil_languaget::from_type( - const typet &type, - std::string &code, - const namespacet &ns) -{ - code=type2jsil(type, ns); - return false; -} - -bool jsil_languaget::to_expr( - const std::string &code, - const std::string &, - exprt &expr, - const namespacet &ns, - message_handlert &message_handler) -{ - expr.make_nil(); - std::istringstream instream(code); - - // parsing - jsil_parsert jsil_parser{message_handler}; - jsil_parser.clear(); - jsil_parser.set_file(irep_idt()); - jsil_parser.in=&instream; - - bool result=jsil_parser.parse(); - - if(jsil_parser.parse_tree.items.size()!=1) - result=true; - else - { - symbol_tablet symbol_table; - result = jsil_convert(parse_tree, symbol_table, message_handler); - - if(symbol_table.symbols.size()!=1) - result=true; - - if(!result) - expr=symbol_table.symbols.begin()->second.value; - - // typecheck it - if(!result) - result = jsil_typecheck(expr, message_handler, ns); - } - - // save some memory - jsil_parser.clear(); - - return result; -} - -jsil_languaget::~jsil_languaget() -{ -} diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h deleted file mode 100644 index bf5ca37406b..00000000000 --- a/src/jsil/jsil_language.h +++ /dev/null @@ -1,87 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_LANGUAGE_H -#define CPROVER_JSIL_JSIL_LANGUAGE_H - -#include - -#include - -#include "jsil_parse_tree.h" - -class jsil_languaget:public languaget -{ -public: - bool preprocess( - std::istream &instream, - const std::string &path, - std::ostream &outstream, - message_handlert &) override; - - bool parse( - std::istream &instream, - const std::string &path, - message_handlert &message_handler) override; - - bool generate_support_functions( - symbol_table_baset &symbol_table, - message_handlert &message_handler) override; - - bool typecheck( - symbol_table_baset &context, - const std::string &module, - message_handlert &message_handler) override; - - void show_parse(std::ostream &out, message_handlert &) override; - - virtual ~jsil_languaget(); - jsil_languaget() { } - - bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) - override; - - bool from_type(const typet &type, std::string &code, const namespacet &ns) - override; - - bool to_expr( - const std::string &code, - const std::string &module, - exprt &expr, - const namespacet &ns, - message_handlert &message_handler) override; - - std::unique_ptr new_language() override - { - return std::make_unique(); - } - - std::string id() const override - { - return "jsil"; - } - std::string description() const override - { return "Javascript Intermediate Language"; } - std::set extensions() const override; - - void modules_provided(std::set &modules) override; - bool interfaces( - symbol_table_baset &symbol_table, - message_handlert &message_handler) override; - -protected: - jsil_parse_treet parse_tree; - std::string parse_path; -}; - -std::unique_ptr new_jsil_language(); - -#endif // CPROVER_JSIL_JSIL_LANGUAGE_H diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp deleted file mode 100644 index 92638195d74..00000000000 --- a/src/jsil/jsil_parse_tree.cpp +++ /dev/null @@ -1,100 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_parse_tree.h" - -#include - -#include - -#include "jsil_types.h" - -static bool insert_at_label( - const codet &code, - const irep_idt &label, - code_blockt &dest) -{ - for(auto &c : dest.statements()) - { - if(c.get_statement()!=ID_label) - continue; - - code_labelt &l=to_code_label(c); - if(l.get_label()!=label) - continue; - - DATA_INVARIANT(l.code().get_statement() == ID_skip, "code should be skip"); - l.code()=code; - - return false; - } - - return true; -} - -symbolt jsil_declarationt::to_symbol() const -{ - symbol_exprt s(to_symbol_expr( - static_cast(find(ID_declarator)))); - - code_typet symbol_type=to_code_type(s.type()); - - irep_idt proc_type=s.get("proc_type"); - - if(proc_type=="builtin") - symbol_type=jsil_builtin_code_typet(symbol_type); - else if(proc_type=="spec") - symbol_type=jsil_spec_code_typet(symbol_type); - - symbolt symbol{s.get_identifier(), symbol_type, "jsil"}; - symbol.base_name=s.get_identifier(); - symbol.location=s.source_location(); - - code_blockt code(to_code_block( - static_cast(find(ID_value)))); - - irept returns(find(ID_return)); - code_frontend_returnt r(symbol_exprt::typeless(returns.get(ID_value))); - - irept throws(find(ID_throw)); - side_effect_expr_throwt t( - symbol_exprt::typeless(throws.get(ID_value)), typet(), s.source_location()); - code_expressiont ct(t); - - if(insert_at_label(r, returns.get(ID_label), code)) - throw "return label "+returns.get_string(ID_label)+" not found"; - if(insert_at_label(ct, throws.get(ID_label), code)) - throw "throw label "+throws.get_string(ID_label)+" not found"; - - symbol.value.swap(code); - - return symbol; -} - -void jsil_declarationt::output(std::ostream &out) const -{ - out << "Declarator: " << find(ID_declarator).pretty() << "\n"; - out << "Returns: " << find(ID_return).pretty() << "\n"; - out << "Throws: " << find(ID_throw).pretty() << "\n"; - out << "Value: " << find(ID_value).pretty() << "\n"; -} - -void jsil_parse_treet::output(std::ostream &out) const -{ - for(itemst::const_iterator - it=items.begin(); - it!=items.end(); - it++) - { - it->output(out); - out << "\n"; - } -} diff --git a/src/jsil/jsil_parse_tree.h b/src/jsil/jsil_parse_tree.h deleted file mode 100644 index b47e50e33f9..00000000000 --- a/src/jsil/jsil_parse_tree.h +++ /dev/null @@ -1,119 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_PARSE_TREE_H -#define CPROVER_JSIL_JSIL_PARSE_TREE_H - -#include -#include - -#include - -class symbolt; - -class jsil_declarationt:public exprt -{ -public: - jsil_declarationt():exprt(ID_declaration) - { - } - - void add_declarator(const symbol_exprt &expr) - { - add(ID_declarator, expr); - } - - const symbol_exprt &declarator() const - { - return static_cast(find(ID_declarator)); - } - - symbol_exprt &declarator() - { - return static_cast(add(ID_declarator)); - } - - void add_returns( - const irep_idt &value, - const irep_idt &label) - { - add(ID_return).set(ID_value, value); - add(ID_return).set(ID_label, label); - } - - const irep_idt &returns_value() const - { - return find(ID_return).get(ID_value); - } - - const irep_idt &returns_label() const - { - return find(ID_return).get(ID_label); - } - - void add_throws( - const irep_idt &value, - const irep_idt &label) - { - add(ID_throw).set(ID_value, value); - add(ID_throw).set(ID_label, label); - } - - const irep_idt &throws_value() const - { - return find(ID_throw).get(ID_value); - } - - const irep_idt &throws_label() const - { - return find(ID_throw).get(ID_label); - } - - void add_value(const code_blockt &code) - { - add(ID_value, code); - } - - const code_blockt &value() const - { - return static_cast(find(ID_value)); - } - - code_blockt &value() - { - return static_cast(add(ID_value)); - } - - symbolt to_symbol() const; - - void output(std::ostream &) const; -}; - -class jsil_parse_treet -{ -public: - typedef std::list itemst; - itemst items; - - void swap(jsil_parse_treet &other) - { - items.swap(other.items); - } - - void clear() - { - items.clear(); - } - - void output(std::ostream &out) const; -}; - -#endif // CPROVER_JSIL_JSIL_PARSE_TREE_H diff --git a/src/jsil/jsil_parser.cpp b/src/jsil/jsil_parser.cpp deleted file mode 100644 index e84b4a662c9..00000000000 --- a/src/jsil/jsil_parser.cpp +++ /dev/null @@ -1,14 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_parser.h" - -int jsil_parsert::instance_count = 0; diff --git a/src/jsil/jsil_parser.h b/src/jsil/jsil_parser.h deleted file mode 100644 index 84cbc65bea0..00000000000 --- a/src/jsil/jsil_parser.h +++ /dev/null @@ -1,65 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_PARSER_H -#define CPROVER_JSIL_JSIL_PARSER_H - -#include - -#include "jsil_parse_tree.h" - -class jsil_parsert; -int yyjsilparse(jsil_parsert &); -void jsil_scanner_init(jsil_parsert &); - -class jsil_parsert:public parsert -{ -public: - explicit jsil_parsert(message_handlert &message_handler) - : parsert(message_handler) - { - // Simplistic check that we don't attempt to do reentrant parsing as the - // Bison-generated parser has global state. - PRECONDITION(++instance_count == 1); - } - - jsil_parsert(const jsil_parsert &) = delete; - - ~jsil_parsert() override - { - --instance_count; - } - - jsil_parse_treet parse_tree; - - bool parse() override - { - jsil_scanner_init(*this); - return yyjsilparse(*this) != 0; - } - - void clear() override - { - parsert::clear(); - parse_tree.clear(); - - // scanner state - string_literal.clear(); - } - - // internal state of the scanner - std::string string_literal; - -protected: - static int instance_count; -}; - -#endif // CPROVER_JSIL_JSIL_PARSER_H diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp deleted file mode 100644 index fb46ed83fe8..00000000000 --- a/src/jsil/jsil_typecheck.cpp +++ /dev/null @@ -1,936 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_typecheck.h" - -#include - -#include -#include -#include -#include - -#include "expr2jsil.h" -#include "jsil_types.h" - -std::string jsil_typecheckt::to_string(const exprt &expr) -{ - return expr2jsil(expr, ns); -} - -std::string jsil_typecheckt::to_string(const typet &type) -{ - return type2jsil(type, ns); -} - -/// Prefix parameters and variables with a procedure name -irep_idt jsil_typecheckt::add_prefix(const irep_idt &ds) -{ - return id2string(proc_name) + "::" + id2string(ds); -} - -void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type) -{ - expr.type()=type; - - if(expr.id()==ID_symbol) - { - const irep_idt &id=to_symbol_expr(expr).get_identifier(); - - const auto maybe_symbol=symbol_table.get_writeable(id); - if(!maybe_symbol) - { - error() << "unexpected symbol: " << id << eom; - throw 0; - } - - symbolt &s=*maybe_symbol; - if(s.type.id().empty() || s.type.is_nil()) - s.type=type; - else - s.type=jsil_union(s.type, type); - } -} - -void jsil_typecheckt::make_type_compatible( - exprt &expr, - const typet &type, - bool must) -{ - if(type.id().empty() || type.is_nil()) - { - error().source_location = expr.source_location(); - error() << "make_type_compatible got empty type: " << expr.pretty() << eom; - throw 0; - } - - if(expr.type().id().empty() || expr.type().is_nil()) - { - // Type is not yet set - update_expr_type(expr, type); - return; - } - - if(must) - { - if(jsil_incompatible_types(expr.type(), type)) - { - error().source_location = expr.source_location(); - error() << "failed to typecheck expr " - << expr.pretty() << " with type " - << expr.type().pretty() - << "; required type " << type.pretty() << eom; - throw 0; - } - } - else if(!jsil_is_subtype(type, expr.type())) - { - // Types are not compatible - typet upper=jsil_union(expr.type(), type); - update_expr_type(expr, upper); - } -} - -void jsil_typecheckt::typecheck_type(typet &type) -{ - if(type.id()==ID_code) - { - code_typet ¶meters=to_code_type(type); - - for(code_typet::parametert &p : parameters.parameters()) - { - // create new symbol - parameter_symbolt new_symbol; - new_symbol.base_name=p.get_identifier(); - - // append procedure name to parameters - p.set_identifier(add_prefix(p.get_identifier())); - new_symbol.name=p.get_identifier(); - - if(is_jsil_builtin_code_type(type)) - new_symbol.type=jsil_value_or_empty_type(); - else if(is_jsil_spec_code_type(type)) - new_symbol.type=jsil_value_or_reference_type(); - else - new_symbol.type=jsil_value_type(); // User defined function - - new_symbol.mode="jsil"; - - // mark as already typechecked - new_symbol.is_extern=true; - - if(symbol_table.add(new_symbol)) - { - error() << "failed to add parameter symbol '" << new_symbol.name - << "' in the symbol table" << eom; - throw 0; - } - } - } -} - -void jsil_typecheckt::typecheck_expr(exprt &expr) -{ - // first do sub-nodes - typecheck_expr_operands(expr); - - // now do case-split - typecheck_expr_main(expr); -} - -void jsil_typecheckt::typecheck_expr_operands(exprt &expr) -{ - Forall_operands(it, expr) - typecheck_expr(*it); -} - -void jsil_typecheckt::typecheck_expr_main(exprt &expr) -{ - if(expr.id()==ID_code) - { - error().source_location = expr.source_location(); - error() << "typecheck_expr_main got code: " << expr.pretty() << eom; - throw 0; - } - else if(expr.id()==ID_symbol) - typecheck_symbol_expr(to_symbol_expr(expr)); - else if(expr.is_constant()) - { - } - else - { - DATA_INVARIANT( - expr.type().is_nil() || expr.type().id().empty(), - "expressions are expected not to have type set just yet"); - - if(expr.id()==ID_null || - expr.id()=="undefined" || - expr.id()==ID_empty) - typecheck_expr_constant(expr); - else if(expr.id()=="null_type" || - expr.id()=="undefined_type" || - expr.id()==ID_boolean || - expr.id()==ID_string || - expr.id()=="number" || - expr.id()=="builtin_object" || - expr.id()=="user_object" || - expr.id()=="object" || - expr.id()==ID_pointer || - expr.id()==ID_member || - expr.id()=="variable") - expr.type()=jsil_kind(); - else if(expr.id()=="proto" || - expr.id()=="fid" || - expr.id()=="scope" || - expr.id()=="constructid" || - expr.id()=="primvalue" || - expr.id()=="targetfunction" || - expr.id()==ID_class) - { - // TODO: have a special type for builtin fields - expr.type()=string_typet(); - } - else if(expr.id()==ID_not) - typecheck_expr_unary_boolean(expr); - else if(expr.id()=="string_to_num") - typecheck_expr_unary_string(expr); - else if(expr.id()==ID_unary_minus || - expr.id()=="num_to_int32" || - expr.id()=="num_to_uint32" || - expr.id()==ID_bitnot) - { - typecheck_expr_unary_num(expr); - expr.type()=floatbv_typet(); - } - else if(expr.id()=="num_to_string") - { - typecheck_expr_unary_num(expr); - expr.type()=string_typet(); - } - else if(expr.id()==ID_equal) - typecheck_exp_binary_equal(expr); - else if(expr.id()==ID_lt || - expr.id()==ID_le) - typecheck_expr_binary_compare(expr); - else if(expr.id()==ID_plus || - expr.id()==ID_minus || - expr.id()==ID_mult || - expr.id()==ID_div || - expr.id()==ID_mod || - expr.id()==ID_bitand || - expr.id()==ID_bitor || - expr.id()==ID_bitxor || - expr.id()==ID_shl || - expr.id()==ID_shr || - expr.id()==ID_lshr) - typecheck_expr_binary_arith(expr); - else if(expr.id()==ID_and || - expr.id()==ID_or) - typecheck_expr_binary_boolean(expr); - else if(expr.id()=="subtype_of") - typecheck_expr_subtype(expr); - else if(expr.id()==ID_concatenation) - typecheck_expr_concatenation(expr); - else if(expr.id()=="ref") - typecheck_expr_ref(expr); - else if(expr.id()=="field") - typecheck_expr_field(expr); - else if(expr.id()==ID_base) - typecheck_expr_base(expr); - else if(expr.id()==ID_typeof) - expr.type()=jsil_kind(); - else if(expr.id()=="new") - expr.type()=jsil_user_object_type(); - else if(expr.id()=="hasField") - typecheck_expr_has_field(expr); - else if(expr.id()==ID_index) - typecheck_expr_index(expr); - else if(expr.id()=="delete") - typecheck_expr_delete(expr); - else if(expr.id()=="protoField") - typecheck_expr_proto_field(expr); - else if(expr.id()=="protoObj") - typecheck_expr_proto_obj(expr); - else if(expr.id()==ID_side_effect) - typecheck_expr_side_effect_throw(to_side_effect_expr_throw(expr)); - else - { - error().source_location = expr.source_location(); - error() << "unexpected expression: " << expr.pretty() << eom; - throw 0; - } - } -} - -void jsil_typecheckt::typecheck_expr_side_effect_throw( - side_effect_expr_throwt &expr) -{ - irept &excep_list=expr.add(ID_exception_list); - PRECONDITION(excep_list.id() == ID_symbol); - symbol_exprt &s=static_cast(excep_list); - typecheck_symbol_expr(s); -} - -void jsil_typecheckt::typecheck_expr_constant(exprt &expr) -{ - if(expr.id()==ID_null) - expr.type()=jsil_null_type(); - else if(expr.id()=="undefined") - expr.type()=jsil_undefined_type(); - else if(expr.id()==ID_empty) - expr.type()=jsil_empty_type(); -} - -void jsil_typecheckt::typecheck_expr_proto_field(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), jsil_object_type(), true); - make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true); - - expr.type()=jsil_value_or_empty_type(); -} - -void jsil_typecheckt::typecheck_expr_proto_obj(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands"; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), jsil_object_type(), true); - make_type_compatible(to_binary_expr(expr).op1(), jsil_object_type(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_delete(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), jsil_object_type(), true); - make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_index(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), jsil_object_type(), true); - make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true); - - // special case for function identifiers - if( - to_binary_expr(expr).op1().id() == "fid" || - to_binary_expr(expr).op1().id() == "constructid") - expr.type() = code_typet({}, typet()); - else - expr.type()=jsil_value_type(); -} - -void jsil_typecheckt::typecheck_expr_has_field(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), jsil_object_type(), true); - make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_field(exprt &expr) -{ - if(expr.operands().size()!=1) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects single operand" << eom; - throw 0; - } - - make_type_compatible(to_unary_expr(expr).op(), jsil_reference_type(), true); - - expr.type()=string_typet(); -} - -void jsil_typecheckt::typecheck_expr_base(exprt &expr) -{ - if(expr.operands().size()!=1) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects single operand" << eom; - throw 0; - } - - make_type_compatible(to_unary_expr(expr).op(), jsil_reference_type(), true); - - expr.type()=jsil_value_type(); -} - -void jsil_typecheckt::typecheck_expr_ref(exprt &expr) -{ - if(expr.operands().size()!=3) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects three operands" << eom; - throw 0; - } - - make_type_compatible(to_multi_ary_expr(expr).op0(), jsil_value_type(), true); - make_type_compatible(to_multi_ary_expr(expr).op1(), string_typet(), true); - - exprt &operand3 = to_multi_ary_expr(expr).op2(); - make_type_compatible(operand3, jsil_kind(), true); - - if(operand3.id()==ID_member) - expr.type()=jsil_member_reference_type(); - else if(operand3.id()=="variable") - expr.type()=jsil_variable_reference_type(); - else - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() - << "' expects reference type in the third parameter. Got:" - << operand3.pretty() << eom; - throw 0; - } -} - -void jsil_typecheckt::typecheck_expr_concatenation(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), string_typet(), true); - make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true); - - expr.type()=string_typet(); -} - -void jsil_typecheckt::typecheck_expr_subtype(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), jsil_kind(), true); - make_type_compatible(to_binary_expr(expr).op1(), jsil_kind(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_binary_boolean(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), bool_typet(), true); - make_type_compatible(to_binary_expr(expr).op1(), bool_typet(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_binary_arith(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), floatbv_typet(), true); - make_type_compatible(to_binary_expr(expr).op1(), floatbv_typet(), true); - - expr.type()=floatbv_typet(); -} - -void jsil_typecheckt::typecheck_exp_binary_equal(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - // operands can be of any types - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_binary_compare(exprt &expr) -{ - if(expr.operands().size()!=2) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects two operands" << eom; - throw 0; - } - - make_type_compatible(to_binary_expr(expr).op0(), floatbv_typet(), true); - make_type_compatible(to_binary_expr(expr).op1(), floatbv_typet(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_unary_boolean(exprt &expr) -{ - if(expr.operands().size()!=1) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects one operand" << eom; - throw 0; - } - - make_type_compatible(to_unary_expr(expr).op(), bool_typet(), true); - - expr.type()=bool_typet(); -} - -void jsil_typecheckt::typecheck_expr_unary_string(exprt &expr) -{ - if(expr.operands().size()!=1) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects one operand" << eom; - throw 0; - } - - make_type_compatible(to_unary_expr(expr).op(), string_typet(), true); - - expr.type()=floatbv_typet(); -} - -void jsil_typecheckt::typecheck_expr_unary_num(exprt &expr) -{ - if(expr.operands().size()!=1) - { - error().source_location = expr.source_location(); - error() << "operator '" << expr.id() << "' expects one operand" << eom; - throw 0; - } - - make_type_compatible(to_unary_expr(expr).op(), floatbv_typet(), true); -} - -void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr) -{ - irep_idt identifier=symbol_expr.get_identifier(); - - // if this is a built-in identifier, check if it exists in the - // symbol table and retrieve it's type - // TODO: add a flag for not needing to prefix internal symbols - // that do not start with hash - if(has_prefix(id2string(identifier), "#") || - identifier=="eval" || - identifier=="nan") - { - symbol_table_baset::symbolst::const_iterator s_it = - symbol_table.symbols.find(identifier); - - if(s_it==symbol_table.symbols.end()) - { - error() << "unexpected internal symbol: " << identifier << eom; - throw 0; - } - else - { - // symbol already exists - const symbolt &symbol=s_it->second; - - // type the expression - symbol_expr.type()=symbol.type; - } - } - else - { - // if this is a variable, we need to check if we already - // prefixed it and add to the symbol table if it is not there already - irep_idt identifier_base = identifier; - if(!has_prefix(id2string(identifier), id2string(proc_name))) - { - identifier = add_prefix(identifier); - symbol_expr.set_identifier(identifier); - } - - symbol_table_baset::symbolst::const_iterator s_it = - symbol_table.symbols.find(identifier); - - if(s_it==symbol_table.symbols.end()) - { - // create new symbol - symbolt new_symbol{identifier, symbol_expr.type(), "jsil"}; - new_symbol.base_name=identifier_base; - new_symbol.is_lvalue=new_symbol.type.id()!=ID_code; - - // mark as already typechecked - new_symbol.is_extern=true; - - if(symbol_table.add(new_symbol)) - { - error() << "failed to add symbol '" << new_symbol.name - << "' in the symbol table" << eom; - throw 0; - } - } - else - { - // symbol already exists - DATA_INVARIANT(!s_it->second.is_type, "non-type symbol expected"); - - const symbolt &symbol=s_it->second; - - // type the expression - symbol_expr.type()=symbol.type; - } - } -} - -void jsil_typecheckt::typecheck_code(codet &code) -{ - const irep_idt &statement=code.get_statement(); - - if(statement==ID_function_call) - typecheck_function_call(to_code_function_call(code)); - else if(statement==ID_return) - typecheck_return(to_code_frontend_return(code)); - else if(statement==ID_expression) - { - if(code.operands().size()!=1) - { - error().source_location = code.source_location(); - error() << "expression statement expected to have one operand" - << eom; - throw 0; - } - - typecheck_expr(code.op0()); - } - else if(statement==ID_label) - { - typecheck_code(to_code_label(code).code()); - // TODO: produce defined label set - } - else if(statement==ID_block) - typecheck_block(code); - else if(statement==ID_ifthenelse) - typecheck_ifthenelse(to_code_ifthenelse(code)); - else if(statement==ID_goto) - { - // TODO: produce used label set - } - else if(statement==ID_assign) - typecheck_assign(to_code_assign(code)); - else if(statement==ID_try_catch) - typecheck_try_catch(to_code_try_catch(code)); - else if(statement==ID_skip) - { - } - else - { - error().source_location = code.source_location(); - error() << "unexpected statement: " << statement << eom; - throw 0; - } -} - -void jsil_typecheckt::typecheck_return(code_frontend_returnt &code) -{ - if(code.has_return_value()) - typecheck_expr(code.return_value()); -} - -void jsil_typecheckt::typecheck_block(codet &code) -{ - Forall_operands(it, code) - typecheck_code(to_code(*it)); -} - -void jsil_typecheckt::typecheck_try_catch(code_try_catcht &code) -{ - // A special case of try catch with one catch clause - if(code.operands().size()!=3) - { - error().source_location = code.source_location(); - error() << "try_catch expected to have three operands" << eom; - throw 0; - } - - // function call - typecheck_function_call(to_code_function_call(code.try_code())); - - // catch decl is not used, but is required by goto-programs - - typecheck_code(code.get_catch_code(0)); -} - -void jsil_typecheckt::typecheck_function_call( - code_function_callt &call) -{ - if(call.operands().size()!=3) - { - error().source_location = call.source_location(); - error() << "function call expected to have three operands" << eom; - throw 0; - } - - exprt &lhs=call.lhs(); - typecheck_expr(lhs); - - exprt &f=call.function(); - typecheck_expr(f); - - for(auto &arg : call.arguments()) - typecheck_expr(arg); - - // Look for a function declaration symbol in the symbol table - if(f.id()==ID_symbol) - { - const irep_idt &id=to_symbol_expr(f).get_identifier(); - - if(const auto maybe_symbol=symbol_table.lookup(id)) - { - const symbolt &s=*maybe_symbol; - - if(s.type.id()==ID_code) - { - const code_typet &codet=to_code_type(s.type); - - for(std::size_t i=0; i=call.arguments().size()) - break; - - const typet ¶m_type=codet.parameters()[i].type(); - - if(!param_type.id().empty() && param_type.is_not_nil()) - { - // check argument's type if parameter's type is given - make_type_compatible(call.arguments()[i], param_type, true); - } - } - - // if there are too few arguments, add undefined - if(codet.parameters().size()>call.arguments().size()) - { - for(std::size_t i=call.arguments().size(); - i identifiers; - identifiers.reserve(symbol_table.symbols.size()); - for(const auto &symbol_pair : symbol_table.symbols) - { - identifiers.push_back(symbol_pair.first); - } - - // We first check all type symbols, - // recursively doing base classes first. - for(const irep_idt &id : identifiers) - { - symbolt &symbol = symbol_table.get_writeable_ref(id); - if(symbol.is_type) - typecheck_type_symbol(symbol); - } - - // We now check all non-type symbols - for(const irep_idt &id : identifiers) - { - symbolt &symbol = symbol_table.get_writeable_ref(id); - if(!symbol.is_type) - typecheck_non_type_symbol(symbol); - } -} - -bool jsil_typecheck( - symbol_table_baset &symbol_table, - message_handlert &message_handler) -{ - jsil_typecheckt jsil_typecheck(symbol_table, message_handler); - return jsil_typecheck.typecheck_main(); -} - -bool jsil_typecheck( - exprt &expr, - message_handlert &message_handler, - const namespacet &) -{ - const unsigned errors_before= - message_handler.get_message_count(messaget::M_ERROR); - - symbol_tablet symbol_table; - - jsil_typecheckt jsil_typecheck( - symbol_table, - message_handler); - - try - { - jsil_typecheck.typecheck_expr(expr); - } - - catch(int) - { - jsil_typecheck.error(); - } - - catch(const char *e) - { - jsil_typecheck.error() << e << messaget::eom; - } - - catch(const std::string &e) - { - jsil_typecheck.error() << e << messaget::eom; - } - - return message_handler.get_message_count(messaget::M_ERROR)!=errors_before; -} diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h deleted file mode 100644 index 248078de577..00000000000 --- a/src/jsil/jsil_typecheck.h +++ /dev/null @@ -1,107 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Michael Tautschnig, tautschn@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_TYPECHECK_H -#define CPROVER_JSIL_JSIL_TYPECHECK_H - -#include - -#include -#include - -class code_assignt; -class code_function_callt; -class code_ifthenelset; -class code_frontend_returnt; -class code_try_catcht; -class codet; -class message_handlert; -class side_effect_expr_throwt; -class symbol_exprt; -class symbol_table_baset; - -bool jsil_typecheck( - symbol_table_baset &symbol_table, - message_handlert &message_handler); - -bool jsil_typecheck( - exprt &expr, - message_handlert &message_handler, - const namespacet &ns); - -class jsil_typecheckt:public typecheckt -{ -public: - jsil_typecheckt( - symbol_table_baset &_symbol_table, - message_handlert &_message_handler) - : typecheckt(_message_handler), - symbol_table(_symbol_table), - ns(symbol_table), - proc_name() - { - } - - virtual ~jsil_typecheckt() { } - - virtual void typecheck(); - virtual void typecheck_expr(exprt &expr); - -protected: - symbol_table_baset &symbol_table; - const namespacet ns; - // prefix to variables which is set in typecheck_declaration - irep_idt proc_name; - - void update_expr_type(exprt &expr, const typet &type); - void make_type_compatible(exprt &expr, const typet &type, bool must); - void typecheck_type_symbol(symbolt &) {} - void typecheck_non_type_symbol(symbolt &symbol); - void typecheck_symbol_expr(symbol_exprt &symbol_expr); - void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr); - void typecheck_expr_delete(exprt &expr); - void typecheck_expr_index(exprt &expr); - void typecheck_expr_proto_field(exprt &expr); - void typecheck_expr_proto_obj(exprt &expr); - void typecheck_expr_has_field(exprt &expr); - void typecheck_expr_ref(exprt &expr); - void typecheck_expr_field(exprt &expr); - void typecheck_expr_base(exprt &expr); - void typecheck_expr_constant(exprt &expr); - void typecheck_expr_concatenation(exprt &expr); - void typecheck_expr_subtype(exprt &expr); - void typecheck_expr_binary_boolean(exprt &expr); - void typecheck_expr_binary_arith(exprt &expr); - void typecheck_exp_binary_equal(exprt &expr); - void typecheck_expr_binary_compare(exprt &expr); - void typecheck_expr_unary_boolean(exprt &expr); - void typecheck_expr_unary_string(exprt &expr); - void typecheck_expr_unary_num(exprt &expr); - void typecheck_expr_operands(exprt &expr); - void typecheck_expr_main(exprt &expr); - void typecheck_code(codet &code); - void typecheck_function_call(code_function_callt &function_call); - void typecheck_return(code_frontend_returnt &); - void typecheck_block(codet &code); - void typecheck_ifthenelse(code_ifthenelset &code); - void typecheck_assign(code_assignt &code); - void typecheck_try_catch(code_try_catcht &code); - void typecheck_type(typet &type); - irep_idt add_prefix(const irep_idt &ds); - - // overload to use language-specific syntax - virtual std::string to_string(const exprt &expr); - virtual std::string to_string(const typet &type); - - std::unordered_set already_typechecked; -}; - -#endif // CPROVER_JSIL_JSIL_TYPECHECK_H diff --git a/src/jsil/jsil_types.cpp b/src/jsil/jsil_types.cpp deleted file mode 100644 index 6855ce54080..00000000000 --- a/src/jsil/jsil_types.cpp +++ /dev/null @@ -1,226 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Daiva Naudziuniene, daivan@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#include "jsil_types.h" - -#include - -#include - -typet jsil_any_type() -{ - return jsil_union_typet( - {jsil_empty_type(), jsil_reference_type(), jsil_value_type()}); -} - -typet jsil_value_or_empty_type() -{ - return jsil_union_typet({jsil_value_type(), jsil_empty_type()}); -} - -typet jsil_value_or_reference_type() -{ - return jsil_union_typet({jsil_value_type(), jsil_reference_type()}); -} - -typet jsil_value_type() -{ - return jsil_union_typet( - {jsil_undefined_type(), - jsil_null_type(), - jsil_prim_type(), - jsil_object_type()}); -} - -typet jsil_prim_type() -{ - return jsil_union_typet({floatbv_typet(), string_typet(), bool_typet()}); -} - -typet jsil_reference_type() -{ - return jsil_union_typet( - {jsil_member_reference_type(), jsil_variable_reference_type()}); -} - -typet jsil_member_reference_type() -{ - return typet("jsil_member_reference_type"); -} - -typet jsil_variable_reference_type() -{ - return typet("jsil_variable_reference_type"); -} - -typet jsil_object_type() -{ - return jsil_union_typet( - {jsil_user_object_type(), jsil_builtin_object_type()}); -} - -typet jsil_user_object_type() -{ - return typet("jsil_user_object_type"); -} - -typet jsil_builtin_object_type() -{ - return typet("jsil_builtin_object_type"); -} - -typet jsil_null_type() -{ - return typet("jsil_null_type"); -} - -typet jsil_undefined_type() -{ - return typet("jsil_undefined_type"); -} - -typet jsil_kind() -{ - return typet("jsil_kind"); -} - -typet jsil_empty_type() -{ - return typet("jsil_empty_type"); -} - -bool jsil_is_subtype(const typet &type1, const typet &type2) -{ - if(type2.id()==ID_union) - { - const jsil_union_typet &type2_union=to_jsil_union_type(type2); - - if(type1.id()==ID_union) - return to_jsil_union_type(type1).is_subtype(type2_union); - else - return jsil_union_typet(type1).is_subtype(type2_union); - } - else - return type1.id()==type2.id(); -} - -bool jsil_incompatible_types(const typet &type1, const typet &type2) -{ - return jsil_union_typet(type1).intersect_with( - jsil_union_typet(type2)).components().empty(); -} - -typet jsil_union(const typet &type1, const typet &type2) -{ - return jsil_union_typet(type1) - .union_with(jsil_union_typet(type2)).to_type(); -} - -bool compare_components( - const union_typet::componentt &comp1, - const union_typet::componentt &comp2) -{ - return comp1.type().id() &types): - union_typet() -{ - auto &elements=components(); - for(const auto &type : types) - { - if(type.id()==ID_union) - { - for(const auto &component : to_union_type(type).components()) - elements.push_back(component); - } - else - elements.push_back(componentt(ID_anonymous, type)); - } - - std::sort(elements.begin(), elements.end(), compare_components); -} - -jsil_union_typet jsil_union_typet::union_with( - const jsil_union_typet &other) const -{ - auto &elements1=components(); - auto &elements2=other.components(); - jsil_union_typet result; - auto &elements=result.components(); - elements.resize(elements1.size()+elements2.size()); - std::vector::iterator it=std::set_union( - elements1.begin(), elements1.end(), - elements2.begin(), elements2.end(), - elements.begin(), compare_components); - elements.resize(it-elements.begin()); - - return result; -} - -jsil_union_typet jsil_union_typet::intersect_with( - const jsil_union_typet &other) const -{ - auto &elements1=components(); - auto &elements2=other.components(); - jsil_union_typet result; - auto &elements=result.components(); - elements.resize(std::min(elements1.size(), elements2.size())); - std::vector::iterator it=std::set_intersection( - elements1.begin(), elements1.end(), - elements2.begin(), elements2.end(), - elements.begin(), compare_components); - elements.resize(it-elements.begin()); - - return result; -} - -bool jsil_union_typet::is_subtype(const jsil_union_typet &other) const -{ - auto it=components().begin(); - auto it2=other.components().begin(); - while(it=other.components().end()) - { - // We haven't found all types, but the second array finishes - return false; - } - - if(it->type().id()==it2->type().id()) - { - // Found the type - it++; - it2++; - } - else if(it->type().id()type().id()) - { - // Missing type - return false; - } - else // it->type().id()>it2->type().id() - { - // Skip one element in the second array - it2++; - } - } - - return true; -} - -const typet &jsil_union_typet::to_type() const -{ - auto &elements=components(); - if(elements.size()==1) - return elements[0].type(); - - return *this; -} diff --git a/src/jsil/jsil_types.h b/src/jsil/jsil_types.h deleted file mode 100644 index a59ba385f11..00000000000 --- a/src/jsil/jsil_types.h +++ /dev/null @@ -1,114 +0,0 @@ -/*******************************************************************\ - -Module: Jsil Language - -Author: Daiva Naudziuniene, daivan@amazon.com - -\*******************************************************************/ - -/// \file -/// Jsil Language - -#ifndef CPROVER_JSIL_JSIL_TYPES_H -#define CPROVER_JSIL_JSIL_TYPES_H - -#include - -typet jsil_kind(); -typet jsil_any_type(); -typet jsil_value_or_empty_type(); -typet jsil_value_or_reference_type(); -typet jsil_value_type(); -typet jsil_prim_type(); -typet jsil_reference_type(); -typet jsil_member_reference_type(); -typet jsil_variable_reference_type(); -typet jsil_object_type(); -typet jsil_user_object_type(); -typet jsil_builtin_object_type(); -typet jsil_null_type(); -typet jsil_undefined_type(); -typet jsil_empty_type(); - -bool jsil_is_subtype(const typet &type1, const typet &type2); -bool jsil_incompatible_types(const typet &type1, const typet &type2); -typet jsil_union(const typet &type1, const typet &type2); - -class jsil_builtin_code_typet:public code_typet -{ -public: - explicit jsil_builtin_code_typet(code_typet &code): - code_typet(code) - { - set("jsil_builtin_proceduret", true); - } -}; - -inline jsil_builtin_code_typet &to_jsil_builtin_code_type( - code_typet &code) -{ - PRECONDITION(code.get_bool("jsil_builtin_proceduret")); - return static_cast(code); -} - -inline bool is_jsil_builtin_code_type(const typet &type) -{ - return type.id()==ID_code && - type.get_bool("jsil_builtin_proceduret"); -} - -class jsil_spec_code_typet:public code_typet -{ -public: - explicit jsil_spec_code_typet(code_typet &code): - code_typet(code) - { - set("jsil_spec_proceduret", true); - } -}; - -inline jsil_spec_code_typet &to_jsil_spec_code_type( - code_typet &code) -{ - PRECONDITION(code.get_bool("jsil_spec_proceduret")); - return static_cast(code); -} - -inline bool is_jsil_spec_code_type(const typet &type) -{ - return type.id()==ID_code && - type.get_bool("jsil_spec_proceduret"); -} - -class jsil_union_typet:public union_typet -{ -public: - jsil_union_typet():union_typet() { } - - explicit jsil_union_typet(const typet &type) - :jsil_union_typet(std::vector({type})) { } - - explicit jsil_union_typet(const std::vector &types); - - jsil_union_typet union_with(const jsil_union_typet &other) const; - - jsil_union_typet intersect_with(const jsil_union_typet &other) const; - - bool is_subtype(const jsil_union_typet &other) const; - - const typet &to_type() const; -}; - -inline jsil_union_typet &to_jsil_union_type(typet &type) -{ - PRECONDITION(type.id() == ID_union); - return static_cast(type); -} - -inline const jsil_union_typet &to_jsil_union_type(const typet &type) -{ - PRECONDITION(type.id() == ID_union); - return static_cast(type); -} - -#endif // CPROVER_JSIL_JSIL_TYPES_H diff --git a/src/jsil/module_dependencies.txt b/src/jsil/module_dependencies.txt deleted file mode 100644 index bad90adbe0a..00000000000 --- a/src/jsil/module_dependencies.txt +++ /dev/null @@ -1,6 +0,0 @@ -ansi-c # should go away -goto-programs -jsil -langapi # should go away -linking -util diff --git a/src/jsil/parser.y b/src/jsil/parser.y deleted file mode 100644 index 31c96d972ed..00000000000 --- a/src/jsil/parser.y +++ /dev/null @@ -1,650 +0,0 @@ -%{ - -// #define YYDEBUG 1 -#define PARSER (*jsil_parser) - -#include "jsil_parser.h" - -int yyjsillex(); -extern char *yyjsiltext; - -static jsil_parsert *jsil_parser; -int yyjsilparse(void); -int yyjsilparse(jsil_parsert &_jsil_parser) -{ - jsil_parser = &_jsil_parser; - return yyjsilparse(); -} - -int yyjsilerror(const std::string &error) -{ - jsil_parser->parse_error(error, yyjsiltext); - return 0; -} - -#define YYSTYPE unsigned -#define YYSTYPE_IS_TRIVIAL 1 - -#include - -#include - -#include "jsil_y.tab.h" - -#ifdef _MSC_VER -// possible loss of data -#pragma warning(disable:4242) -// possible loss of data -#pragma warning(disable:4244) -// signed/unsigned mismatch -#pragma warning(disable:4365) -// switch with default but no case labels -#pragma warning(disable:4065) -// unreachable code -#pragma warning(disable:4702) -#endif - -/*** token declaration **************************************************/ -%} - -/*** special scanner reports ***/ - -%token TOK_SCANNER_ERROR /* used by scanner to report errors */ -%token TOK_NEWLINE "" - -/*** keywords ***/ - -%token TOK_PROCEDURE "procedure" -%token TOK_RETURNS "returns" -%token TOK_TO "to" -%token TOK_THROWS "throws" -%token TOK_EVAL "eval" -%token TOK_LABEL "label" -%token TOK_GOTO "goto" -%token TOK_SKIP "skip" -%token TOK_WITH "with" -%token TOK_NEW "new" -%token TOK_HAS_FIELD "hasField" -%token TOK_DELETE "delete" -%token TOK_PROTO_FIELD "protoField" -%token TOK_PROTO_OBJ "protoObj" -%token TOK_REF "ref" -%token TOK_FIELD "field" -%token TOK_BASE "base" -%token TOK_TYPEOF "typeOf" -%token TOK_NULL "null" -%token TOK_UNDEFINED "#undefined" -%token TOK_EMPTY "#empty" -%token TOK_TRUE "true" -%token TOK_FALSE "false" -%token TOK_PROTO "#proto" -%token TOK_FID "#fid" -%token TOK_SCOPE "#scope" -%token TOK_CONSTRUCTID "#constructid" -%token TOK_PRIMVALUE "#primvalue" -%token TOK_TARGETFUNCTION "#targetfunction" -%token TOK_CLASS "#class" -%token TOK_NUM_TO_STRING "num_to_string" -%token TOK_STRING_TO_NUM "string_to_num" -%token TOK_NUM_TO_INT32 "num_to_int32" -%token TOK_NUM_TO_UINT32 "num_to_uint32" -%token TOK_MEMBER_REFERENCE "#MemberReference" -%token TOK_VARIABLE_REFERENCE "#VariableReference" - -/*** type classes ***/ - -%token TOK_T_NULL "#Null" -%token TOK_T_UNDEFINED "#Undefined" -%token TOK_T_BOOLEAN "#Boolean" -%token TOK_T_STRING "#String" -%token TOK_T_NUMBER "#Number" -%token TOK_T_BUILTIN_OBJECT "#BuiltinObject" -%token TOK_T_USER_OBJECT "#UserObject" -%token TOK_T_OBJECT "#Object" -%token TOK_T_REFERENCE "#Reference" - -/*** multi-character operators ***/ - -%token TOK_DEFEQ ":=" -%token TOK_LEQ "<=" -%token TOK_AND "and" -%token TOK_OR "or" -%token TOK_SUBTYPE_OF "<:" -%token TOK_LEFT_SHIFT "<<" -%token TOK_SIGNED_RIGHT_SHIFT ">>" -%token TOK_UNSIGNED_RIGHT_SHIFT ">>>" -%token TOK_NOT "not" - -/*** scanner parsed tokens (these have a value!) ***/ - -%token TOK_IDENTIFIER -%token TOK_FLOATING -%token TOK_STRING -%token TOK_BUILTIN_LOC -%token TOK_BUILTIN_IDENTIFIER -%token TOK_SPEC_IDENTIFIER - -/*** priority, associativity, etc. definitions **************************/ - -%start program - -%expect 0 - -%% - -program: procedure_decls - ; - -procedure_decls: procedure_decl - | procedure_decls procedure_decl - ; - -procedure_decl: TOK_PROCEDURE proc_ident '(' parameters_opt ')' - TOK_RETURNS TOK_IDENTIFIER TOK_TO TOK_IDENTIFIER - TOK_THROWS TOK_IDENTIFIER TOK_TO TOK_IDENTIFIER - '{' statements_opt '}' - { - symbol_exprt proc(to_symbol_expr(parser_stack($2))); - code_typet::parameterst parameters; - forall_operands(it, parser_stack($4)) - { - symbol_exprt s(to_symbol_expr(*it)); - code_typet::parametert p(typet{}); - p.set_identifier(s.get_identifier()); - parameters.push_back(p); - } - proc.type() = code_typet(std::move(parameters), typet()); - - symbol_exprt rv(to_symbol_expr(parser_stack($7))); - symbol_exprt rl(to_symbol_expr(parser_stack($9))); - - symbol_exprt tv(to_symbol_expr(parser_stack($11))); - symbol_exprt tl(to_symbol_expr(parser_stack($13))); - - jsil_declarationt decl; - decl.add_declarator(proc); - decl.add_returns(rv.get_identifier(), rl.get_identifier()); - decl.add_throws(tv.get_identifier(), tl.get_identifier()); - if(parser_stack($15).is_not_nil()) - decl.add_value(to_code_block(to_code(parser_stack($15)))); - - PARSER.parse_tree.items.push_back(decl); - } - ; - -proc_ident: TOK_IDENTIFIER - | TOK_EVAL - { - symbol_exprt e = symbol_exprt::typeless("eval"); - newstack($$).swap(e); - } - | TOK_BUILTIN_IDENTIFIER - { - parser_stack($$).set("proc_type", "builtin"); - } - | TOK_SPEC_IDENTIFIER - { - parser_stack($$).set("proc_type", "spec"); - } - ; - -proc_ident_expr: proc_ident - | TOK_STRING - { - symbol_exprt s = symbol_exprt::typeless( - to_string_constant(parser_stack($$)).value()); - parser_stack($$).swap(s); - } - ; - -parameters_opt: /* empty */ - { - newstack($$); - } - | parameters - ; - -parameters: TOK_IDENTIFIER - { - newstack($$).id(ID_parameters); - parser_stack($$).add_to_operands(std::move(parser_stack($1))); - } - | parameters ',' TOK_IDENTIFIER - { - $$=$1; - parser_stack($$).add_to_operands(std::move(parser_stack($3))); - } - ; - -statements_opt: /* empty */ - { - newstack($$); - } - | statements - ; - -statements: statement - { - code_blockt b({static_cast(parser_stack($1))}); - newstack($$).swap(b); - } - | statements statement - { - $$=$1; - parser_stack($$).add_to_operands(std::move(parser_stack($2))); - } - ; - -statement: TOK_NEWLINE - { - newstack($$)=code_skipt(); - } - | instruction TOK_NEWLINE - { - $$=$1; - } - ; - -instruction: TOK_LABEL TOK_IDENTIFIER - { - code_labelt l( - to_symbol_expr(parser_stack($2)).get_identifier(), - code_skipt()); - newstack($$).swap(l); - } - | TOK_GOTO TOK_IDENTIFIER - { - code_gotot g(to_symbol_expr(parser_stack($2)).get_identifier()); - newstack($$).swap(g); - } - | TOK_GOTO '[' expression ']' TOK_IDENTIFIER ',' TOK_IDENTIFIER - { - code_gotot lt(to_symbol_expr(parser_stack($5)).get_identifier()); - code_gotot lf(to_symbol_expr(parser_stack($7)).get_identifier()); - - code_ifthenelset ite(parser_stack($3), std::move(lt), std::move(lf)); - - newstack($$).swap(ite); - } - | TOK_SKIP - { - newstack($$)=code_skipt(); - } - | TOK_IDENTIFIER TOK_DEFEQ rhs - { - code_assignt a(parser_stack($1), parser_stack($3)); - newstack($$).swap(a); - } - | '[' expression ',' expression ']' TOK_DEFEQ expression - { - index_exprt i(parser_stack($2), parser_stack($4)); - code_assignt a(i, parser_stack($7)); - newstack($$).swap(a); - } - ; - -rhs: expression - | proc_ident_expr '(' expressions_opt ')' with_opt - { - side_effect_expr_function_callt f(parser_stack($1), {}, typet{}, {}); - if(parser_stack($3).is_not_nil()) - f.arguments().swap(parser_stack($3).operands()); - - newstack($$).swap(f); - - if(parser_stack($5).is_not_nil()) - { - with_exprt w(parser_stack($$), parser_stack($5), nil_exprt()); - parser_stack($$).swap(w); - } - } - | TOK_NEW '(' ')' - { - exprt n("new"); - newstack($$).swap(n); - } - | TOK_HAS_FIELD '(' expression ',' expression ')' - { - exprt has_field("hasField"); - has_field.add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($5))); - - newstack($$).swap(has_field); - } - | '[' expression ',' expression ']' - { - index_exprt i(parser_stack($2), parser_stack($4)); - newstack($$).swap(i); - } - | TOK_DELETE '(' expression ',' expression ')' - { - exprt d("delete"); - d.add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($5))); - - newstack($$).swap(d); - } - | TOK_PROTO_FIELD '(' expression ',' expression ')' - { - exprt proto_field("protoField"); - proto_field.add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($5))); - - newstack($$).swap(proto_field); - } - | TOK_PROTO_OBJ '(' expression ',' expression ')' - { - exprt proto_obj("protoObj"); - proto_obj.add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($5))); - - newstack($$).swap(proto_obj); - } - ; - -with_opt: /* empty */ - { - newstack($$); - } - | TOK_WITH TOK_IDENTIFIER - { - $$=$2; - } - ; - -expressions_opt: /* empty */ - { - newstack($$); - } - | expressions - ; - -expressions: expression - { - newstack($$).id(ID_expression_list); - parser_stack($$).add_to_operands(std::move(parser_stack($1))); - } - | expressions ',' expression - { - $$=$1; - parser_stack($$).add_to_operands(std::move(parser_stack($3))); - } - ; - -expression: atom_expression - | expression binary_op atom_expression - { - $$=$2; - parser_stack($$).add_to_operands(std::move(parser_stack($1)), std::move(parser_stack($3))); - } - ; - -atom_expression: literal - | unary_op atom_expression - { - $$=$1; - parser_stack($$).add_to_operands(std::move(parser_stack($2))); - } - | '(' expression ')' - { - $$=$2; - } - | TOK_REF '(' expression ',' expression ',' ref_type ')' - { - exprt ref("ref"); - ref.add_to_operands( - std::move(parser_stack($3)), - std::move(parser_stack($5)), - std::move(parser_stack($7))); - - newstack($$).swap(ref); - } - | TOK_FIELD '(' expression ')' - { - exprt field("field"); - field.add_to_operands(std::move(parser_stack($3))); - - newstack($$).swap(field); - } - | TOK_BASE '(' expression ')' - { - exprt base(ID_base); - base.add_to_operands(std::move(parser_stack($3))); - - newstack($$).swap(base); - } - | TOK_TYPEOF '(' expression ')' - { - exprt typeof_expr(ID_typeof); - typeof_expr.add_to_operands(std::move(parser_stack($3))); - - newstack($$).swap(typeof_expr); - } - ; - -literal: TOK_IDENTIFIER - | TOK_NULL - { - newstack($$).id(ID_null); - } - | TOK_UNDEFINED - { - newstack($$).id("undefined"); - } - | TOK_EMPTY - { - newstack($$).id(ID_empty); - } - | TOK_TRUE - { - newstack($$) = true_exprt(); - } - | TOK_FALSE - { - newstack($$) = false_exprt(); - } - | TOK_FLOATING - | TOK_STRING - { - constant_exprt c(to_string_constant(parser_stack($$)) - .value(), string_typet()); - parser_stack($$).swap(c); - } - | TOK_BUILTIN_LOC - | jsil_type - | builtin_field - ; - -builtin_field: TOK_PROTO - { - newstack($$).id("proto"); - } - | TOK_FID - { - newstack($$).id("fid"); - } - | TOK_SCOPE - { - newstack($$).id("scope"); - } - | TOK_CONSTRUCTID - { - newstack($$).id("constructid"); - } - | TOK_PRIMVALUE - { - newstack($$).id("primvalue"); - } - | TOK_TARGETFUNCTION - { - newstack($$).id("targetfunction"); - } - | TOK_CLASS - { - newstack($$).id(ID_class); - } - ; - -binary_op: compare_op - | arithmetic_op - | boolean_op - | bitwise_op - ; - -compare_op: '=' - { - newstack($$).id(ID_equal); - } - | '<' - { - newstack($$).id(ID_lt); - } - | TOK_LEQ - { - newstack($$).id(ID_le); - } - ; - -arithmetic_op: '+' - { - newstack($$).id(ID_plus); - } - | '-' - { - newstack($$).id(ID_minus); - } - | '*' - { - newstack($$).id(ID_mult); - } - | '/' - { - newstack($$).id(ID_div); - } - | '%' - { - newstack($$).id(ID_mod); - } - ; - -boolean_op: TOK_AND - { - newstack($$).id(ID_and); - } - | TOK_OR - { - newstack($$).id(ID_or); - } - | TOK_SUBTYPE_OF - { - newstack($$).id("subtype_of"); - } - | ':' - { - newstack($$).id(ID_concatenation); - } - ; - -bitwise_op: '&' - { - newstack($$).id(ID_bitand); - } - | '|' - { - newstack($$).id(ID_bitor); - } - | '^' - { - newstack($$).id(ID_bitxor); - } - | TOK_LEFT_SHIFT - { - newstack($$).id(ID_shl); - } - | TOK_SIGNED_RIGHT_SHIFT - { - newstack($$).id(ID_shr); - } - | TOK_UNSIGNED_RIGHT_SHIFT - { - newstack($$).id(ID_lshr); - } - ; - -unary_op: TOK_NOT - { - newstack($$).id(ID_not); - } - | '-' - { - newstack($$).id(ID_unary_minus); - } - | TOK_NUM_TO_STRING - { - newstack($$).id("num_to_string"); - } - | TOK_STRING_TO_NUM - { - newstack($$).id("string_to_num"); - } - | TOK_NUM_TO_INT32 - { - newstack($$).id("num_to_int32"); - } - | TOK_NUM_TO_UINT32 - { - newstack($$).id("num_to_uint32"); - } - | '!' - { - newstack($$).id(ID_bitnot); - } - ; - -jsil_type: TOK_T_NULL - { - newstack($$).id("null_type"); - } - | TOK_T_UNDEFINED - { - newstack($$).id("undefined_type"); - } - | TOK_T_BOOLEAN - { - newstack($$).id(ID_boolean); - } - | TOK_T_STRING - { - newstack($$).id(ID_string); - } - | TOK_T_NUMBER - { - newstack($$).id("number"); - } - | TOK_T_BUILTIN_OBJECT - { - newstack($$).id("builtin_object"); - } - | TOK_T_USER_OBJECT - { - newstack($$).id("user_object"); - } - | TOK_T_OBJECT - { - newstack($$).id("object"); - } - | ref_type - | TOK_T_REFERENCE - { - newstack($$).id(ID_pointer); - newstack($$).set(ID_C_reference, true); - } - ; - -ref_type: TOK_MEMBER_REFERENCE - { - newstack($$).id(ID_member); - } - | TOK_VARIABLE_REFERENCE - { - newstack($$).id("variable"); - } - ; - -%% diff --git a/src/jsil/scanner.l b/src/jsil/scanner.l deleted file mode 100755 index 4ec6cef9336..00000000000 --- a/src/jsil/scanner.l +++ /dev/null @@ -1,351 +0,0 @@ -%option nounput -%option noinput -%option nounistd -%option never-interactive -%option stack - -%{ - -#if defined _MSC_VER -// signed/unsigned mismatch -#pragma warning(disable:4365) -// macro re-definition: flex conditonally defines INT32_MAX et al. and thus -// they are set before library headers get to define them -#pragma warning(disable:4005) -#endif - -#include -#include - -#define PARSER (*jsil_parser) -#define YYSTYPE unsigned - -#include "jsil_parser.h" -#include "jsil_y.tab.h" -// extern int yyjsildebug; - -static jsil_parsert *jsil_parser; -void jsil_scanner_init(jsil_parsert &_jsil_parser) -{ - jsil_parser = &_jsil_parser; - YY_FLUSH_BUFFER; - BEGIN(0); -} - -int yyjsilerror(const std::string &error); - -#define loc() \ - { newstack(yyjsillval); PARSER.set_source_location(parser_stack(yyjsillval)); } - -static int make_identifier() -{ - loc(); - - // this hashes the identifier - irep_idt base_name=yytext; - - parser_stack(yyjsillval).id(ID_symbol); - parser_stack(yyjsillval).set(ID_C_base_name, base_name); - parser_stack(yyjsillval).set(ID_identifier, base_name); - return TOK_IDENTIFIER; -} - -#include // IWYU pragma: keep -#include // IWYU pragma: keep -#include // IWYU pragma: keep - -%} - -delimiter [ \t\b\r] -newline [\n\f\v]|"\\\n" -whitespace {delimiter}+ -ucletter [A-Z] -lcletter [a-z] -letter ({ucletter}|{lcletter}) -digit [0-9] -identifier (({letter}|"_")({letter}|{digit}|"_"|".")*) -integer {digit}+ -exponent [eE][+-]?{integer} -fraction {integer} -float1 {integer}"."{fraction}?({exponent})? -float2 "."{fraction}({exponent})? -float3 {integer}{exponent} -float {float1}|{float2}|{float3} -escape_sequence [\\][^\n] -s_char [^"\\\n]|{escape_sequence} -string_lit ["]{s_char}*["] - -%x GRAMMAR -%x COMMENT -%x STRING_LITERAL -%x STRING_LITERAL_COMMENT -%x STATEMENTS - - /* %option debug */ - -%% - -.|\n { - BEGIN(GRAMMAR); - yyless(0); /* start again with this character */ - } - -{ - "/*" { - yy_push_state(COMMENT); /* begin comment state */ - // make the compiler happy - (void)yy_top_state(); - } -} - -{ - "*/" { yy_pop_state(); } /* end comment state, back to GRAMMAR */ - "/*" { yyjsilerror("Probably nested comments"); } - <> { yyjsilerror("Unterminated comment"); return TOK_SCANNER_ERROR; } - [^*/\n]* { } /* ignore every char except '*' and NL (performance!) */ - . { } /* all single characters within comments are ignored */ - \n { } -} - -{ - "*/" { yy_pop_state(); } /* end comment state, back to STRING_LITERAL */ - "/*" { yyjsilerror("Probably nested comments"); } - <> { yyjsilerror("Unterminated comment"); return TOK_SCANNER_ERROR; } - [^*/\n]* { } /* ignore every char except '*' and NL (performance!) */ - . { } /* all single characters within comments are ignored */ - \n { } -} - -{ - {string_lit} { - PARSER.string_literal.clear(); - PARSER.string_literal.append(yytext); - newstack(yyjsillval); - PARSER.set_source_location(parser_stack(yyjsillval)); - // String literals can be continued - yy_push_state(STRING_LITERAL); - } -} - -{ - {string_lit} { PARSER.string_literal.append(yytext); } - {whitespace} { } /* ignore */ - "/*" { yy_push_state(STRING_LITERAL_COMMENT); } /* C comment, ignore */ - {newline}|. { // anything else: back to normal - source_locationt l=parser_stack(yyjsillval).source_location(); - parser_stack(yyjsillval)=convert_string_literal(PARSER.string_literal); - parser_stack(yyjsillval).add_source_location().swap(l); - yy_pop_state(); // back to normal - yyless(0); // put back - return TOK_STRING; - } -} - -{ - "#global_is_nan" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#global_is_finite" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#boolean_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#boolean_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#boolean_prototype_to_string" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#boolean_prototype_value_of" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#object_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#object_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#object_prototype_to_string" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#object_prototype_value_of" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#object_prototype_is_prototype_of" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#object_get_prototype_of" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#number_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#number_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#number_prototype_to_string" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#number_prototype_value_of" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#string_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#string_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#string_prototype_to_string" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#string_prototype_value_of" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#error_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#terror_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#rerror_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#serror_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#evalerror_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#rangeerror_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#urierror_call_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#function_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#function_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#function_protottype_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#array_call" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - "#array_construct" { make_identifier(); return TOK_BUILTIN_IDENTIFIER; } - - "#[[GetOwnPropertyDefault]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[GetOwnPropertyString]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#GetValue" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#PutValue" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[Get]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[GetDefault]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[GetFunction]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[Put]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[HasProperty]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[DefaultValue]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[DefineOwnPropery]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[DefineOwnProperyDefault]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#[[DefineOwnProperyArray]]" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToPrimitive" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToBoolean" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToNumber" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToNumberPrim" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToUint32" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToString" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToStringPrim" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#ToObject" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#CheckObjectCoercible" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#IsCallable" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#AbstractRelation" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#StrictEquality" { make_identifier(); return TOK_SPEC_IDENTIFIER; } - "#StrictEqualitySameType" { make_identifier(); return TOK_SPEC_IDENTIFIER; } -} - -{ - {newline} { } /* skipped */ - {whitespace} { } /* skipped */ - - /*** keywords ***/ - - "procedure" { loc(); return TOK_PROCEDURE; } - "returns" { loc(); return TOK_RETURNS; } - "to" { loc(); return TOK_TO; } - "throws" { loc(); return TOK_THROWS; } - - /*** scanner parsed tokens (these have a value!) ***/ - - {identifier} { return make_identifier(); } - - "{" { loc(); BEGIN(STATEMENTS); return '{'; } - /* This catches all one-character operators */ - . { loc(); return yytext[0]; } -} - -{ - {newline} { loc(); return TOK_NEWLINE; } - {whitespace} { } /* skipped */ - - "eval" { loc(); return TOK_EVAL; } - "label" { loc(); return TOK_LABEL; } - "goto" { loc(); return TOK_GOTO; } - "skip" { loc(); return TOK_SKIP; } - "with" { loc(); return TOK_WITH; } - "new" { loc(); return TOK_NEW; } - "hasField" { loc(); return TOK_HAS_FIELD; } - "delete" { loc(); return TOK_DELETE; } - "protoField" { loc(); return TOK_PROTO_FIELD; } - "protoObj" { loc(); return TOK_PROTO_OBJ; } - "ref" { loc(); return TOK_REF; } - "field" { loc(); return TOK_FIELD; } - "base" { loc(); return TOK_BASE; } - "typeOf" { loc(); return TOK_TYPEOF; } - "null" { loc(); return TOK_NULL; } - "#undefined" { loc(); return TOK_UNDEFINED; } - "#empty" { loc(); return TOK_EMPTY; } - "true" { loc(); return TOK_TRUE; } - "false" { loc(); return TOK_FALSE; } - "#proto" { loc(); return TOK_PROTO; } - "#fid" { loc(); return TOK_FID; } - "#scope" { loc(); return TOK_SCOPE; } - "#constructid" { loc(); return TOK_CONSTRUCTID; } - "#primvalue" { loc(); return TOK_PRIMVALUE; } - "#targetfunction" { loc(); return TOK_TARGETFUNCTION; } - "#class" { loc(); return TOK_CLASS; } - "num_to_string" { loc(); return TOK_NUM_TO_STRING; } - "string_to_num" { loc(); return TOK_STRING_TO_NUM; } - "num_to_int32" { loc(); return TOK_NUM_TO_INT32; } - "num_to_uint32" { loc(); return TOK_NUM_TO_UINT32; } - "#MemberReference" { loc(); return TOK_MEMBER_REFERENCE; } - "#VariableReference" { loc(); return TOK_VARIABLE_REFERENCE; } - - /*** type classes ***/ - - "#Null" { loc(); return TOK_T_NULL; } - "#Undefined" { loc(); return TOK_T_UNDEFINED; } - "#Boolean" { loc(); return TOK_T_BOOLEAN; } - "#String" { loc(); return TOK_T_STRING; } - "#Number" { loc(); return TOK_T_NUMBER; } - "#BuiltinObject" { loc(); return TOK_T_BUILTIN_OBJECT; } - "#UserObject" { loc(); return TOK_T_USER_OBJECT; } - "#Object" { loc(); return TOK_T_OBJECT; } - "#Reference" { loc(); return TOK_T_REFERENCE; } - - /*** multi-character operators ***/ - - ":=" { loc(); return TOK_DEFEQ; } - "<=" { loc(); return TOK_LEQ; } - "and" { loc(); return TOK_AND; } - "or" { loc(); return TOK_OR; } - "<:" { loc(); return TOK_SUBTYPE_OF; } - "<<" { loc(); return TOK_LEFT_SHIFT; } - ">>" { loc(); return TOK_SIGNED_RIGHT_SHIFT; } - ">>>" { loc(); return TOK_UNSIGNED_RIGHT_SHIFT; } - "not" { loc(); return TOK_NOT; } - - /*** scanner parsed tokens (these have a value!) ***/ - - {identifier} { return make_identifier(); } - - {float}|{integer} { - newstack(yyjsillval); - parser_stack(yyjsillval)=convert_float_literal(yytext); - PARSER.set_source_location(parser_stack(yyjsillval)); - return TOK_FLOATING; - } - - "#lg" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lg_isNan" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lg_isFinite" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lop" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lop_toString" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lop_valueOf" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lop_isPrototypeOf" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lfunction" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lfp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#leval" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lerror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lep" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lrerror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lrep" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lterror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#ltep" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lserror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lsep" { make_identifier(); return TOK_BUILTIN_LOC; } - "#levalerror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#levalerrorp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lrangeerror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lrangeerrorp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lurierror" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lurierrorp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lobject" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lobject_get_prototype_of" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lboolean" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lbp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lbp_toString" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lbp_valueOf" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lnumber" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lnp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lnp_toString" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lnp_valueOf" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lmath" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lstring" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lsp" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lsp_toString" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lsp_valueOf" { make_identifier(); return TOK_BUILTIN_LOC; } - "#larray" { make_identifier(); return TOK_BUILTIN_LOC; } - "#lap" { make_identifier(); return TOK_BUILTIN_LOC; } - "#ljson" { make_identifier(); return TOK_BUILTIN_LOC; } - - "}" { loc(); BEGIN(GRAMMAR); return '}'; } - /* This catches all one-character operators */ - . { loc(); return yytext[0]; } -} - -<> { yyterminate(); /* done! */ } - -%% - -int yywrap() { return 1; } - diff --git a/src/libcprover-cpp/CMakeLists.txt b/src/libcprover-cpp/CMakeLists.txt index adf1a331f6e..d32b4074bf5 100644 --- a/src/libcprover-cpp/CMakeLists.txt +++ b/src/libcprover-cpp/CMakeLists.txt @@ -41,7 +41,6 @@ list(APPEND "xml" "json" "json-symtab-language" - "jsil" "statement-list" "goto-symex" "pointer-analysis" diff --git a/src/libcprover-cpp/Makefile b/src/libcprover-cpp/Makefile index 96a8ef29be5..54746d50058 100644 --- a/src/libcprover-cpp/Makefile +++ b/src/libcprover-cpp/Makefile @@ -28,7 +28,6 @@ OBJ += \ ../goto-instrument/unwindset$(OBJEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../goto-symex/goto-symex$(LIBEXT) \ - ../jsil/jsil$(LIBEXT) \ ../json-symtab-language/json-symtab-language$(LIBEXT) \ ../json/json$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b304d6edb18..ecc73c69b42 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -215,7 +215,6 @@ IREP_ID_ONE(input) IREP_ID_ONE(output) IREP_ID_ONE(nondet) IREP_ID_ONE(NULL) -IREP_ID_ONE(null) IREP_ID_ONE(nullptr) IREP_ID_ONE(c_enum) IREP_ID_ONE(enum_underlying_type) diff --git a/unit/Makefile b/unit/Makefile index d4394762618..b29f8c56ee1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -259,7 +259,6 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \ ../src/goto-synthesizer/expr_enumerator$(OBJEXT) \ ../src/xmllang/xmllang$(LIBEXT) \ ../src/goto-symex/goto-symex$(LIBEXT) \ - ../src/jsil/jsil$(LIBEXT) \ # Empty last line # CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \