stack_budget.h

Go to the documentation of this file.

#ifndef ESBMC_UTIL_STACK_BUDGET_H
#define ESBMC_UTIL_STACK_BUDGET_H
 
#include <cstddef>
#include <cstdint>

template <class Tag>
class stack_budget_guardt
{
public:
  stack_budget_guardt()
  {
    if (depth++ == 0)
      base = here();
  }
 
  ~stack_budget_guardt()
  {
    if (--depth == 0)
      base = 0;
  }
 
  stack_budget_guardt(const stack_budget_guardt &) = delete;
  stack_budget_guardt &operator=(const stack_budget_guardt &) = delete;

  std::ptrdiff_t bytes_used() const
  {
    // Direction is platform business, not ours -- take the magnitude.
    const std::uintptr_t now = here();
    return static_cast<std::ptrdiff_t>(now > base ? now - base : base - now);
  }
 
  bool exceeded(std::ptrdiff_t budget) const
  {
    return bytes_used() > budget;
  }
 
private:
  /* An integer, not a pointer: the address is only ever differenced, never
   * dereferenced, and storing it as a pointer to a local trips GCC's
   * -Wdangling-pointer even though the guard clears it on the way out. */
  std::uintptr_t here() const
  {
    return reinterpret_cast<std::uintptr_t>(&marker);
  }
 
  char marker;
  static thread_local std::uintptr_t base;
  static thread_local unsigned depth;
};
 
template <class Tag>
thread_local std::uintptr_t stack_budget_guardt<Tag>::base = 0;
template <class Tag>
thread_local unsigned stack_budget_guardt<Tag>::depth = 0;

constexpr std::ptrdiff_t default_stack_budget = 384L * 1024 * 1024;
 
#endif