jimple_expr.h

Go to the documentation of this file.

#include <jimple-frontend/AST/jimple_ast.h>
#include <util/irep/migrate.h>
#include <jimple-frontend/AST/jimple_type.h>
 
#pragma once

class jimple_expr : public jimple_ast
{
public:
  virtual exprt
  to_exprt(contextt &, const std::string &, const std::string &) const
  {
    exprt val("at_identifier");
    return val;
  };

  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const
  {
    expr2tc e;
    migrate_expr(to_exprt(ctx, class_name, function_name), e);
    return e;
  }

  static std::shared_ptr<jimple_expr> get_expression(const json &j);
 
protected:
  static expr2tc lower_invoke2t(
    contextt &ctx,
    const std::string &base_class,
    const std::string &method,
    const std::string &this_variable,
    const std::vector<std::shared_ptr<jimple_expr>> &parameters,
    const expr2tc &lhs,
    const std::string &class_name,
    const std::string &function_name);
};

class jimple_constant : public jimple_expr
{
public:
  jimple_constant() = default;
  explicit jimple_constant(const std::string &value) : value(value)
  {
  }
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return value;
  }
 
  virtual void setValue(const std::string &v)
  {
    value = v;
  }
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string value;
};

class jimple_symbol : public jimple_expr
{
public:
  jimple_symbol() = default;
  explicit jimple_symbol(std::string name) : var_name(name)
  {
  }
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return var_name;
  }
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  const std::string &getVarName() const
  {
    return var_name;
  }
 
protected:
  std::string var_name;
};

class jimple_binop : public jimple_expr
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple BinOP";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string binop;
  std::shared_ptr<jimple_expr> lhs;
  std::shared_ptr<jimple_expr> rhs;
};

class jimple_cast : public jimple_expr
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple Cast";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string var_name;
  std::shared_ptr<jimple_expr> from;
  std::shared_ptr<jimple_type> to;
};

class jimple_lengthof : public jimple_expr
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple Lengthof";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::shared_ptr<jimple_expr> from;
};

class jimple_newarray : public jimple_expr
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple New array";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::shared_ptr<jimple_type> type;
  std::shared_ptr<jimple_expr> size;
};

class jimple_expr_invoke : public jimple_expr
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple Invoke";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string base_class;
  std::string method;
  expr2tc lhs;
  std::vector<std::shared_ptr<jimple_expr>> parameters;
 
  void set_lhs(const expr2tc &expr)
  {
    lhs = expr;
  }
 
  bool is_nondet_call() const
  {
    return base_class == "org.sosy_lab.sv_benchmarks.Verifier";
  }
 
  bool is_intrinsic_method = false;
 
protected:
  // We need an unique name for each function
  std::string get_hash_name() const
  {
    return std::to_string(parameters.size());
  }
};

class jimple_virtual_invoke : public jimple_expr
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple Virtual Invoke";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string base_class;
  std::string method;
  expr2tc lhs;
  std::string variable;
  std::vector<std::shared_ptr<jimple_expr>> parameters;
 
  void set_lhs(const expr2tc &expr)
  {
    lhs = expr;
  }
 
  bool is_nondet_call() const
  {
    return base_class == "java.util.Random";
  }
 
protected:
  // We need an unique name for each function
  std::string get_hash_name() const
  {
    return std::to_string(parameters.size() + 1);
  }
};

class jimple_new : public jimple_newarray
{
public:
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple New";
  }
};

class jimple_deref : public jimple_expr
{
public:
  jimple_deref() = default;
  jimple_deref(
    std::shared_ptr<jimple_expr> index,
    std::shared_ptr<jimple_expr> base)
    : index(index), base(base)
  {
  }
  virtual void from_json(const json &j) override;
  virtual std::string to_string() const override
  {
    return "Jimple Deref";
  }
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::shared_ptr<jimple_expr> index;
  std::shared_ptr<jimple_expr> base;
};

class jimple_nondet : public jimple_expr
{
public:
  jimple_nondet() = default;
  explicit jimple_nondet(std::string mode) : mode(mode)
  {
  }
  virtual std::string to_string() const override
  {
    return "Jimple Nondet";
  }
  virtual void from_json(const json &) override
  {
    assert("This class shouldn't be used from Jimple directly");
    abort();
  }
 
  const std::string mode; // Int, char, long, etc... e.g. Random().nextInt()
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
};

class jimple_static_member : public jimple_expr
{
public:
  virtual std::string to_string() const override
  {
    return "Jimple Static Member";
  }
  virtual void from_json(const json &j) override;
 
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string from;
  std::string field;
  std::shared_ptr<jimple_type> type;
};

class jimple_virtual_member : public jimple_expr
{
public:
  virtual std::string to_string() const override
  {
    return "Jimple Virtual Member";
  }
  virtual void from_json(const json &j) override;
  virtual expr2tc to_expr2t(
    contextt &ctx,
    const std::string &class_name,
    const std::string &function_name) const override;
 
  std::string variable;
  std::string from;
  std::string field;
  std::shared_ptr<jimple_type> type;
};