andersen.h

Go to the documentation of this file.

#ifndef CPROVER_POINTER_ANALYSIS_ANDERSEN_H
#define CPROVER_POINTER_ANALYSIS_ANDERSEN_H
 
#include <optional>
#include <unordered_map>
#include <unordered_set>
#include <vector>
 
#include <goto-programs/goto_functions.h>
#include <irep2/irep2.h>
#include <pointer-analysis/value_sets.h>

class andersent : public value_setst
{
public:
  andersent();

  typedef unsigned node_id;

  static constexpr node_id TOP = 0;

  static constexpr const char *nondet_object_name = "andersen::nondet";

  static bool is_nondet_object(const expr2tc &object)
  {
    return is_symbol2t(object) &&
           to_symbol2t(object).thename == nondet_object_name;
  }

  enum class constraint_kindt
  {
    ADDRESS_OF, 
    COPY,       
    LOAD,       
    STORE       
  };
 
  struct constraintt
  {
    constraint_kindt kind;
    node_id lhs;
    node_id rhs;
  };


  node_id get_node(const expr2tc &e);

  void add_constraint(constraint_kindt kind, node_id lhs, node_id rhs);

  void points_to_top(node_id n);

  void solve();

  const std::unordered_set<node_id> &points_to(node_id n) const;

  bool may_point_to(node_id a, node_id b) const;



  void collect_constraints(const goto_functionst &goto_functions);



  void operator()(const goto_functionst &goto_functions);

  void get_values(locationt l, const expr2tc &expr, valuest &dest) override;

  void
  get_reference_set(locationt l, const expr2tc &expr, valuest &dest) override;

  bool has_location(locationt) const override
  {
    return solved;
  }

 
protected:
  std::vector<std::unordered_set<node_id>> pts;

  std::vector<constraintt> constraints;

  std::vector<std::unordered_set<node_id>> copy_edges;

  std::unordered_map<irep_idt, node_id, irep_id_hash> symbol_to_node;
  std::unordered_map<expr2tc, node_id, irep2_hash> expr_to_node;
  std::vector<expr2tc> node_to_expr; // reverse lookup

  unsigned tmp_count = 0;

  bool solved = false;

  bool everything_escapes = false;

  const node_id *find_node(const expr2tc &e) const;

  void ensure_node(node_id n);

  node_id fresh_node();

  bool join(node_id dst, node_id src);

  bool add_copy_edge(node_id from, node_id to);

  node_id allocation(const type2tc &type, unsigned loc);

  std::unordered_set<irep_idt, irep_id_hash> allocators;

  std::unordered_map<irep_idt, bool, irep_id_hash> reads_varargs;

  node_id unconstrained();

  node_id top_source();

  node_id return_node(const irep_idt &fn);

  node_id eval_rhs(const expr2tc &rhs, unsigned location_number);

  node_id eval_address_of(const address_of2t &rhs, unsigned location_number);
  std::optional<node_id>
  eval_sideeffect(const sideeffect2t &rhs, unsigned location_number);
  node_id
  eval_realloc(node_id fresh, const expr2tc &old, unsigned location_number);
  std::optional<node_id>
  eval_pointer_arithmetic(const expr2tc &rhs, unsigned location_number);
  node_id eval_branch(const if2t &rhs, unsigned location_number);
  node_id eval_value(const expr2tc &rhs, unsigned location_number);
  node_id eval_integer(const expr2tc &rhs, unsigned location_number);
  node_id eval_constant_aggregate(const expr2tc &rhs, unsigned location_number);

  void handle_assign(
    const expr2tc &lhs,
    const expr2tc &rhs,
    unsigned location_number);

  void assign_node(const expr2tc &lhs, node_id src, unsigned loc);

  void assign_top(const expr2tc &lhs, unsigned loc);

  void handle_other(const expr2tc &code, unsigned location_number);

  void handle_function_call(
    const code_function_call2t &call,
    const goto_functionst &goto_functions,
    unsigned location_number);

  struct indirect_callt
  {
    node_id function; 
    expr2tc ret;
    std::vector<expr2tc> arguments;
    unsigned location_number;
    std::set<irep_idt> bound; 
    bool widened = false;     
  };
 
  std::vector<indirect_callt> indirect_calls;

  bool resolve_indirect_calls(const goto_functionst &goto_functions);

  void bind_call(
    const irep_idt &callee_name,
    const goto_functiont &callee,
    const expr2tc &ret,
    const std::vector<expr2tc> &arguments,
    unsigned location_number);

  void widen_call(
    const expr2tc &ret,
    const std::vector<expr2tc> &arguments,
    unsigned location_number);

  void to_object_descriptors(node_id n, valuest &dest) const;
};
 
#endif // CPROVER_POINTER_ANALYSIS_ANDERSEN_H