Language mode utils

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

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,

src/langapi/language_util.cpp

@@ -17,32 +17,12 @@ Author: Daniel Kroening, [email protected]
 #include "language.h"
 #include "mode.h"
 
-static std::unique_ptr<languaget> 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<languaget> 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<languaget> p(get_language(ns, identifier));
+  std::unique_ptr<languaget> 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<languaget> p(get_language(ns, identifier));
+  std::unique_ptr<languaget> 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<languaget> p(get_language(ns, identifier));
+  std::unique_ptr<languaget> 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<languaget> p(get_language(ns, identifier));
+  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
 
   null_message_handlert null_message_handler;
   p->set_message_handler(null_message_handler);

src/langapi/mode.cpp

@@ -18,6 +18,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "language.h"
 
+#include <util/invariant.h>
+#include <util/namespace.h>
+
 struct language_entryt
 {
   language_factoryt factory;
@@ -28,6 +31,10 @@ struct language_entryt
 typedef std::list<language_entryt> 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<languaget> 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<languaget>
+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<languaget> 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<languaget> get_language_from_filename(
   const std::string &filename)
 {
@@ -83,8 +133,10 @@ std::unique_ptr<languaget> get_language_from_filename(
   return nullptr;
 }
 
+/// Returns the default language
+/// \return the first registered language
 std::unique_ptr<languaget> get_default_language()
 {
-  assert(!languages.empty());
+  PRECONDITION(!languages.empty());
   return languages.front().factory();
 }

src/langapi/mode.h

@@ -15,8 +15,13 @@ Author: Daniel Kroening, [email protected]
 #include <memory> // unique_ptr
 
 class languaget;
+class namespacet;
 
 std::unique_ptr<languaget> 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<languaget>
+get_language_from_identifier(const namespacet &ns, const irep_idt &identifier);
 std::unique_ptr<languaget> get_language_from_filename(
   const std::string &filename);
 std::unique_ptr<languaget> get_default_language();