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