1 /* Boolector: Satisfiablity Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "btoribv.hh"
10
11 #include <cstdarg>
12 #include <cstdio>
13 #include <cstdlib>
14 #include <cstring>
15
16 extern "C" {
17 #include <sys/stat.h>
18 #include <sys/types.h>
19 #include <unistd.h>
20 };
21
22 #include <iostream>
23 #include <map>
24 #include <string>
25 #include <vector>
26
27 using namespace std;
28
29 struct Var
30 {
31 string name;
32 unsigned width;
VarVar33 Var () {}
VarVar34 Var (string n, int w) : name (n), width (w) {}
35 };
36
37 struct Assertion
38 {
39 string name;
40 int nfalsified;
AssertionAssertion41 Assertion (string n) : name (n), nfalsified (0) {}
42 };
43
44 static BtorIBV* ibvm;
45
46 static map<string, unsigned> symtab;
47 static map<unsigned, Var> idtab;
48 static vector<unsigned> vartab;
49
50 static int lineno = 1;
51 static FILE* input = stdin;
52 static const char* input_name = "<stdin>";
53 static int close_input;
54
55 static char *line, *nts;
56 static int szline, nline;
57
58 static vector<Assertion> assertions;
59 static int nfalsified;
60
61 static struct
62 {
63 int addAssertion;
64 int addAssignment;
65 int addAssumption;
66 int addBitAnd;
67 int addBitNot;
68 int addBitOr;
69 int addBitXor;
70 int addCase;
71 int addConcat;
72 int addCondition;
73 int addConstant;
74 int addDiv;
75 int addEqual;
76 int addLessThan;
77 int addLessEqual;
78 int addGreaterThan;
79 int addGreaterEqual;
80 int addLogicalAnd;
81 int addLogicalNot;
82 int addLogicalOr;
83 int addLShift;
84 int addLShiftNonConst;
85 int addMod;
86 int addMul;
87 int addNonState;
88 int addRangeName;
89 int addReplicate;
90 int addRShift;
91 int addRShiftNonConst;
92 int addSignExtension;
93 int addState;
94 int addSub;
95 int addSum;
96 int addVariable;
97 int addZeroExtension;
98
99 } stats;
100
101 static void
err(const char * fmt,...)102 err (const char* fmt, ...)
103 {
104 va_list ap;
105 fputs ("*** btorimc: ", stderr);
106 va_start (ap, fmt);
107 vfprintf (stderr, fmt, ap);
108 va_end (ap);
109 fputc ('\n', stderr);
110 fflush (stderr);
111 exit (1);
112 }
113
114 static int verbosity;
115
116 static void
msg(const char * fmt,...)117 msg (const char* fmt, ...)
118 {
119 va_list ap;
120 if (!verbosity) return;
121 fputs ("[btorimc] ", stdout);
122 va_start (ap, fmt);
123 vprintf (fmt, ap);
124 va_end (ap);
125 fputc ('\n', stdout);
126 fflush (stdout);
127 }
128
129 static void
perr(const char * fmt,...)130 perr (const char* fmt, ...)
131 {
132 va_list ap;
133 fprintf (stderr, "%s:%d: ", input_name, lineno);
134 va_start (ap, fmt);
135 vfprintf (stderr, fmt, ap);
136 va_end (ap);
137 fputc ('\n', stderr);
138 fflush (stderr);
139 exit (1);
140 }
141
142 static void
pushch(int ch)143 pushch (int ch)
144 {
145 if (nline >= szline)
146 {
147 szline = szline ? 2 * szline : 1;
148 line = (char*) realloc (line, szline);
149 }
150 line[nline++] = ch;
151 }
152
153 static bool
read_line()154 read_line ()
155 {
156 nline = 0;
157 int ch;
158 while ((ch = getc (input)) != '\n')
159 {
160 // if (ch == ' ' || ch == '\t' || ch == '\r') continue;
161 if (ch == EOF)
162 {
163 if (nline) perr ("unexpected end-of-file");
164 if (line) free (line);
165 #if 0 // TODO print stats
166 if (stats.vars) msg ("parsed %d variables", stats.vars);
167 if (stats.rangenames) msg ("parsed %d range names", stats.rangenames);
168 #endif
169 return false;
170 }
171 pushch (ch);
172 }
173 pushch (0);
174 return true;
175 }
176
177 static int
str_to_id_or_number(const char * s)178 str_to_id_or_number (const char* s)
179 {
180 return atoi ((s[0] == 'i' && s[1] == 'd' && s[2] == '=') ? s + 3 : s);
181 }
182
183 #define CHKARGS(EXPECTED) \
184 do \
185 { \
186 if (EXPECTED != size - 1) \
187 perr ("operator '%s' expected exactly %d arguments but got %d", \
188 op, \
189 EXPECTED, \
190 size - 1); \
191 } while (0)
192
193 #define CHKIDUNUSED(ID) \
194 do \
195 { \
196 if (idtab.find (ID) != idtab.end ()) perr ("id %u already used", ID); \
197 } while (0)
198
199 #define CHKID(ID) \
200 do \
201 { \
202 if (idtab.find (ID) == idtab.end ()) perr ("id %u undefined", ID); \
203 } while (0)
204
205 #define CHKSYMUNUSED(SYM) \
206 do \
207 { \
208 if (symtab.find (SYM) != symtab.end ()) \
209 perr ("symbol '%s' already used", SYM.c_str ()); \
210 } while (0)
211
212 #define N(I) \
213 (assert ((I) < size), (unsigned) str_to_id_or_number (toks[I].c_str ()))
214
215 #define T(I) (assert ((I) < size), toks[I])
216
217 #define CHKBIT(SYM, B) \
218 do \
219 { \
220 if (symtab.find (SYM) == symtab.end ()) \
221 perr ("symbol '%s' undefined", (SYM).c_str ()); \
222 Var& V = idtab[symtab[(SYM)]]; \
223 if ((B) >= V.width) perr ("BIT %u >= width of '%s'", (B), (SYM).c_str ()); \
224 } while (0)
225
226 #define BIT(NAME, SYM, B) \
227 CHKBIT (SYM, B); \
228 BitVector::Bit NAME (symtab[(SYM)], B)
229
230 #define CHKRANGE(SYM, MSB, LSB) \
231 do \
232 { \
233 if (symtab.find (SYM) == symtab.end ()) \
234 perr ("symbol '%s' undefined", (SYM).c_str ()); \
235 if ((MSB) < (LSB)) perr ("MSB %u < LSB %u", (MSB), (LSB)); \
236 Var& V = idtab[symtab[(SYM)]]; \
237 if ((MSB) >= V.width) \
238 perr ("MSB %u >= width of '%s'", (MSB), (SYM).c_str ()); \
239 } while (0)
240
241 #define RANGE(NAME, SYM, MSB, LSB) \
242 CHKRANGE (SYM, MSB, LSB); \
243 BitVector::BitRange NAME (symtab[(SYM)], MSB, LSB)
244
245 #define CHKRANGESAMEWIDTH(RANGE0, RANGE1) \
246 do \
247 { \
248 if (RANGE0.getWidth () != RANGE1.getWidth ()) \
249 perr ("range [%u:%u] and [%u:%u] do not match", \
250 RANGE0.m_nMsb, \
251 RANGE0.m_nLsb, \
252 RANGE1.m_nMsb, \
253 RANGE1.m_nLsb); \
254 } while (0)
255
256 #define UNARY(NAME) \
257 (!strcmp (op, #NAME)) do \
258 { \
259 CHKARGS (6); \
260 RANGE (c, T (1), N (2), N (3)); \
261 RANGE (n, T (4), N (5), N (6)); \
262 CHKRANGESAMEWIDTH (c, n); \
263 ibvm->NAME (c, n); \
264 stats.NAME++; \
265 } \
266 while (0)
267
268 #define EXTEND(NAME) \
269 (!strcmp (op, #NAME)) do \
270 { \
271 CHKARGS (6); \
272 RANGE (c, T (1), N (2), N (3)); \
273 RANGE (n, T (4), N (5), N (6)); \
274 if (c.getWidth () < n.getWidth ()) \
275 perr ("range [%u:%u] smaller than range [%u:%u] ", \
276 c.m_nMsb, \
277 c.m_nLsb, \
278 n.m_nMsb, \
279 n.m_nLsb); \
280 ibvm->NAME (c, n); \
281 stats.NAME++; \
282 } \
283 while (0)
284
285 #define BINARY(NAME) \
286 (!strcmp (op, #NAME)) do \
287 { \
288 CHKARGS (9); \
289 RANGE (c, T (1), N (2), N (3)); \
290 RANGE (a, T (4), N (5), N (6)); \
291 RANGE (b, T (7), N (8), N (9)); \
292 CHKRANGESAMEWIDTH (c, a); \
293 CHKRANGESAMEWIDTH (c, b); \
294 ibvm->NAME (c, a, b); \
295 stats.NAME++; \
296 } \
297 while (0)
298
299 #define UNARYARG(NAME) \
300 (!strcmp (op, #NAME)) do \
301 { \
302 CHKARGS (7); \
303 RANGE (c, T (1), N (2), N (3)); \
304 RANGE (n, T (4), N (5), N (6)); \
305 CHKRANGESAMEWIDTH (c, n); \
306 unsigned arg = N (7); \
307 ibvm->NAME (c, n, arg); \
308 stats.NAME++; \
309 } \
310 while (0)
311
312 #define PRED1(NAME) \
313 (!strcmp (op, #NAME)) do \
314 { \
315 CHKARGS (5); \
316 RANGE (c, T (1), N (2), N (2)); \
317 RANGE (a, T (3), N (4), N (5)); \
318 assert (c.getWidth () == 1); \
319 ibvm->NAME (c, a); \
320 stats.NAME++; \
321 } \
322 while (0)
323
324 #define PRED2(NAME) \
325 (!strcmp (op, #NAME)) do \
326 { \
327 CHKARGS (8); \
328 RANGE (c, T (1), N (2), N (2)); \
329 RANGE (a, T (3), N (4), N (5)); \
330 RANGE (b, T (6), N (7), N (8)); \
331 assert (c.getWidth () == 1); \
332 CHKRANGESAMEWIDTH (a, b); \
333 ibvm->NAME (c, a, b); \
334 stats.NAME++; \
335 } \
336 while (0)
337
338 static const char*
firstok()339 firstok ()
340 {
341 for (nts = line; *nts && *nts != '('; nts++)
342 ;
343 if (!*nts) return 0;
344 assert (*nts == '(');
345 *nts++ = 0;
346 return line;
347 }
348
349 static bool
myisspace(int ch)350 myisspace (int ch)
351 {
352 if (ch == ' ') return 1;
353 if (ch == '\t') return 1;
354 if (ch == '\n') return 1;
355 if (ch == '\r') return 1;
356 return 0;
357 }
358
359 static const char*
nextok()360 nextok ()
361 {
362 const char* res;
363 int open;
364 if (nts >= line + nline) return 0;
365 while (myisspace (*nts)) nts++;
366 if (!*nts) return 0;
367 res = nts;
368 open = 0;
369 for (;;)
370 {
371 int ch = *nts;
372 if (!ch)
373 perr ("unexpected end-of-line");
374 else if (ch == '\\' && !*++nts)
375 perr ("unexpected end-of-line after '\\'");
376 else if (ch == '(')
377 open++, assert (open > 0);
378 else if (ch == ',' && !open)
379 break;
380 else if (ch == ')')
381 {
382 if (open > 0)
383 open--;
384 else
385 {
386 assert (!open);
387 if (nts[1]) perr ("trailing characters after last ')'");
388 break;
389 }
390 }
391 nts++;
392 }
393 *nts++ = 0;
394 char* p = nts - 2;
395 while (p >= res && myisspace (*p)) *p-- = 0;
396 return *res ? res : 0;
397 }
398
399 static void
parse_line()400 parse_line ()
401 {
402 const char* str;
403 vector<string> toks;
404 char* p;
405 if (line[0] == '#' || line[0] == ';') return;
406 for (p = line; *p; p++)
407 ;
408 while (p > line && myisspace (p[-1])) *--p = 0;
409 #if 0
410 if (p == line) perr ("empty line");
411 #else
412 if (p == line)
413 {
414 msg ("empty line");
415 return;
416 }
417 #endif
418 if (p[-1] != ')') perr ("line does not end with ')'");
419 if (!(str = firstok ())) perr ("'(' missing");
420 toks.push_back (string (str));
421 while ((str = nextok ())) toks.push_back (string (str));
422 if (verbosity >= 3)
423 {
424 printf ("[btorimc] line %d:", lineno);
425 for (vector<string>::const_iterator it = toks.begin (); it != toks.end ();
426 it++)
427 {
428 printf (" %s", (*it).c_str ());
429 }
430 printf ("\n");
431 }
432 size_t size = toks.size ();
433 assert (size > 0);
434 const char* op = toks[0].c_str ();
435 if (!strcmp (op, "addVariable"))
436 {
437 if (size != 5 && size != 7 && size != 8)
438 perr ("operator 'addVariable' expected 4, 6 or 7 arguments but got %d",
439 size - 1);
440 string sym = T (2);
441 unsigned id = N (1);
442 CHKIDUNUSED (id);
443 CHKSYMUNUSED (sym);
444 unsigned width = N (3);
445 if (width <= 0) perr ("expected positive width but got %u", width);
446 symtab[sym] = id;
447 Var v (sym, width);
448 idtab[id] = Var (sym, width);
449 stats.addVariable++;
450 if (size == 5)
451 ibvm->addVariableOld (id,
452 sym,
453 width,
454 (bool) N (4),
455 (bool) 0,
456 (bool) 0,
457 (BitVector::DirectionKind) 0);
458 else if (size == 8)
459 ibvm->addVariableOld (id,
460 sym,
461 width,
462 (bool) N (4),
463 (bool) N (5),
464 (bool) N (6),
465 (BitVector::DirectionKind) N (7));
466 else
467 ibvm->addVariable (id,
468 sym,
469 width,
470 (bool) N (4),
471 (BitVector::BvVariableSource) N (5),
472 (BitVector::DirectionKind) N (6));
473 vartab.push_back (id);
474 }
475 else if (!strcmp (op, "addRangeName"))
476 {
477 CHKARGS (6);
478 RANGE (range, T (1), N (2), N (3));
479 unsigned msb = N (5), lsb = N (6);
480 if (msb < lsb) perr ("MSB %u < LSB %u", msb, lsb);
481 ibvm->addRangeName (range, T (4), msb, lsb);
482 stats.addRangeName++;
483 }
484 else if (!strcmp (op, "addState"))
485 {
486 CHKARGS (9);
487 RANGE (n, T (1), N (2), N (3));
488 bool undeclared = (T (4) == "undeclared");
489 RANGE (next, T (7), N (8), N (9));
490 CHKRANGESAMEWIDTH (n, next);
491 if (!undeclared) CHKRANGE (T (4), N (5), N (6));
492 BitVector::BitRange init (undeclared ? 0 : symtab[T (4)],
493 undeclared ? 0 : N (5),
494 undeclared ? 0 : N (6));
495 if (!undeclared) CHKRANGESAMEWIDTH (n, init);
496 ibvm->addState (n, init, next);
497 stats.addState++;
498 }
499 else if (!strcmp (op, "addConstant"))
500 {
501 CHKARGS (3);
502 unsigned id = N (1);
503 CHKIDUNUSED (id);
504 unsigned width = N (3);
505 if (T (2).size () != width)
506 perr ("constant string '%s' does not match width %u",
507 T (2).c_str (),
508 width);
509 idtab[id] = Var (T (2), width);
510 {
511 // TODO: hack to get 'LSD' example through ...
512 char buf[20];
513 sprintf (buf, "%u", id);
514 string sym (buf);
515 symtab["b0_v" + sym] = id;
516 symtab["b1_v" + sym] = id;
517 }
518 {
519 // TODO: hack to get 'regtoy' examples through ...
520 char buf[20];
521 sprintf (buf, "%u", id);
522 string sym = string ("const(") + T (2) + ")";
523 symtab[sym] = id;
524 }
525 symtab[T (2)] = id;
526 ibvm->addConstant (id, T (2), width);
527 stats.addConstant++;
528 }
529 else if (!strcmp (op, "addCondition"))
530 {
531 CHKARGS (12);
532 RANGE (n, T (1), N (2), N (3));
533 RANGE (c, T (4), N (5), N (6));
534 RANGE (t, T (7), N (8), N (9));
535 RANGE (e, T (10), N (11), N (12));
536 CHKRANGESAMEWIDTH (n, t);
537 CHKRANGESAMEWIDTH (n, e);
538 if (c.getWidth () != 1) CHKRANGESAMEWIDTH (n, c);
539 ibvm->addCondition (n, c, t, e);
540 stats.addCondition++;
541 }
542 else if (!strcmp (op, "addCase"))
543 {
544 ADDCASE:
545 if (size < 5) perr ("non enough arguments for 'addCase'");
546 RANGE (n, T (1), N (2), N (3));
547 unsigned nargs = N (4);
548 if (!nargs) perr ("no cases");
549 if (nargs & 1) perr ("odd number of 'addCase' arguments %u", nargs);
550 if (size != 3 * nargs + 5)
551 perr ("number of 'addCase' arguments does not match");
552 vector<BitVector::BitRange> args;
553 for (unsigned i = 5; nargs; i += 3, nargs--)
554 {
555 bool undeclared = (T (i) == "undeclared");
556 if (undeclared && (nargs & 1)) perr ("'undeclared' at wrong position");
557 if (!undeclared) CHKRANGE (T (i), N (i + 1), N (i + 2));
558 BitVector::BitRange arg (undeclared ? 0 : symtab[T (i)],
559 undeclared ? 0 : N (i + 1),
560 undeclared ? 0 : N (i + 2));
561 if (!undeclared && !(nargs & 1) && arg.getWidth () != 1)
562 CHKRANGESAMEWIDTH (n, arg);
563 args.push_back (arg);
564 }
565 ibvm->addCase (n, args);
566 stats.addCase++;
567 }
568 else if (!strcmp (op, "addParallelCase"))
569 goto ADDCASE;
570 else if (!strcmp (op, "addConcat"))
571 {
572 if (size < 5) perr ("not enough arguments for 'addConcat'");
573 RANGE (n, T (1), N (2), N (3));
574 unsigned nargs = N (4);
575 if (!nargs) perr ("no arguments");
576 if (size != 3 * nargs + 5)
577 perr ("number of 'addConcat' arguments does not match");
578 vector<BitVector::BitRange> args;
579 unsigned width = 0;
580 for (unsigned i = 5; nargs; i += 3, nargs--)
581 {
582 CHKRANGE (T (i), N (i + 1), N (i + 2));
583 BitVector::BitRange arg (symtab[T (i)], N (i + 1), N (i + 2));
584 args.push_back (arg);
585 width += arg.getWidth ();
586 }
587 if (width != n.getWidth ())
588 perr ("sum of width of 'addConcat' arguments does not match %u",
589 n.getWidth ());
590 ibvm->addConcat (n, args);
591 stats.addConcat++;
592 }
593 else if
594 UNARY (addNonState);
595 else if
596 UNARY (addAssignment);
597 else if
598 UNARY (addBitNot);
599 else if
600 EXTEND (addZeroExtension);
601 else if
602 EXTEND (addSignExtension);
603 else if
604 PRED1 (addLogicalNot);
605 else if
606 UNARYARG (addRShift);
607 else if
608 UNARYARG (addLShift);
609 else if
610 BINARY (addRShiftNonConst);
611 else if
612 BINARY (addLShiftNonConst);
613 else if
614 BINARY (addState);
615 else if
616 BINARY (addBitAnd);
617 else if
618 BINARY (addBitOr);
619 else if
620 BINARY (addBitXor);
621 else if
622 BINARY (addDiv);
623 else if
624 BINARY (addMod);
625 else if
626 BINARY (addMul);
627 else if
628 BINARY (addSum);
629 else if
630 BINARY (addSub);
631 else if
632 PRED2 (addEqual);
633 else if
634 PRED2 (addLogicalOr);
635 else if
636 PRED2 (addLogicalAnd);
637 else if
638 PRED2 (addLessThan);
639 else if
640 PRED2 (addLessEqual);
641 else if
642 PRED2 (addGreaterEqual);
643 else if
644 PRED2 (addGreaterThan);
645 else if (!strcmp (op, "addReplicate"))
646 {
647 CHKARGS (7);
648 RANGE (c, T (1), N (2), N (3));
649 RANGE (n, T (4), N (5), N (6));
650 if (c.getWidth () != N (7) * (long long) n.getWidth ())
651 perr ("range [%u:%u] does not match %u times range [%u:%u] ",
652 c.m_nMsb,
653 c.m_nLsb,
654 N (7),
655 n.m_nMsb,
656 n.m_nLsb);
657 ibvm->addReplicate (c, n, N (7));
658 stats.addReplicate++;
659 }
660 else if (!strcmp (op, "addAssertion"))
661 {
662 CHKARGS (2);
663 RANGE (r, T (1), N (2), N (2));
664 if (r.getWidth () != 1) perr ("invalid assertion width %u", r.getWidth ());
665 ibvm->addAssertion (r);
666 Var& a = idtab[symtab[T (1)]];
667 if (a.width != 1)
668 {
669 string name = T (1);
670 char buffer[20];
671 sprintf (buffer, "[%u]", N (2));
672 name += buffer;
673 assertions.push_back (Assertion (name));
674 }
675 else
676 assertions.push_back (Assertion (T (1)));
677 stats.addAssertion++;
678 }
679 else if (!strcmp (op, "addAssumption"))
680 {
681 CHKARGS (3);
682 RANGE (r, T (1), N (2), N (2));
683 if (r.getWidth () != 1) perr ("invalid assumption width %u", r.getWidth ());
684 ibvm->addAssumption (r, (bool) N (3));
685 stats.addAssumption++;
686 }
687 else
688 perr ("unknown operator '%s'", op);
689 }
690
691 static void
parse()692 parse ()
693 {
694 while (read_line ()) parse_line (), lineno++;
695 }
696
697 static int
hasuffix(const char * arg,const char * suffix)698 hasuffix (const char* arg, const char* suffix)
699 {
700 if (strlen (arg) < strlen (suffix)) return 0;
701 if (strcmp (arg + strlen (arg) - strlen (suffix), suffix)) return 0;
702 return 1;
703 }
704
705 static bool
cmd(const char * arg,const char * suffix,const char * fmt)706 cmd (const char* arg, const char* suffix, const char* fmt)
707 {
708 struct stat buf;
709 char* cmd;
710 int len;
711 if (!hasuffix (arg, suffix)) return 0;
712 if (stat (arg, &buf)) err ("can not stat file '%s'", arg);
713 len = strlen (fmt) + strlen (arg) + 1;
714 cmd = (char*) malloc (len);
715 sprintf (cmd, fmt, arg);
716 input = popen (cmd, "r");
717 free (cmd);
718 close_input = 2;
719 return 1;
720 }
721
722 static bool
isfile(const char * p)723 isfile (const char* p)
724 {
725 struct stat buf;
726 return !stat (p, &buf);
727 }
728
729 static bool
isbound(const char * str)730 isbound (const char* str)
731 {
732 const char* p = str;
733 if (!isdigit (*p++)) return 0;
734 while (isdigit (*p)) p++;
735 return !*p;
736 }
737
738 static const char* USAGE =
739 "usage: btorimc [ <option> ... ] [<k>] [<ibv>]\n"
740 "\n"
741 "where <option> is one of the following:\n"
742 "\n"
743 " -h print this command line option summary\n"
744 " -s stop checking after first assertion failed\n"
745 " -n do not print witness even if '-s' is specified\n"
746 " -f force translation:\n"
747 "\n"
748 " once: replace 'x' by '0'\n"
749 " twice: terminate forward cycles by '0'\n"
750 "\n"
751 " -d dump BTOR model\n"
752 " -o path of dump file (default is stdout)\n"
753 " -i ignore and do not check properties at initial state\n"
754 " -v increment verbose level (can be used multiple times)\n"
755 "\n"
756 " -rwl1 set rewrite level to 1\n"
757 " -rwl2 set rewrite level to 2\n"
758 " -rwl3 set rewrite level to 3 (default)\n"
759 "\n"
760 "and\n"
761 "\n"
762 "<k> maximal bound for bounded model checking (default 20)\n"
763 "<ibv> IBV input file (default '<stdin>')\n";
764
765 static void
printWitness(int a,int r)766 printWitness (int a, int r)
767 {
768 for (int i = 0; i <= r; i++)
769 {
770 if (i) printf ("\n");
771 for (vector<unsigned>::const_iterator it = vartab.begin ();
772 it != vartab.end ();
773 it++)
774 {
775 unsigned id = *it;
776 printf ("assertion=%d time=%d id=%d ", a, i, id);
777 Var& var = idtab[id];
778 printf ("%s ", var.name.c_str ());
779 assert (var.width > 0);
780 BitVector::BitRange range (id, var.width - 1, 0);
781 string val = ibvm->assignment (range, i);
782 printf ("%s\n", val.c_str ());
783 }
784 fflush (stdout);
785 }
786 }
787
788 static bool witness = true;
789
790 static void
assertionFailedCallBack(void * state,int i,int k)791 assertionFailedCallBack (void* state, int i, int k)
792 {
793 (void) state;
794 assert (!state);
795 assert (0 <= i), assert (i < (int) assertions.size ());
796 Assertion& a = assertions[i];
797 a.nfalsified++;
798 nfalsified++;
799 int mod10 = a.nfalsified % 10;
800 const char* suffix;
801 switch (mod10)
802 {
803 case 1: suffix = "ST"; break;
804 case 2: suffix = "ND"; break;
805 case 3: suffix = "RD"; break;
806 default: suffix = "TH"; break;
807 }
808 if (witness && nfalsified > 1) printf ("\n");
809 printf ("ASSERTION %d '%s' FALSIFIED AT BOUND %d THE %d'%s TIME\n",
810 i,
811 a.name.c_str (),
812 k,
813 a.nfalsified,
814 suffix);
815 fflush (stdout);
816 if (witness) printf ("\n"), printWitness (i, k);
817 }
818
819 namespace IMC {
820
821 class ReachedAtBoundListener : public virtual BtorIBV::ReachedAtBoundListener
822 {
823 public:
~ReachedAtBoundListener()824 ~ReachedAtBoundListener () {}
reachedAtBound(int i,int k)825 void reachedAtBound (int i, int k) { assertionFailedCallBack (0, i, k); }
826 };
827
828 class StartingBoundListener : public virtual BtorIBV::StartingBoundListener
829 {
830 public:
~StartingBoundListener()831 ~StartingBoundListener () {}
startingBound(int k)832 void startingBound (int k) { msg ("bound %d", k); }
833 };
834
835 } // namespace IMC
836
837 static IMC::ReachedAtBoundListener reached_at_bound_listener;
838 static IMC::StartingBoundListener starting_bound_listener;
839
840 int
main(int argc,char ** argv)841 main (int argc, char** argv)
842 {
843 bool dump = false, ignore = false, multi = true;
844 const char* outputname = 0;
845 int k = -1, r, rwl = 3, force = 0;
846 for (int i = 1; i < argc; i++)
847 {
848 if (!strcmp (argv[i], "-h"))
849 {
850 fputs (USAGE, stdout);
851 exit (0);
852 }
853 else if (!strcmp (argv[i], "-n"))
854 witness = false;
855 else if (!strcmp (argv[i], "-d"))
856 dump = true;
857 else if (!strcmp (argv[i], "-v"))
858 verbosity++;
859 else if (!strcmp (argv[i], "-s"))
860 multi = false;
861 else if (!strcmp (argv[i], "-i"))
862 ignore = true;
863 else if (!strcmp (argv[i], "-f"))
864 force++;
865 else if (!strcmp (argv[i], "-rwl1"))
866 rwl = 1;
867 else if (!strcmp (argv[i], "-rwl2"))
868 rwl = 2;
869 else if (!strcmp (argv[i], "-rwl3"))
870 rwl = 3;
871 else if (!strcmp (argv[i], "-o"))
872 {
873 if (++i == argc) err ("argument to '-o' missing");
874 outputname = argv[i];
875 }
876 else if (argv[i][0] == '-')
877 err ("invalid command line option '%s'", argv[i]);
878 else if (isbound (argv[i]))
879 {
880 if (k >= 0) err ("more than one bound");
881 if ((k = atoi (argv[i])) < 0) err ("invalid bound");
882 }
883 else if (close_input)
884 err ("more than one input");
885 else if (!isfile (argv[i]))
886 err ("'%s' does not seem to be a file", argv[i]);
887 else if (cmd ((input_name = argv[i]), ".gz", "gunzip -c %s"))
888 ;
889 else if (cmd (argv[i], ".bz2", "bzcat %s"))
890 ;
891 else if (!(input = fopen (argv[i], "r")))
892 err ("can not read '%s'", argv[i]);
893 else
894 close_input = true;
895 }
896 if (multi) witness = false;
897 msg ("reading '%s'", input_name);
898 ibvm = new BtorIBV ();
899 ibvm->setVerbosity ((verbosity ? verbosity - 1 : 0));
900 ibvm->setRewriteLevel (rwl);
901 if (force) ibvm->setForce (force);
902 if (witness) ibvm->enableTraceGeneration ();
903 ibvm->setStop (!multi);
904 ibvm->setReachedAtBoundListener (&reached_at_bound_listener);
905 if (verbosity) ibvm->setStartingBoundListener (&starting_bound_listener);
906 parse ();
907 if (close_input == 1) fclose (input);
908 if (close_input == 2) pclose (input);
909 ibvm->analyze ();
910 ibvm->translate ();
911 if (dump)
912 {
913 if (outputname)
914 {
915 FILE* output = fopen (outputname, "w");
916 if (!output) err ("failed to write to '%s'", outputname);
917 msg ("dumping BTOR model to '%s'", outputname);
918 ibvm->dump_btor (output);
919 fclose (output);
920 }
921 else
922 {
923 msg ("dumping BTOR model to '<stdout>'");
924 ibvm->dump_btor (stdout);
925 }
926 }
927 else
928 {
929 if (k < 0) k = 20;
930 msg ("running bounded model checking up to bound %d", k);
931 if (witness) msg ("will print witness");
932 if (multi) msg ("will not stop at first falsified assertion necessarily");
933 r = ibvm->bmc ((int) ignore, k);
934 int notfalsified = 0, i;
935 for (i = 0; i < (int) assertions.size (); i++)
936 {
937 Assertion& a = assertions[i];
938 if (a.nfalsified)
939 {
940 if (!multi) break;
941 continue;
942 }
943 notfalsified++;
944 if (witness && (notfalsified + nfalsified > 1)) printf ("\n");
945 printf ("ASSERTION %d '%s' VALID UNTIL BOUND %d (INCLUSIVE AND FROM 0)\n",
946 i,
947 a.name.c_str (),
948 k);
949 fflush (stdout);
950 }
951 if (!assertions.size ())
952 msg ("no assertion found");
953 else if (notfalsified)
954 msg ("%d assertions not falsified", notfalsified);
955 else
956 msg ("all assertions falsified within bound 0 to bound %d", r ? k : r);
957 }
958 delete ibvm;
959 return 0;
960 }
961