feat(kernel): add memory consumption checks at replace_fn and for_each_fn

This commit is contained in:
Leonardo de Moura 2015-01-15 16:46:18 -08:00
parent 8ab775bd6f
commit 907f90096e
2 changed files with 7 additions and 0 deletions

View file

@ -7,6 +7,8 @@ Author: Leonardo de Moura
#include <vector>
#include <utility>
#include "util/flet.h"
#include "util/memory.h"
#include "util/interrupt.h"
#include "kernel/for_each_fn.h"
#include "kernel/cache_stack.h"
@ -59,6 +61,8 @@ class for_each_fn {
begin_loop:
if (todo.empty())
break;
check_interrupted();
check_memory("expression traversal");
auto p = todo.back();
todo.pop_back();
expr const & e = p.first;

View file

@ -151,6 +151,7 @@ public:
while (!m_fs.empty()) {
begin_loop:
check_interrupted();
check_memory("replace");
frame & f = m_fs.back();
expr const & e = f.m_expr;
unsigned offset = f.m_offset;
@ -218,6 +219,8 @@ class replace_rec_fn {
return *r;
shared = true;
}
check_interrupted();
check_memory("replace");
if (optional<expr> r = m_f(e, offset)) {
return save_result(e, offset, *r, shared);