1 /********************************************************************
2 * AUTHORS: Trevor Hansen, Dan Liew
3 *
4 * BEGIN DATE: Augq, 2010
5 *
6 Permission is hereby granted, free of charge, to any person obtaining a copy
7 of this software and associated documentation files (the "Software"), to deal
8 in the Software without restriction, including without limitation the rights
9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
12
13 The above copyright notice and this permission notice shall be included in
14 all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
22 THE SOFTWARE.
23 ********************************************************************/
24
25 #include <iostream>
26 #include <cstdlib>
27 #include <cassert>
28 #include <cmath>
29 #include "stp/AST/AST.h"
30 #include "extlib-constbv/constantbv.h"
31
32 /*
33 * Generates random (a op b = c) triples to check that solver.
34 * Only for complicated instructions like modulus, remainder and divide.
35 */
36
37 using std::endl;
38 using std::cout;
39 using std::cerr;
40 using namespace BEEV;
41 using namespace CONSTANTBV;
42
43 int width = 64;
44 typedef uint64_t uns;
45 typedef int64_t sig;
46
47 const bool debug = false;
48
getUnsignedResult(uns a,Kind k,uns b)49 uns getUnsignedResult(uns a, Kind k, uns b)
50 {
51 uns gold;
52
53 if (BVMULT == k)
54 {
55 return a * b;
56 }
57 else if (BVMOD == k)
58 {
59 return a % b;
60 }
61 else if (BVDIV == k)
62 {
63 return a / b;
64 }else if (BVLEFTSHIFT == k)
65 {
66 return (b > (sizeof(a) * 8) ? 0 : a << b);
67 }
68 else if (BVRIGHTSHIFT == k)
69 {
70 return (b > (sizeof(a) * 8) ? 0 : a << b);
71 }
72 cerr << "not implemetned" << endl;
73 exit(2);
74
75 }
76
getSignedResult(sig a,Kind k,sig b)77 sig getSignedResult(sig a, Kind k, sig b)
78 {
79 sig gold;
80
81 if (SBVMOD == k)
82 {
83 sig Q_prime = (sig) (trunc((double) a / (double) b));
84 if ((a < 0) != (b < 0))
85 {
86 Q_prime = Q_prime - 1;
87 }
88
89 gold = a - Q_prime * b;
90 if (debug)
91 fprintf(stderr, "a=%d; b=%d; Q_prime=%d\n", a, b, Q_prime);
92 }
93 else if (SBVREM == k)
94 {
95 gold = a % b;
96 }
97 else if (SBVDIV == k)
98 {
99 gold = a / b;
100 }
101 else if (BVSRSHIFT == k)
102 {
103 return (b > (sizeof(a) * 8) ? 0 : a >> b);
104 }
105 else
106 {
107 cerr << "not implemetned" << endl;
108 exit(2);
109 }
110 return gold;
111
112 }
113
go(int count,uns a,uns b,uns result,const char * name)114 void go(int count, uns a, uns b, uns result, const char* name)
115 {
116 cout << ":extrafuns ((a" << count << " BitVec[" << width << "])) " << endl;
117 cout << ":extrafuns ((b" << count << " BitVec[" << width << "])) " << endl;
118 cout << ":extrafuns ((op" << count << " BitVec[" << width << "])) " << endl;
119
120 cout << ":assumption (= ";
121 cout << "(" << name << " ";
122 if ((rand() % 3) == 0)
123 cout << "a" << count << " ";
124 else
125 cout << "bv" << a << "[" << width << "] ";
126
127 if ((rand() % 3) == 0)
128 cout << "b" << count << " ";
129 else
130 cout << "bv" << b << "[" << width << "]";
131 cout << " ) ";
132
133 if ((rand() % 3) == 0)
134 cout << "op" << count << " ";
135 else
136 cout << "bv" << result << "[" << width << "]";
137
138 cout << ")" << endl;
139 }
140
testSolver(void)141 void testSolver(void)
142 {
143 cout << "(" << endl;
144 cout << "benchmark blah" << endl;
145 cout << ":logic QF_BV" << endl;
146 cout << ":source {automatically generated}" << endl;
147 cout << ":status sat" << endl;
148
149 uns a, b;
150 sig aS, bS;
151
152 do
153 {
154 a = rand();
155 b = rand();
156 aS = rand();
157 bS = rand();
158 } while (bS == 0 || b == 0);
159
160 switch (rand() % 9)
161 {
162 case 0:
163 go(0, a, b, getUnsignedResult(a, BVMULT, b), "bvmul");
164 break;
165 case 1:
166 go(1, a, b, getUnsignedResult(a, BVDIV, b), "bvudiv");
167 break;
168 case 2:
169 go(2, a, b, getUnsignedResult(a, BVMOD, b), "bvurem");
170 break;
171 case 3:
172 go(3, aS, bS, getSignedResult(aS, SBVDIV, bS), "bvsdiv");
173 break;
174 case 4:
175 go(4, aS, bS, getSignedResult(aS, SBVREM, bS), "bvsrem");
176 break;
177 case 5:
178 go(5, aS, bS, getSignedResult(aS, SBVMOD, bS), "bvsmod");
179 break;
180 case 6:
181 go(5, aS, bS, getUnsignedResult(aS, BVLEFTSHIFT, bS), "bvshl");
182 break;
183 case 7:
184 go(5, aS, bS, getUnsignedResult(aS, BVRIGHTSHIFT, bS), "bvshl");
185 break;
186 case 8:
187 go(5, aS, bS, getSignedResult(aS, BVSRSHIFT, bS), "bvshl");
188 break;
189
190
191 }
192 cout << ")" << endl;
193 }
194
main(int argc,char ** argv)195 int main(int argc, char**argv)
196 {
197 int nonce;
198 if (argc >= 2)
199 nonce = atoi(argv[1]);
200 else
201 nonce = 1;
202 int seed = time(0) * nonce;
203 if (debug)
204 {
205 cerr << "Seed = " << seed << endl;
206 }
207 srand(seed);
208
209 BitVector_Boot();
210
211 testSolver();
212
213 return 0;
214 }
215
216