language.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Abstract interface to support a programming language
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_LANGAPI_LANGUAGE_H
#define CPROVER_LANGAPI_LANGUAGE_H
 
#include <util/invariant.h>
#include <util/irep.h>
 
#include <iosfwd>
#include <memory> // unique_ptr
#include <set>
#include <string>
#include <unordered_set>
 
class exprt;
class message_handlert;
class namespacet;
class optionst;
class symbol_table_baset;
class typet;
 
#define OPT_FUNCTIONS \
  "(function):"
 
#define HELP_FUNCTIONS " {y--function} {uname} \t set main function name\n"
 
class languaget
{
public:
  virtual void set_language_options(const optionst &, message_handlert &)
  {
  }
 
  // parse file
 
  virtual bool preprocess(
    std::istream &instream,
    const std::string &path,
    std::ostream &outstream,
    message_handlert &)
  {
    // unused parameters
    (void)instream;
    (void)path;
    (void)outstream;
    return false;
  }
 
  virtual bool parse(
    std::istream &instream,
    const std::string &path,
    message_handlert &message_handler) = 0;
 
  virtual bool generate_support_functions(
    symbol_table_baset &symbol_table,
    message_handlert &message_handler) = 0;
 
  // add external dependencies of a given module to set
 
  virtual void dependencies(
    const std::string &module,
    std::set<std::string> &modules);
 
  // add modules provided by currently parsed file to set
 
  virtual void modules_provided(std::set<std::string> &modules)
  {
    (void)modules; // unused parameter
  }
 
  virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
  {
    (void)methods; // unused parameter
  }
 
  virtual void convert_lazy_method(
    const irep_idt &function_id,
    symbol_table_baset &symbol_table,
    message_handlert &message_handler)
  {
    // unused parameters
    (void)function_id;
    (void)symbol_table;
    (void)message_handler;
  }
 
  virtual bool final(symbol_table_baset &symbol_table);
 
  // type check interfaces of currently parsed file
 
  virtual bool interfaces(
    symbol_table_baset &symbol_table,
    message_handlert &message_handler);
 
  // type check a module in the currently parsed file
 
  virtual bool typecheck(
    symbol_table_baset &symbol_table,
    const std::string &module,
    message_handlert &message_handler) = 0;
 
  virtual bool can_keep_file_local()
  {
    return false;
  }
 
  virtual bool typecheck(
    symbol_table_baset &symbol_table,
    const std::string &module,
    message_handlert &message_handler,
    const bool keep_file_local)
  {
    INVARIANT(
      false,
      "three-argument typecheck should only be called for files written"
      " in a language that allows file-local symbols, like C");
  }
 
  // language id / description
 
  virtual std::string id() const = 0;
  virtual std::string description() const = 0;
  virtual std::set<std::string> extensions() const = 0;
 
  // show parse tree
 
  virtual void
  show_parse(std::ostream &out, message_handlert &message_handler) = 0;
 
  // conversion of expressions
 
  virtual bool from_expr(
    const exprt &expr,
    std::string &code,
    const namespacet &ns);
 
  virtual bool from_type(
    const typet &type,
    std::string &code,
    const namespacet &ns);
 
  virtual bool type_to_name(
    const typet &type,
    std::string &name,
    const namespacet &ns);
 
  virtual bool to_expr(
    const std::string &code,
    const std::string &module,
    exprt &expr,
    const namespacet &ns,
    message_handlert &message_handler) = 0;
 
  virtual std::unique_ptr<languaget> new_language()=0;
 
  // constructor / destructor
 
  languaget() { }
  virtual ~languaget() { }
};
 
#endif // CPROVER_UTIL_LANGUAGE_H