remove a bunch of unneeded memory allocations

Z3Prover · Feb 25, 2022 · 689e2d4 · 689e2d4
1 parent 7f149a3
commit 689e2d4
Show file tree

Hide file tree

Showing 7 changed files with 52 additions and 64 deletions.
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
@@ -644,7 +644,7 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
     for code in cmds:
         fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code)
     for (mod, code) in mod_cmds:
-        fout.write('{ std::function<param_descrs *(void)> f = []() { auto* d = alloc(param_descrs); %s(*d); return d; }; gparams::register_module("%s", f); }\n' % (code, mod))
+        fout.write('{ auto f = []() { auto* d = alloc(param_descrs); %s(*d); return d; }; gparams::register_module("%s", f); }\n' % (code, mod))
     for (mod, descr) in mod_descrs:
         fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr))
     fout.write('}\n')

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
@@ -1759,13 +1759,13 @@ ast * ast_manager::register_node_core(ast * n) {
     switch (n->get_kind()) {
     case AST_SORT:
         if (to_sort(n)->m_info != nullptr) {
-            to_sort(n)->m_info = alloc(sort_info, *(to_sort(n)->get_info()));
+            to_sort(n)->m_info = alloc(sort_info, std::move(*(to_sort(n)->get_info())));
             to_sort(n)->m_info->init_eh(*this);
         }
         break;
     case AST_FUNC_DECL:
         if (to_func_decl(n)->m_info != nullptr) {
-            to_func_decl(n)->m_info = alloc(func_decl_info, *(to_func_decl(n)->get_info()));
+            to_func_decl(n)->m_info = alloc(func_decl_info, std::move(*(to_func_decl(n)->get_info())));
             to_func_decl(n)->m_info->init_eh(*this);
         }
         inc_array_ref(to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
@@ -1993,7 +1993,7 @@ sort * ast_manager::substitute(sort* s, unsigned n, sort * const * src, sort * c
         return s;
     }
     decl_info dinfo(s->get_family_id(), s->get_decl_kind(), ps.size(), ps.data(), s->private_parameters());
-    sort_info sinfo(dinfo, s->get_num_elements());
+    sort_info sinfo(std::move(dinfo), s->get_num_elements());
     return mk_sort(s->get_name(), &sinfo);
 }
 

diff --git a/src/ast/ast.h b/src/ast/ast.h
@@ -367,8 +367,8 @@ class sort_info : public decl_info {
         decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) {
     }
 
-    sort_info(decl_info const& di, sort_size const& num_elements) : 
-        decl_info(di), m_num_elements(num_elements) {}
+    sort_info(decl_info && di, sort_size const& num_elements) :
+        decl_info(std::move(di)), m_num_elements(num_elements) {}
 
     bool is_infinite() const { return m_num_elements.is_infinite(); }
     bool is_very_big() const { return m_num_elements.is_very_big(); }

diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
@@ -86,13 +86,13 @@ static char const * get_new_param_name(std::string const & p) {
 template <typename T>
 class smap : public map<char const*, T, str_hash_proc, str_eq_proc> {};
 
-typedef std::function<param_descrs*(void)> lazy_descrs_t;
+typedef param_descrs* (*lazy_descrs_t)(void);
 
 class lazy_param_descrs {
     param_descrs*      m_descrs;
-    ptr_vector<lazy_descrs_t>      m_mk;
+    svector<lazy_descrs_t> m_mk;
 
-    void apply(lazy_descrs_t& f) {
+    void apply(lazy_descrs_t f) {
         param_descrs* d = f();
         if (m_descrs) {
             m_descrs->copy(*d);
@@ -104,18 +104,16 @@ class lazy_param_descrs {
     }
 
     void reset_mk() {
-        for (auto* f : m_mk) dealloc(f);
         m_mk.reset();
     }
 
 public:
-    lazy_param_descrs(lazy_descrs_t& f): m_descrs(nullptr) {
+    lazy_param_descrs(lazy_descrs_t f): m_descrs(nullptr) {
         append(f);
     }
 
     ~lazy_param_descrs() { 
-        dealloc(m_descrs);  
-        reset_mk();
+        dealloc(m_descrs);
     }
 
     param_descrs* deref() {
@@ -124,8 +122,8 @@ class lazy_param_descrs {
         return m_descrs;
     }
 
-    void append(lazy_descrs_t& f) {
-        m_mk.push_back(alloc(lazy_descrs_t, f));        
+    void append(lazy_descrs_t f) {
+        m_mk.push_back(f);
     }
 };
 
@@ -204,7 +202,7 @@ struct gparams::imp {
         m_param_descrs.copy(d);
     }
 
-    void register_module(char const * module_name, lazy_descrs_t& f) {
+    void register_module(char const * module_name, lazy_descrs_t f) {
         // Don't need synchronization here, this method
         // is invoked from check_registered that is already protected.
 
@@ -599,7 +597,7 @@ void gparams::register_global(param_descrs & d) {
     g_imp->register_global(d);
 }
 
-void gparams::register_module(char const * module_name, lazy_descrs_t& f) {
+void gparams::register_module(char const * module_name, lazy_descrs_t f) {
     SASSERT(g_imp);
     g_imp->register_module(module_name, f);
 }

diff --git a/src/util/gparams.h b/src/util/gparams.h
@@ -85,8 +85,8 @@ class gparams {
        module.
     */
 
-    typedef std::function<param_descrs*(void)> lazy_descrs_t;
-    static void register_module(char const* module_name, lazy_descrs_t& get_descrs);
+    typedef param_descrs* (*lazy_descrs_t)(void);
+    static void register_module(char const* module_name, lazy_descrs_t get_descrs);
 
     /**
        \brief Add a (small) description to the given module.

diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
@@ -76,56 +76,45 @@ static void thread_func(scoped_timer_state *s) {
 }
 
 
-struct scoped_timer::imp {
-private:
-    scoped_timer_state *s;
+scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
+    if (ms == 0 || ms == UINT_MAX)
+        return;
 
-public:
-    imp(unsigned ms, event_handler * eh) {
-        workers.lock();
-        bool new_worker = false;
-        if (available_workers.empty()) {
-            workers.unlock();
-            s = new scoped_timer_state;
-            new_worker = true;
-            ++num_workers;
-        } 
-        else {
-            s = available_workers.back();
-            available_workers.pop_back();
-            workers.unlock();
-        }
-        s->ms = ms;
-        s->eh = eh;
-        s->m_mutex.lock();
-        s->work = WORKING;
-        if (new_worker) {
-            s->m_thread = std::thread(thread_func, s);
-        } 
-        else {
-            s->cv.notify_one();
-        }
+    workers.lock();
+    bool new_worker = false;
+    if (available_workers.empty()) {
+        workers.unlock();
+        s = new scoped_timer_state;
+        new_worker = true;
+        ++num_workers;
     }
-
-    ~imp() {
-        s->m_mutex.unlock();
-        while (s->work == WORKING)
-            std::this_thread::yield();
-        workers.lock();
-        available_workers.push_back(s);
+    else {
+        s = available_workers.back();
+        available_workers.pop_back();
         workers.unlock();
     }
-};
-
-scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
-    if (ms != UINT_MAX && ms != 0)
-        m_imp = alloc(imp, ms, eh);
-    else
-        m_imp = nullptr;
+    s->ms = ms;
+    s->eh = eh;
+    s->m_mutex.lock();
+    s->work = WORKING;
+    if (new_worker) {
+        s->m_thread = std::thread(thread_func, s);
+    }
+    else {
+        s->cv.notify_one();
+    }
 }
 
 scoped_timer::~scoped_timer() {
-    dealloc(m_imp);
+    if (!s)
+        return;
+
+    s->m_mutex.unlock();
+    while (s->work == WORKING)
+        std::this_thread::yield();
+    workers.lock();
+    available_workers.push_back(s);
+    workers.unlock();
 }
 
 void scoped_timer::initialize() {

diff --git a/src/util/scoped_timer.h b/src/util/scoped_timer.h
@@ -20,9 +20,10 @@ Revision History:
 
 #include "util/event_handler.h"
 
+struct scoped_timer_state;
+
 class scoped_timer {
-    struct imp;
-    imp *  m_imp;
+    scoped_timer_state *s = nullptr;
 public:
     scoped_timer(unsigned ms, event_handler * eh);
     ~scoped_timer();