commit 4f5cafdebfa02c041f4dcd8c2ebe3e463bf32343 Author: Leonardo de Moura Date: Mon Jul 15 18:43:32 2013 -0700 Add support files Signed-off-by: Leonardo de Moura diff --git a/src/util/debug.cpp b/src/util/debug.cpp new file mode 100644 index 0000000000..32e8f710c1 --- /dev/null +++ b/src/util/debug.cpp @@ -0,0 +1,101 @@ +/* +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 "debug.h" +#include +#include +#include +#include +#include + +#ifndef _WINDOWS +// Support for pid +#include +#endif + +namespace lean { + +static volatile bool g_enable_assertions = true; +static std::unique_ptr> g_enabled_debug_tags; + +void enable_assertions(bool f) { + g_enable_assertions = f; +} + +bool assertions_enabled() { + return g_enable_assertions; +} + +void notify_assertion_violation(const char * fileName, int line, const char * condition) { + std::cerr << "LEAN ASSERTION VIOLATION\n"; + std::cerr << "File: " << fileName << "\n"; + std::cerr << "Line: " << line << "\n"; + std::cerr << condition << "\n"; + std::cerr.flush(); +} + +void enable_debug(char const * tag) { + if (!g_enabled_debug_tags) + g_enabled_debug_tags.reset(new std::set()); + g_enabled_debug_tags->insert(tag); +} + +void disable_debug(char const * tag) { + if (g_enabled_debug_tags) + g_enabled_debug_tags->erase(tag); +} + +bool is_debug_enabled(const char * tag) { + return g_enabled_debug_tags && g_enabled_debug_tags->find(tag) != g_enabled_debug_tags->end(); +} + +void invoke_debugger() { + int * x = 0; + for (;;) { + #ifdef _WINDOWS + std::cerr << "(C)ontinue, (A)bort, (S)top\n"; + #else + std::cerr << "(C)ontinue, (A)bort, (S)top, Invoke (G)DB\n"; + #endif + char result; + std::cin >> result; + switch(result) { + case 'C': + case 'c': + return; + case 'A': + case 'a': + exit(1); + case 'S': + case 's': + // force seg fault... + *x = 0; + return; + #ifndef _WINDOWS + case 'G': + case 'g': { + std::cerr << "INVOKING GDB...\n"; + std::ostringstream buffer; + buffer << "gdb -nw /proc/" << getpid() << "/exe " << getpid(); + if (system(buffer.str().c_str()) == 0) { + std::cerr << "continuing the execution...\n"; + } + else { + std::cerr << "ERROR STARTING GDB...\n"; + // forcing seg fault. + int * x = 0; + *x = 0; + } + return; + } + #endif + default: + std::cerr << "INVALID COMMAND\n"; + } + } +} + +} diff --git a/src/util/debug.h b/src/util/debug.h new file mode 100644 index 0000000000..abe5733698 --- /dev/null +++ b/src/util/debug.h @@ -0,0 +1,42 @@ +/* +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 + +#ifndef __has_builtin +#define __has_builtin(x) 0 +#endif + +#ifdef LEAN_DEBUG +#define DEBUG_CODE(CODE) CODE +#else +#define DEBUG_CODE(CODE) +#endif + +#define lean_assert(COND) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }}) +#define lean_cond_assert(TAG, COND) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }}) + +#if __has_builtin(__builtin_unreachable) +#define lean_unreachable() __builtin_unreachable() +#else +#define lean_unreachable() DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();}) +#endif + +#ifdef LEAN_DEBUG +#define lean_verify(COND) if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); } +#else +#define lean_verify(COND) (COND) +#endif + +namespace lean { + +void notify_assertion_violation(char const * file_name, int line, char const * condition); +void enable_debug(char const * tag); +void disable_debug(char const * tag); +bool is_debug_enabled(char const * tag); +void invoke_debugger(); + +} diff --git a/src/util/exception.cpp b/src/util/exception.cpp new file mode 100644 index 0000000000..689dbd1620 --- /dev/null +++ b/src/util/exception.cpp @@ -0,0 +1,27 @@ +/* +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 "exception.h" + +namespace lean { + +exception::exception(char const * msg):m_msg(msg) { +} + +exception::exception(std::string const & msg):m_msg(msg) { +} + +exception::exception(exception const & e):m_msg(e.m_msg) { +} + +exception::~exception() { +} + +char const * exception::what() const noexcept { + return m_msg.c_str(); +} + +} diff --git a/src/util/exception.h b/src/util/exception.h new file mode 100644 index 0000000000..05c864ad79 --- /dev/null +++ b/src/util/exception.h @@ -0,0 +1,23 @@ +/* +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 + +namespace lean { + +class exception : public std::exception { + std::string m_msg; +public: + exception(char const * msg); + exception(std::string const & msg); + exception(exception const & ex); + virtual ~exception(); + virtual char const * what() const noexcept; +}; + +} diff --git a/src/util/name.cpp b/src/util/name.cpp new file mode 100644 index 0000000000..5d88aed635 --- /dev/null +++ b/src/util/name.cpp @@ -0,0 +1,229 @@ +/* +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 "name.h" +#include "debug.h" + +namespace lean { + +constexpr char const * anonymous_str = "[anonymous]"; + +struct name::imp { + bool m_is_string; + unsigned m_rc; + imp * m_prefix; + union { + char * m_str; + unsigned m_k; + }; + + void inc_ref() { m_rc++; } + + void dec_ref() { + imp * curr = this; + while (curr) { + lean_assert(curr->m_rc > 0); + curr->m_rc--; + if (curr->m_rc == 0) { + imp * p = curr->m_prefix; + if (curr->m_is_string) + delete[] reinterpret_cast(curr); + else + delete curr; + curr = p; + } + else { + curr = 0; + } + } + } + + imp(bool s, imp * p):m_is_string(s), m_rc(1), m_prefix(p) { if (p) p->inc_ref(); } + + static void display_core(std::ostream & out, char const * sep, imp * p) { + lean_assert(p != nullptr); + if (p->m_prefix) { + display_core(out, sep, p->m_prefix); + out << sep; + } + if (p->m_is_string) + out << p->m_str; + else + out << p->m_k; + } + + static void display(std::ostream & out, char const * sep, imp * p) { + if (p == nullptr) + out << anonymous_str; + else + display_core(out, sep, p); + } +}; + +name::name(imp * p) { + m_imp = p; + if (m_imp) + m_imp->inc_ref(); +} + +name::name() { + m_imp = nullptr; +} + +name::name(name const & prefix, char const * name) { + size_t sz = strlen(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); + m_imp->m_str = mem + sizeof(imp); +} + +name::name(name const & prefix, unsigned k) { + m_imp = new imp(false, prefix.m_imp); + m_imp->m_k = k; +} + +name::name(char const * n):name(name(), n) { +} + +name::name(unsigned k):name(name(), k) { +} + +name::name(name const & other):m_imp(other.m_imp) { + m_imp->inc_ref(); +} + +name::name(name && other):m_imp(other.m_imp) { + other.m_imp = 0; +} + +name::~name() { + if (m_imp) + m_imp->dec_ref(); +} + +name & name::operator=(name const & other) { + if (other.m_imp) + other.m_imp->inc_ref(); + if (m_imp) + m_imp->dec_ref(); + m_imp = other.m_imp; + return *this; +} + +name & name::operator=(name && other) { + lean_assert(this != &other); + if (m_imp) + m_imp->dec_ref(); + m_imp = other.m_imp; + other.m_imp = 0; + return *this; +} + +name::kind name::get_kind() const { + if (m_imp == nullptr) + return kind::ANONYMOUS; + else + return m_imp->m_is_string ? kind::STRING : kind::NUMERAL; +} + +unsigned name::get_numeral() const { + lean_assert(is_numeral()); + return m_imp->m_k; +} + +char const * name::get_string() const { + lean_assert(is_string()); + return m_imp->m_str; +} + +bool name::operator==(name const & other) const { + imp * i1 = m_imp; + imp * i2 = other.m_imp; + while (true) { + if (i1 == i2) + return true; + if ((i1 == nullptr) != (i2 == nullptr)) + return false; + lean_assert(i1 != nullptr); + lean_assert(i2 != nullptr); + if (i1->m_is_string != i2->m_is_string) + return false; + if (m_imp->m_is_string) { + if (strcmp(get_string(), other.get_string()) != 0) + return false; + } + else { + if (get_numeral() != other.get_numeral()) + return false; + } + i1 = i1->m_prefix; + i2 = i2->m_prefix; + } +} + +bool name::is_atomic() const { + return m_imp == nullptr || m_imp->m_prefix == nullptr; +} + +name name::get_prefix() const { + lean_assert(!is_atomic()); + return name(m_imp->m_prefix); +} + +static unsigned num_digits(unsigned k) { + if (k == 0) + return 1; + int r = 0; + while (k != 0) { + k /= 10; + r++; + } + return r; +} + +size_t name::size(char const * sep) const { + if (m_imp == nullptr) { + return strlen(anonymous_str); + } + else { + imp * i = m_imp; + size_t sep_sz = strlen(sep); + size_t r = 0; + while (true) { + if (i->m_is_string) { + r += strlen(i->m_str); + } + else { + r += num_digits(i->m_k); + } + if (i->m_prefix) { + r += sep_sz; + i = i->m_prefix; + } + else { + break; + } + } + return r; + } +} + +std::ostream & operator<<(std::ostream & out, name const & n) { + name::imp::display(out, default_name_separator, n.m_imp); + return out; +} + +name::sep::sep(name const & n, char const * s):m_name(n), m_sep(s) {} + +std::ostream & operator<<(std::ostream & out, name::sep const & s) { + name::imp::display(out, s.m_sep, s.m_name.m_imp); + return out; +} + +} diff --git a/src/util/name.h b/src/util/name.h new file mode 100644 index 0000000000..ab0bf1fd8c --- /dev/null +++ b/src/util/name.h @@ -0,0 +1,58 @@ +/* +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 + +namespace lean { + +constexpr char const * default_name_separator = "::"; + +/** + \brief Hierarchical names. +*/ +class name { + enum class kind { ANONYMOUS, STRING, NUMERAL }; + struct imp; + imp * m_imp; + name(imp * p); +public: + name(); + name(char const * name); + name(unsigned k); + name(name const & prefix, char const * name); + name(name const & prefix, unsigned k); + name(name const & other); + name(name && other); + ~name(); + name & operator=(name const & other); + name & operator=(name && other); + bool operator==(name const & other) const; + bool operator!=(name const & other) const { return !operator==(other); } + kind get_kind() const; + bool is_anonymous() const { return get_kind() == kind::ANONYMOUS; } + bool is_string() const { return get_kind() == kind::STRING; } + bool is_numeral() const { return get_kind() == kind::NUMERAL; } + unsigned get_numeral() const; + char const * get_string() const; + bool is_atomic() const; + name get_prefix() const; + /** + \brief Size of the this name (in characters) when using the given separator. + */ + size_t size(char const * sep = default_name_separator) const; + friend std::ostream & operator<<(std::ostream & out, name const & n); + class sep { + name const & m_name; + char const * m_sep; + public: + sep(name const & n, char const * s); + friend std::ostream & operator<<(std::ostream & out, sep const & s); + }; + friend std::ostream & operator<<(std::ostream & out, sep const & s); +}; + +} diff --git a/src/util/trace.cpp b/src/util/trace.cpp new file mode 100644 index 0000000000..29cf2348fa --- /dev/null +++ b/src/util/trace.cpp @@ -0,0 +1,42 @@ +/* +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 "trace.h" +#include +#include +#include + +#ifndef LEAN_TRACE_OUT +#define LEAN_TRACE_OUT ".lean_trace" +#endif + +namespace lean { + +#ifdef LEAN_TRACE +std::ofstream tout(LEAN_TRACE_OUT); +std::mutex trace_mutex; +#endif + +static std::unique_ptr> g_enabled_trace_tags; + +void enable_trace(char const * tag) { + if (!g_enabled_trace_tags) + g_enabled_trace_tags.reset(new std::set()); + g_enabled_trace_tags->insert(tag); +} + +void disable_trace(char const * tag) { + if (g_enabled_trace_tags) + g_enabled_trace_tags->erase(tag); +} + +bool is_trace_enabled(char const * tag) { + return g_enabled_trace_tags && g_enabled_trace_tags->find(tag) != g_enabled_trace_tags->end(); +} + +} + diff --git a/src/util/trace.h b/src/util/trace.h new file mode 100644 index 0000000000..14032c08f0 --- /dev/null +++ b/src/util/trace.h @@ -0,0 +1,31 @@ +/* +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 + +#ifdef LEAN_TRACE +#include +#include +namespace lean { +extern std::ofstream tout; +extern std::mutex trace_mutex; +} +#define TRACE_CODE(CODE) { std::lock_guard _lean_trace_lock_(lean::trace_mutex); CODE } +#else +#define TRACE_CODE(CODE) +#endif + +#define lean_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); }) + +#define lean_simple_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { CODE lean::tout.flush(); }) + +#define lean_cond_trace(TAG, COND, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG) && (COND)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); }) + +namespace lean { +void enable_trace(char const * tag); +void disable_trace(char const * tag); +bool is_trace_enabled(char const * tag); +}