From a134a079b1dd40f3824bf12ddea1841416bc46a2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Dec 2015 10:18:51 -0800
Subject: [PATCH] ensure limit children are safe for race conditions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h           |  5 +--
 src/solver/solver.h                       | 12 ------
 src/tactic/aig/aig_tactic.cpp             |  1 +
 src/tactic/core/blast_term_ite_tactic.cpp |  8 +---
 src/util/rlimit.cpp                       | 48 +++++++++++++++++++----
 src/util/rlimit.h                         | 10 +++--
 6 files changed, 51 insertions(+), 33 deletions(-)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 05eebead2..9bfe47f46 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -576,10 +576,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
     SASSERT(!frame_stack().empty());
     while (!frame_stack().empty()) {
         if (m().canceled()) {
-            if (m().limit().cancel_flag_set()) {
-                throw rewriter_exception(Z3_CANCELED_MSG);
-            }
-            throw rewriter_exception(Z3_MAX_RESOURCE_MSG);
+            throw rewriter_exception(m().limit().get_cancel_msg());
         }
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
         frame & fr = frame_stack().back();
diff --git a/src/solver/solver.h b/src/solver/solver.h
index a53ea07ee..851aa2644 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -41,7 +41,6 @@ public:
      - parameter setting (updt_params)
      - statistics
      - results based on check_sat_result API
-     - interruption (set_cancel)
 */
 class solver : public check_sat_result {
 public:
@@ -105,14 +104,6 @@ public:
     */
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
 
-    /**
-       \brief Interrupt this solver.
-    */
-    //void cancel() { set_cancel(true); }
-    /**
-       \brief Reset the interruption.
-    */
-    //void reset_cancel() { set_cancel(false); }
 
     /**
        \brief Set a progress callback procedure that is invoked by this solver during check_sat.
@@ -156,9 +147,6 @@ public:
         ~scoped_push() { if (!m_nopop) s.pop(1); }
         void disable_pop() { m_nopop = true; }
     };
-
-protected:
-    //virtual void set_cancel(bool f) = 0;
 };
 
 #endif
diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp
index ccb7086a2..59d114ed6 100644
--- a/src/tactic/aig/aig_tactic.cpp
+++ b/src/tactic/aig/aig_tactic.cpp
@@ -37,6 +37,7 @@ class aig_tactic : public tactic {
         
         ~mk_aig_manager() {
             dealloc(m_owner.m_aig_manager);
+            m_owner.m_aig_manager = 0;
         }
     };
 
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index 03b8e6cfa..ea59641c9 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -182,12 +182,8 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
-        m_imp = 0;
-        
-        dealloc(d);
-        d = alloc(imp, m, m_params);
-        m_imp = d;        
+        dealloc(m_imp);
+        m_imp = alloc(imp, m, m_params);
     }
 
     static void blast_term_ite(expr_ref& fml) {
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 2ff079043..44d4603d4 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -57,15 +57,47 @@ void reslimit::pop() {
     m_cancel = false;
 }
 
-void reslimit::cancel() { 
-    m_cancel = true; 
-    for (unsigned i = 0; i < m_children.size(); ++i) {
-        m_children[i]->cancel();
+char const* get_cancel_msg() const {
+    if (m_cancel) {
+        return Z3_CANCELED_MSG;
+    }
+    else {
+        return Z3_MAX_RESOURCE_MSG;
     }
 }
-void reslimit::reset_cancel() { 
-    m_cancel = false; 
-    for (unsigned i = 0; i < m_children.size(); ++i) {
-        m_children[i]->reset_cancel();
+
+void reslimit::push_child(reslimit* r) {
+    #pragma omp critical (reslimit_cancel)
+    {
+        m_children.push_back(r); 
+    }
+}
+
+void reslimit::pop_child() {
+    #pragma omp critical (reslimit_cancel)
+    {
+        m_children.pop_back(); 
+    }
+}
+
+void reslimit::cancel() {
+    #pragma omp critical (reslimit_cancel)
+    {
+        set_cancel(false);
+    }
+}
+
+
+void reslimit::reset_cancel() {
+    #pragma omp critical (reslimit_cancel)
+    {
+        set_cancel(false);
+    }
+}
+
+void reslimit::set_cancel(bool f) { 
+    m_cancel = f; 
+    for (unsigned i = 0; i < m_children.size(); ++i) {
+        m_children[i]->set_cancel(f);
     }
 }
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index 9e7b4345a..c16a8d49b 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -27,19 +27,23 @@ class reslimit {
     uint64          m_limit;
     svector<uint64> m_limits;
     ptr_vector<reslimit> m_children;
+
+    void set_cancel(bool f);
+    
 public:    
     reslimit();
     void push(unsigned delta_limit);
     void pop();
-    void push_child(reslimit* r) { m_children.push_back(r); }
-    void pop_child() { m_children.pop_back(); }
+    void push_child(reslimit* r);
+    void pop_child();
 
     bool inc();
     bool inc(unsigned offset);
     uint64 count() const; 
 
 
-    bool cancel_flag_set() { return m_cancel; }
+    bool get_cancel_flag() const { return m_cancel; }
+    char const* get_cancel_msg() const;
     void cancel();
     void reset_cancel();
 };