dereference.h

Go to the documentation of this file.

#ifndef CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
#define CPROVER_POINTER_ANALYSIS_DEREFERENCE_H
 
#include <pointer-analysis/value_sets.h>
#include <set>
#include <util/irep/expr.h>
#include <irep2/irep2_guard.h>
#include <util/symtab/namespace.h>
#include <util/config/options.h>


class dereference_callbackt
{
public:
  virtual ~dereference_callbackt() = default;

  virtual void dereference_failure(
    const std::string &property,
    const std::string &msg,
    const guard2tc &guard) = 0;
 
  virtual void dereference_assume(const guard2tc &guard) = 0;

  virtual void
  get_value_set(const expr2tc &expr, value_setst::valuest &value_set) = 0;

  virtual bool
  has_failed_symbol(const expr2tc &expr, const symbolt *&symbol) = 0;

  virtual void rename(expr2tc &expr [[maybe_unused]])
  {
  }
 
  struct internal_item
  {
    expr2tc object;
    expr2tc offset;
    expr2tc guard;
  };
 
  virtual void dump_internal_state(
    const std::list<struct internal_item> &data [[maybe_unused]])
  {
  }

  virtual bool is_live_variable(const expr2tc &sym) = 0;
};

class dereferencet
{
public:
  dereferencet(
    const namespacet &_ns,
    contextt &_new_context,
    const optionst &_options,
    dereference_callbackt &_dereference_callback)
    : ns(_ns),
      new_context(_new_context),
      options(_options),
      dereference_callback(_dereference_callback),
      block_assertions(false)
  {
    is_big_endian =
      (config.ansi_c.endianess == configt::ansi_ct::IS_BIG_ENDIAN);
  }
 
  virtual ~dereferencet() = default;

  struct modet
  {
    enum : unsigned
    {
      READ,     
      WRITE,    
      FREE,     
      INTERNAL, 
    } op : 2;

    unsigned unaligned : 1;
 
    /* Intentionally provide no comparison operators in order to avoid counter-
     * intuitive results when comparing, e.g., an unaligned mode with one of
     * the (!unaligned) dereferencet::(READ|WRITE|FREE|INTERNAL) constants.
     *
     * For that the below predicates exist. */
 
    friend bool is_read(const modet &m)
    {
      return m.op == READ;
    }
 
    friend bool is_write(const modet &m)
    {
      return m.op == WRITE;
    }
 
    friend bool is_free(const modet &m)
    {
      return m.op == FREE;
    }
 
    friend bool is_internal(const modet &m)
    {
      return m.op == INTERNAL;
    }
  };
 
  static const constexpr modet READ = {modet::READ, false};
  static const constexpr modet WRITE = {modet::WRITE, false};
  static const constexpr modet FREE = {modet::FREE, false};
  static const constexpr modet INTERNAL = {modet::INTERNAL, false};

  virtual void dereference_expr(expr2tc &expr, guard2tc &guard, modet mode);
 
  virtual expr2tc dereference(
    const expr2tc &dest,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    const expr2tc &extra_offset);

  bool has_dereference(const expr2tc &expr) const;

  static void reset_object_counter();
 
private:
  const namespacet &ns;
  contextt &new_context;
  const optionst &options;
  dereference_callbackt &dereference_callback;
  static thread_local unsigned invalid_counter;
  bool is_big_endian;
  std::list<dereference_callbackt::internal_item> internal_items;
  bool block_assertions;

  virtual void
  dereference_guard_expr(expr2tc &expr, guard2tc &guard, modet mode);

  virtual void
  dereference_addrof_expr(expr2tc &expr, guard2tc &guard, modet mode);

  virtual expr2tc dereference_expr_nonscalar(
    expr2tc &expr,
    guard2tc &guard,
    modet mode,
    const expr2tc &base);

  expr2tc
  resolve_nonscalar_if(const expr2tc &expr, guard2tc &guard, modet mode);

  void check_pointer_alignment(
    modet mode,
    const type2tc &type,
    const expr2tc &deref_expr,
    const guard2tc &guard,
    const expr2tc &what);

  expr2tc create_pointer_offset_bits(const expr2tc &deref_expr);

  bool dereference_type_compare(
    expr2tc &object,
    const type2tc &dereference_type) const;

  expr2tc make_failed_symbol(const type2tc &out_type);

