analyze_symbol.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbol Analyzer
 
Author: Malte Mues <mail.mues@gmail.com>
        Daniel Poetzl
 
\*******************************************************************/
 
 
#ifndef CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
#define CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
 
#include <map>
#include <string>
 
#include "gdb_api.h"
 
#include <ansi-c/expr2c_class.h>
 
#include <util/message.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
 
#include <goto-programs/allocate_objects.h>
 
class gdb_apit;
class exprt;
class source_locationt;
 
class gdb_value_extractort
{
public:
  gdb_value_extractort(
    const symbol_tablet &symbol_table,
    const std::vector<std::string> &args);
 
  void analyze_symbols(const std::list<std::string> &symbols);
 
  std::string get_snapshot_as_c_code();
 
  symbol_tablet get_snapshot_as_symbol_table();
 
  using pointer_valuet = gdb_apit::pointer_valuet;
  using memory_addresst = gdb_apit::memory_addresst;
 
  void create_gdb_process()
  {
    gdb_api.create_gdb_process();
  }
  bool run_gdb_to_breakpoint(const std::string &breakpoint)
  {
    return gdb_api.run_gdb_to_breakpoint(breakpoint);
  }
  void run_gdb_from_core(const std::string &corefile)
  {
    gdb_api.run_gdb_from_core(corefile);
  }
 
private:
  gdb_apit gdb_api;
 
  symbol_tablet symbol_table;
  const namespacet ns;
  expr2ct c_converter;
  allocate_objectst allocate_objects;
 
  std::map<exprt, exprt> assignments;
 
  std::map<exprt, memory_addresst> outstanding_assignments;
 
  std::map<memory_addresst, exprt> values;
 
  struct memory_scopet
  {
  private:
    size_t begin_int;
    mp_integer byte_size;
    irep_idt name;
 
    size_t address2size_t(const memory_addresst &point) const;
 
    bool check_containment(const size_t &point_int) const
    {
      return point_int >= begin_int && (begin_int + byte_size) > point_int;
    }
 
  public:
    memory_scopet(
      const memory_addresst &begin,
      const mp_integer &byte_size,
      const irep_idt &name);
 
    bool contains(const memory_addresst &point) const
    {
      return check_containment(address2size_t(point));
    }
 
    mp_integer
    distance(const memory_addresst &point, mp_integer member_size) const;
 
    irep_idt id() const
    {
      return name;
    }
 
    mp_integer size() const
    {
      return byte_size;
    }
  };
 
  std::vector<memory_scopet> dynamically_allocated;
 
  std::map<irep_idt, pointer_valuet> memory_map;
 
  bool has_known_memory_location(const irep_idt &id) const
  {
    return memory_map.count(id) != 0;
  }
 
  std::vector<memory_scopet>::iterator find_dynamic_allocation(irep_idt name);
 
  std::vector<memory_scopet>::iterator
  find_dynamic_allocation(const memory_addresst &point);
 
  mp_integer get_malloc_size(irep_idt name);
 
  optionalt<std::string>
  get_malloc_pointee(const memory_addresst &point, mp_integer member_size);
 
  mp_integer get_type_size(const typet &type) const;
 
  void analyze_symbol(const irep_idt &symbol_name);
 
  void add_assignment(const exprt &lhs, const exprt &value);
 
  exprt get_array_value(
    const exprt &expr,
    const exprt &array,
    const source_locationt &location);
 
  exprt get_expr_value(
    const exprt &expr,
    const exprt &zero_expr,
    const source_locationt &location);
 
  exprt get_struct_value(
    const exprt &expr,
    const exprt &zero_expr,
    const source_locationt &location);
 
  exprt get_union_value(
    const exprt &expr,
    const exprt &zero_expr,
    const source_locationt &location);
 
  exprt get_pointer_value(
    const exprt &expr,
    const exprt &zero_expr,
    const source_locationt &location);
 
  exprt get_pointer_to_member_value(
    const exprt &expr,
    const pointer_valuet &pointer_value,
    const source_locationt &location);
 
  exprt get_non_char_pointer_value(
    const exprt &expr,
    const pointer_valuet &value,
    const source_locationt &location);
 
  exprt get_pointer_to_function_value(
    const exprt &expr,
    const pointer_valuet &pointer_value,
    const source_locationt &location);
 
  exprt get_char_pointer_value(
    const exprt &expr,
    const memory_addresst &memory_location,
    const source_locationt &location);
 
  void process_outstanding_assignments();
 
  std::string get_gdb_value(const exprt &expr);
 
  bool points_to_member(
    pointer_valuet &pointer_value,
    const pointer_typet &expected_type);
};
 
#endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H