1 /********************************************************************
2 * AUTHORS: Vijay Ganesh, Trevor Hansen
3 *
4 * BEGIN DATE: November, 2005
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 "stp/AST/AST.h"
26 #include "stp/STPManager/STPManager.h"
27 #include "stp/Util/NodeIterator.h"
28
29 #if !defined(_MSC_VER)
30 // Needed for signal()
31 #include <unistd.h>
32 #endif
33
34 #include <sys/time.h>
35
36 namespace stp
37 {
38 using std::cout;
39 using std::cerr;
40 using std::endl;
41
42 THREAD_LOCAL uint64_t ASTInternal::node_uid_cntr = 0;
43
44 /****************************************************************
45 * Universal Helper Functions *
46 ****************************************************************/
47
48 // Sort ASTNodes by expression numbers
exprless(const ASTNode n1,const ASTNode n2)49 bool exprless(const ASTNode n1, const ASTNode n2)
50 {
51 return (n1.GetNodeNum() < n2.GetNodeNum());
52 }
53
54 // This is for sorting by arithmetic expressions (for
55 // combining like terms, etc.)
arithless(const ASTNode n1,const ASTNode n2)56 bool arithless(const ASTNode n1, const ASTNode n2)
57 {
58 Kind k1 = n1.GetKind();
59 Kind k2 = n2.GetKind();
60
61 if (n1 == n2)
62 {
63 // necessary for "strict weak ordering"
64 return false;
65 }
66 else if (BVCONST == k1 && BVCONST != k2)
67 {
68 // put consts first
69 return true;
70 }
71 else if (BVCONST != k1 && BVCONST == k2)
72 {
73 // put consts first
74 return false;
75 }
76 else if (SYMBOL == k1 && SYMBOL != k2)
77 {
78 // put symbols next
79 return true;
80 }
81 else if (SYMBOL != k1 && SYMBOL == k2)
82 {
83 // put symbols next
84 return false;
85 }
86 else
87 {
88 // otherwise, sort by exprnum (descendents will appear
89 // before ancestors).
90 return (n1.GetNodeNum() < n2.GetNodeNum());
91 }
92 }
93
94 // counts the number of reads. Shortcut when we get to the limit.
numberOfReadsLessThan(const ASTNode & n,std::unordered_set<int> & visited,int & soFar,const int limit)95 void numberOfReadsLessThan(const ASTNode& n, std::unordered_set<int>& visited,
96 int& soFar, const int limit)
97 {
98 if (n.isAtom())
99 return;
100
101 if (visited.find(n.GetNodeNum()) != visited.end())
102 return;
103
104 if (n.GetKind() == READ)
105 soFar++;
106
107 if (soFar > limit)
108 return;
109
110 visited.insert(n.GetNodeNum());
111
112 for (size_t i = 0; i < n.Degree(); i++)
113 numberOfReadsLessThan(n[i], visited, soFar, limit);
114 }
115
116 // True if the number of reads in "n" is less than "limit"
numberOfReadsLessThan(const ASTNode & n,int limit)117 bool numberOfReadsLessThan(const ASTNode& n, int limit)
118 {
119 std::unordered_set<int> visited;
120 int reads = 0;
121 numberOfReadsLessThan(n, visited, reads, limit);
122 return reads < limit;
123 }
124
125 // True if any descendants are arrays.
containsArrayOps(const ASTNode & n,STPMgr * mgr)126 bool containsArrayOps(const ASTNode& n, STPMgr* mgr)
127 {
128
129 NodeIterator ni(n, mgr->ASTUndefined, *mgr);
130 ASTNode current;
131 while ((current = ni.next()) != ni.end())
132 if (current.GetIndexWidth() > 0)
133 return true;
134
135 return false;
136 }
137
isCommutative(const Kind k)138 bool isCommutative(const Kind k)
139 {
140 switch (k)
141 {
142 case BVOR:
143 case BVAND:
144 case BVXOR:
145 case BVNAND:
146 case BVNOR:
147 case BVXNOR:
148 case BVPLUS:
149 case BVMULT:
150 case EQ:
151 case AND:
152 case OR:
153 case NAND:
154 case NOR:
155 case XOR:
156 case IFF:
157 case BVNOT:
158 case NOT:
159 case BVUMINUS:
160 return true;
161 default:
162 return false;
163 }
164
165 return false;
166 }
167
FatalError(const char * str,const ASTNode & a,int w)168 void FatalError(const char* str, const ASTNode& a, int w)
169 {
170 if (a.GetKind() != UNDEFINED)
171 {
172 cerr << "Fatal Error: " << str << endl << a << endl;
173 cerr << w << endl;
174 }
175 else
176 {
177 cerr << "Fatal Error: " << str << endl;
178 cerr << w << endl;
179 }
180 if (vc_error_hdlr)
181 {
182 vc_error_hdlr(str);
183 }
184 abort();
185 }
186
FatalError(const char * str)187 void FatalError(const char* str)
188 {
189 cerr << "Fatal Error: " << str << endl;
190 if (vc_error_hdlr)
191 {
192 vc_error_hdlr(str);
193 }
194 abort();
195 }
196
SortByExprNum(ASTVec & v)197 void SortByExprNum(ASTVec& v)
198 {
199 sort(v.begin(), v.end(), exprless);
200 }
201
SortByArith(ASTVec & v)202 void SortByArith(ASTVec& v)
203 {
204 sort(v.begin(), v.end(), arithless);
205 }
206
isAtomic(Kind kind)207 bool isAtomic(Kind kind)
208 {
209 if (TRUE == kind || FALSE == kind || EQ == kind || BVLT == kind ||
210 BVLE == kind || BVGT == kind || BVGE == kind || BVSLT == kind ||
211 BVSLE == kind || BVSGT == kind || BVSGE == kind || SYMBOL == kind ||
212 BOOLEXTRACT == kind)
213 return true;
214 return false;
215 }
216
217 // If there is a lot of sharing in the graph, this will take a long
218 // time. it doesn't mark subgraphs as already having been
219 // typechecked.
BVTypeCheckRecursive(const ASTNode & n)220 bool BVTypeCheckRecursive(const ASTNode& n)
221 {
222 const ASTVec& c = n.GetChildren();
223
224 if (!BVTypeCheck(n))
225 {
226 return false;
227 }
228
229 for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend;
230 it++)
231 {
232 if (!BVTypeCheckRecursive(*it))
233 {
234 return false;
235 }
236 }
237
238 return true;
239 }
240
buildListOfSymbols(const ASTNode & n,ASTNodeSet & visited,ASTNodeSet & symbols)241 void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited,
242 ASTNodeSet& symbols)
243 {
244 if (visited.find(n) != visited.end())
245 return; // already visited.
246
247 visited.insert(n);
248
249 if (n.GetKind() == SYMBOL)
250 {
251 symbols.insert(n);
252 }
253
254 for (unsigned i = 0; i < n.GetChildren().size(); i++)
255 buildListOfSymbols(n[i], visited, symbols);
256 }
257
checkChildrenAreBV(const ASTVec & v,const ASTNode & n)258 void checkChildrenAreBV(const ASTVec& v, const ASTNode& n)
259 {
260 for (ASTVec::const_iterator it = v.begin(), itend = v.end(); it != itend;
261 it++)
262 {
263 if (BITVECTOR_TYPE != it->GetType())
264 {
265 cerr << "The type is: " << it->GetType() << endl;
266 FatalError(
267 "BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors\n", n);
268 }
269 }
270 }
271
272 /* Maintains a set of nodes that have already been seen. So that deeply shared
273 * AND,OR operations are not
274 * flattened multiple times.
275 */
FlattenKindNoDuplicates(const Kind k,const ASTVec & children,ASTVec & flat_children,ASTNodeSet & alreadyFlattened)276 void FlattenKindNoDuplicates(const Kind k, const ASTVec& children,
277 ASTVec& flat_children,
278 ASTNodeSet& alreadyFlattened)
279 {
280 const ASTVec::const_iterator ch_end = children.end();
281 for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)
282 {
283 const Kind ck = it->GetKind();
284 if (k == ck)
285 {
286 if (alreadyFlattened.find(*it) == alreadyFlattened.end())
287 {
288 alreadyFlattened.insert(*it);
289 FlattenKindNoDuplicates(k, it->GetChildren(), flat_children,
290 alreadyFlattened);
291 }
292 }
293 else
294 {
295 flat_children.push_back(*it);
296 }
297 }
298 }
299
FlattenKind(const Kind k,const ASTVec & children,ASTVec & flat_children)300 void FlattenKind(const Kind k, const ASTVec& children, ASTVec& flat_children)
301 {
302 ASTVec::const_iterator ch_end = children.end();
303 for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)
304 {
305 Kind ck = it->GetKind();
306 if (k == ck)
307 {
308 FlattenKind(k, it->GetChildren(), flat_children);
309 }
310 else
311 {
312 flat_children.push_back(*it);
313 }
314 }
315 }
316
317 // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...)
FlattenKind(Kind k,const ASTVec & children)318 ASTVec FlattenKind(Kind k, const ASTVec& children)
319 {
320 ASTVec flat_children;
321 if (k == OR || k == BVOR || k == BVAND || k == AND)
322 {
323 ASTNodeSet alreadyFlattened;
324 FlattenKindNoDuplicates(k, children, flat_children, alreadyFlattened);
325 }
326 else
327 {
328 FlattenKind(k, children, flat_children);
329 }
330
331 return flat_children;
332 }
333
BVTypeCheck_term_kind(const ASTNode & n,const Kind & k)334 bool BVTypeCheck_term_kind(const ASTNode& n, const Kind& k)
335 {
336 // The children of bitvector terms are in turn bitvectors.
337 const ASTVec& v = n.GetChildren();
338
339 switch (k)
340 {
341 case BVCONST:
342 if (BITVECTOR_TYPE != n.GetType())
343 FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",
344 n);
345 break;
346
347 case SYMBOL:
348 return true;
349
350 case ITE:
351 if (n.Degree() != 3)
352 FatalError("BVTypeCheck: should have exactly 3 args\n", n);
353 if (BOOLEAN_TYPE != n[0].GetType() || (n[1].GetType() != n[2].GetType()))
354 FatalError("BVTypeCheck: The term t does not typecheck, where t = \n",
355 n);
356 if (n[1].GetValueWidth() != n[2].GetValueWidth())
357 FatalError("BVTypeCheck: length of THENbranch != length of "
358 "ELSEbranch in the term t = \n",
359 n);
360 if (n[1].GetIndexWidth() != n[2].GetIndexWidth())
361 FatalError("BVTypeCheck: length of THENbranch != length of "
362 "ELSEbranch in the term t = \n",
363 n);
364 break;
365
366 case READ:
367 if (n.GetChildren().size() != 2)
368 FatalError("2 params to read.");
369 if (n[0].GetIndexWidth() != n[1].GetValueWidth())
370 {
371 cerr << "Length of indexwidth of array: " << n[0]
372 << " is : " << n[0].GetIndexWidth() << endl;
373 cerr << "Length of the actual index is: " << n[1]
374 << " is : " << n[1].GetValueWidth() << endl;
375 FatalError("BVTypeCheck: length of indexwidth of array != length of "
376 "actual index in the term t = \n",
377 n);
378 }
379 if (ARRAY_TYPE != n[0].GetType())
380 FatalError("First parameter to read should be an array", n[0]);
381 if (BITVECTOR_TYPE != n[1].GetType())
382 FatalError("Second parameter to read should be a bitvector", n[1]);
383 break;
384
385 case WRITE:
386 if (n.GetChildren().size() != 3)
387 FatalError("3 params to write.");
388 if (n[0].GetIndexWidth() != n[1].GetValueWidth())
389 FatalError("BVTypeCheck: length of indexwidth of array != length of "
390 "actual index in the term t = \n",
391 n);
392 if (n[0].GetValueWidth() != n[2].GetValueWidth())
393 FatalError("BVTypeCheck: valuewidth of array != length of actual "
394 "value in the term t = \n",
395 n);
396 if (ARRAY_TYPE != n[0].GetType())
397 FatalError("First parameter to read should be an array", n[0]);
398 if (BITVECTOR_TYPE != n[1].GetType())
399 FatalError("Second parameter to read should be a bitvector", n[1]);
400 if (BITVECTOR_TYPE != n[2].GetType())
401 FatalError("Third parameter to read should be a bitvector", n[2]);
402 break;
403
404 case BVDIV:
405 case BVMOD:
406 case BVSUB:
407
408 case SBVDIV:
409 case SBVREM:
410 case SBVMOD:
411
412 case BVLEFTSHIFT:
413 case BVRIGHTSHIFT:
414 case BVSRSHIFT:
415 if (n.Degree() != 2)
416 FatalError("BVTypeCheck: should have exactly 2 args\n", n);
417 // run on.
418 case BVOR:
419 case BVAND:
420 case BVXOR:
421 case BVNOR:
422 case BVNAND:
423 case BVXNOR:
424
425 case BVPLUS:
426 case BVMULT:
427 {
428 if (!(v.size() >= 2))
429 FatalError("BVTypeCheck:bitwise Booleans and BV arith operators must "
430 "have at least two arguments\n",
431 n);
432
433 unsigned int width = n.GetValueWidth();
434 for (ASTVec::const_iterator it = v.begin(), itend = v.end(); it != itend;
435 it++)
436 {
437 if (width != it->GetValueWidth())
438 {
439 cerr << "BVTypeCheck:Operands of bitwise-Booleans and BV arith "
440 "operators must be of equal length\n";
441 cerr << n << endl;
442 cerr << "width of term:" << width << endl;
443 cerr << "width of offending operand:" << it->GetValueWidth() << endl;
444 FatalError("BVTypeCheck:Offending operand:\n", *it);
445 }
446 if (BITVECTOR_TYPE != it->GetType())
447 FatalError("BVTypeCheck: ChildNodes of bitvector-terms must be "
448 "bitvectors\n",
449 n);
450 }
451 break;
452 }
453 case BVSX:
454 case BVZX:
455 // in BVSX(n[0],len), the length of the BVSX term must be
456 // greater than the length of n[0]
457 if (n[0].GetValueWidth() > n.GetValueWidth())
458 {
459 FatalError("BVTypeCheck: BV[SZ]X(t,bv[sz]x_len) : length of 't' must "
460 "be <= bv[sz]x_len\n",
461 n);
462 }
463 if ((v.size() != 2))
464 FatalError("BVTypeCheck:BV[SZ]X must have two arguments. The second "
465 "is the new width\n",
466 n);
467 break;
468
469 case BVCONCAT:
470 checkChildrenAreBV(v, n);
471 if (n.Degree() != 2)
472 FatalError("BVTypeCheck: should have exactly 2 args\n", n);
473 if (n.GetValueWidth() != n[0].GetValueWidth() + n[1].GetValueWidth())
474 FatalError("BVTypeCheck:BVCONCAT: lengths do not add up\n", n);
475 break;
476
477 case BVUMINUS:
478 case BVNOT:
479 checkChildrenAreBV(v, n);
480 if (n.Degree() != 1)
481 FatalError("BVTypeCheck: should have exactly 1 args\n", n);
482 if (n.GetValueWidth() != n[0].GetValueWidth())
483 FatalError("BVTypeCheck: should have same value width\n", n);
484 break;
485
486 case BVEXTRACT:
487 checkChildrenAreBV(v, n);
488 if (n.Degree() != 3)
489 FatalError("BVTypeCheck: should have exactly 3 args\n", n);
490 if (!(BVCONST == n[1].GetKind() && BVCONST == n[2].GetKind()))
491 FatalError("BVTypeCheck: indices should be BVCONST\n", n);
492 if (n.GetValueWidth() !=
493 n[1].GetUnsignedConst() - n[2].GetUnsignedConst() + 1)
494 FatalError("BVTypeCheck: length mismatch\n", n);
495 if (n[1].GetUnsignedConst() >= n[0].GetValueWidth())
496 FatalError("BVTypeCheck: Top index of select is greater or equal to "
497 "the bitwidth.\n",
498 n);
499 break;
500
501 default:
502 cerr << _kind_names[k];
503 FatalError("No type checking for type");
504 break;
505 }
506 return true;
507 }
508
BVTypeCheck_nonterm_kind(const ASTNode & n,const Kind & k)509 bool BVTypeCheck_nonterm_kind(const ASTNode& n, const Kind& k)
510 {
511 // The children of bitvector terms are in turn bitvectors.
512 const ASTVec& v = n.GetChildren();
513
514 if (!(is_Form_kind(k) && BOOLEAN_TYPE == n.GetType()))
515 FatalError("BVTypeCheck: not a formula:", n);
516
517 switch (k)
518 {
519 case TRUE:
520 case FALSE:
521 case SYMBOL:
522 return true;
523
524 case BOOLEXTRACT:
525 checkChildrenAreBV(v, n);
526
527 if (n.Degree() != 2)
528 FatalError("BVTypeCheck: should have exactly 2 args\n", n);
529 if (!(BVCONST == n[1].GetKind()))
530 FatalError("BVTypeCheck: index should be BVCONST\n", n);
531 if (n[1].GetUnsignedConst() >= n[0].GetValueWidth())
532 {
533 FatalError("BVTypeCheck: index is greater or equal to the bitwidth.\n",
534 n);
535 }
536 break;
537
538 case PARAMBOOL:
539 if (2 != n.Degree())
540 {
541 FatalError(
542 "BVTypeCheck: PARAMBOOL formula can have exactly two childNodes",
543 n);
544 }
545 break;
546
547 case EQ:
548 if (n.Degree() != 2)
549 FatalError("BVTypeCheck: should have exactly 2 args\n", n);
550
551 if (!(n[0].GetValueWidth() == n[1].GetValueWidth() &&
552 n[0].GetIndexWidth() == n[1].GetIndexWidth()))
553 {
554 cerr << "valuewidth of lhs of EQ: " << n[0].GetValueWidth() << endl;
555 cerr << "valuewidth of rhs of EQ: " << n[1].GetValueWidth() << endl;
556 cerr << "indexwidth of lhs of EQ: " << n[0].GetIndexWidth() << endl;
557 cerr << "indexwidth of rhs of EQ: " << n[1].GetIndexWidth() << endl;
558 FatalError(
559 "BVTypeCheck: terms in atomic formulas must be of equal length", n);
560 }
561 break;
562
563 case BVLT:
564 case BVLE:
565 case BVGT:
566 case BVGE:
567 case BVSLT:
568 case BVSLE:
569 case BVSGT:
570 case BVSGE:
571 if (n.Degree() != 2)
572 FatalError("BVTypeCheck: should have exactly 2 args\n", n);
573 if (BITVECTOR_TYPE != n[0].GetType() && BITVECTOR_TYPE != n[1].GetType())
574 {
575 FatalError("BVTypeCheck: terms in atomic formulas must be bitvectors",
576 n);
577 }
578 if (n[0].GetValueWidth() != n[1].GetValueWidth())
579 FatalError(
580 "BVTypeCheck: terms in atomic formulas must be of equal length", n);
581 if (n[0].GetIndexWidth() != n[1].GetIndexWidth())
582 {
583 FatalError(
584 "BVTypeCheck: terms in atomic formulas must be of equal length", n);
585 }
586 break;
587
588 case NOT:
589 if (1 != n.Degree())
590 {
591 FatalError("BVTypeCheck: NOT formula can have exactly one childNode",
592 n);
593 }
594 assert(n.GetNodeNum() == n[0].GetNodeNum() + 1);
595 break;
596
597 case AND:
598 case OR:
599 case XOR:
600 case NAND:
601 case NOR:
602 if (2 > n.Degree())
603 {
604 FatalError("BVTypeCheck: AND/OR/XOR/NAND/NOR: must have atleast 2 "
605 "ChildNodes",
606 n);
607 }
608 break;
609
610 case IFF:
611 case IMPLIES:
612 if (2 != n.Degree())
613 {
614 FatalError("BVTypeCheck:IFF/IMPLIES must have exactly 2 ChildNodes", n);
615 }
616 break;
617
618 case ITE:
619 if (3 != n.Degree())
620 FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes", n);
621 break;
622
623 default:
624 FatalError("BVTypeCheck: Unrecognized kind: ");
625 break;
626 }
627 return true;
628 }
629
630 /* FUNCTION: Typechecker for terms and formulas
631 *
632 * TypeChecker: Assumes that the immediate Children of the input
633 * ASTNode have been typechecked. This function is suitable in
634 * scenarios like where you are building the ASTNode Tree, and you
635 * typecheck as you go along. It is not suitable as a general
636 * typechecker.
637 *
638 * If this returns, this ALWAYS returns true. If there is an error it
639 * will call FatalError() and abort.
640 */
BVTypeCheck(const ASTNode & n)641 bool BVTypeCheck(const ASTNode& n)
642 {
643 const Kind k = n.GetKind();
644
645 if (is_Term_kind(k))
646 {
647 return BVTypeCheck_term_kind(n, k);
648 }
649 else
650 {
651 return BVTypeCheck_nonterm_kind(n, k);
652 }
653 }
654
getCurrentTime()655 long getCurrentTime()
656 {
657 timeval t;
658 gettimeofday(&t, NULL);
659 return (1000 * t.tv_sec) + (t.tv_usec / 1000);
660 }
661
662 } // end of namespace
663