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 <cstddef>
 
#include <util/nodiscard.h>
 
class exprt;
class ssa_exprt;
class namespacet;
class goto_symex_statet;
class symex_targett;
 
class field_sensitivityt
{
public:
  field_sensitivityt(std::size_t max_array_size, bool should_simplify)
    : max_field_sensitivity_array_size(max_array_size),
      should_simplify(should_simplify)
  {
  }
 
  void field_assignments(
    const namespacet &ns,
    goto_symex_statet &state,
    const ssa_exprt &lhs,
    const exprt &rhs,
    symex_targett &target,
    bool allow_pointer_unsoundness);
 
  NODISCARD
  exprt
  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
    const;
  exprt apply(
    const namespacet &ns,
    goto_symex_statet &state,
    ssa_exprt expr,
    bool write) const;
 
  exprt get_fields(
    const namespacet &ns,
    goto_symex_statet &state,
    const ssa_exprt &ssa_expr) const;
 
  bool is_divisible(const ssa_exprt &expr) const;
 
private:
  bool run_apply = true;
 
  const std::size_t max_field_sensitivity_array_size;
 
  const bool should_simplify;
 
  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);
 
  exprt simplify_opt(exprt e, const namespacet &ns) const;
};
 
#endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H