gcse.h

Go to the documentation of this file.

#pragma once
 
// GCSE - Global Common Subexpression Elimination
 
#include <util/message/message.h>
#include <goto-programs/abstract-interpretation/ai.h>
#include <pointer-analysis/value_sets.h>
 
class cse_domaint : public ai_domain_baset
{
public:
  cse_domaint() = default;
 
  virtual void transform(
    goto_programt::const_targett from,
    goto_programt::const_targett to,
    ai_baset &ai,
    const namespacet &ns) override;
 
  virtual void output(std::ostream &out) const override;
 
  virtual void make_bottom() override
  {
    available_expressions.clear();
    bottom = true;
  }

  virtual void make_entry() override
  {
    available_expressions.clear();
    bottom = false;
  };
  virtual void make_top() override
  {
    // Theoretically there exists a TOP (all possible AE in the program).
    // In practice, there is no need for it.
    log_error("[CSE] Available Expressions does not implement make_top()");
    abort();
  };
 
  virtual bool is_bottom() const override
  {
    return bottom;
  }
  virtual bool is_top() const override
  {
    // Not needed
    return false;
  }
  virtual bool ai_simplify(expr2tc &, const namespacet &) const override
  {
    return false;
  }
 
public:
  bool merge(
    const cse_domaint &b,
    goto_programt::const_targett,
    goto_programt::const_targett);
  std::unordered_set<expr2tc, irep2_hash> available_expressions;

  bool bottom = true;
 
protected:
  void make_expression_available(const expr2tc &e);

  void havoc_expr(const expr2tc &e, const goto_programt::const_targett &);

  void havoc_symbol(const irep_idt &sym);

  void havoc_pointee(expr2tc ptr, const goto_programt::const_targett &);
 
  // Helper function to check whether `src` depends on `taint`
  bool should_remove_expr(const expr2tc &taint, const expr2tc &src) const;
  // Helper function to check whether `src` depends on symbol `sym`
  bool should_remove_expr(const irep_idt &sym, const expr2tc &src) const;
 
public:
  // TODO: clearly this shouldn't be here. The proper way is to create a new
  // Abstract Interpreter that contains a points-to analysis
  static std::shared_ptr<value_setst> vsa;
};
 
#include <goto-programs/goto_functions_algorithm.h>
class goto_cse : public goto_functions_algorithm
{
public:
  goto_cse(contextt &ns, std::shared_ptr<value_setst> &vsa)
    : goto_functions_algorithm(true), context(ns)
  {
    cse_domaint::vsa = vsa;
  }
 
  virtual bool runOnProgram(goto_functionst &) override;
  virtual bool
  runOnFunction(std::pair<const irep_idt, goto_functiont> &F) override;
 
  // TODO: we should have a method to convert an cse_symbol back to the original
  // expr for CE.
 
protected:
  ait<cse_domaint> available_expressions;
  contextt &context;
  expr2tc obtain_max_sub_expr(const expr2tc &e, const cse_domaint &state) const;
  void replace_max_sub_expr(
    expr2tc &e,
    const std::unordered_map<expr2tc, expr2tc, irep2_hash> &expr2symbol,
    const goto_programt::const_targett &to,
    std::unordered_set<expr2tc, irep2_hash> &matched_expressions) const;
  void replace_in_lvalue(
    expr2tc &lhs,
    const std::unordered_map<expr2tc, expr2tc, irep2_hash> &expr2symbol,
    const goto_programt::const_targett &to,
    std::unordered_set<expr2tc, irep2_hash> &matched_expressions) const;
 
  symbolt
  create_cse_symbol(const type2tc &t, const goto_programt::const_targett &to);
 
private:
  unsigned symbol_counter = 0;
  const std::string prefix = "__ESBMC_cse_symbol";
};