diff --git a/src/Makefile b/src/Makefile index d570dbb641a..d28a2bdc976 100644 --- a/src/Makefile +++ b/src/Makefile @@ -25,6 +25,8 @@ languages: util.dir langapi.dir \ cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \ jsil.dir +solvers.dir: util.dir langapi.dir + goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \ goto-symex.dir linking.dir analyses.dir solvers.dir \ json.dir diff --git a/src/langapi/language.h b/src/langapi/language.h index a3b6cbc0206..9e35daa17c9 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -114,21 +114,42 @@ class languaget:public messaget // 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 + /// \param expr: the parsed expression + /// \param ns: a namespace + /// \return false if the conversion succeeds virtual bool to_expr( const std::string &code, const std::string &module, diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 7a2e691af38..87c51c9877f 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -17,32 +17,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "language.h" #include "mode.h" -static std::unique_ptr get_language( - const namespacet &ns, - const irep_idt &identifier) -{ - const symbolt *symbol; - - if(identifier=="" || - ns.lookup(identifier, symbol) || - symbol->mode=="") - return get_default_language(); - - std::unique_ptr ptr=get_language_from_mode(symbol->mode); - - if(ptr==nullptr) - throw "symbol `"+id2string(symbol->name)+ - "' has unknown mode '"+id2string(symbol->mode)+"'"; - - return ptr; -} - std::string from_expr( const namespacet &ns, const irep_idt &identifier, const exprt &expr) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p(get_language_from_identifier(ns, identifier)); std::string result; p->from_expr(expr, result, ns); @@ -55,7 +35,7 @@ std::string from_type( const irep_idt &identifier, const typet &type) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p(get_language_from_identifier(ns, identifier)); std::string result; p->from_type(type, result, ns); @@ -68,7 +48,7 @@ std::string type_to_name( const irep_idt &identifier, const typet &type) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p(get_language_from_identifier(ns, identifier)); std::string result; p->type_to_name(type, result, ns); @@ -93,7 +73,7 @@ exprt to_expr( const irep_idt &identifier, const std::string &src) { - std::unique_ptr p(get_language(ns, identifier)); + std::unique_ptr p(get_language_from_identifier(ns, identifier)); null_message_handlert null_message_handler; p->set_message_handler(null_message_handler); diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index dd12882c544..d2bc2474189 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -18,6 +18,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "language.h" +#include +#include + struct language_entryt { language_factoryt factory; @@ -28,6 +31,10 @@ struct language_entryt 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) { languages.push_back(language_entryt()); @@ -37,17 +44,60 @@ void register_language(language_factoryt factory) languages.back().mode=l->id(); } +/// Get the language corresponding to the given mode +/// \param mode: the mode, e.g. `ID_C` +/// \return the language or `nullptr` if the language has not been registered std::unique_ptr get_language_from_mode(const irep_idt &mode) { - for(languagest::const_iterator it=languages.begin(); - it!=languages.end(); - it++) - if(mode==it->mode) - return it->factory(); + for(const auto &language : languages) + if(mode == language.mode) + return language.factory(); return nullptr; } +/// Get the mode of the given identifier's symbol +/// \param ns: a namespace +/// \param identifier: an identifier +/// \return the mode, e.g. `ID_C`, if the identifier is in the given +/// symbol table, or `ID_unknown` otherwise +const irep_idt & +get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier) +{ + if(identifier.empty()) + return ID_unknown; + const symbolt *symbol; + if(ns.lookup(identifier, symbol)) + return ID_unknown; + return symbol->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 +/// the default language otherwise; +/// Note: It is assumed as an invariant that languages of symbols in the symbol +/// table have been registered. +std::unique_ptr +get_language_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(); + + std::unique_ptr language = get_language_from_mode(mode); + INVARIANT( + language, + "symbol `" + id2string(identifier) + "' has unknown mode '" + + id2string(mode) + "'"); + return language; +} + +/// Get the language corresponding to the registered file name extensions +/// \param filename: a filename +/// \return the corresponding language or `nullptr` if the extension cannot +/// be resolved to any registered language std::unique_ptr get_language_from_filename( const std::string &filename) { @@ -83,8 +133,10 @@ std::unique_ptr get_language_from_filename( return nullptr; } +/// Returns the default language +/// \return the first registered language std::unique_ptr get_default_language() { - assert(!languages.empty()); + PRECONDITION(!languages.empty()); return languages.front().factory(); } diff --git a/src/langapi/mode.h b/src/langapi/mode.h index 3edb7a30be8..3223cf4a960 100644 --- a/src/langapi/mode.h +++ b/src/langapi/mode.h @@ -15,8 +15,13 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include // unique_ptr class languaget; +class namespacet; std::unique_ptr get_language_from_mode(const irep_idt &mode); +const irep_idt & +get_mode_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();