From 3f2da256a976d738f376a6bf0b40d29e86b1b282 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 7 May 2018 11:46:40 +0200 Subject: [PATCH 1/2] Factor out language_infot from languaget Previously, using language-specific methods such as from_expr() required creating a new languaget instance which could be potentially costly. This commit introduces a language_infot class that offers language-specific methods that don't require parsing functionality. language_infot is now used for language registration (instead of language_entryt). The immutable registered *_language_infot instances are shared among the corresponding *_languaget instances that are requested by the get_language_from_* functions. --- src/analyses/goto_check.cpp | 3 +- src/ansi-c/Makefile | 1 + src/ansi-c/ansi_c_language.cpp | 38 +----- src/ansi-c/ansi_c_language.h | 28 +--- src/ansi-c/ansi_c_language_info.cpp | 52 +++++++ src/ansi-c/ansi_c_language_info.h | 48 +++++++ src/ansi-c/cprover_library.cpp | 10 +- src/cbmc/cbmc_languages.cpp | 12 +- src/clobber/clobber_parse_options.cpp | 8 +- src/cpp/Makefile | 1 + src/cpp/cpp_language.cpp | 49 +------ src/cpp/cpp_language.h | 30 +---- src/cpp/cpp_language_info.cpp | 64 +++++++++ src/cpp/cpp_language_info.h | 46 +++++++ .../goto_analyzer_parse_options.cpp | 16 +-- src/goto-cc/compile.cpp | 8 +- src/goto-cc/goto_cc_languages.cpp | 12 +- src/goto-diff/goto_diff_languages.cpp | 13 +- src/goto-diff/goto_diff_languages.h | 8 +- src/goto-diff/goto_diff_parse_options.cpp | 20 +-- src/goto-instrument/dump_c.cpp | 24 +--- src/goto-instrument/dump_c_class.h | 18 +-- .../goto_instrument_languages.cpp | 8 +- src/goto-instrument/model_argc_argv.cpp | 10 +- src/goto-programs/show_symbol_table.cpp | 38 +----- src/java_bytecode/Makefile | 1 + src/java_bytecode/java_bytecode_language.cpp | 31 +---- src/java_bytecode/java_bytecode_language.h | 35 ++--- .../java_bytecode_language_info.cpp | 41 ++++++ .../java_bytecode_language_info.h | 43 ++++++ src/jbmc/jbmc_parse_options.cpp | 15 ++- src/jsil/Makefile | 1 + src/jsil/jsil_language.cpp | 27 +--- src/jsil/jsil_language.h | 49 +++---- src/jsil/jsil_language_info.cpp | 44 ++++++ src/jsil/jsil_language_info.h | 43 ++++++ src/langapi/Makefile | 1 + src/langapi/language.cpp | 31 +---- src/langapi/language.h | 48 +------ src/langapi/language_file.cpp | 17 +-- src/langapi/language_info.cpp | 55 ++++++++ src/langapi/language_info.h | 81 +++++++++++ src/langapi/language_ui.cpp | 18 +-- src/langapi/language_util.cpp | 23 ++-- src/langapi/mode.cpp | 127 ++++++++++++------ src/langapi/mode.h | 17 ++- src/util/irep_ids.def | 1 + src/util/json_expr.cpp | 4 +- unit/analyses/ai/ai_simplify_lhs.cpp | 15 ++- unit/analyses/dependence_graph.cpp | 16 ++- unit/goto-programs/class_hierarchy_output.cpp | 7 + .../gen_nondet_string_init.cpp | 13 +- .../convert_exprt_to_string_exprt.cpp | 15 ++- .../custom_value_set_analysis.cpp | 5 +- .../instantiate_not_contains.cpp | 30 +++-- .../string_refinement/dependency_graph.cpp | 1 + .../string_symbol_resolution.cpp | 11 +- unit/testing-utils/c_to_expr.cpp | 7 +- unit/testing-utils/c_to_expr.h | 6 +- unit/testing-utils/load_java_class.cpp | 31 +---- unit/testing-utils/load_java_class.h | 7 - 61 files changed, 881 insertions(+), 601 deletions(-) create mode 100644 src/ansi-c/ansi_c_language_info.cpp create mode 100644 src/ansi-c/ansi_c_language_info.h create mode 100644 src/cpp/cpp_language_info.cpp create mode 100644 src/cpp/cpp_language_info.h create mode 100644 src/java_bytecode/java_bytecode_language_info.cpp create mode 100644 src/java_bytecode/java_bytecode_language_info.h create mode 100644 src/jsil/jsil_language_info.cpp create mode 100644 src/jsil/jsil_language_info.h create mode 100644 src/langapi/language_info.cpp create mode 100644 src/langapi/language_info.h diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 27d5fc318da..6735653e7d9 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1275,7 +1275,8 @@ void goto_checkt::add_guarded_claim( goto_programt::targett t=new_code.add_instruction(type); std::string source_expr_string; - get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns); + get_language_from_mode(mode)->info.from_expr( + src_expr, source_expr_string, ns); t->guard.swap(new_expr); t->source_location=source_location; diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index d57c0934a7d..b5747acbbd7 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -4,6 +4,7 @@ SRC = anonymous_member.cpp \ ansi_c_entry_point.cpp \ ansi_c_internal_additions.cpp \ ansi_c_language.cpp \ + ansi_c_language_info.cpp \ ansi_c_lex.yy.cpp \ ansi_c_parse_tree.cpp \ ansi_c_parser.cpp \ diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index bbb1236e9e7..e5c7fd0c420 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -21,15 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_entry_point.h" #include "ansi_c_typecheck.h" #include "ansi_c_parser.h" -#include "expr2c.h" #include "c_preprocess.h" #include "ansi_c_internal_additions.h" -#include "type2name.h" - -std::set ansi_c_languaget::extensions() const -{ - return { "c", "i" }; -} void ansi_c_languaget::modules_provided(std::set &modules) { @@ -144,36 +137,9 @@ void ansi_c_languaget::show_parse(std::ostream &out) parse_tree.output(out); } -std::unique_ptr new_ansi_c_language() -{ - return util_make_unique(); -} - -bool ansi_c_languaget::from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) -{ - code=expr2c(expr, ns); - return false; -} - -bool ansi_c_languaget::from_type( - const typet &type, - std::string &code, - const namespacet &ns) +std::unique_ptr new_ansi_c_language(const language_infot &info) { - code=type2c(type, ns); - return false; -} - -bool ansi_c_languaget::type_to_name( - const typet &type, - std::string &name, - const namespacet &ns) -{ - name=type2name(type, ns); - return false; + return std::unique_ptr(new ansi_c_languaget(info)); } bool ansi_c_languaget::to_expr( diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index b23bdad6469..82e8c0c1538 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -39,23 +39,10 @@ class ansi_c_languaget:public languaget void show_parse(std::ostream &out) override; + explicit ansi_c_languaget(const language_infot &info) : languaget(info) + { + } ~ansi_c_languaget() override; - ansi_c_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 type_to_name( - const typet &type, - std::string &name, - const namespacet &ns) override; bool to_expr( const std::string &code, @@ -63,13 +50,6 @@ class ansi_c_languaget:public languaget exprt &expr, const namespacet &ns) override; - std::unique_ptr new_language() override - { return util_make_unique(); } - - std::string id() const override { return "C"; } - std::string description() const override { return "ANSI-C 99"; } - std::set extensions() const override; - void modules_provided(std::set &modules) override; protected: @@ -77,6 +57,6 @@ class ansi_c_languaget:public languaget std::string parse_path; }; -std::unique_ptr new_ansi_c_language(); +std::unique_ptr new_ansi_c_language(const language_infot &info); #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H diff --git a/src/ansi-c/ansi_c_language_info.cpp b/src/ansi-c/ansi_c_language_info.cpp new file mode 100644 index 00000000000..018e27fcd01 --- /dev/null +++ b/src/ansi-c/ansi_c_language_info.cpp @@ -0,0 +1,52 @@ +/*******************************************************************\ + +Module: C Language + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "ansi_c_language_info.h" + +#include "expr2c.h" +#include "type2name.h" + +#include "ansi_c_language.h" + +std::set ansi_c_language_infot::extensions() const +{ + return {"c", "i"}; +} + +bool ansi_c_language_infot::from_expr( + const exprt &expr, + std::string &code, + const namespacet &ns) const +{ + code = expr2c(expr, ns); + return false; +} + +bool ansi_c_language_infot::from_type( + const typet &type, + std::string &code, + const namespacet &ns) const +{ + code = type2c(type, ns); + return false; +} + +bool ansi_c_language_infot::type_to_name( + const typet &type, + std::string &name, + const namespacet &ns) const +{ + name = type2name(type, ns); + return false; +} + +std::unique_ptr new_ansi_c_language_info() +{ + return std::unique_ptr( + new ansi_c_language_infot(new_ansi_c_language)); +} diff --git a/src/ansi-c/ansi_c_language_info.h b/src/ansi-c/ansi_c_language_info.h new file mode 100644 index 00000000000..9e74f4b4142 --- /dev/null +++ b/src/ansi-c/ansi_c_language_info.h @@ -0,0 +1,48 @@ +/*******************************************************************\ + +Module: C Language + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H +#define CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H + +#include + +#include + +class ansi_c_language_infot : public language_infot +{ +public: + explicit ansi_c_language_infot(language_factoryt _factory) + : language_infot(_factory) + { + } + + irep_idt id() const override + { + return ID_C; + } + + std::string description() const override + { + return "C"; + } + + std::set extensions() const override; + + bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) + const override; + + bool from_type(const typet &type, std::string &code, const namespacet &ns) + const override; + + bool type_to_name(const typet &type, std::string &name, const namespacet &ns) + const override; +}; + +std::unique_ptr new_ansi_c_language_info(); + +#endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_INFO_H diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index f13e321d752..908381a6273 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include #include "ansi_c_language.h" @@ -88,9 +90,9 @@ void add_library( std::istringstream in(src); - ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(message_handler); - ansi_c_language.parse(in, ""); + auto ansi_c_language = get_language_from_mode(ID_C); + ansi_c_language->set_message_handler(message_handler); + ansi_c_language->parse(in, ""); - ansi_c_language.typecheck(symbol_table, ""); + ansi_c_language->typecheck(symbol_table, ""); } diff --git a/src/cbmc/cbmc_languages.cpp b/src/cbmc/cbmc_languages.cpp index 55cc8cda97d..c76324261d1 100644 --- a/src/cbmc/cbmc_languages.cpp +++ b/src/cbmc/cbmc_languages.cpp @@ -13,19 +13,19 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include +#include +#include #ifdef HAVE_JSIL -#include +#include #endif void cbmc_parse_optionst::register_languages() { - register_language(new_ansi_c_language); - register_language(new_cpp_language); + register_language(new_ansi_c_language_info); + register_language(new_cpp_language_info); #ifdef HAVE_JSIL - register_language(new_jsil_language); + register_language(new_jsil_language_info); #endif } diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 42693cb16cb..e0a8dd771ae 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -20,8 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include +#include +#include #include #include @@ -105,8 +105,8 @@ int clobber_parse_optionst::doit() return 0; } - register_language(new_ansi_c_language); - register_language(new_cpp_language); + register_language(new_ansi_c_language_info); + register_language(new_cpp_language_info); // // command line options diff --git a/src/cpp/Makefile b/src/cpp/Makefile index b98e4766b42..20a542b432d 100644 --- a/src/cpp/Makefile +++ b/src/cpp/Makefile @@ -11,6 +11,7 @@ SRC = cpp_constructor.cpp \ cpp_internal_additions.cpp \ cpp_is_pod.cpp \ cpp_language.cpp \ + cpp_language_info.cpp \ cpp_name.cpp \ cpp_namespace_spec.cpp \ cpp_parse_tree.cpp \ diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index e47d887d292..6f6489f5a16 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -30,24 +30,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" #include "cpp_type2name.h" -std::set cpp_languaget::extensions() const -{ - std::set s; - - s.insert("cpp"); - s.insert("CPP"); - s.insert("cc"); - s.insert("c++"); - s.insert("ii"); - s.insert("cxx"); - - #ifndef _WIN32 - s.insert("C"); - #endif - - return s; -} - void cpp_languaget::modules_provided(std::set &modules) { modules.insert(get_base_name(parse_path, true)); @@ -203,36 +185,9 @@ void cpp_languaget::show_parse( out << "UNKNOWN: " << item.pretty() << '\n'; } -std::unique_ptr new_cpp_language() -{ - return util_make_unique(); -} - -bool cpp_languaget::from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) -{ - code=expr2cpp(expr, ns); - return false; -} - -bool cpp_languaget::from_type( - const typet &type, - std::string &code, - const namespacet &ns) -{ - code=type2cpp(type, ns); - return false; -} - -bool cpp_languaget::type_to_name( - const typet &type, - std::string &name, - const namespacet &ns) +std::unique_ptr new_cpp_language(const language_infot &info) { - name=cpp_type2name(type); - return false; + return std::unique_ptr(new cpp_languaget(info)); } bool cpp_languaget::to_expr( diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index 3f474005f15..c9c5d1f845d 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -49,24 +49,9 @@ class cpp_languaget:public languaget // constructor, destructor ~cpp_languaget() override; - cpp_languaget() { } - - // conversion from expression into string - bool from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) override; - - // conversion from type into string - bool from_type( - const typet &type, - std::string &code, - const namespacet &ns) override; - - bool type_to_name( - const typet &type, - std::string &name, - const namespacet &ns) override; + explicit cpp_languaget(const language_infot &info) : languaget(info) + { + } // conversion from string into expression bool to_expr( @@ -75,13 +60,6 @@ class cpp_languaget:public languaget exprt &expr, const namespacet &ns) override; - std::unique_ptr new_language() override - { return util_make_unique(); } - - std::string id() const override { return "cpp"; } - std::string description() const override { return "C++"; } - std::set extensions() const override; - void modules_provided(std::set &modules) override; protected: @@ -96,6 +74,6 @@ class cpp_languaget:public languaget } }; -std::unique_ptr new_cpp_language(); +std::unique_ptr new_cpp_language(const language_infot &); #endif // CPROVER_CPP_CPP_LANGUAGE_H diff --git a/src/cpp/cpp_language_info.cpp b/src/cpp/cpp_language_info.cpp new file mode 100644 index 00000000000..932bc9ced32 --- /dev/null +++ b/src/cpp/cpp_language_info.cpp @@ -0,0 +1,64 @@ +/*******************************************************************\ + +Module: C++ Language + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "cpp_language_info.h" + +#include "cpp_language.h" +#include "cpp_type2name.h" +#include "expr2cpp.h" + +std::set cpp_language_infot::extensions() const +{ + std::set s; + + s.insert("cpp"); + s.insert("CPP"); + s.insert("cc"); + s.insert("c++"); + s.insert("ii"); + s.insert("cxx"); + +#ifndef _WIN32 + s.insert("C"); +#endif + + return s; +} + +bool cpp_language_infot::from_expr( + const exprt &expr, + std::string &code, + const namespacet &ns) const +{ + code = expr2cpp(expr, ns); + return false; +} + +bool cpp_language_infot::from_type( + const typet &type, + std::string &code, + const namespacet &ns) const +{ + code = type2cpp(type, ns); + return false; +} + +bool cpp_language_infot::type_to_name( + const typet &type, + std::string &name, + const namespacet &ns) const +{ + name = cpp_type2name(type); + return false; +} + +std::unique_ptr new_cpp_language_info() +{ + return std::unique_ptr( + new cpp_language_infot(new_cpp_language)); +} diff --git a/src/cpp/cpp_language_info.h b/src/cpp/cpp_language_info.h new file mode 100644 index 00000000000..84fbda41a5d --- /dev/null +++ b/src/cpp/cpp_language_info.h @@ -0,0 +1,46 @@ +/*******************************************************************\ + +Module: C++ Language + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_CPP_CPP_LANGUAGE_INFO_H +#define CPROVER_CPP_CPP_LANGUAGE_INFO_H + +#include + +#include + +class cpp_language_infot : public language_infot +{ +public: + explicit cpp_language_infot(language_factoryt _factory) + : language_infot(_factory) + { + } + + bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) + const override; + + bool from_type(const typet &type, std::string &code, const namespacet &ns) + const override; + + bool type_to_name(const typet &type, std::string &name, const namespacet &ns) + const override; + + irep_idt id() const override + { + return ID_cpp; + } + std::string description() const override + { + return "C++"; + } + std::set extensions() const override; +}; + +std::unique_ptr new_cpp_language_info(); + +#endif // CPROVER_CPP_CPP_LANGUAGE_INFO_H diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 04cd02412d1..9a15efd9583 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -16,10 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include +#include +#include +#include +#include #include #include @@ -74,10 +74,10 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( void goto_analyzer_parse_optionst::register_languages() { - register_language(new_ansi_c_language); - register_language(new_cpp_language); - register_language(new_java_bytecode_language); - register_language(new_jsil_language); + register_language(new_ansi_c_language_info); + register_language(new_cpp_language_info); + register_language(new_java_bytecode_language_info); + register_language(new_jsil_language_info); } void goto_analyzer_parse_optionst::eval_verbosity() diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index fd92c7aeb63..49811ed98ed 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -527,9 +527,9 @@ bool compilet::parse(const std::string &file_name) /// \return true on error, false otherwise bool compilet::parse_stdin() { - ansi_c_languaget language; + auto language = get_language_from_mode(ID_C); - language.set_message_handler(get_message_handler()); + language->set_message_handler(get_message_handler()); statistics() << "Parsing: (stdin)" << eom; @@ -551,11 +551,11 @@ bool compilet::parse_stdin() } } - language.preprocess(std::cin, "", *os); + language->preprocess(std::cin, "", *os); } else { - if(language.parse(std::cin, "")) + if(language->parse(std::cin, "")) { if(get_ui()==ui_message_handlert::uit::PLAIN) error() << "PARSING ERROR" << eom; diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp index 3e0b56aeed4..0b78130fb5b 100644 --- a/src/goto-cc/goto_cc_languages.cpp +++ b/src/goto-cc/goto_cc_languages.cpp @@ -13,13 +13,13 @@ Author: CM Wintersteiger #include -#include -#include -#include +#include +#include +#include void goto_cc_modet::register_languages() { - register_language(new_ansi_c_language); - register_language(new_cpp_language); - register_language(new_jsil_language); + register_language(new_ansi_c_language_info); + register_language(new_cpp_language_info); + register_language(new_jsil_language_info); } diff --git a/src/goto-diff/goto_diff_languages.cpp b/src/goto-diff/goto_diff_languages.cpp index 814ef326488..299ca207e7e 100644 --- a/src/goto-diff/goto_diff_languages.cpp +++ b/src/goto-diff/goto_diff_languages.cpp @@ -13,14 +13,15 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include +#include -#include +#include + +#include void goto_diff_languagest::register_languages() { - register_language(new_ansi_c_language); - register_language(new_cpp_language); - register_language(new_java_bytecode_language); + register_language(new_ansi_c_language_info); + register_language(new_cpp_language_info); + register_language(new_java_bytecode_language_info); } diff --git a/src/goto-diff/goto_diff_languages.h b/src/goto-diff/goto_diff_languages.h index 7bd4c24e525..563adf92e95 100644 --- a/src/goto-diff/goto_diff_languages.h +++ b/src/goto-diff/goto_diff_languages.h @@ -20,10 +20,12 @@ class goto_diff_languagest:public language_uit public: explicit goto_diff_languagest( const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler) : - language_uit(cmdline, ui_message_handler) + ui_message_handlert &ui_message_handler, + bool do_register = true) + : language_uit(cmdline, ui_message_handler) { - register_languages(); + if(do_register) + register_languages(); } protected: diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 889fee4c0ed..56cfb626ad6 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -64,22 +64,22 @@ Author: Peter Schrammel #include "unified_diff.h" #include "change_impact.h" -goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv): - parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv), - goto_diff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION), - languages2(cmdline, ui_message_handler) +goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv) + : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv), + goto_diff_languagest(cmdline, ui_message_handler), + ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION), + languages2(cmdline, ui_message_handler, false) { } ::goto_diff_parse_optionst::goto_diff_parse_optionst( int argc, const char **argv, - const std::string &extra_options): - parse_options_baset(GOTO_DIFF_OPTIONS+extra_options, argc, argv), - goto_diff_languagest(cmdline, ui_message_handler), - ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION), - languages2(cmdline, ui_message_handler) + const std::string &extra_options) + : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv), + goto_diff_languagest(cmdline, ui_message_handler), + ui_message_handler(cmdline, "GOTO-DIFF " CBMC_VERSION), + languages2(cmdline, ui_message_handler, false) { } diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 2715f303063..cee21ba53c3 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -469,7 +469,7 @@ void dump_ct::convert_compound( if(t.get_width()<=config.ansi_c.long_long_int_width) struct_body << "long long int " << comp_name << " : " << t.get_width(); - else if(language->id()=="cpp") + else if(language_info.id() == ID_cpp) struct_body << "__signedbv<" << t.get_width() << "> " << comp_name; else @@ -481,7 +481,7 @@ void dump_ct::convert_compound( if(t.get_width()<=config.ansi_c.long_long_int_width) struct_body << "unsigned long long " << comp_name << " : " << t.get_width(); - else if(language->id()=="cpp") + else if(language_info.id() == ID_cpp) struct_body << "__unsignedbv<" << t.get_width() << "> " << comp_name; else @@ -512,7 +512,7 @@ void dump_ct::convert_compound( os << type_to_string(unresolved_clean); if(!base_decls.str().empty()) { - PRECONDITION(language->id()=="cpp"); + PRECONDITION(language_info.id() == ID_cpp); os << ": " << base_decls.str(); } os << '\n'; @@ -1384,7 +1384,7 @@ std::string dump_ct::type_to_string(const typet &type) std::string ret; typet t=type; cleanup_type(t); - language->from_type(t, ret, ns); + language_info.from_type(t, ret, ns); return ret; } @@ -1393,7 +1393,7 @@ std::string dump_ct::expr_to_string(const exprt &expr) std::string ret; exprt e=expr; cleanup_expr(e); - language->from_expr(e, ret, ns); + language_info.from_expr(e, ret, ns); return ret; } @@ -1406,12 +1406,7 @@ void dump_c( std::ostream &out) { dump_ct goto2c( - src, - use_system_headers, - use_all_headers, - include_harness, - ns, - new_ansi_c_language); + src, use_system_headers, use_all_headers, include_harness, ns, ID_C); out << goto2c; } @@ -1424,11 +1419,6 @@ void dump_cpp( std::ostream &out) { dump_ct goto2cpp( - src, - use_system_headers, - use_all_headers, - include_harness, - ns, - new_cpp_language); + src, use_system_headers, use_all_headers, include_harness, ns, ID_cpp); out << goto2cpp; } diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index 10368d9e044..a7325358dd3 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include // unique_ptr -#include +#include #include #include @@ -30,13 +30,13 @@ class dump_ct const bool use_all_headers, const bool include_harness, const namespacet &_ns, - language_factoryt factory): - goto_functions(_goto_functions), - copied_symbol_table(_ns.get_symbol_table()), - ns(copied_symbol_table), - language(factory()), - harness(include_harness), - system_symbols(use_system_headers) + const irep_idt &mode) + : goto_functions(_goto_functions), + copied_symbol_table(_ns.get_symbol_table()), + ns(copied_symbol_table), + language_info(get_language_info_from_mode(mode)), + harness(include_harness), + system_symbols(use_system_headers) { system_symbols.set_use_all_headers(use_all_headers); } @@ -49,7 +49,7 @@ class dump_ct const goto_functionst &goto_functions; symbol_tablet copied_symbol_table; const namespacet ns; - std::unique_ptr language; + const language_infot &language_info; const bool harness; typedef std::unordered_set convertedt; diff --git a/src/goto-instrument/goto_instrument_languages.cpp b/src/goto-instrument/goto_instrument_languages.cpp index a52628601e6..60ff3559b16 100644 --- a/src/goto-instrument/goto_instrument_languages.cpp +++ b/src/goto-instrument/goto_instrument_languages.cpp @@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include +#include +#include void goto_instrument_parse_optionst::register_languages() { - register_language(new_ansi_c_language); - register_language(new_cpp_language); + register_language(new_ansi_c_language_info); + register_language(new_cpp_language_info); } diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index eab95aed6a8..03e135cb8c7 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -30,6 +30,8 @@ Date: April 2016 #include #include +#include + /// Set up argv with up to max_argc pointers into an array of 4096 bytes. /// \param symbol_table: Input program's symbol table /// \param goto_functions: Input program's intermediate representation @@ -99,15 +101,15 @@ bool model_argc_argv( << "}"; std::istringstream iss(oss.str()); - ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(message_handler); + auto ansi_c_language = get_language_from_mode(ID_C); + ansi_c_language->set_message_handler(message_handler); configt::ansi_ct::preprocessort pp=config.ansi_c.preprocessor; config.ansi_c.preprocessor=configt::ansi_ct::preprocessort::NONE; - ansi_c_language.parse(iss, ""); + ansi_c_language->parse(iss, ""); config.ansi_c.preprocessor=pp; symbol_tablet tmp_symbol_table; - ansi_c_language.typecheck(tmp_symbol_table, ""); + ansi_c_language->typecheck(tmp_symbol_table, ""); goto_programt init_instructions; exprt value=nil_exprt(); diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 771bc88da00..924c386ce71 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "goto_model.h" @@ -41,22 +40,11 @@ void show_symbol_table_brief_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode=="") - ptr=get_default_language(); - else - { - ptr=get_language_from_mode(symbol.mode); - if(ptr==nullptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - } - std::string type_str; - if(symbol.type.is_not_nil()) - ptr->from_type(symbol.type, type_str, ns); - + const language_infot &language_info = + get_language_info_from_mode(symbol.mode); + language_info.from_type(symbol.type, type_str, ns); out << symbol.name << " " << type_str << '\n'; } } @@ -81,27 +69,15 @@ void show_symbol_table_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode=="") - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - std::string type_str, value_str; + const language_infot &language_info = + get_language_info_from_mode(symbol.mode); if(symbol.type.is_not_nil()) - ptr->from_type(symbol.type, type_str, ns); + language_info.from_type(symbol.type, type_str, ns); if(symbol.value.is_not_nil()) - ptr->from_expr(symbol.value, value_str, ns); + language_info.from_expr(symbol.value, value_str, ns); out << "Symbol......: " << symbol.name << '\n' << std::flush; out << "Pretty name.: " << symbol.pretty_name << '\n'; diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 13aa8e6c2ca..89d1251ff88 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -10,6 +10,7 @@ SRC = bytecode_info.cpp \ java_bytecode_instrument.cpp \ java_bytecode_internal_additions.cpp \ java_bytecode_language.cpp \ + java_bytecode_language_info.cpp \ java_bytecode_parse_tree.cpp \ java_bytecode_parser.cpp \ java_bytecode_typecheck.cpp \ diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 72deab72194..299558ce5ae 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: +Module: Java Bytecode Language Author: Daniel Kroening, kroening@kroening.com @@ -134,11 +134,6 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) language_options_initialized=true; } -std::set java_bytecode_languaget::extensions() const -{ - return { "class", "jar" }; -} - void java_bytecode_languaget::modules_provided(std::set &modules) { // modules.insert(translation_unit(parse_path)); @@ -1031,27 +1026,11 @@ void java_bytecode_languaget::show_parse(std::ostream &out) } } -std::unique_ptr new_java_bytecode_language() -{ - return util_make_unique(); -} - -bool java_bytecode_languaget::from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) +std::unique_ptr +new_java_bytecode_language(const language_infot &info) { - code=expr2java(expr, ns); - return false; -} - -bool java_bytecode_languaget::from_type( - const typet &type, - std::string &code, - const namespacet &ns) -{ - code=type2java(type, ns); - return false; + return std::unique_ptr( + new java_bytecode_languaget(info)); } bool java_bytecode_languaget::to_expr( diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 29c347fe227..80ca0a08af5 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -1,12 +1,11 @@ /*******************************************************************\ -Module: +Module: Java Bytecode Language Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H @@ -95,7 +94,9 @@ class java_bytecode_languaget:public languaget virtual ~java_bytecode_languaget(); java_bytecode_languaget( - std::unique_ptr pointer_type_selector): + const language_infot &info, + std::unique_ptr pointer_type_selector) + : languaget(info), assume_inputs_non_null(false), object_factory_parameters(), max_user_array_length(0), @@ -104,35 +105,18 @@ class java_bytecode_languaget:public languaget pointer_type_selector(std::move(pointer_type_selector)) {} - java_bytecode_languaget(): - java_bytecode_languaget( - std::unique_ptr(new select_pointer_typet())) + explicit java_bytecode_languaget(const language_infot &info) + : java_bytecode_languaget( + info, + std::unique_ptr(new select_pointer_typet())) {} - - 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) override; - std::unique_ptr new_language() override - { return util_make_unique(); } - - std::string id() const override { return "java"; } - std::string description() const override { return "Java Bytecode"; } - std::set extensions() const override; - void modules_provided(std::set &modules) override; virtual void methods_provided(std::unordered_set &methods) const override; @@ -187,6 +171,7 @@ class java_bytecode_languaget:public languaget std::unordered_set no_load_classes; }; -std::unique_ptr new_java_bytecode_language(); +std::unique_ptr +new_java_bytecode_language(const language_infot &info); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H diff --git a/src/java_bytecode/java_bytecode_language_info.cpp b/src/java_bytecode/java_bytecode_language_info.cpp new file mode 100644 index 00000000000..3e9337cb106 --- /dev/null +++ b/src/java_bytecode/java_bytecode_language_info.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Java Bytecode Language + +Author: Diffblue Ltd + +\*******************************************************************/ + +#include "java_bytecode_language_info.h" + +#include "expr2java.h" +#include "java_bytecode_language.h" + +std::set java_bytecode_language_infot::extensions() const +{ + return {"class", "jar"}; +} + +bool java_bytecode_language_infot::from_expr( + const exprt &expr, + std::string &code, + const namespacet &ns) const +{ + code = expr2java(expr, ns); + return false; +} + +bool java_bytecode_language_infot::from_type( + const typet &type, + std::string &code, + const namespacet &ns) const +{ + code = type2java(type, ns); + return false; +} + +std::unique_ptr new_java_bytecode_language_info() +{ + return std::unique_ptr( + new java_bytecode_language_infot(new_java_bytecode_language)); +} diff --git a/src/java_bytecode/java_bytecode_language_info.h b/src/java_bytecode/java_bytecode_language_info.h new file mode 100644 index 00000000000..8fa175bd83c --- /dev/null +++ b/src/java_bytecode/java_bytecode_language_info.h @@ -0,0 +1,43 @@ +/*******************************************************************\ + +Module: Java Bytecode Language + +Author: Diffblue Ltd + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_INFO_H +#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_INFO_H + +#include + +#include + +class java_bytecode_language_infot : public language_infot +{ +public: + explicit java_bytecode_language_infot(language_factoryt _factory) + : language_infot(_factory) + { + } + + bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) + const override; + + bool from_type(const typet &type, std::string &code, const namespacet &ns) + const override; + + irep_idt id() const override + { + return ID_java; + } + std::string description() const override + { + return "Java Bytecode"; + } + std::set extensions() const override; +}; + +std::unique_ptr new_java_bytecode_language_info(); + +#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_INFO_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 72c7c1eacdd..1c6e227f2c6 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -22,9 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - -#include +#include +#include #include #include @@ -50,9 +49,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include -#include +#include #include #include #include @@ -451,8 +450,10 @@ int jbmc_parse_optionst::doit() << config.this_architecture() << " " << config.this_operating_system() << eom; - register_language(new_ansi_c_language); - register_language(new_java_bytecode_language); + // still required for __CPROVER_initialize + register_language(new_ansi_c_language_info); + + register_language(new_java_bytecode_language_info); if(cmdline.isset("show-parse-tree")) { diff --git a/src/jsil/Makefile b/src/jsil/Makefile index 61380167d05..15eef358ebd 100644 --- a/src/jsil/Makefile +++ b/src/jsil/Makefile @@ -3,6 +3,7 @@ SRC = expr2jsil.cpp \ jsil_entry_point.cpp \ jsil_internal_additions.cpp \ jsil_language.cpp \ + jsil_language_info.cpp \ jsil_lex.yy.cpp \ jsil_parse_tree.cpp \ jsil_parser.cpp \ diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index 83462732c1d..4c175b076ac 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -21,11 +21,6 @@ Author: Michael Tautschnig, tautschn@amazon.com #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)); @@ -99,27 +94,9 @@ void jsil_languaget::show_parse(std::ostream &out) parse_tree.output(out); } -std::unique_ptr new_jsil_language() -{ - return util_make_unique(); -} - -bool jsil_languaget::from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) +std::unique_ptr new_jsil_language(const language_infot &info) { - 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; + return std::unique_ptr(new jsil_languaget(info)); } bool jsil_languaget::to_expr( diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 8b902b86ded..75b2bfec13e 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -20,62 +20,43 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_parse_tree.h" +#include "jsil_language_info.h" + class jsil_languaget:public languaget { public: - virtual bool preprocess( + bool preprocess( std::istream &instream, const std::string &path, std::ostream &outstream) override; - virtual bool parse( - std::istream &instream, - const std::string &path) override; - - virtual bool generate_support_functions( - symbol_tablet &symbol_table) override; - - virtual bool typecheck( - symbol_tablet &context, - const std::string &module) override; + bool parse(std::istream &instream, const std::string &path) override; - virtual void show_parse(std::ostream &out) override; + bool generate_support_functions(symbol_tablet &symbol_table) override; - virtual ~jsil_languaget(); - jsil_languaget() { } + bool typecheck(symbol_tablet &context, const std::string &module) override; - virtual bool from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) override; + void show_parse(std::ostream &out) override; - virtual bool from_type( - const typet &type, - std::string &code, - const namespacet &ns) override; + ~jsil_languaget(); + explicit jsil_languaget(const language_infot &info) : languaget(info) + { + } - virtual bool to_expr( + bool to_expr( const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override; - virtual std::unique_ptr new_language() override - { return util_make_unique(); } - - virtual std::string id() const override { return "jsil"; } - virtual std::string description() const override - { return "Javascript Intermediate Language"; } - virtual std::set extensions() const override; - - virtual void modules_provided(std::set &modules) override; - virtual bool interfaces(symbol_tablet &symbol_table) override; + void modules_provided(std::set &modules) override; + bool interfaces(symbol_tablet &symbol_table) override; protected: jsil_parse_treet parse_tree; std::string parse_path; }; -std::unique_ptr new_jsil_language(); +std::unique_ptr new_jsil_language(const language_infot &); #endif // CPROVER_JSIL_JSIL_LANGUAGE_H diff --git a/src/jsil/jsil_language_info.cpp b/src/jsil/jsil_language_info.cpp new file mode 100644 index 00000000000..39e22627d54 --- /dev/null +++ b/src/jsil/jsil_language_info.cpp @@ -0,0 +1,44 @@ +/*******************************************************************\ + +Module: Jsil Language + +Author: Michael Tautschnig, tautschn@amazon.com + +\*******************************************************************/ + +/// \file +/// Jsil Language + +#include "jsil_language_info.h" + +#include "expr2jsil.h" +#include "jsil_language.h" + +std::set jsil_language_infot::extensions() const +{ + return {"jsil"}; +} + +bool jsil_language_infot::from_expr( + const exprt &expr, + std::string &code, + const namespacet &ns) const +{ + code = expr2jsil(expr, ns); + return false; +} + +bool jsil_language_infot::from_type( + const typet &type, + std::string &code, + const namespacet &ns) const +{ + code = type2jsil(type, ns); + return false; +} + +std::unique_ptr new_jsil_language_info() +{ + return std::unique_ptr( + new jsil_language_infot(new_jsil_language)); +} diff --git a/src/jsil/jsil_language_info.h b/src/jsil/jsil_language_info.h new file mode 100644 index 00000000000..4c08d93cf6c --- /dev/null +++ b/src/jsil/jsil_language_info.h @@ -0,0 +1,43 @@ +/*******************************************************************\ + +Module: Jsil Language + +Author: Michael Tautschnig, tautschn@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_JSIL_JSIL_LANGUAGE_INFO_H +#define CPROVER_JSIL_JSIL_LANGUAGE_INFO_H + +#include + +#include + +class jsil_language_infot : public language_infot +{ +public: + explicit jsil_language_infot(language_factoryt _factory) + : language_infot(_factory) + { + } + + irep_idt id() const override + { + return ID_jsil; + } + std::string description() const override + { + return "Javascript Intermediate Language"; + } + std::set extensions() const override; + + bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) + const override; + + bool from_type(const typet &type, std::string &code, const namespacet &ns) + const override; +}; + +std::unique_ptr new_jsil_language_info(); + +#endif // CPROVER_JSIL_JSIL_LANGUAGE_INFO_H diff --git a/src/langapi/Makefile b/src/langapi/Makefile index ea85a9213b8..395a84206a7 100644 --- a/src/langapi/Makefile +++ b/src/langapi/Makefile @@ -1,6 +1,7 @@ SRC = language_ui.cpp \ language_util.cpp \ language_file.cpp \ + language_info.cpp \ language.cpp \ mode.cpp \ # Empty last line diff --git a/src/langapi/language.cpp b/src/langapi/language.cpp index 443062dce08..6e7fd2b0b4e 100644 --- a/src/langapi/language.cpp +++ b/src/langapi/language.cpp @@ -34,35 +34,6 @@ void languaget::dependencies( { } -bool languaget::from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns) -{ - code=expr.pretty(); - return false; -} - -bool languaget::from_type( - const typet &type, - std::string &code, - const namespacet &ns) -{ - code=type.pretty(); - return false; -} - -bool languaget::type_to_name( - const typet &type, - std::string &name, - const namespacet &ns) -{ - // probably ansi-c/type2name could be used as better fallback if moved to - // util/ - name=type.pretty(); - return false; -} - /// Turn on or off stub generation. /// \param should_generate_stubs: Should stub generation be enabled void languaget::set_should_generate_opaque_method_stubs( @@ -131,7 +102,7 @@ parameter_symbolt languaget::build_stub_parameter_symbol( size_t parameter_index, const code_typet::parametert ¶meter) { - error() << "language " << id() + error() << "language " << info.id() << " doesn't implement build_stub_parameter_symbol. " << "This means cannot use opaque functions." << eom; diff --git a/src/langapi/language.h b/src/langapi/language.h index 9e35daa17c9..f5fbbb8b58e 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "language_info.h" + class symbol_tablet; class symbol_table_baset; class exprt; @@ -101,49 +103,12 @@ class languaget:public messaget symbol_tablet &symbol_table, const std::string &module)=0; - // language id / description - - virtual std::string id() const { return ""; } - virtual std::string description() const { return ""; } - virtual std::set extensions() const - { return std::set(); } - // show parse tree virtual void show_parse(std::ostream &out)=0; // conversion of expressions - /// Formats the given expression in a language-specific way - /// \param expr: the expression to format - /// \param code: the formatted expression - /// \param ns: a namespace - /// \return false if conversion succeeds - virtual bool from_expr( - const exprt &expr, - std::string &code, - const namespacet &ns); - - /// Formats the given type in a language-specific way - /// \param type: the type to format - /// \param code: the formatted type - /// \param ns: a namespace - /// \return false if conversion succeeds - virtual bool from_type( - const typet &type, - std::string &code, - const namespacet &ns); - - /// Encodes the given type in a language-specific way - /// \param type: the type to encode - /// \param name: the encoded type - /// \param ns: a namespace - /// \return false if the conversion succeeds - virtual bool type_to_name( - const typet &type, - std::string &name, - const namespacet &ns); - /// Parses the given string into an expression /// \param code: the string to parse /// \param module: prefix to be used for identifiers @@ -156,16 +121,17 @@ class languaget:public messaget exprt &expr, const namespacet &ns)=0; - virtual std::unique_ptr new_language()=0; - void set_should_generate_opaque_method_stubs(bool should_generate_stubs); - // constructor / destructor + const language_infot &info; - languaget() { } virtual ~languaget() { } protected: + explicit languaget(const language_infot &_info) : info(_info) + { + } + void generate_opaque_method_stubs(symbol_tablet &symbol_table); virtual irep_idt generate_opaque_stub_body( symbolt &symbol, diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp index e28cdafd7ff..3cb524757ca 100644 --- a/src/langapi/language_file.cpp +++ b/src/langapi/language_file.cpp @@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "language.h" -language_filet::language_filet(const language_filet &rhs): - modules(rhs.modules), - language(rhs.language==nullptr?nullptr:rhs.language->new_language()), - filename(rhs.filename) +language_filet::language_filet(const language_filet &rhs) + : modules(rhs.modules), + language( + rhs.language == nullptr ? nullptr : rhs.language->info.new_language()), + filename(rhs.filename) { } @@ -165,11 +166,11 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) bool language_filest::generate_support_functions( symbol_tablet &symbol_table) { - std::set languages; + std::set languages; for(auto &file : file_map) { - if(languages.insert(file.second.language->id()).second) + if(languages.insert(file.second.language->info.id()).second) if(file.second.language->generate_support_functions(symbol_table)) return true; } @@ -179,11 +180,11 @@ bool language_filest::generate_support_functions( bool language_filest::final(symbol_table_baset &symbol_table) { - std::set languages; + std::set languages; for(auto &file : file_map) { - if(languages.insert(file.second.language->id()).second) + if(languages.insert(file.second.language->info.id()).second) if(file.second.language->final(symbol_table)) return true; } diff --git a/src/langapi/language_info.cpp b/src/langapi/language_info.cpp new file mode 100644 index 00000000000..f519ea1c83f --- /dev/null +++ b/src/langapi/language_info.cpp @@ -0,0 +1,55 @@ +/*******************************************************************\ + +Module: Language frontend info interface + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Language frontend info interface + +#include "language_info.h" + +#include +#include +#include +#include +#include +#include + +#include "language.h" + +bool language_infot::from_expr( + const exprt &expr, + std::string &code, + const namespacet &ns) const +{ + code = expr.pretty(); + return false; +} + +bool language_infot::from_type( + const typet &type, + std::string &code, + const namespacet &ns) const +{ + code = type.pretty(); + return false; +} + +bool language_infot::type_to_name( + const typet &type, + std::string &name, + const namespacet &ns) const +{ + // probably ansi-c/type2name could be used as better fallback if moved to + // util/ + name = type.pretty(); + return false; +} + +std::unique_ptr language_infot::new_language() const +{ + return factory(*this); +} diff --git a/src/langapi/language_info.h b/src/langapi/language_info.h new file mode 100644 index 00000000000..89ec0d0a05a --- /dev/null +++ b/src/langapi/language_info.h @@ -0,0 +1,81 @@ +/*******************************************************************\ + +Module: Language frontend info interface + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Language frontend info interface + +#ifndef CPROVER_LANGAPI_LANGUAGE_INFO_H +#define CPROVER_LANGAPI_LANGUAGE_INFO_H + +#include +#include +#include +#include +#include + +#include +#include + +class languaget; +class language_infot; + +typedef std::unique_ptr (*language_factoryt)(const language_infot &); +typedef std::unique_ptr (*language_info_factoryt)(); + +class language_infot +{ +public: + /// \return the language's id (aka mode) + virtual irep_idt id() const = 0; + + /// \return a textual description of the language + virtual std::string description() const = 0; + + /// \return a set of file extensions associated with this language + virtual std::set extensions() const = 0; + + /// Formats the given expression in a language-specific way + /// \param expr: the expression to format + /// \param code: the formatted expression + /// \param ns: a namespace + /// \return false if conversion succeeds + virtual bool + from_expr(const exprt &expr, std::string &code, const namespacet &ns) const; + + /// Formats the given type in a language-specific way + /// \param type: the type to format + /// \param code: the formatted type + /// \param ns: a namespace + /// \return false if conversion succeeds + virtual bool + from_type(const typet &type, std::string &code, const namespacet &ns) const; + + /// Encodes the given type in a language-specific way + /// \param type: the type to encode + /// \param name: the encoded type + /// \param ns: a namespace + /// \return false if the conversion succeeds + virtual bool type_to_name( + const typet &type, + std::string &name, + const namespacet &ns) const; + + virtual ~language_infot() = default; + + /// \return a new language instance + std::unique_ptr new_language() const; + +protected: + const language_factoryt factory; + + explicit language_infot(language_factoryt _factory) : factory(_factory) + { + } +}; + +#endif // CPROVER_UTIL_LANGUAGE_INFO_H diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 4f3f3ec479e..40dd4965444 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -166,27 +166,15 @@ void language_uit::show_symbol_table_plain( { const symbolt &symbol=ns.lookup(id); - std::unique_ptr ptr; - - if(symbol.mode=="") - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; + const auto &language_info = get_language_info_from_mode(symbol.mode); std::string type_str, value_str; if(symbol.type.is_not_nil()) - ptr->from_type(symbol.type, type_str, ns); + language_info.from_type(symbol.type, type_str, ns); if(symbol.value.is_not_nil()) - ptr->from_expr(symbol.value, value_str, ns); + language_info.from_expr(symbol.value, value_str, ns); if(brief) { diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 87c51c9877f..e596b748ec6 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -10,11 +10,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include #include +#include #include "language.h" +#include "language_info.h" #include "mode.h" std::string from_expr( @@ -22,10 +23,10 @@ std::string from_expr( const irep_idt &identifier, const exprt &expr) { - std::unique_ptr p(get_language_from_identifier(ns, identifier)); + const auto &language_info = get_language_info_from_identifier(ns, identifier); std::string result; - p->from_expr(expr, result, ns); + language_info.from_expr(expr, result, ns); return result; } @@ -35,10 +36,10 @@ std::string from_type( const irep_idt &identifier, const typet &type) { - std::unique_ptr p(get_language_from_identifier(ns, identifier)); + const auto &language_info = get_language_info_from_identifier(ns, identifier); std::string result; - p->from_type(type, result, ns); + language_info.from_type(type, result, ns); return result; } @@ -48,10 +49,10 @@ std::string type_to_name( const irep_idt &identifier, const typet &type) { - std::unique_ptr p(get_language_from_identifier(ns, identifier)); + const auto &language_info = get_language_info_from_identifier(ns, identifier); std::string result; - p->type_to_name(type, result, ns); + language_info.type_to_name(type, result, ns); return result; } @@ -73,16 +74,14 @@ exprt to_expr( const irep_idt &identifier, const std::string &src) { - std::unique_ptr p(get_language_from_identifier(ns, identifier)); - - null_message_handlert null_message_handler; - p->set_message_handler(null_message_handler); + std::unique_ptr language = + get_language_from_identifier(ns, identifier); const symbolt &symbol=ns.lookup(identifier); exprt expr; - if(p->to_expr(src, id2string(symbol.module), expr, ns)) + if(language->to_expr(src, id2string(symbol.module), expr, ns)) return nil_exprt(); return expr; diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index d2bc2474189..31b971234cf 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -17,31 +17,35 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #endif #include "language.h" +#include "language_info.h" #include #include -struct language_entryt -{ - language_factoryt factory; - std::set extensions; - irep_idt mode; -}; - -typedef std::list languagest; +typedef std::list> languagest; languagest languages; /// Register a language /// Note: registering a language is required for using the functions /// in language_util.h -/// \param factory: a language factory, e.g. `new_ansi_c_language` -void register_language(language_factoryt factory) +/// \param factory: a language info factory, e.g. `new_ansi_c_language_info` +void register_language(language_info_factoryt factory) +{ + auto language_info = factory(); + + // check whether we attempt to register the same language twice + for(const auto &info : languages) + { + PRECONDITION(language_info->id() != info->id()); + } + + languages.push_back(std::move(language_info)); +} + +/// Unregister all registered languages +void clear_languages() { - languages.push_back(language_entryt()); - std::unique_ptr l(factory()); - languages.back().factory=factory; - languages.back().extensions=l->extensions(); - languages.back().mode=l->id(); + languages.clear(); } /// Get the language corresponding to the given mode @@ -49,13 +53,29 @@ void register_language(language_factoryt factory) /// \return the language or `nullptr` if the language has not been registered std::unique_ptr get_language_from_mode(const irep_idt &mode) { - for(const auto &language : languages) - if(mode == language.mode) - return language.factory(); + for(const auto &language_info : languages) + { + if(mode == language_info->id()) + return language_info->new_language(); + } return nullptr; } +/// Get the language info corresponding to the given mode +/// \param mode: the mode, e.g. `ID_C` +/// \return the language info (assumes that the language has been registered) +const language_infot &get_language_info_from_mode(const irep_idt &mode) +{ + for(const auto &language_info : languages) + { + if(mode == language_info->id()) + return *language_info; + } + + INVARIANT(false, "unregistered language `" + id2string(mode) + "'"); +} + /// Get the mode of the given identifier's symbol /// \param ns: a namespace /// \param identifier: an identifier @@ -72,10 +92,30 @@ get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier) return symbol->mode; } -/// Get the language corresponding to the mode of the given identifier's symbol +/// Get the language info corresponding to the mode of +/// the given identifier's symbol +/// \param ns: a namespace +/// \param identifier: an identifier +/// \return the corresponding language info if the mode is not `ID_unknown`, or +/// the default language otherwise; +/// Note: It is assumed as an invariant that languages of symbols in the symbol +/// table have been registered. +const language_infot &get_language_info_from_identifier( + const namespacet &ns, + const irep_idt &identifier) +{ + const irep_idt &mode = get_mode_from_identifier(ns, identifier); + if(mode == ID_unknown) + return get_default_language_info(); + + return get_language_info_from_mode(mode); +} + +/// Get the language corresponding to the mode of +/// the given identifier's symbol /// \param ns: a namespace /// \param identifier: an identifier -/// \return the corresponding language if the mode is not `ID_unknown`, or +/// \return the corresponding language info if the mode is not `ID_unknown`, or /// the default language otherwise; /// Note: It is assumed as an invariant that languages of symbols in the symbol /// table have been registered. @@ -86,12 +126,7 @@ get_language_from_identifier(const namespacet &ns, const irep_idt &identifier) if(mode == ID_unknown) return get_default_language(); - std::unique_ptr language = get_language_from_mode(mode); - INVARIANT( - language, - "symbol `" + id2string(identifier) + "' has unknown mode '" + - id2string(mode) + "'"); - return language; + return get_language_from_mode(mode); } /// Get the language corresponding to the registered file name extensions @@ -103,30 +138,27 @@ std::unique_ptr get_language_from_filename( { std::size_t ext_pos=filename.rfind('.'); - if(ext_pos==std::string::npos) + if(ext_pos == std::string::npos) return nullptr; - std::string extension= - std::string(filename, ext_pos+1, std::string::npos); + std::string file_extension = + std::string(filename, ext_pos + 1, std::string::npos); - if(extension=="") + if(file_extension.empty()) return nullptr; - for(languagest::const_iterator - l_it=languages.begin(); - l_it!=languages.end(); - l_it++) + for(const auto &language_info : languages) { + const auto &extensions = language_info->extensions(); #ifdef _WIN32 - for(std::set::const_iterator - e_it=l_it->extensions.begin(); - e_it!=l_it->extensions.end(); - e_it++) - if(_stricmp(extension.c_str(), e_it->c_str())==0) - return l_it->factory(); + for(const auto &language_extension : extensions) + { + if(_stricmp(file_extension.c_str(), language_extension.c_str()) == 0) + return language_info->new_language(); + } #else - if(l_it->extensions.find(extension)!=l_it->extensions.end()) - return l_it->factory(); + if(extensions.find(file_extension) != extensions.end()) + return language_info->new_language(); #endif } @@ -138,5 +170,14 @@ std::unique_ptr get_language_from_filename( std::unique_ptr get_default_language() { PRECONDITION(!languages.empty()); - return languages.front().factory(); + const auto &language_info = languages.front(); + return language_info->new_language(); +} + +/// Returns the default language info +/// \return the info of the first registered language +const language_infot &get_default_language_info() +{ + PRECONDITION(!languages.empty()); + return *languages.front(); } diff --git a/src/langapi/mode.h b/src/langapi/mode.h index 3223cf4a960..04b16b33fd5 100644 --- a/src/langapi/mode.h +++ b/src/langapi/mode.h @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #ifndef CPROVER_LANGAPI_MODE_H #define CPROVER_LANGAPI_MODE_H +#include + #include #include // unique_ptr @@ -18,15 +20,26 @@ class languaget; class namespacet; std::unique_ptr get_language_from_mode(const irep_idt &mode); + +const language_infot &get_language_info_from_mode(const irep_idt &mode); + const irep_idt & get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier); + +const language_infot &get_language_info_from_identifier( + const namespacet &ns, + const irep_idt &identifier); + std::unique_ptr get_language_from_identifier(const namespacet &ns, const irep_idt &identifier); + std::unique_ptr get_language_from_filename( const std::string &filename); + std::unique_ptr get_default_language(); +const language_infot &get_default_language_info(); -typedef std::unique_ptr (*language_factoryt)(); -void register_language(language_factoryt factory); +void clear_languages(); +void register_language(language_info_factoryt); #endif // CPROVER_LANGAPI_MODE_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b0fac1ce788..f4422a7c2aa 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -667,6 +667,7 @@ IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation) IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation) IREP_ID_TWO(C_annotations, #annotations) +IREP_ID_ONE(jsil) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.h in their source tree and diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index aa8b63a0dc7..36320cd0134 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -249,11 +249,11 @@ json_objectt json( type; std::string type_string; - bool error=lang->from_type(underlying_type, type_string, ns); + bool error = lang->info.from_type(underlying_type, type_string, ns); CHECK_RETURN(!error); std::string value_string; - lang->from_expr(expr, value_string, ns); + lang->info.from_expr(expr, value_string, ns); const constant_exprt &constant_expr=to_constant_expr(expr); if(type.id()==ID_unsignedbv || diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 72da63050ae..7421f21c4cf 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -13,7 +13,10 @@ #include -#include +#include + +#include +#include #include #include @@ -64,9 +67,11 @@ bool constant_simplification_mockt::ai_simplify( SCENARIO("ai_domain_baset::ai_simplify_lhs", "[core][analyses][ai][ai_simplify_lhs]") { + clear_languages(); + register_language(new_ansi_c_language_info); + auto language = get_language_from_mode(ID_C); ui_message_handlert message_handler; - ansi_c_languaget language; - language.set_message_handler(message_handler); + language->set_message_handler(message_handler); symbol_tablet symbol_table; namespacet ns(symbol_table); @@ -79,8 +84,8 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", { // Construct an expression that the simplify_expr can simplify exprt simplifiable_expression; - bool compile_failed= - language.to_expr("1 + 1", "", simplifiable_expression, ns); + bool compile_failed = + language->to_expr("1 + 1", "", simplifiable_expression, ns); const unsigned int array_size=5; array_typet array_type( diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp index 6a499be1a76..f6270deff9e 100644 --- a/unit/analyses/dependence_graph.cpp +++ b/unit/analyses/dependence_graph.cpp @@ -9,14 +9,19 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include + #include -#include -#include -#include + #include +#include +#include +#include + #include + #include -#include + +#include static symbolt create_void_function_symbol( const irep_idt &name, @@ -57,7 +62,8 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]") // } // void b() { } - register_language(new_java_bytecode_language); + clear_languages(); + register_language(new_java_bytecode_language_info); goto_modelt goto_model; namespacet ns(goto_model.symbol_table); diff --git a/unit/goto-programs/class_hierarchy_output.cpp b/unit/goto-programs/class_hierarchy_output.cpp index 3cd6c751a14..bbf15885300 100644 --- a/unit/goto-programs/class_hierarchy_output.cpp +++ b/unit/goto-programs/class_hierarchy_output.cpp @@ -11,6 +11,10 @@ #include +#include + +#include + #include #include @@ -39,6 +43,9 @@ SCENARIO( "Output a simple class hierarchy" "[core][goto-programs][class_hierarchy]") { + clear_languages(); + register_language(new_java_bytecode_language_info); + symbol_tablet symbol_table = load_java_class("HierarchyTest", "goto-programs/"); class_hierarchyt hierarchy; diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 31071dace29..3ee35e76ce7 100644 --- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -7,16 +7,20 @@ \*******************************************************************/ +#include + #include + #include -#include #include +#include + +#include #include -#include #include + #include #include -#include SCENARIO( "Generate string object", @@ -26,7 +30,8 @@ SCENARIO( { source_locationt loc; symbol_tablet symbol_table; - register_language(new_java_bytecode_language); + clear_languages(); + register_language(new_java_bytecode_language_info); // Add java.lang.Object to symbol table symbolt jlo_sym; diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp index fb65105afbb..8c5db39ddc7 100644 --- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp +++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -7,15 +7,17 @@ \*******************************************************************/ +#include + +#include +#include +#include +#include #include #include #include -#include -#include -#include -#include #include -#include +#include refined_string_exprt convert_exprt_to_string_exprt_unit_test( java_string_library_preprocesst &preprocess, @@ -55,7 +57,8 @@ TEST_CASE("Convert exprt to string exprt") THEN("Code is produced") { - register_language(new_java_bytecode_language); + clear_languages(); + register_language(new_java_bytecode_language_info); std::vector code_string; const std::regex spaces("\\s+"); diff --git a/unit/pointer-analysis/custom_value_set_analysis.cpp b/unit/pointer-analysis/custom_value_set_analysis.cpp index 01791c36528..98a0add4d25 100644 --- a/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -10,7 +10,7 @@ Author: Chris Smowton, chris@smowton.net #include #include -#include +#include #include #include #include @@ -179,7 +179,8 @@ SCENARIO("test_value_set_analysis", config.java.classpath={"."}; command_line.args.push_back("pointer-analysis/CustomVSATest.jar"); - register_language(new_java_bytecode_language); + clear_languages(); + register_language(new_java_bytecode_language_info); goto_modelt goto_model= initialize_goto_model(command_line, null_output); diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 7e6773e50c0..e15839814a1 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -8,9 +8,9 @@ #include -#include -#include +#include #include +#include #include #include @@ -18,8 +18,9 @@ #include #include -#include #include +#include +#include /// \class Types used throughout the test. Currently it is impossible to /// statically initialize this value, there is a PR to allow this @@ -136,7 +137,7 @@ std::string create_info(std::vector &lemmas, const namespacet &ns) { simplify(lemma, ns); std::string lemma_string; - get_language_from_mode(ID_java)->from_expr(lemma, lemma_string, ns); + get_language_info_from_mode(ID_java).from_expr(lemma, lemma_string, ns); new_lemmas += lemma_string + "\n\n"; } return "Instantiated lemmas:\n"+new_lemmas; @@ -164,8 +165,9 @@ SCENARIO("instantiate_not_contains", "[!mayfail][core][solvers][refinement][string_constraint_instantiation]") { // For printing expression - register_language(new_java_bytecode_language); - std::unique_ptr java_lang = get_language_from_mode(ID_java); + clear_languages(); + register_language(new_java_bytecode_language_info); + const auto &java_lang_info = get_language_info_from_mode(ID_java); symbol_tablet symtbl; const namespacet ns(symtbl); @@ -208,7 +210,7 @@ SCENARIO("instantiate_not_contains", [&](const std::string &accu, string_constraintt sc) { simplify(sc, ns); std::string s; - java_lang->from_expr(sc, s, ns); + java_lang_info.from_expr(sc, s, ns); return accu + s + "\n\n"; }); @@ -222,7 +224,7 @@ SCENARIO("instantiate_not_contains", generator.witness[sc] = generator.fresh_symbol("w", t.witness_type()); nc_axioms.push_back(sc); std::string s; - java_lang->from_expr(sc, s, ns); + java_lang_info.from_expr(sc, s, ns); return accu + s + "\n\n"; }); @@ -234,7 +236,7 @@ SCENARIO("instantiate_not_contains", [&](const std::string &accu, exprt axiom) { simplify(axiom, ns); std::string s; - java_lang->from_expr(axiom, s, ns); + java_lang_info.from_expr(axiom, s, ns); return accu + s + "\n\n"; }); @@ -301,7 +303,7 @@ SCENARIO("instantiate_not_contains", INFO("Original axiom:\n"); std::string s; - java_lang->from_expr(vacuous, s, ns); + java_lang_info.from_expr(vacuous, s, ns); INFO(s + "\n\n"); WHEN("we instantiate and simplify") @@ -356,7 +358,7 @@ SCENARIO("instantiate_not_contains", INFO("Original axiom:\n"); std::string s; - java_lang->from_expr(trivial, s, ns); + java_lang_info.from_expr(trivial, s, ns); INFO(s + "\n\n"); WHEN("we instantiate and simplify") @@ -412,7 +414,7 @@ SCENARIO("instantiate_not_contains", INFO("Original axiom:\n"); std::string s; - java_lang->from_expr(trivial, s, ns); + java_lang_info.from_expr(trivial, s, ns); INFO(s + "\n\n"); WHEN("we instantiate and simplify") @@ -471,7 +473,7 @@ SCENARIO("instantiate_not_contains", INFO("Original axiom:\n"); std::string s; - java_lang->from_expr(trivial, s, ns); + java_lang_info.from_expr(trivial, s, ns); INFO(s + "\n\n"); WHEN("we instantiate and simplify") @@ -527,7 +529,7 @@ SCENARIO("instantiate_not_contains", INFO("Original axiom:\n"); std::string s; - java_lang->from_expr(trivial, s, ns); + java_lang_info.from_expr(trivial, s, ns); INFO(s + "\n\n"); WHEN("we instantiate and simplify") diff --git a/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/unit/solvers/refinement/string_refinement/dependency_graph.cpp index de6bd2d69e6..d93a055edfb 100644 --- a/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -102,6 +102,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") #ifdef DEBUG // useful output for visualizing the graph { + clear_languages(); register_language(new_java_bytecode_language); symbol_tablet symbol_table; namespacet ns(symbol_table); diff --git a/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp index e7b6eb22478..e209659a54f 100644 --- a/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp +++ b/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp @@ -9,20 +9,21 @@ #include +#include +#include +#include +#include #include #include #include -#include #include -#include -#include -#include SCENARIO("string_identifiers_resolution_from_equations", "[core][solvers][refinement][string_refinement]") { // For printing expression - register_language(new_java_bytecode_language); + clear_languages(); + register_language(new_java_bytecode_language_info); symbol_tablet symbol_table; namespacet ns(symbol_table); messaget::mstreamt &stream = messaget().debug(); diff --git a/unit/testing-utils/c_to_expr.cpp b/unit/testing-utils/c_to_expr.cpp index 3c1dff6a7c2..7fc82feb0e8 100644 --- a/unit/testing-utils/c_to_expr.cpp +++ b/unit/testing-utils/c_to_expr.cpp @@ -12,13 +12,16 @@ /// #include "c_to_expr.h" +#include +#include #include c_to_exprt::c_to_exprt(): message_handler( std::unique_ptr(new ui_message_handlert())) { - language.set_message_handler(*message_handler); + language = get_language_from_mode(ID_C); + language->set_message_handler(*message_handler); } /// Take an input string that should be a valid C rhs expression @@ -29,7 +32,7 @@ exprt c_to_exprt::operator()( const std::string &input_string, const namespacet &ns) { exprt expr; - bool result=language.to_expr(input_string, "", expr, ns); + bool result = language->to_expr(input_string, "", expr, ns); REQUIRE(!result); return expr; } diff --git a/unit/testing-utils/c_to_expr.h b/unit/testing-utils/c_to_expr.h index 3c8a81c5bac..7149e53090e 100644 --- a/unit/testing-utils/c_to_expr.h +++ b/unit/testing-utils/c_to_expr.h @@ -15,11 +15,11 @@ #include +#include #include #include -#include #include -#include +#include class c_to_exprt { @@ -29,7 +29,7 @@ class c_to_exprt private: std::unique_ptr message_handler; - ansi_c_languaget language; + std::unique_ptr language; }; #endif // CPROVER_TESTING_UTILS_C_TO_EXPR_H diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index 217a3bb25d7..c22bd88a8c3 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -18,7 +18,6 @@ #include -#include #include /// Go through the process of loading, type-checking and finalising loading a @@ -39,13 +38,10 @@ symbol_tablet load_java_class_lazy( free_form_cmdlinet lazy_command_line; lazy_command_line.add_flag("lazy-methods"); - register_language(new_java_bytecode_language); - return load_java_class( java_class_name, class_path, main, - get_language_from_mode(ID_java), lazy_command_line); } @@ -63,10 +59,8 @@ symbol_tablet load_java_class( const std::string &class_path, const std::string &main) { - register_language(new_java_bytecode_language); - - return load_java_class( - java_class_name, class_path, main, get_language_from_mode(ID_java)); + cmdlinet cmdline; + return load_java_class(java_class_name, class_path, main, cmdline); } /// Go through the process of loading, type-checking and finalising loading a @@ -77,14 +71,11 @@ symbol_tablet load_java_class( /// the unit directory. /// \param main: The name of the main function or "" to use the default /// behaviour to find a main function. -/// \param java_lang: The language implementation to use for the loading, -/// which will be destroyed by this function. /// \return The symbol table that is generated by parsing this file. symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, const std::string &main, - std::unique_ptr &&java_lang, const cmdlinet &command_line) { // We expect the name of the class without the .class suffix to allow us to @@ -106,7 +97,7 @@ symbol_tablet load_java_class( // Add the language to the model language_filet &lf=lazy_goto_model.add_language_file(filename); - lf.language=std::move(java_lang); + lf.language = get_language_from_mode(ID_java); languaget &language=*lf.language; std::istringstream java_code_stream("ignored"); @@ -147,19 +138,3 @@ symbol_tablet load_java_class( REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); return std::move(maybe_goto_model->symbol_table); } - -symbol_tablet load_java_class( - const std::string &java_class_name, - const std::string &class_path, - const std::string &main, - std::unique_ptr &&java_lang) -{ - cmdlinet command_line; - // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an - // TODO(tkiley): unknown argument. This could be changed by using the - // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail. - // TODO(tkiley): TG-2708 to investigate and fix - command_line.set("java-cp-include-files", class_path); - return load_java_class( - java_class_name, class_path, main, std::move(java_lang), command_line); -} diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index 0a29a2304aa..630c4526f71 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -29,13 +29,6 @@ symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, const std::string &main, - std::unique_ptr &&java_lang); - -symbol_tablet load_java_class( - const std::string &java_class_name, - const std::string &class_path, - const std::string &main, - std::unique_ptr &&java_lang, const cmdlinet &command_line); symbol_tablet load_java_class_lazy( From 17e13259a180cf0247cbe39f1b443638ab5cf1dc Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 7 May 2018 16:48:38 +0200 Subject: [PATCH 2/2] Remove conditional inclusion of JSIL --- src/cbmc/CMakeLists.txt | 2 +- src/cbmc/Makefile | 9 +++------ src/cbmc/cbmc_languages.cpp | 6 ------ src/goto-analyzer/CMakeLists.txt | 2 +- src/goto-analyzer/Makefile | 9 +++------ src/goto-cc/Makefile | 9 +++------ src/goto-diff/CMakeLists.txt | 1 - 7 files changed, 11 insertions(+), 27 deletions(-) diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index b1cae0f8b01..d1fed79bde9 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -16,6 +16,7 @@ target_link_libraries(cbmc-lib goto-instrument-lib goto-programs goto-symex + jsil json langapi linking @@ -26,7 +27,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 9da2d96efc2..c94fc2c5677 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -49,7 +49,9 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../json/json$(LIBEXT) + ../json/json$(LIBEXT) \ + ../jsil/jsil$(LIBEXT) \ + # Empty last line INCLUDES= -I .. @@ -67,11 +69,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 c76324261d1..974de68206f 100644 --- a/src/cbmc/cbmc_languages.cpp +++ b/src/cbmc/cbmc_languages.cpp @@ -15,17 +15,11 @@ 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_info); register_language(new_cpp_language_info); - - #ifdef HAVE_JSIL register_language(new_jsil_language_info); - #endif } diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt index 354069d913a..cd471f7744b 100644 --- a/src/goto-analyzer/CMakeLists.txt +++ b/src/goto-analyzer/CMakeLists.txt @@ -16,13 +16,13 @@ target_link_libraries(goto-analyzer-lib analyses pointer-analysis langapi + jsil json assembler util ) add_if_library(goto-analyzer-lib java_bytecode) -add_if_library(goto-analyzer-lib jsil) # Executable add_executable(goto-analyzer goto_analyzer_main.cpp) diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 1be5be97dc7..152318034bb 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -20,7 +20,9 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../json/json$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../jsil/jsil$(LIBEXT) \ + # Empty last line INCLUDES= -I .. @@ -33,11 +35,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-cc/Makefile b/src/goto-cc/Makefile index 6874910fbcc..ba2e7ccc15b 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -28,7 +28,9 @@ OBJ += ../big-int/big-int$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../miniz/miniz$(OBJEXT) \ - ../json/json$(LIBEXT) + ../json/json$(LIBEXT) \ + ../jsil/jsil$(LIBEXT) \ + # Empty last line INCLUDES= -I .. @@ -44,11 +46,6 @@ all: goto-cl$(EXEEXT) endif all: goto-cc$(EXEEXT) -ifneq ($(wildcard ../jsil/Makefile),) - OBJ += ../jsil/jsil$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JSIL -endif - ############################################################################### goto-cc$(EXEEXT): $(OBJ) diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index ebaec4b3b99..263bb890e05 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -24,7 +24,6 @@ target_link_libraries(goto-diff-lib ) add_if_library(goto-diff-lib java_bytecode) -add_if_library(goto-diff-lib jsil) # Executable add_executable(goto-diff goto_diff_main.cpp)