1 
2 /*
3  * File UnitTesting.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 UnitTesting.hpp
21  * Defines macros for testing
22  */
23 
24 #ifndef __UnitTesting__
25 #define __UnitTesting__
26 
27 /**
28 
29 The way testing work is as follows.
30 
31 <ol>
32   <li> You should create a test file, say TestFile.cpp in the UnitTests directory of the Vampire
33 	tree. The test file must define <b>the test id</b> and one or more <b>test functions</b>.</li>
34 
35 	<li>Update the definition of VUT_OBJ in the Makefile by adding TestFile.o</li>
36 
37 	<li>To build the test with debugging use <span style='color:red'>make vtest</span>
38 	and without debugging <span style='color:red'>make vtest_rel</span>.</li>
39 
40 	<li>Call the test using <span style='color:red'>vtest test_id</span>. The call will execute
41 	all the test functions in the file.</li>
42 </ol>
43 The following macros should be used:
44 <dl>
45   <dt>UNIT_ID</dt>
46     <dd>must be defined in the beginning of each unit test .cpp file. Unit IDs must be unique,
47 		and must be valid variable names</dd>
48   <dt>UT_CREATE</dt>
49     <dd>must be called after the definition of UNIT_ID</dd>
50 	<dt>TEST_FUN(proc)</dt>
51 	  <dd>used to declare a function of the type void->void with the name proc.
52 		Due to the test framework, there is no need to use the CALL macro in the beginning of this
53 		function.</dd>
54 </dl>
55 
56 If all works well, tests should not produce any output. If test should fail,
57 an assertion must be violated or an exception thrown.
58 
59 A sample test file:
60 
61 <code><tt>
62 \#include "Debug/Assertion.hpp"<br/>
63 \#include "Test/UnitTesting.hpp"<br/>
64 <br/>
65 \#define UNIT_ID test1  //the UNIT_ID must be a valid variable name<br/>
66 UT_CREATE;<br/>
67 <br/>
68 TEST_FUN(commTest)<br/>
69 {<br/>
70 &nbsp;&nbsp;//there is no need to use the CALL macro at the beginning of a test function<br/>
71 <br/>
72 &nbsp;&nbsp;ASS_EQ(1+2,2+1);<br/>
73 }<br/>
74 <br/>
75 TEST_FUN(assocTest)<br/>
76 {<br/>
77 &nbsp;&nbsp;ASS_EQ(1+(2+3),(1+2)+3);<br/>
78 }<br/>
79 </tt></code>
80 To execute tests do the following:
81 
82 <ul>
83 	<li><b>vtest</b>	to run all tests</li>
84 	<li><b>vtest -l</b> to list all test IDs</li>
85 	<li><b>vtest test1</b> to run only test1</li>
86 </ul>
87 */
88 
89 #include <string.h>
90 #include <ostream>
91 
92 #include "Forwards.hpp"
93 
94 #include "Debug/Tracer.hpp"
95 
96 #include "Lib/List.hpp"
97 
98 namespace Test {
99 
100 using namespace std;
101 using namespace Lib;
102 
103 typedef void (*TestProc)();
104 
105 class TestUnit
106 {
107 public:
108   struct Test
109   {
TestTest::TestUnit::Test110     Test() {}
TestTest::TestUnit::Test111     Test(TestProc proc, const char* name) : proc(proc), name(name) {}
112 
113     TestProc proc;
114     const char* name;
115   };
116 
117   typedef List<Test> TestList;
118   typedef TestList::DestructiveIterator Iterator;
119 
120   TestUnit(const char* id);
121 
id()122   const char* id() { return _id; }
123 
addTest(TestProc proc,const char * name)124   void addTest(TestProc proc, const char* name)
125   { TestList::push(Test(proc, name), _tests); }
126 
127   Iterator getTests();
128 private:
129   const char* _id;
130 
131   TestList* _tests;
132 };
133 
134 struct TU_Aux_Test_Adder
135 {
TU_Aux_Test_AdderTest::TU_Aux_Test_Adder136   TU_Aux_Test_Adder(TestUnit& tu, TestProc proc, const char* name)
137   {
138     tu.addTest(proc, name);
139   }
140 };
141 
142 class UnitTesting
143 {
144 private:
145   typedef List<TestUnit*> TestUnitList;
146 public:
147   static UnitTesting* instance();
148 
149   /** Returns the test unit with the given id, if it exists or NULL otherwise. */
150   TestUnit* get(const char* unitId);
151 
152   /** Runs all tests of all existing test units
153    *
154    * returns true iff all tests were successfull.
155    */
156   bool runAllTests(ostream& out);
157   void printTestNames(ostream& out);
158 
add(TestUnit * tu)159   void add(TestUnit* tu)
160   { TestUnitList::push(tu, _units); }
161 
162   /** Runs all tests of the given test unit.
163    *
164    * returns true iff all tests of the unit were successfull.
165    */
166   bool runUnit(TestUnit* unit, ostream& out);
167 
168 private:
169   UnitTesting();
170   ~UnitTesting();
171 
172 
173   /** Runs a test as a single process and awaits its termination.
174    * This is to provide isolation when running multiple tests in one go.
175    *
176    *  returns true iff the test process exited with status code 0
177    */
178   bool spawnTest(TestProc proc);
179 
180   TestUnitList* _units;
181 };
182 
183 #define UT_AUX_NAME__(ID) _ut_aux_##ID##_
184 #define UT_AUX_NAME_(ID) UT_AUX_NAME__(ID)
185 #define UT_AUX_NAME UT_AUX_NAME_(UNIT_ID)
186 
187 #define UT_AUX_NAME_STR__(ID) #ID
188 #define UT_AUX_NAME_STR_(ID) UT_AUX_NAME_STR__(ID)
189 #define UT_AUX_NAME_STR UT_AUX_NAME_STR_(UNIT_ID)
190 
191 #define UT_AUX_ADDER_NAME__(ID,LINE,NAME) _ut_aux_adder_##ID##_##LINE##_##NAME##_
192 #define UT_AUX_ADDER_NAME_(ID,LINE,NAME) UT_AUX_ADDER_NAME__(ID,LINE,NAME)
193 #define UT_AUX_ADDER_NAME(NAME) UT_AUX_ADDER_NAME_(UNIT_ID, __LINE__,NAME)
194 
195 
196 #define UT_CREATE Test::TestUnit UT_AUX_NAME(UT_AUX_NAME_STR)
197 
198 // #define TEST_FUN_MULTI_PER_LINE(name, id_in_line)   \
199 //   void name(); \
200 //   Test::TU_Aux_Test_Adder _ut_aux_adder_##ID##_##LINE##_##id_in_line(UT_AUX_NAME,name,#name); \
201 //   void name()
202 
203 #define TEST_FUN(name)  void name(); \
204 			Test::TU_Aux_Test_Adder UT_AUX_ADDER_NAME(name)(UT_AUX_NAME,name,#name); \
205 			void name()
206 
207 }
208 
209 #endif // __RuntimeStatistics__
210