From 1f7011353be826e37c03c81ca6c9f163f03e84ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Jul 2013 14:41:03 -0700 Subject: [PATCH] Add (temporary) buffer class Signed-off-by: Leonardo de Moura --- src/kernel/deep_copy.cpp | 4 +- src/kernel/max_sharing.cpp | 4 +- src/kernel/replace.h | 4 +- src/tests/util/CMakeLists.txt | 6 ++ src/tests/util/buffer.cpp | 32 +++++++++ src/util/buffer.h | 119 ++++++++++++++++++++++++++++++++++ src/util/name.cpp | 2 +- 7 files changed, 164 insertions(+), 7 deletions(-) create mode 100644 src/tests/util/buffer.cpp create mode 100644 src/util/buffer.h diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp index 43a48b6c3..36bb7d613 100644 --- a/src/kernel/deep_copy.cpp +++ b/src/kernel/deep_copy.cpp @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include "expr.h" #include "maps.h" +#include "buffer.h" namespace lean { class deep_copy_fn { @@ -23,7 +23,7 @@ class deep_copy_fn { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: r = copy(a); break; // shallow copy is equivalent to deep copy for these ones. case expr_kind::App: { - std::vector new_args; + buffer new_args; for (expr const & old_arg : args(a)) new_args.push_back(apply(old_arg)); r = app(new_args.size(), new_args.data()); diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index 7c5acb656..d9c03a52a 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include +#include "buffer.h" #include "max_sharing.h" namespace lean { @@ -36,7 +36,7 @@ struct max_sharing_fn::imp { cache(a); return a; case expr_kind::App: { - std::vector new_args; + buffer new_args; bool modified = false; for (expr const & old_arg : args(a)) { new_args.push_back(apply(old_arg)); diff --git a/src/kernel/replace.h b/src/kernel/replace.h index df96550ca..b5a97c4f1 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include "buffer.h" #include "expr.h" #include "maps.h" namespace lean { @@ -38,7 +38,7 @@ class replace_fn { case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var: break; case expr_kind::App: { - std::vector new_args; + buffer new_args; bool modified = false; for (expr const & a : args(e)) { new_args.push_back(apply(a, offset)); diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 9596712e6..9cda4093e 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -4,6 +4,12 @@ add_test(interrupt ${CMAKE_CURRENT_BINARY_DIR}/interrupt) add_executable(name name.cpp) target_link_libraries(name ${EXTRA_LIBS}) add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name) +<<<<<<< HEAD add_executable(format format.cpp) target_link_libraries(format ${EXTRA_LIBS}) add_test(format ${CMAKE_CURRENT_BINARY_DIR}/format) +======= +add_executable(buffer buffer.cpp) +target_link_libraries(buffer ${EXTRA_LIBS}) +add_test(buffer ${CMAKE_CURRENT_BINARY_DIR}/buffer) +>>>>>>> Add (temporary) buffer class diff --git a/src/tests/util/buffer.cpp b/src/tests/util/buffer.cpp new file mode 100644 index 000000000..cf1cc5712 --- /dev/null +++ b/src/tests/util/buffer.cpp @@ -0,0 +1,32 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "buffer.h" +using namespace lean; + +template +static void loop(int n) { + C b; + b.push_back(n); + lean_assert(b.size() == 1); + lean_assert(b.back() == n); + lean_assert(b[0] == n); + if (n > 0) + loop(n-1); +} + +void perftest() { + for (unsigned i = 0; i < 10000; i++) + loop>(10000); +// for (unsigned i = 0; i < 10000; i++) +// loop>(10000); +} + +int main() { + loop>(100); + return 0; +} diff --git a/src/util/buffer.h b/src/util/buffer.h new file mode 100644 index 000000000..f3fc9d66d --- /dev/null +++ b/src/util/buffer.h @@ -0,0 +1,119 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include "debug.h" + +namespace lean { + +template +class buffer { +protected: + T * m_buffer; + unsigned m_pos; + unsigned m_capacity; + char m_initial_buffer[INITIAL_SIZE * sizeof(T)]; + + void free_memory() { + if (m_buffer != reinterpret_cast(m_initial_buffer)) + delete[] reinterpret_cast(m_buffer); + } + + void expand() { + unsigned new_capacity = m_capacity << 1; + T * new_buffer = reinterpret_cast(new char[sizeof(T) * new_capacity]); + std::memcpy(new_buffer, m_buffer, m_pos * sizeof(T)); + free_memory(); + m_buffer = new_buffer; + m_capacity = new_capacity; + } + + void destroy_elements() { + std::for_each(begin(), end(), [](T & e) { e.~T(); }); + } + + void destroy() { + destroy_elements(); + free_memory(); + } + +public: + typedef T value_type; + typedef T * iterator; + typedef T const * const_iterator; + + buffer(): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + } + + buffer(buffer const & source): + m_buffer(reinterpret_cast(m_initial_buffer)), + m_pos(0), + m_capacity(INITIAL_SIZE) { + std::for_each(source.begin(), source.end(), [=](T const & e) { push_back(e); }); + } + + ~buffer() { destroy(); } + + buffer & operator=(buffer const & source) { + clear(); + std::for_each(source.begin(), source.end(), [=](T const & e) { push_back(e); }); + return *this; + } + + T const & back() const { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; } + T & back() { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; } + T & operator[](unsigned idx) { lean_assert(idx < size()); return m_buffer[idx]; } + T const & operator[](unsigned idx) const { lean_assert(idx < size()); return m_buffer[idx]; } + void clear() { destroy_elements(); m_pos = 0; } + unsigned size() const { return m_pos; } + T const * data() const { return m_buffer; } + T * data() { return m_buffer; } + bool empty() const { return m_pos == 0; } + iterator begin() { return m_buffer; } + iterator end() { return m_buffer + size(); } + const_iterator begin() const { return m_buffer; } + const_iterator end() const { return m_buffer + size(); } + + void push_back(T const & elem) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(elem); + m_pos++; + } + + void pop_back() { + back().~T(); + m_pos--; + } + + void resize(unsigned nsz, T const & elem=T()) { + unsigned sz = size(); + if (nsz > sz) { + for (unsigned i = sz; i < nsz; i++) + push_back(elem); + } + else if (nsz < sz) { + for (unsigned i = nsz; i < sz; i++) + pop_back(); + } + lean_assert(size() == nsz); + } + + void shrink(unsigned nsz) { + unsigned sz = size(); + lean_assert(nsz <= sz); + for (unsigned i = nsz; i < sz; i++) + pop_back(); + lean_assert(size() == nsz); + } +}; + +} diff --git a/src/util/name.cpp b/src/util/name.cpp index c783dfcbe..5655afff6 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -88,7 +88,7 @@ name::name(name const & prefix, char const * name) { lean_assert(sz < 1u<<31); char * mem = new char[sizeof(imp) + sz + 1]; m_imp = new (mem) imp(true, prefix.m_imp); - memcpy(mem + sizeof(imp), name, sz + 1); + std::memcpy(mem + sizeof(imp), name, sz + 1); m_imp->m_str = mem + sizeof(imp); if (m_imp->m_prefix) m_imp->m_hash = hash_str(sz, name, m_imp->m_prefix->m_hash);