Add support files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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 <iostream>
+#include <sstream>
+#include <set>
+#include <string>
+#include <memory>
+
+#ifndef _WINDOWS
+// Support for pid
+#include<unistd.h>
+#endif
+
+namespace lean {
+
+static volatile bool                          g_enable_assertions = true;
+static std::unique_ptr<std::set<std::string>> 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<std::string>());
+    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";
+        }
+    }
+}
+
+}

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();
+
+}

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();
+}
+
+}

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 <exception>
+#include <string>
+
+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;
+};
+
+}