From 689e2d41de8776b2af3be8d78ba5b15c86ff531e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 25 Feb 2022 14:32:20 +0000 Subject: [PATCH] remove a bunch of unneeded memory allocations --- scripts/mk_genfile_common.py | 2 +- src/ast/ast.cpp | 6 +-- src/ast/ast.h | 4 +- src/util/gparams.cpp | 20 +++++----- src/util/gparams.h | 4 +- src/util/scoped_timer.cpp | 75 +++++++++++++++--------------------- src/util/scoped_timer.h | 5 ++- 7 files changed, 52 insertions(+), 64 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index ef73e5f3fd6..f4b54cba059 100644 --- 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 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 index 2472e9efdb5..23ad2332904 100644 --- 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 index 13898c2a6ef..3cb90193f17 100644 --- 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 index 0c679e38866..25504edddaf 100644 --- 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 class smap : public map {}; -typedef std::function lazy_descrs_t; +typedef param_descrs* (*lazy_descrs_t)(void); class lazy_param_descrs { param_descrs* m_descrs; - ptr_vector m_mk; + svector 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 index 0efad4a071c..0959c20fc56 100644 --- a/src/util/gparams.h +++ b/src/util/gparams.h @@ -85,8 +85,8 @@ class gparams { module. */ - typedef std::function 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 index a36e762aa34..e8a72e24585 100644 --- 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 index 95920b71f8a..dfd97810cb5 100644 --- 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();