jimple_ast.h

Go to the documentation of this file.

#ifndef ESBMC_JIMPLE_AST_H
#define ESBMC_JIMPLE_AST_H
 
#include <irep2/irep2_type.h>
#include <util/irep/expr.h>
#include <util/symtab/context.h>
#include <util/irep/std_types.h>
#include <util/lang/c_types.h>
#include <util/message/message.h>
#include <nlohmann/json.hpp>
 
// For json parsing
using json = nlohmann::json;

class jimple_ast
{
public:
  void dump() const
  {
    log_debug("jimple", "{}", this->to_string());
  }

  virtual void from_json(const json &) = 0;

  virtual std::string to_string() const = 0;
 
protected:
  static symbolt create_jimple_symbolt(
    const type2tc &t,
    const std::string &module,
    const std::string &name,
    const std::string &id,
    const std::string function_name = "")
  {
    symbolt symbol;
    symbol.mode = "C";
    symbol.module = module;
    symbol.location = std::move(get_location(module, function_name));
    symbol.set_type(t);
    symbol.name = name;
    symbol.id = id;
    return symbol;
  }

  static symbolt get_temp_symbol(
    const type2tc &t,
    const std::string &class_name,
    const std::string &function_name)
  {
    static unsigned int counter = 0;
 
    std::string id, name;
    id = get_symbol_name(
      class_name,
      function_name,
      "return_value$tmp$" + std::to_string(counter++));
    name = "return_value$tmp$";
    name += counter;
    auto tmp_symbol =
      create_jimple_symbolt(t, class_name, name, id, function_name);
 
    tmp_symbol.lvalue = true;
    tmp_symbol.static_lifetime = false;
    tmp_symbol.is_extern = false;
    tmp_symbol.file_local = true;
    return tmp_symbol;
  }

  static symbolt get_allocation_function()
  {
    std::string allocation_function = "malloc";
    symbolt symbol;
    symbol.mode = "C";
    symbol.set_type(code_type2tc(
      std::vector<type2tc>{uint_type2()},
      pointer_type2tc(get_empty_type()),
      std::vector<irep_idt>{irep_idt()},
      /*ellipsis=*/false));
    symbol.name = allocation_function;
    symbol.id = allocation_function;
    symbol.is_extern = false;
    symbol.file_local = false;
    return symbol;
  }

  static symbolt get_lengthof_function()
  {
    std::string func = "__ESBMC_get_object_size";
    symbolt symbol;
    symbol.mode = "C";
    symbol.set_type(code_type2tc(
      std::vector<type2tc>{pointer_type2tc(get_empty_type())},
      uint_type2(),
      std::vector<irep_idt>{irep_idt()},
      /*ellipsis=*/false));
    symbol.name = func;
    symbol.id = func;
    symbol.is_extern = false;
    symbol.file_local = false;
    return symbol;
  }

  static std::string
  get_method_name(std::string class_name, std::string function_name)
  {
    std::ostringstream oss;
    oss << class_name << ":" << function_name;
    return oss.str();
  }

  static std::string get_symbol_name(
    std::string class_name,
    std::string function_name,
    std::string symbol)
  {
    std::ostringstream oss;
    oss << get_method_name(class_name, function_name) << "@" << symbol;
    return oss.str();
  }

  static locationt
  get_location(const std::string &module, const std::string function_name = "")
  {
    locationt l;
    l.set_file(module + ".jimple");
    if (!function_name.empty())
      l.set_function(function_name);
    return l;
  }
 
public:
  int line_location = -1;
};
 
// These functions are used by nlohmann::json. Making it easier to
// parse the JSON file. Avoid using them directly.
void from_json(const json &j, jimple_ast &p);
void to_json(json &, const jimple_ast &);
#endif // ESBMC_JIMPLE_AST_H