local_bitvector_analysis.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Field-insensitive, location-sensitive bitvector analysis
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
#define CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H
 
#include <util/expanding_vector.h>
#include <util/numbering.h>
 
#include "locals.h"
#include "dirty.h"
#include "local_cfg.h"
 
class local_bitvector_analysist
{
public:
  typedef goto_functionst::goto_functiont goto_functiont;
 
  local_bitvector_analysist(
    const goto_functiont &_goto_function,
    const namespacet &ns)
    : dirty(_goto_function),
      locals(_goto_function),
      cfg(_goto_function.body),
      ns(ns)
  {
    build();
  }
 
  void output(
    std::ostream &out,
    const goto_functiont &goto_function,
    const namespacet &ns) const;
 
  dirtyt dirty;
  localst locals;
  local_cfgt cfg;
 
  // categories of things one can point to
  struct flagst
  {
    flagst():bits(0)
    {
    }
 
    void clear()
    {
      bits=0;
    }
 
    // the bits for the "bitvector analysis"
    enum bitst
    {
      B_unknown=1<<0,
      B_uninitialized=1<<1,
      B_uses_offset=1<<2,
      B_dynamic_local=1<<3,
      B_dynamic_heap=1<<4,
      B_null=1<<5,
      B_static_lifetime=1<<6,
      B_integer_address=1<<7
    };
 
    explicit flagst(const bitst _bits):bits(_bits)
    {
    }
 
    unsigned bits;
 
    bool merge(const flagst &other)
    {
      unsigned old=bits;
      bits|=other.bits; // bit-wise or
      return old!=bits;
    }
 
    static flagst mk_unknown()
    {
      return flagst(B_unknown);
    }
 
    bool is_unknown() const
    {
      return (bits&B_unknown)!=0;
    }
 
    static flagst mk_uninitialized()
    {
      return flagst(B_uninitialized);
    }
 
    bool is_uninitialized() const
    {
      return (bits&B_uninitialized)!=0;
    }
 
    static flagst mk_uses_offset()
    {
      return flagst(B_uses_offset);
    }
 
    bool is_uses_offset() const
    {
      return (bits&B_uses_offset)!=0;
    }
 
    static flagst mk_dynamic_local()
    {
      return flagst(B_dynamic_local);
    }
 
    bool is_dynamic_local() const
    {
      return (bits&B_dynamic_local)!=0;
    }
 
    static flagst mk_dynamic_heap()
    {
      return flagst(B_dynamic_heap);
    }
 
    bool is_dynamic_heap() const
    {
      return (bits&B_dynamic_heap)!=0;
    }
 
    static flagst mk_null()
    {
      return flagst(B_null);
    }
 
    bool is_null() const
    {
      return (bits&B_null)!=0;
    }
 
    static flagst mk_static_lifetime()
    {
      return flagst(B_static_lifetime);
    }
 
    bool is_static_lifetime() const
    {
      return (bits&B_static_lifetime)!=0;
    }
 
    static flagst mk_integer_address()
    {
      return flagst(B_integer_address);
    }
 
    bool is_integer_address() const
    {
      return (bits&B_integer_address)!=0;
    }
 
    void print(std::ostream &) const;
 
    flagst operator|(const flagst other) const
    {
      flagst result(*this);
      result.bits|=other.bits;
      return result;
    }
  };
 
  flagst get(
    const goto_programt::const_targett t,
    const exprt &src);
 
protected:
  const namespacet &ns;
  void build();
 
  numberingt<irep_idt> pointers;
 
  // pointers -> flagst
  // This is a vector, so it's fast.
  typedef expanding_vectort<flagst> points_tot;
 
  static bool merge(points_tot &a, points_tot &b);
 
  typedef std::vector<points_tot> loc_infost;
  loc_infost loc_infos;
 
  void assign_lhs(
    const exprt &lhs,
    const exprt &rhs,
    points_tot &loc_info_src,
    points_tot &loc_info_dest);
 
  flagst get_rec(
    const exprt &rhs,
    points_tot &loc_info_src);
 
  bool is_tracked(const irep_idt &identifier);
};
 
inline std::ostream &operator<<(
  std::ostream &out,
  const local_bitvector_analysist::flagst &flags)
{
  flags.print(out);
  return out;
}
 
#endif // CPROVER_ANALYSES_LOCAL_BITVECTOR_ANALYSIS_H