havoc_utils.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Utilities for building havoc code for expressions.
 
Author: Saswat Padhi, saspadhi@amazon.com
 
Date: July 2021
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
#define CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H
 
#include <set>
 
#include <goto-programs/goto_program.h>
 
#include <util/expr_util.h>
 
typedef std::set<exprt> assignst;
 
class havoc_utils_is_constantt : public is_constantt
{
public:
  explicit havoc_utils_is_constantt(const assignst &mod) : assigns(mod)
  {
  }
 
  bool is_constant(const exprt &expr) const override
  {
    // Besides the "usual" constants (checked in is_constantt::is_constant),
    // we also treat unmodified symbols as constants
    if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end())
      return true;
 
    return is_constantt::is_constant(expr);
  }
 
protected:
  const assignst &assigns;
};
 
class havoc_utilst
{
public:
  explicit havoc_utilst(const assignst &mod) : assigns(mod), is_constant(mod)
  {
  }
 
  void append_full_havoc_code(
    const source_locationt location,
    goto_programt &dest) const;
 
  virtual void append_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest) const;
 
  virtual void append_object_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest) const;
 
  virtual void append_scalar_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest) const;
 
protected:
  const assignst &assigns;
  const havoc_utils_is_constantt is_constant;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H