1
2 /*
3 * File Tracer.hpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file Tracer.hpp
21 * Implements call tracing.
22 * @since 01/05/2002 Manchester
23 * @since 24/10/2002 Manchester, changed after talking with Shura
24 * @since 08/12/2005 Redmond, moved to the Debug namespace with the purpose
25 * of making global to Vampire
26 */
27
28
29 #ifndef __Tracer__
30 # define __Tracer__
31
32 #if VDEBUG
33
34 #include <iostream>
35
36 using namespace std;
37
38 namespace Debug {
39
40 /**
41 * What kind of control point it is.
42 */
43 enum ControlPointKind {
44 /** Entry to a function */
45 CP_ENTRY,
46 /** Exit from a function */
47 CP_EXIT,
48 /** Point inside a function */
49 CP_MID
50 }; // enum ControlPointKind
51
52 class Tracer {
53 public:
54 explicit Tracer (const char* fun);
55 virtual ~Tracer ();
56 static void printStack (ostream&);
57 static void printOnlyStack (ostream&);
58 static void controlPoint (const char* name);
passedControlPoints()59 static unsigned passedControlPoints () { return _passedControlPoints; }
60 /** start outputting the trace independently of the first and last
61 * control point setting */
forceOutput()62 static void forceOutput() { _forced = true; }
63 /** stop outputting forced by startOutput */
stopOutput()64 static void stopOutput() { _forced = false; }
65 static bool canWatch;
66 private:
67 const char* _fun;
68 Tracer* _previous;
69
70 static void printStackRec (Tracer* current, ostream&, int& depth);
71 static void spaces(ostream& str,int number);
72
73 /** current trace point */
74 static Tracer* _current;
75 /** current depth */
76 static unsigned _depth;
77 /** description of the last control point (function name) */
78 static const char* _lastControlPoint;
79 /** total number of passed control points */
80 static unsigned _passedControlPoints;
81 /** kind of the last point */
82 static ControlPointKind _lastPointKind;
83 /** forced by startTrace */
84 static bool _forced;
85 static void controlPoint (const char*, ControlPointKind);
86 static void outputLastControlPoint (ostream& str);
87 public:
88 /* prints a message with indent in the of the same size as the current _depth */
89 template<class... A>
90 static void printDbg(A... msg);
91 };
92
93 template<class... As>
94 struct _printDbg {
95 void operator()(const As&... msg);
96 };
97
98 template<> struct _printDbg<>{
operator ()Debug::_printDbg99 void operator()() { }
100 };
101
102 template<class A, class... As> struct _printDbg<A, As...>{
operator ()Debug::_printDbg103 void operator()(const A& a, const As&... as) {
104 cout << a;
105 _printDbg<As...>{}(as...);
106 }
107 };
108
printDbg(A...msg)109 template<class... A> void Tracer::printDbg(A... msg)
110 {
111 for (unsigned i = 0; i< _depth; i++) {
112 cout << " ";
113 }
114 // cout << _lastControlPoint << ": ";
115 cout << _current->_fun << ": ";
116
117 _printDbg<A...>{}(msg...);
118 }
119
120
121 } // namespace Debug
122
123 # define AUX_CALL_(SEED,Fun) Debug::Tracer _tmp_##SEED##_(Fun);
124 # define AUX_CALL(SEED,Fun) AUX_CALL_(SEED,Fun)
125 # define CALL(Fun) AUX_CALL(__LINE__,Fun)
126 # define DBG(...) {\
127 std::cout << "[ debug ] " << __FILE__ << "@" << __LINE__ << ":";\
128 Debug::Tracer::printDbg(__VA_ARGS__); \
129 std::cout << std::endl; \
130 }
131 # define CALLC(Fun,check) if (check){ AUX_CALL(__LINE__,Fun) }
132 # define CONTROL(description) Debug::Tracer::controlPoint(description)
133 # define AFTER(number,command) \
134 if (Debug::Tracer::passedControlPoints() >= number) { command };
135 # define BETWEEN(number1,number2,command) \
136 if (Debug::Tracer::passedControlPoints() >= number1 && \
137 Debug::Tracer::passedControlPoints() <= number2) \
138 { command };
139
140 #else // ! VDEBUG
141 # define DBG(...) {}
142 # define CALL(Fun)
143 # define CALLC(Fun,check)
144 # define CONTROL(description)
145 #endif
146
147 #ifndef CALL
148 #error BLIN
149 #endif
150
151 #endif // Tracer
152