diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-09 23:14:40 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-09 23:14:40 +0000 |
commit | 2f121daa042c6f25a3f9ed8ece60ac5dccb11976 (patch) | |
tree | 58ee28d73e8638b100abe09e961bc3dbdf9d79d9 /src/util | |
parent | d697d1e91be226339a28bd7e8dce3862901cba8a (diff) |
some fixes and organizational adjustments to assert code, parsers/lexers, and build process
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.cpp | 101 | ||||
-rw-r--r-- | src/util/Assert.h | 189 | ||||
-rw-r--r-- | src/util/Makefile.am | 16 | ||||
-rw-r--r-- | src/util/Makefile.in | 29 | ||||
-rw-r--r-- | src/util/exception.h | 12 |
5 files changed, 262 insertions, 85 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp new file mode 100644 index 000000000..799af12ab --- /dev/null +++ b/src/util/Assert.cpp @@ -0,0 +1,101 @@ +/********************* -*- C++ -*- */ +/** Assert.cpp + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Assertion utility classes, functions, and exceptions. Implementation. + **/ + +#include <new> +#include <cstdarg> +#include <cstdio> +#include "util/Assert.h" +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" + +using namespace std; + +namespace CVC4 { + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, + va_list args) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args); + va_end(args_copy); + + if(size < n) { + break; + } + } + + if(size >= n) { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + delete [] buf; +} + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + break; + } else { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + delete [] buf; +} + +}/* CVC4 namespace */ diff --git a/src/util/Assert.h b/src/util/Assert.h index 8fd970c6c..3da76c5db 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** assert.h +/** Assert.h ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -7,13 +7,15 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Assertion utility classes, functions, and exceptions. + ** Assertion utility classes, functions, exceptions, and macros. **/ #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H #include <string> +#include <cstdio> +#include <cstdarg> #include "util/exception.h" #include "cvc4_config.h" #include "config.h" @@ -21,91 +23,136 @@ namespace CVC4 { class CVC4_PUBLIC AssertionException : public Exception { -public: +protected: + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, ...) { + va_list args; + va_start(args, fmt); + construct(header, extra, function, file, line, fmt, args); + va_end(args); + } + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, va_list args); + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line); + AssertionException() : Exception() {} - AssertionException(std::string msg) : Exception(msg) {} - AssertionException(const char* msg) : Exception(msg) {} + +public: + AssertionException(const char* extra, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + Exception() { + va_list args; + va_start(args, fmt); + construct("Assertion failure", extra, function, file, line, fmt, args); + va_end(args); + } + + AssertionException(const char* extra, const char* function, + const char* file, unsigned line) : + Exception() { + construct("Assertion failure", extra, function, file, line); + } };/* class AssertionException */ class CVC4_PUBLIC UnreachableCodeException : public AssertionException { -public: +protected: UnreachableCodeException() : AssertionException() {} - UnreachableCodeException(std::string msg) : AssertionException(msg) {} - UnreachableCodeException(const char* msg) : AssertionException(msg) {} + +public: + UnreachableCodeException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unreachable code reached", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnreachableCodeException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unreachable code reached", NULL, function, file, line); + } };/* class UnreachableCodeException */ class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException { -public: +protected: UnhandledCaseException() : UnreachableCodeException() {} - UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {} - UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {} + +public: + UnhandledCaseException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + UnreachableCodeException() { + va_list args; + va_start(args, fmt); + construct("Unhandled case encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnhandledCaseException(const char* function, const char* file, + unsigned line, int theCase) : + UnreachableCodeException() { + construct("Unhandled case encountered", + NULL, function, file, line, "The case was: %d", theCase); + } + + UnhandledCaseException(const char* function, const char* file, + unsigned line) : + UnreachableCodeException() { + construct("Unhandled case encountered", NULL, function, file, line); + } };/* class UnhandledCaseException */ +class CVC4_PUBLIC IllegalArgumentException : public AssertionException { +protected: + IllegalArgumentException() : AssertionException() {} + +public: + IllegalArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + argDesc, function, file, line, fmt, args); + va_end(args); + } + + IllegalArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line) : + AssertionException() { + construct("Illegal argument detected", + argDesc, function, file, line); + } +};/* class IllegalArgumentException */ + +#define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw AssertionException(#cond, __FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) +#define Unreachable(msg...) \ + throw UnreachableCodeException(__FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unhandled(msg...) \ + throw UnhandledCaseException(__FUNCTION__, __FILE__, __LINE__, ## msg) +#define IllegalArgument(arg, msg...) \ + throw IllegalArgumentException(#arg, __FUNCTION__, __FILE__, __LINE__, ## msg) + #ifdef CVC4_ASSERTIONS -# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +# define Assert(cond, msg...) AlwaysAssert(cond, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ -#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) -#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg) -#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg) - -#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) -#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg) -#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg) - -inline void AssertImpl(const char* info, bool cond, std::string msg) { - if(EXPECT_FALSE( ! cond )) - throw AssertionException(std::string(info) + "\n" + msg); -} - -inline void AssertImpl(const char* info, bool cond, const char* msg) { - if(EXPECT_FALSE( ! cond )) - throw AssertionException(std::string(info) + "\n" + msg); -} - -inline void AssertImpl(const char* info, bool cond) { - if(EXPECT_FALSE( ! cond )) - throw AssertionException(info); -} - -#ifdef __GNUC__ -inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); -inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); -inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); -#endif /* __GNUC__ */ - -inline void UnreachableImpl(const char* info, std::string msg) { - throw UnreachableCodeException(std::string(info) + "\n" + msg); -} - -inline void UnreachableImpl(const char* info, const char* msg) { - throw UnreachableCodeException(std::string(info) + "\n" + msg); -} - -inline void UnreachableImpl(const char* info) { - throw UnreachableCodeException(info); -} - -#ifdef __GNUC__ -inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn)); -inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn)); -inline void UnhandledImpl(const char* info) __attribute__ ((noreturn)); -#endif /* __GNUC__ */ - -inline void UnhandledImpl(const char* info, std::string msg) { - throw UnhandledCaseException(std::string(info) + "\n" + msg); -} - -inline void UnhandledImpl(const char* info, const char* msg) { - throw UnhandledCaseException(std::string(info) + "\n" + msg); -} - -inline void UnhandledImpl(const char* info) { - throw UnhandledCaseException(info); -} - }/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 8baf872d2..b6c116a6d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -5,6 +5,20 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la libutil_la_SOURCES = \ + Assert.h \ + Assert.cpp \ + Makefile.am \ + Makefile.in \ command.cpp \ + command.h \ + debug.h \ decision_engine.cpp \ - output.cpp + decision_engine.h \ + exception.h \ + literal.h \ + model.h \ + options.h \ + output.cpp \ + output.h \ + result.h \ + unique_id.h diff --git a/src/util/Makefile.in b/src/util/Makefile.in index ac8d4b522..9f17df4c7 100644 --- a/src/util/Makefile.in +++ b/src/util/Makefile.in @@ -52,7 +52,8 @@ CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libutil_la_LIBADD = -am_libutil_la_OBJECTS = command.lo decision_engine.lo output.lo +am_libutil_la_OBJECTS = Assert.lo command.lo decision_engine.lo \ + output.lo libutil_la_OBJECTS = $(am_libutil_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -67,6 +68,15 @@ CXXLD = $(CXX) CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \ $(LDFLAGS) -o $@ +COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ + $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +CCLD = $(CC) +LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ + --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ + $(LDFLAGS) -o $@ SOURCES = $(libutil_la_SOURCES) DIST_SOURCES = $(libutil_la_SOURCES) ETAGS = etags @@ -211,9 +221,23 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la libutil_la_SOURCES = \ + Assert.h \ + Assert.cpp \ + Makefile.am \ + Makefile.in \ command.cpp \ + command.h \ + debug.h \ decision_engine.cpp \ - output.cpp + decision_engine.h \ + exception.h \ + literal.h \ + model.h \ + options.h \ + output.cpp \ + output.h \ + result.h \ + unique_id.h all: all-am @@ -267,6 +291,7 @@ mostlyclean-compile: distclean-compile: -rm -f *.tab.c +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/Assert.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/command.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/decision_engine.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/output.Plo@am__quote@ diff --git a/src/util/exception.h b/src/util/exception.h index 164cda8b5..d239f48de 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -31,7 +31,7 @@ public: Exception(const char* msg) : d_msg(msg) {} // Destructor virtual ~Exception() {} - // NON-VIRTUAL METHODs for setting and printing the error message + // NON-VIRTUAL METHOD for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } // Printing: feel free to redefine toString(). When inherited, // it's recommended that this method print the type of exception @@ -41,20 +41,10 @@ public: friend std::ostream& operator<<(std::ostream& os, const Exception& e); };/* class Exception */ - -class CVC4_PUBLIC IllegalArgumentException : public Exception { -public: - IllegalArgumentException() : Exception("Illegal argument to method or function") {} - IllegalArgumentException(const std::string& msg) : Exception(msg) {} - IllegalArgumentException(const char* msg) : Exception(msg) {} -};/* class IllegalArgumentException */ - - inline std::ostream& operator<<(std::ostream& os, const Exception& e) { return os << e.toString(); } - }/* CVC4 namespace */ #endif /* __CVC4__EXCEPTION_H */ |