shadow_memory_util.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symex Shadow Memory Instrumentation
 
Author: Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
#define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
 
#include <util/irep.h>
#include <util/message.h> // IWYU pragma: keep
 
#include "goto_symex_state.h" // IWYU pragma: keep
 
// To enable logging of Shadow Memory functions define DEBUG_SHADOW_MEMORY
 
class exprt;
class typet;
 
void shadow_memory_log_set_field(
  const namespacet &ns,
  const messaget &log,
  const irep_idt &field_name,
  const exprt &expr,
  const exprt &value);
 
void shadow_memory_log_value_set(
  const namespacet &ns,
  const messaget &log,
  const std::vector<exprt> &value_set);
 
void shadow_memory_log_get_field(
  const namespacet &ns,
  const messaget &log,
  const irep_idt &field_name,
  const exprt &expr);
 
void shadow_memory_log_value_set_match(
  const namespacet &ns,
  const messaget &log,
  const exprt &address,
  const exprt &expr);
 
void shadow_memory_log_text_and_expr(
  const namespacet &ns,
  const messaget &log,
  const char *text,
  const exprt &expr);
 
irep_idt extract_field_name(const exprt &string_expr);
 
void clean_pointer_expr(exprt &expr, const typet &type);
 
exprt deref_expr(const exprt &expr);
 
void replace_invalid_object_by_null(exprt &expr);
 
const exprt &
get_field_init_expr(const irep_idt &field_name, const goto_symex_statet &state);
 
std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
  const namespacet &ns,
  const messaget &log,
  const exprt &matched_object,
  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
  const typet &field_type,
  const exprt &expr,
  const typet &lhs_type,
  bool &exact_match);
 
const typet &
get_field_init_type(const irep_idt &field_name, const goto_symex_statet &state);
 
bool contains_null_or_invalid(
  const std::vector<exprt> &value_set,
  const exprt &address);
 
exprt compute_or_over_bytes(
  const exprt &expr,
  const typet &field_type,
  const namespacet &ns,
  const messaget &log,
  const bool is_union);
 
exprt compute_max_over_bytes(
  const exprt &expr,
  const typet &field_type,
  const namespacet &ns);
 
exprt build_if_else_expr(
  const std::vector<std::pair<exprt, exprt>> &conds_values);
 
bool check_value_set_contains_only_null_ptr(
  const namespacet &ns,
  const messaget &log,
  const std::vector<exprt> &value_set,
  const exprt &expr);
 
std::optional<exprt> get_shadow_memory(
  const exprt &expr,
  const std::vector<exprt> &value_set,
  const std::vector<shadow_memory_statet::shadowed_addresst> &addresses,
  const namespacet &ns,
  const messaget &log,
  size_t &mux_size);
 
#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H