1 /********************* */
2 /*! \file exception.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief CVC4's exception base class and some associated utilities
13 **
14 ** CVC4's exception base class and some associated utilities.
15 **/
16
17 #include "cvc4_public.h"
18
19 #ifndef __CVC4__EXCEPTION_H
20 #define __CVC4__EXCEPTION_H
21
22 #include <cstdarg>
23 #include <cstdlib>
24 #include <exception>
25 #include <iosfwd>
26 #include <sstream>
27 #include <stdexcept>
28 #include <string>
29
30 namespace CVC4 {
31
32 class CVC4_PUBLIC Exception : public std::exception {
33 protected:
34 std::string d_msg;
35
36 public:
37 // Constructors
Exception()38 Exception() : d_msg("Unknown exception") {}
Exception(const std::string & msg)39 Exception(const std::string& msg) : d_msg(msg) {}
Exception(const char * msg)40 Exception(const char* msg) : d_msg(msg) {}
41
42 // Destructor
~Exception()43 virtual ~Exception() {}
44
45 // NON-VIRTUAL METHOD for setting and printing the error message
setMessage(const std::string & msg)46 void setMessage(const std::string& msg) { d_msg = msg; }
getMessage()47 std::string getMessage() const { return d_msg; }
48
49 // overridden from base class std::exception
what()50 const char* what() const noexcept override { return d_msg.c_str(); }
51
52 /**
53 * Get this exception as a string. Note that
54 * cout << ex.toString();
55 * is subtly different from
56 * cout << ex;
57 * which is equivalent to
58 * ex.toStream(cout);
59 * That is because with the latter two, the output language (and
60 * other preferences) for exprs on the stream is respected. In
61 * toString(), there is no stream, so the parameters are default
62 * and you'll get exprs and types printed using the AST language.
63 */
toString()64 std::string toString() const
65 {
66 std::stringstream ss;
67 toStream(ss);
68 return ss.str();
69 }
70
71 /**
72 * Printing: feel free to redefine toStream(). When overridden in
73 * a derived class, it's recommended that this method print the
74 * type of exception before the actual message.
75 */
toStream(std::ostream & os)76 virtual void toStream(std::ostream& os) const { os << d_msg; }
77
78 };/* class Exception */
79
80 class CVC4_PUBLIC IllegalArgumentException : public Exception {
81 protected:
IllegalArgumentException()82 IllegalArgumentException() : Exception() {}
83
84 void construct(const char* header, const char* extra,
85 const char* function, const char* tail);
86
87 void construct(const char* header, const char* extra,
88 const char* function);
89
90 static std::string format_extra(const char* condStr, const char* argDesc);
91
92 static const char* s_header;
93
94 public:
95
IllegalArgumentException(const char * condStr,const char * argDesc,const char * function,const char * tail)96 IllegalArgumentException(const char* condStr, const char* argDesc,
97 const char* function, const char* tail) :
98 Exception() {
99 construct(s_header, format_extra(condStr, argDesc).c_str(), function, tail);
100 }
101
IllegalArgumentException(const char * condStr,const char * argDesc,const char * function)102 IllegalArgumentException(const char* condStr, const char* argDesc,
103 const char* function) :
104 Exception() {
105 construct(s_header, format_extra(condStr, argDesc).c_str(), function);
106 }
107
108 /**
109 * This is a convenience function for building usages that are variadic.
110 *
111 * Having IllegalArgumentException itself be variadic is problematic for
112 * making sure calls to IllegalArgumentException clean up memory.
113 */
114 static std::string formatVariadic();
115 static std::string formatVariadic(const char* format, ...);
116 };/* class IllegalArgumentException */
117
118 inline std::ostream& operator<<(std::ostream& os,
119 const Exception& e) CVC4_PUBLIC;
120 inline std::ostream& operator<<(std::ostream& os, const Exception& e)
121 {
122 e.toStream(os);
123 return os;
124 }
125
126 template <class T> inline void CheckArgument(bool cond, const T& arg,
127 const char* tail) CVC4_PUBLIC;
CheckArgument(bool cond,const T & arg,const char * tail)128 template <class T> inline void CheckArgument(bool cond, const T& arg,
129 const char* tail) {
130 if(__builtin_expect( ( !cond ), false )) { \
131 throw ::CVC4::IllegalArgumentException("", "", ""); \
132 } \
133 }
134 template <class T> inline void CheckArgument(bool cond, const T& arg)
135 CVC4_PUBLIC;
CheckArgument(bool cond,const T & arg)136 template <class T> inline void CheckArgument(bool cond, const T& arg) {
137 if(__builtin_expect( ( !cond ), false )) { \
138 throw ::CVC4::IllegalArgumentException("", "", ""); \
139 } \
140 }
141
142 class CVC4_PUBLIC LastExceptionBuffer {
143 public:
144 LastExceptionBuffer();
145 ~LastExceptionBuffer();
146
147 void setContents(const char* string);
getContents()148 const char* getContents() const { return d_contents; }
149
getCurrent()150 static LastExceptionBuffer* getCurrent() { return s_currentBuffer; }
setCurrent(LastExceptionBuffer * buffer)151 static void setCurrent(LastExceptionBuffer* buffer) { s_currentBuffer = buffer; }
152
currentContents()153 static const char* currentContents() {
154 return (getCurrent() == NULL) ? NULL : getCurrent()->getContents();
155 }
156
157 private:
158 /* Disallow copies */
159 LastExceptionBuffer(const LastExceptionBuffer&) = delete;
160 LastExceptionBuffer& operator=(const LastExceptionBuffer&) = delete;
161
162 char* d_contents;
163
164 static thread_local LastExceptionBuffer* s_currentBuffer;
165 }; /* class LastExceptionBuffer */
166
167 }/* CVC4 namespace */
168
169 #endif /* __CVC4__EXCEPTION_H */
170