  expr2tc build_reference_to(
    const expr2tc &what,
    modet mode,
    const expr2tc &deref_expr,
    const type2tc &type,
    const guard2tc &guard,
    const expr2tc &lexical_offset,
    expr2tc &pointer_guard);
 
  void deref_invalid_ptr(
    const expr2tc &deref_expr,
    const guard2tc &guard,
    modet mode,
    const expr2tc &resolved = expr2tc());
 
  static const expr2tc &get_symbol(const expr2tc &object);
  void bounds_check(
    const expr2tc &expr,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    const expr2tc &deref = expr2tc());
  void valid_check(const expr2tc &expr, const guard2tc &guard, modet mode);
  std::vector<expr2tc> extract_bytes(
    const expr2tc &object,
    unsigned int bytes,
    const expr2tc &offset) const;
  expr2tc stitch_together_from_byte_array(
    unsigned int num_bytes,
    const std::vector<expr2tc> &bytes);
  expr2tc stitch_together_from_byte_array(
    const type2tc &type,
    const expr2tc &byte_array,
    const expr2tc &offset_bits);
  void dereference_failure(
    const std::string &error_class,
    const std::string &error_name,
    const guard2tc &guard);
  void alignment_failure(const std::string &error_name, const guard2tc &guard);
 
  void bad_base_type_failure(
    const guard2tc &guard,
    const std::string &wants,
    const std::string &have);
 
  bool check_code_access(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode);
  void check_data_obj_access(
    const expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode);
  void check_alignment(
    BigInt minwidth,
    const expr2tc &offset,
    const guard2tc &guard,
    const expr2tc &object);
  BigInt object_base_alignment(const expr2tc &object) const;
  unsigned int static compute_num_bytes_to_extract(
    const expr2tc &offset,
    unsigned long num_bits);
  static expr2tc extract_bits_from_byte_array(
    const expr2tc &value,
    const expr2tc &offset,
    unsigned long num_bits);
 
public:
  void build_reference_rec(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    unsigned long alignment = 0);
 
private:
  void construct_from_const_offset(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type);
  void construct_from_dyn_offset(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type);
  void construct_from_const_struct_offset(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode);
  void construct_from_dyn_struct_offset(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    unsigned long alignment,
    modet mode,
    const expr2tc *failed_symbol = nullptr);
  void construct_from_multidir_array(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    unsigned long alignment,
    modet mode);
  void construct_struct_ref_from_const_offset_array(
    expr2tc &value,
    const expr2tc &offs,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    unsigned long alignment);
  void construct_struct_ref_from_const_offset(
    expr2tc &value,
    const expr2tc &offs,
    const type2tc &type,
    const guard2tc &guard,
    modet mode);
  void construct_struct_ref_from_dyn_offset(
    expr2tc &value,
    const expr2tc &offs,
    const type2tc &type,
    const guard2tc &guard,
    modet mode);
  void construct_struct_ref_from_dyn_offs_rec(
    const expr2tc &value,
    const expr2tc &offs,
    const type2tc &type,
    const guard2tc &guard,
    const expr2tc &accuml_guard,
    modet mode,
    std::list<std::pair<expr2tc, expr2tc>> &output);
  void construct_struct_ref_from_dyn_offs_members(
    const expr2tc &value,
    const expr2tc &offs,
    const type2tc &type,
    const guard2tc &guard,
    const expr2tc &accuml_guard,
    modet mode,
    std::list<std::pair<expr2tc, expr2tc>> &output);
  void construct_struct_member_from_byte_array(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode);
  void construct_from_array(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    unsigned long alignment = 0);
  bool construct_value_ref(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    unsigned long alignment);
  void construct_vector_ref(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    unsigned long alignment);
  void construct_array_ref(
    expr2tc &value,
    const expr2tc &offset,
    const type2tc &type,
    const guard2tc &guard,
    modet mode,
    unsigned long alignment);
  class quantifier_scopet;

  std::multiset<irep_idt> quantifier_bound_vars;
  unsigned opaque_binders = 0;

  bool mentions_bound_var(const expr2tc &expr) const;

  bool may_fold_index(const expr2tc &index) const;
 
public:
  void set_block_assertions(void)
  {
    block_assertions = true;
  }
 
  void clear_block_assertions(void)
  {
    block_assertions = false;
  }
};
 
#endif