From 907f90096e0f278bb4f0d9b3683fc422f30c9b10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Jan 2015 16:46:18 -0800
Subject: [PATCH] feat(kernel): add memory consumption checks at replace_fn and
 for_each_fn

---
 src/kernel/for_each_fn.cpp | 4 ++++
 src/kernel/replace_fn.cpp  | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index a858d2d9f..470ecf98b 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -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;
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index e424941b0..060046834 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -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);