field_sensitivity.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Field-sensitive SSA
 
Author: Michael Tautschnig
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
#define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 
#include <util/ssa_expr.h>
 
class byte_extract_exprt;
class namespacet;
class goto_symex_statet;
class symex_targett;
class value_sett;
 
class field_sensitive_ssa_exprt : public exprt
{
public:
  field_sensitive_ssa_exprt(const ssa_exprt &ssa, exprt::operandst &&fields)
    : exprt(ID_field_sensitive_ssa, ssa.type(), std::move(fields))
  {
    add(ID_expression, ssa);
  }
 
  const ssa_exprt &get_object_ssa() const
  {
    return static_cast<const ssa_exprt &>(find(ID_expression));
  }
};
 
template <>
inline bool can_cast_expr<field_sensitive_ssa_exprt>(const exprt &base)
{
  return base.id() == ID_field_sensitive_ssa;
}
 
inline const field_sensitive_ssa_exprt &
to_field_sensitive_ssa_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_field_sensitive_ssa);
  const field_sensitive_ssa_exprt &ret =
    static_cast<const field_sensitive_ssa_exprt &>(expr);
  return ret;
}
 
inline field_sensitive_ssa_exprt &to_field_sensitive_ssa_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_field_sensitive_ssa);
  field_sensitive_ssa_exprt &ret =
    static_cast<field_sensitive_ssa_exprt &>(expr);
  return ret;
}

class field_sensitivityt
{
public:
  field_sensitivityt(
    std::size_t max_array_size,
    bool should_simplify,
    const irep_idt &language_mode)
    : max_field_sensitivity_array_size(max_array_size),
      should_simplify(should_simplify),
      language_mode(language_mode)
  {
  }

  void field_assignments(
    const namespacet &ns,
    goto_symex_statet &state,
    const ssa_exprt &lhs,
    const exprt &rhs,
    symex_targett &target,
    bool allow_pointer_unsoundness) const;

  [[nodiscard]] exprt
  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
    const;
  [[nodiscard]] exprt apply(
    const namespacet &ns,
    goto_symex_statet &state,
    ssa_exprt expr,
    bool write) const;

  [[nodiscard]] exprt get_fields(
    const namespacet &ns,
    goto_symex_statet &state,
    const ssa_exprt &ssa_expr,
    bool disjoined_fields_only) const;

  [[nodiscard]] bool
  is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
 
private:
  const std::size_t max_field_sensitivity_array_size;
 
  const bool should_simplify;
  const irep_idt &language_mode;
 
  void field_assignments_rec(
    const namespacet &ns,
    goto_symex_statet &state,
    const exprt &lhs_fs,
    const exprt &ssa_rhs,
    symex_targett &target,
    bool allow_pointer_unsoundness) const;
 
  [[nodiscard]] exprt simplify_opt(
    exprt e,
    const value_sett &value_set,
    const namespacet &ns) const;

  [[nodiscard]] exprt apply_byte_extract(
    const namespacet &ns,
    goto_symex_statet &state,
    const byte_extract_exprt &expr,
    bool write) const;
};
 
#endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H