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 <util/expr.h>
#include <util/expr_util.h>
 
#include <set>
 
class goto_programt;
 
typedef std::set<exprt> assignst;

class havoc_utils_can_forward_propagatet : public can_forward_propagatet
{
public:
  explicit havoc_utils_can_forward_propagatet(
    const assignst &mod,
    const namespacet &ns)
    : can_forward_propagatet(ns), assigns(mod)
  {
  }
 
  bool is_constant(const exprt &expr) const override
  {
    // Besides the "usual" constants (checked in
    // can_forward_propagatet::is_constant), we also treat unmodified symbols as
    // constants
    if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end())
      return true;
 
    return can_forward_propagatet::is_constant(expr);
  }
 
protected:
  const assignst &assigns;
};
 
class havoc_utilst
{
public:
  explicit havoc_utilst(const assignst &mod, const namespacet &ns)
    : assigns(mod), is_constant(mod, ns)
  {
  }

  void
  append_full_havoc_code(const source_locationt location, goto_programt &dest);

  virtual void append_havoc_code_for_expr(
    const source_locationt location,
    const exprt &expr,
    goto_programt &dest);

  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_can_forward_propagatet is_constant;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H