diff --git a/Makefile b/Makefile index 6d4901b88..a9d9b79c5 100644 --- a/Makefile +++ b/Makefile @@ -33,7 +33,7 @@ MODULES := \ src/map/amap src/map/cov src/map/scl src/map/mpm \ src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \ src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \ - src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ + src/misc/mem src/misc/bar src/misc/bbl src/misc/parse src/misc/btor \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \ src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim src/opt/ufar src/opt/untk src/opt/util \ diff --git a/abclib.dsp b/abclib.dsp index 1ab567cce..f7c80a25b 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -5302,6 +5302,30 @@ SOURCE=.\src\misc\parse\parseInt.h SOURCE=.\src\misc\parse\parseStack.c # End Source File # End Group +# Begin Group "btor" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\misc\btor\btor2mem.h +# End Source File +# Begin Source File + +SOURCE=.\src\misc\btor\btor2parser.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\btor\btor2parser.h +# End Source File +# Begin Source File + +SOURCE=.\src\misc\btor\btor2stack.h +# End Source File +# Begin Source File + +SOURCE=.\src\misc\btor\catbtor.c +# End Source File +# End Group # End Group # Begin Group "ai" diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4eee95227..ff09c085e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -663,6 +663,8 @@ static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9eSLIM ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9CatBtor ( Abc_Frame_t * pAbc, int argc, char ** argv ); + extern int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1502,6 +1504,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 ); + + Cmd_CommandAdd( pAbc, "ABC9", "&catbtor", Abc_CommandAbc9CatBtor, 0 ); { // extern Mf_ManTruthCount(); // Mf_ManTruthCount(); @@ -59462,6 +59466,42 @@ int Abc_CommandAbc9eSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) { return 1; } +int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Abc_BtorCat( char * pFileName, int fVerbose ); + + int c, fVerbose = 0; + char * pFileName; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "v" ) ) != EOF ) + { + switch ( c ) { + case 'v' : + fVerbose ^= 1; + break; + default: + goto usage; + } + } + if ( argc == globalUtilOptind + 1 ) + pFileName = argv[globalUtilOptind]; + else + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 0; + } + + Abc_BtorCat( pFileName, fVerbose ); + + return 0; + +usage: + Abc_Print( -2, "usage: &catbtor [-v] \n" ); + Abc_Print( -2, "\t parse BTOR file and print to stdout.\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information\n"); + Abc_Print( -2, "\t : input BTOR file\n"); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/btor/LICENSE.txt b/src/misc/btor/LICENSE.txt new file mode 100644 index 000000000..665729e2b --- /dev/null +++ b/src/misc/btor/LICENSE.txt @@ -0,0 +1,25 @@ +The Btor2Tools package provides a generic parser and tools for the BTOR2 format. + +Copyright (c) 2012-2018 Armin Biere. +Copyright (c) 2013-2018 Mathias Preiner. +Copyright (c) 2015-2018 Aina Niemetz. + +MIT License + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the "Software"), +to deal in the Software without restriction, including without limitation +the rights to use, copy, modify, merge, publish, distribute, sublicense, +and/or sell copies of the Software, and to permit persons to whom the +Software is furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL +THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR +OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, +ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR +OTHER DEALINGS IN THE SOFTWARE. diff --git a/src/misc/btor/VERSION b/src/misc/btor/VERSION new file mode 100644 index 000000000..6d7de6e6a --- /dev/null +++ b/src/misc/btor/VERSION @@ -0,0 +1 @@ +1.0.2 diff --git a/src/misc/btor/btor2mem.h b/src/misc/btor/btor2mem.h new file mode 100644 index 000000000..bd1f348c0 --- /dev/null +++ b/src/misc/btor/btor2mem.h @@ -0,0 +1,88 @@ +/** + * Btor2Tools: A tool package for the BTOR format. + * + * Copyright (C) 2007-2009 Robert Daniel Brummayer. + * Copyright (C) 2007-2012 Armin Biere. + * Copyright (C) 2012-2015 Mathias Preiner. + * Copyright (c) 2018 Aina Niemetz. + * + * All rights reserved. + * + * This file is part of the Btor2Tools package. + * See LICENSE.txt for more information on using this software. + */ + +#ifndef BTOR2MEM_H_INCLUDED +#define BTOR2MEM_H_INCLUDED + +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +#include +#include +#include + +/*------------------------------------------------------------------------*/ + +#define BTOR2_CLRN(ptr, nelems) (memset ((ptr), 0, (nelems) * sizeof *(ptr))) + +#define BTOR2_CLR(ptr) BTOR2_CLRN ((ptr), 1) + +#define BTOR2_DELETE(ptr) (free (ptr)) + +static inline void * +btorsim_malloc (size_t size) +{ + void *res; + if (!size) return 0; + res = malloc (size); + if (!res) + { + fprintf (stderr, "[btorsim] memory allocation failed\n"); + abort (); + } + return res; +} + +static inline void * +btorsim_calloc (size_t nobj, size_t size) +{ + void *res; + res = calloc (nobj, size); + if (!res) + { + fprintf (stderr, "[btorsim] memory allocation failed\n"); + abort (); + } + return res; +} + +static inline void * +btorsim_realloc (void *p, size_t new_size) +{ + void *res; + res = realloc (p, new_size); + if (!res) + { + fprintf (stderr, "[btorsim] memory allocation failed\n"); + abort (); + } + return res; +} + +static inline char * +btorsim_strdup (const char *str) +{ + char *res = 0; + if (str) + { + res = (char *) btorsim_malloc ((strlen (str) + 1) * sizeof (char)); + strcpy (res, str); + } + return res; +} + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/misc/btor/btor2parser.c b/src/misc/btor/btor2parser.c new file mode 100644 index 000000000..595f1806b --- /dev/null +++ b/src/misc/btor/btor2parser.c @@ -0,0 +1,1565 @@ +/** + * Btor2Tools: A tool package for the BTOR2 format. + * + * Copyright (c) 2012-2018 Armin Biere. + * Copyright (c) 2017 Mathias Preiner. + * Copyright (c) 2017-2019 Aina Niemetz. + * + * All rights reserved. + * + * This file is part of the Btor2Tools package. + * See LICENSE.txt for more information on using this software. + */ + +#include "btor2parser.h" + +#include +#include +#include +#include +#include +#include + +#include "btor2stack.h" + +ABC_NAMESPACE_IMPL_START + +struct Btor2Parser +{ + char *error; + Btor2Line **table, *new_line; + Btor2Sort **stable; + int64_t sztable, ntable, szstable, nstable, szbuf, nbuf, lineno; + int32_t saved; + char *buf; + FILE *file; +}; + +static void * +btor2parser_malloc (size_t size) +{ + assert (size); + + void *res = malloc (size); + if (!res) + { + fprintf (stderr, "[btor2parser] memory allocation failed\n"); + abort (); + } + return res; +} + +static void * +btor2parser_realloc (void *ptr, size_t size) +{ + assert (size); + + void *res = realloc (ptr, size); + if (!res) + { + fprintf (stderr, "[btor2parser] memory reallocation failed\n"); + abort (); + } + return res; +} + +static char * +btor2parser_strdup (const char *str) +{ + assert (str); + + char *res = (char *)btor2parser_malloc (strlen (str) + 1); + strcpy (res, str); + return res; +} + +Btor2Parser * +btor2parser_new () +{ + Btor2Parser *res = (Btor2Parser *)btor2parser_malloc (sizeof *res); + memset (res, 0, sizeof *res); + return res; +} + +static void +reset_bfr (Btor2Parser *bfr) +{ + int32_t i; + assert (bfr); + if (bfr->error) + { + free (bfr->error); + bfr->error = 0; + } + if (bfr->table) + { + for (i = 0; i < bfr->ntable; i++) + { + Btor2Line *l = bfr->table[i]; + if (!l) continue; + if (l->symbol) free (l->symbol); + if (l->constant) free (l->constant); + free (l->args); + free (l); + } + free (bfr->table); + bfr->table = 0; + bfr->ntable = bfr->sztable = 0; + } + if (bfr->buf) + { + free (bfr->buf); + bfr->buf = 0; + bfr->nbuf = bfr->szbuf = 0; + } +} + +void +btor2parser_delete (Btor2Parser *bfr) +{ + reset_bfr (bfr); + free (bfr); +} + +static int32_t +getc_bfr (Btor2Parser *bfr) +{ + int32_t ch; + if ((ch = bfr->saved) == EOF) + ch = getc (bfr->file); + else + bfr->saved = EOF; + if (ch == '\n') bfr->lineno++; + return ch; +} + +static void +ungetc_bfr (Btor2Parser *bfr, int32_t ch) +{ + assert (bfr->saved == EOF); + if (ch == EOF) return; + bfr->saved = ch; + if (ch == '\n') + { + assert (bfr->lineno > 1); + bfr->lineno--; + } +} + +static int32_t +perr_bfr (Btor2Parser *bfr, const char *fmt, ...) +{ + assert (!bfr->error); + char buf[1024]; + + va_list ap; + va_start (ap, fmt); + vsnprintf (buf, 1023, fmt, ap); + va_end (ap); + buf[1023] = '\0'; + + bfr->error = (char *)btor2parser_malloc (strlen (buf) + 28); + sprintf (bfr->error, "line %" PRId64 ": %s", bfr->lineno, buf); + return 0; +} + +static void +pushc_bfr (Btor2Parser *bfr, int32_t ch) +{ + if (bfr->nbuf >= bfr->szbuf) + { + bfr->szbuf = bfr->szbuf ? 2 * bfr->szbuf : 1; + bfr->buf = (char *)btor2parser_realloc (bfr->buf, bfr->szbuf * sizeof *bfr->buf); + } + bfr->buf[bfr->nbuf++] = ch; +} + +static void +pusht_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + if (bfr->ntable >= bfr->sztable) + { + bfr->sztable = bfr->sztable ? 2 * bfr->sztable : 1; + bfr->table = + (Btor2Line **)btor2parser_realloc (bfr->table, bfr->sztable * sizeof *bfr->table); + } + bfr->table[bfr->ntable++] = l; +} + +static int32_t +parse_id_bfr (Btor2Parser *bfr, int64_t *res) +{ + int64_t id; + int32_t ch; + ch = getc_bfr (bfr); + if (ch == '0') return perr_bfr (bfr, "id should start with non-zero digit"); + if (!isdigit (ch)) return perr_bfr (bfr, "id should start with digit"); + id = ch - '0'; + while (isdigit (ch = getc_bfr (bfr))) + { + id = 10 * id + (ch - '0'); + if (id >= BTOR2_FORMAT_MAXID) return perr_bfr (bfr, "id exceeds maximum"); + } + ungetc_bfr (bfr, ch); + *res = id; + return 1; +} + +static int32_t +parse_signed_id_bfr (Btor2Parser *bfr, int64_t *res) +{ + int32_t ch, sign; + ch = getc_bfr (bfr); + if (ch == '-') + sign = -1; + else + { + ungetc_bfr (bfr, ch); + sign = 1; + } + if (!parse_id_bfr (bfr, res)) return 0; + if (sign < 0) *res = -*res; + return 1; +} + +static int32_t +parse_pos_number_bfr (Btor2Parser *bfr, uint32_t *res) +{ + int64_t num; + int32_t ch; + ch = getc_bfr (bfr); + if (!isdigit (ch)) + { + if (isprint (ch)) + return perr_bfr (bfr, "expected number but got '%c'", ch); + else if (ch == '\n') + return perr_bfr (bfr, "expected number but got new line"); + else + return perr_bfr ( + bfr, "expected number but got character code 0x%02x", ch); + } + num = ch - '0'; + ch = getc_bfr (bfr); + /* number with leading zero */ + if (num == 0 && isdigit (ch)) + return perr_bfr (bfr, "number should start with non-zero digit"); + while (isdigit (ch)) + { + num = 10 * num + (ch - '0'); + if (num >= BTOR2_FORMAT_MAXBITWIDTH) + return perr_bfr (bfr, + "number exceeds maximum bit width of %" PRId64, + BTOR2_FORMAT_MAXBITWIDTH); + ch = getc_bfr (bfr); + } + ungetc_bfr (bfr, ch); + *res = num; + return 1; +} + +static Btor2Line * +id2line_bfr (Btor2Parser *bfr, int64_t id) +{ + int64_t absid = labs (id); + if (!absid || absid >= bfr->ntable) return 0; + return bfr->table[absid]; +} + +static int32_t +skip_comment (Btor2Parser *bfr) +{ + int32_t ch; + while ((ch = getc_bfr (bfr)) != '\n') + { + if (ch == EOF) return perr_bfr (bfr, "unexpected end-of-file in comment"); + } + return 1; +} + +static int32_t +cmp_sort_ids (Btor2Parser *bfr, int64_t sort_id1, int64_t sort_id2) +{ + (void) bfr; + Btor2Line *s1, *s2; + + s1 = id2line_bfr (bfr, sort_id1); + s2 = id2line_bfr (bfr, sort_id2); + if (s1->sort.tag != s2->sort.tag) return 1; + if (s1->sort.tag == BTOR2_TAG_SORT_bitvec) + return s1->sort.bitvec.width - s2->sort.bitvec.width; + assert (s1->sort.tag == BTOR2_TAG_SORT_array); + if (cmp_sort_ids (bfr, s1->sort.array.index, s2->sort.array.index)) return 1; + return cmp_sort_ids (bfr, s1->sort.array.element, s2->sort.array.element); +} + +static int32_t +cmp_sorts (Btor2Parser *bfr, Btor2Line *l1, Btor2Line *l2) +{ + return cmp_sort_ids (bfr, l1->sort.id, l2->sort.id); +} + +static int32_t +parse_sort_id_bfr (Btor2Parser *bfr, Btor2Sort *res) +{ + int64_t sort_id; + Btor2Line *s; + if (!parse_id_bfr (bfr, &sort_id)) return 0; + + if (sort_id >= bfr->ntable || id2line_bfr (bfr, sort_id) == 0) + return perr_bfr (bfr, "undefined sort id"); + + s = id2line_bfr (bfr, sort_id); + if (s->tag != BTOR2_TAG_sort) + return perr_bfr (bfr, "id after tag is not a sort id"); + *res = s->sort; + return 1; +} + +static const char * +parse_tag (Btor2Parser *bfr) +{ + int32_t ch; + bfr->nbuf = 0; + while ('a' <= (ch = getc_bfr (bfr)) && ch <= 'z') pushc_bfr (bfr, ch); + if (!bfr->nbuf) + { + perr_bfr (bfr, "expected tag"); + return 0; + } + if (ch != ' ') + { + perr_bfr (bfr, "expected space after tag"); + return 0; + } + pushc_bfr (bfr, 0); + return bfr->buf; +} + +static int32_t +parse_symbol_bfr (Btor2Parser *bfr) +{ + int32_t ch; + bfr->nbuf = 0; + while ((ch = getc_bfr (bfr)) != '\n') + { + if (ch == EOF) + return perr_bfr (bfr, "unexpected end-of-file in symbol"); + else if (ch == ' ' || ch == '\t') + { + ch = getc_bfr (bfr); + if (ch == ';') + { + if (!skip_comment (bfr)) return 0; + break; + } + else + return perr_bfr (bfr, "unexpected white-space in symbol"); + } + pushc_bfr (bfr, ch); + } + if (!bfr->nbuf) + { + assert (bfr->lineno > 1); + bfr->lineno--; + return perr_bfr (bfr, "empty symbol"); + } + pushc_bfr (bfr, 0); + return 1; +} + +static int32_t +parse_opt_symbol_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + int32_t ch; + if ((ch = getc_bfr (bfr)) == ' ') + { + ch = getc_bfr (bfr); + if (ch == ';') + { + if (!skip_comment (bfr)) return 0; + } + else + { + ungetc_bfr (bfr, ch); + if (!parse_symbol_bfr (bfr)) return 0; + l->symbol = btor2parser_strdup (bfr->buf); + } + } + else if (ch != '\n') + return perr_bfr ( + bfr, "expected new-line at the end of the line got '%c'", ch); + return 1; +} + +static Btor2Line * +new_line_bfr (Btor2Parser *bfr, + int64_t id, + int64_t lineno, + const char *name, + Btor2Tag tag) +{ + Btor2Line *res; + assert (0 < id); + assert (bfr->ntable <= id); + res = (Btor2Line *)btor2parser_malloc (sizeof *res); + memset (res, 0, sizeof (*res)); + res->id = id; + res->lineno = lineno; + res->tag = tag; + res->name = name; + res->args = (int64_t *)btor2parser_malloc (sizeof (int64_t) * 3); + memset (res->args, 0, sizeof (int64_t) * 3); + while (bfr->ntable < id) pusht_bfr (bfr, 0); + assert (bfr->ntable == id); + return res; +} + +static int32_t +check_sort_bitvec (Btor2Parser *bfr, Btor2Line *l, Btor2Line *args[]) +{ + uint32_t i; + /* check if bit-vector operators have bit-vector operands */ + if (l->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, "expected bitvec sort for %s", l->name); + for (i = 0; i < l->nargs; i++) + { + if (args[i]->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, + "expected bitvec sort for %s argument of %s", + i == 0 ? "first" : (i == 1 ? "second" : "third"), + l->name); + } + return 1; +} + +static int32_t +is_constant_bfr (Btor2Parser *bfr, int64_t id) +{ + Btor2Line *l = id2line_bfr (bfr, id); + assert (l); + Btor2Tag tag = l->tag; + return tag == BTOR2_TAG_const || tag == BTOR2_TAG_constd + || tag == BTOR2_TAG_consth || tag == BTOR2_TAG_one + || tag == BTOR2_TAG_ones || tag == BTOR2_TAG_zero; +} + +static int32_t +check_sorts_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + Btor2Line *arg; + Btor2Line *args[3]; + uint32_t i; + if (l->tag != BTOR2_TAG_justice) + { + for (i = 0; i < l->nargs; i++) + { + args[i] = id2line_bfr (bfr, l->args[i]); + // Disallow negative array ids. This is only valid for bit-vectors. + if (args[i]->sort.tag == BTOR2_TAG_SORT_array && l->args[i] < 0) + { + return perr_bfr (bfr, "negated arrays not allowed"); + } + } + } + + switch (l->tag) + { + /* n -> n */ + case BTOR2_TAG_dec: + case BTOR2_TAG_inc: + case BTOR2_TAG_neg: + case BTOR2_TAG_not: + assert (l->nargs == 1); + if (!check_sort_bitvec (bfr, l, args)) return 0; + if (l->sort.bitvec.width != args[0]->sort.bitvec.width) + return perr_bfr (bfr, + "expected bitvec of size %u for " + "argument but got %u", + l->sort.bitvec.width, + args[0]->sort.bitvec.width); + break; + + /* n -> 1 */ + case BTOR2_TAG_redand: + case BTOR2_TAG_redor: + case BTOR2_TAG_redxor: + assert (l->nargs == 1); + if (!check_sort_bitvec (bfr, l, args)) return 0; + if (l->sort.bitvec.width != 1) + return perr_bfr (bfr, + "expected bitvec of size 1 for " + "%s but got %u", + l->name, + l->sort.bitvec.width); + break; + + /* n x n -> n */ + case BTOR2_TAG_add: + case BTOR2_TAG_and: + case BTOR2_TAG_mul: + case BTOR2_TAG_nand: + case BTOR2_TAG_nor: + case BTOR2_TAG_or: + case BTOR2_TAG_rol: + case BTOR2_TAG_ror: + case BTOR2_TAG_sdiv: + case BTOR2_TAG_sll: + case BTOR2_TAG_smod: + case BTOR2_TAG_sra: + case BTOR2_TAG_srem: + case BTOR2_TAG_srl: + case BTOR2_TAG_sub: + case BTOR2_TAG_udiv: + case BTOR2_TAG_urem: + case BTOR2_TAG_xnor: + case BTOR2_TAG_xor: + assert (l->nargs == 2); + if (!check_sort_bitvec (bfr, l, args)) return 0; + if (l->sort.bitvec.width != args[0]->sort.bitvec.width) + return perr_bfr (bfr, + "expected bitvec of size %u for " + "first argument but got %u", + l->sort.bitvec.width, + args[0]->sort.bitvec.width); + if (l->sort.bitvec.width != args[1]->sort.bitvec.width) + return perr_bfr (bfr, + "expected bitvec of size %u for " + "second argument but got %u", + l->sort.bitvec.width, + args[1]->sort.bitvec.width); + break; + + case BTOR2_TAG_init: + if (l->sort.tag == BTOR2_TAG_SORT_array) + { + if (cmp_sorts (bfr, l, args[0])) + return perr_bfr (bfr, "sort of first argument does not match"); + + // special case for constant initialization for arrays + if (args[1]->sort.tag == BTOR2_TAG_SORT_bitvec) + { + if (!is_constant_bfr (bfr, args[1]->id)) + return perr_bfr (bfr, + "expected bit-vector constant as second argument"); + if (cmp_sort_ids (bfr, l->sort.array.element, args[1]->sort.id)) + return perr_bfr (bfr, + "sort of init value does not match element " + "sort of state '%" PRId64 "'", + args[0]->id); + } + break; + } + // else fall through + case BTOR2_TAG_next: + assert (l->nargs == 2); + if (cmp_sorts (bfr, l, args[0])) + return perr_bfr (bfr, "sort of first argument does not match"); + if (cmp_sorts (bfr, l, args[1])) + return perr_bfr (bfr, "sort of second argument does not match"); + break; + + /* n x n -> 1 */ + case BTOR2_TAG_uaddo: + case BTOR2_TAG_ugt: + case BTOR2_TAG_ugte: + case BTOR2_TAG_ult: + case BTOR2_TAG_ulte: + case BTOR2_TAG_umulo: + case BTOR2_TAG_usubo: + case BTOR2_TAG_saddo: + case BTOR2_TAG_sdivo: + case BTOR2_TAG_sgt: + case BTOR2_TAG_sgte: + case BTOR2_TAG_slt: + case BTOR2_TAG_slte: + case BTOR2_TAG_smulo: + case BTOR2_TAG_ssubo: + assert (l->nargs == 2); + if (!check_sort_bitvec (bfr, l, args)) return 0; + if (l->sort.bitvec.width != 1) + return perr_bfr (bfr, + "expected bitvec of size 1 for " + "%s but got %u", + l->name, + l->sort.bitvec.width); + if (args[0]->sort.bitvec.width != args[1]->sort.bitvec.width) + return perr_bfr (bfr, + "sorts of first and second " + "argument do not match"); + break; + + case BTOR2_TAG_eq: + case BTOR2_TAG_neq: + assert (l->nargs == 2); + if (l->sort.bitvec.width != 1) + return perr_bfr (bfr, + "expected bitvec of size 1 for %s but got %u", + l->name, + l->sort.bitvec.width); + if (cmp_sorts (bfr, args[0], args[1])) + return perr_bfr (bfr, + "sorts of first and second " + "argument do not match"); + break; + + /* n x m -> n + m */ + case BTOR2_TAG_concat: + assert (l->nargs == 2); + if (!check_sort_bitvec (bfr, l, args)) return 0; + if (l->sort.bitvec.width + != args[0]->sort.bitvec.width + args[1]->sort.bitvec.width) + return perr_bfr ( + bfr, + "expected bitvec of size %u for %s but got %u", + l->sort.bitvec.width, + l->name, + args[0]->sort.bitvec.width + args[1]->sort.bitvec.width); + break; + + /* [u:l] -> u - l + 1 */ + case BTOR2_TAG_slice: { + assert (l->nargs == 1); + if (!check_sort_bitvec (bfr, l, args)) return 0; + /* NOTE: this cast is safe since l->args[1] and l->args[2] contains + * upper and lower indices, which are uint32_t */ + uint32_t upper = (uint32_t) l->args[1]; + uint32_t lower = (uint32_t) l->args[2]; + if (l->sort.bitvec.width != upper - lower + 1) + return perr_bfr (bfr, + "expected bitvec of size %u for %s but got %u", + l->sort.bitvec.width, + l->name, + upper - lower + 1); + break; + } + /* 1 x 1 -> 1 */ + case BTOR2_TAG_iff: + case BTOR2_TAG_implies: + assert (l->nargs == 2); + if (!check_sort_bitvec (bfr, l, args)) return 0; + if (l->sort.tag != BTOR2_TAG_SORT_bitvec || l->sort.bitvec.width != 1) + return perr_bfr (bfr, "expected bitvec of size 1"); + if (cmp_sorts (bfr, args[0], l)) + return perr_bfr (bfr, + "expected bitvec of size 1 for " + "first argument"); + if (cmp_sorts (bfr, args[1], l)) + return perr_bfr (bfr, + "expected bitvec of size 1 for " + "second argument"); + break; + + /* 1 */ + case BTOR2_TAG_bad: + case BTOR2_TAG_constraint: + case BTOR2_TAG_fair: + assert (l->nargs == 1); + if (args[0]->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, "expected bitvec of size 1 for %s", l->name); + if (args[0]->sort.bitvec.width != 1) + return perr_bfr (bfr, + "expected bitvec of size 1 for %s " + "but got %u", + l->name, + args[0]->sort.bitvec.width); + break; + + /* n */ + case BTOR2_TAG_output: + assert (l->nargs == 1); + if (args[0]->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, "expected bitvec sort for %s", l->name); + break; + + case BTOR2_TAG_ite: + assert (l->nargs == 3); + if (args[0]->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, + "expected bitvec of size 1 for ", + "first argument of %s", + l->name); + if (args[0]->sort.bitvec.width != 1) + return perr_bfr (bfr, + "expected bitvec of size 1 for " + "first argument of %s but got %u", + l->name, + args[0]->sort.bitvec.width); + if (cmp_sorts (bfr, args[1], args[2])) + return perr_bfr (bfr, + "sorts of second and third " + "argument do not match"); + break; + + case BTOR2_TAG_justice: + for (i = 0; i < l->nargs; i++) + { + arg = id2line_bfr (bfr, l->args[i]); + if (arg->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, "expected bitvec of size 1 for argument %u", i); + if (arg->sort.bitvec.width != 1) + return perr_bfr (bfr, + "expected bitvec of size 1 for argument %u " + "but got %u", + i, + arg->sort.bitvec.width); + } + break; + + case BTOR2_TAG_sext: + case BTOR2_TAG_uext: { + assert (l->nargs == 1); + if (!check_sort_bitvec (bfr, l, args)) return 0; + /* NOTE: this cast is safe since l->args[1] contains the extension + * bit-width, which is uint32_t */ + uint32_t ext = args[0]->sort.bitvec.width + (uint32_t) l->args[1]; + if (l->sort.bitvec.width != ext) + return perr_bfr (bfr, + "expected bitvec of size %u for %s but got %u", + l->sort.bitvec.width, + l->name, + ext); + break; + } + case BTOR2_TAG_read: + assert (l->nargs == 2); + if (args[0]->sort.tag != BTOR2_TAG_SORT_array) + return perr_bfr ( + bfr, "expected array sort for first argument of %s", l->name); + if (cmp_sort_ids (bfr, l->sort.id, args[0]->sort.array.element)) + return perr_bfr (bfr, + "sort of %s does not match element sort of first " + "argument", + l->name); + if (cmp_sort_ids (bfr, args[1]->sort.id, args[0]->sort.array.index)) + return perr_bfr (bfr, + "sort of second argument does not match index " + "sort of first argument"); + break; + + case BTOR2_TAG_write: + assert (l->nargs == 3); + if (l->sort.tag != BTOR2_TAG_SORT_array) + return perr_bfr (bfr, "expected array sort for %s", l->name); + if (args[0]->sort.tag != BTOR2_TAG_SORT_array) + return perr_bfr ( + bfr, "expected array sort for first argument of %s", l->name); + if (cmp_sort_ids (bfr, args[1]->sort.id, args[0]->sort.array.index)) + return perr_bfr (bfr, + "sort of second argument does not match index " + "sort of first argument", + l->name); + + if (cmp_sort_ids (bfr, args[2]->sort.id, args[0]->sort.array.element)) + return perr_bfr (bfr, + "sort of third argument does not match element " + "sort of first argument", + l->name); + break; + + /* no sort checking */ + case BTOR2_TAG_const: + case BTOR2_TAG_constd: + case BTOR2_TAG_consth: + case BTOR2_TAG_input: + case BTOR2_TAG_one: + case BTOR2_TAG_ones: + case BTOR2_TAG_sort: + case BTOR2_TAG_state: + case BTOR2_TAG_zero: break; + + default: + assert (0); + return perr_bfr (bfr, "invalid tag '%s' for sort checking", l->tag); + } + return 1; +} + +static int64_t +parse_arg_bfr (Btor2Parser *bfr) +{ + Btor2Line *l; + int64_t res, absres; + if (!parse_signed_id_bfr (bfr, &res)) return 0; + absres = labs (res); + if (absres >= bfr->ntable) + return perr_bfr (bfr, "argument id too large (undefined)"); + l = bfr->table[absres]; + if (!l) return perr_bfr (bfr, "undefined argument id"); + if (l->tag == BTOR2_TAG_sort || l->tag == BTOR2_TAG_init + || l->tag == BTOR2_TAG_next || l->tag == BTOR2_TAG_bad + || l->tag == BTOR2_TAG_constraint || l->tag == BTOR2_TAG_fair + || l->tag == BTOR2_TAG_justice) + { + return perr_bfr (bfr, "'%s' cannot be used as argument", l->name); + } + if (!l->sort.id) return perr_bfr (bfr, "declaration used as argument"); + return res; +} + +static int32_t +parse_sort_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + const char *tag; + Btor2Sort tmp, s; + tag = parse_tag (bfr); + if (!tag) return 0; + if (!strcmp (tag, "bitvec")) + { + tmp.tag = BTOR2_TAG_SORT_bitvec; + tmp.name = "bitvec"; + if (!parse_pos_number_bfr (bfr, &tmp.bitvec.width)) return 0; + if (tmp.bitvec.width == 0) + return perr_bfr (bfr, "bit width must be greater than 0"); + } + else if (!strcmp (tag, "array")) + { + tmp.tag = BTOR2_TAG_SORT_array; + tmp.name = "array"; + s.id = 0; /* get rid of false positive compiler warning */ + if (!parse_sort_id_bfr (bfr, &s)) return 0; + if (getc_bfr (bfr) != ' ') return perr_bfr (bfr, "expected space"); + tmp.array.index = s.id; + if (!parse_sort_id_bfr (bfr, &s)) return 0; + tmp.array.element = s.id; + } + else + { + return perr_bfr (bfr, "invalid sort tag"); + } + tmp.id = l->id; + l->sort = tmp; + return 1; +} + +static int32_t +parse_args (Btor2Parser *bfr, Btor2Line *l, uint32_t nargs) +{ + uint32_t i = 0; + if (getc_bfr (bfr) != ' ') + return perr_bfr (bfr, "expected space after sort id"); + while (i < nargs) + { + if (!(l->args[i] = parse_arg_bfr (bfr))) return 0; + if (i < nargs - 1 && getc_bfr (bfr) != ' ') + return perr_bfr (bfr, "expected space after argument (argument missing)"); + i++; + } + l->nargs = nargs; + return 1; +} + +static int32_t +parse_unary_op_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + if (!parse_args (bfr, l, 1)) return 0; + return 1; +} + +static int32_t +parse_ext_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + uint32_t ext; + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + if (!parse_args (bfr, l, 1)) return 0; + if (getc_bfr (bfr) != ' ') + return perr_bfr (bfr, "expected space after first argument"); + if (!parse_pos_number_bfr (bfr, &ext)) return 0; + l->args[1] = ext; + return 1; +} + +static int32_t +parse_slice_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + uint32_t lower; + if (!parse_ext_bfr (bfr, l)) return 0; + if (getc_bfr (bfr) != ' ') + return perr_bfr (bfr, "expected space after second argument"); + if (!parse_pos_number_bfr (bfr, &lower)) return 0; + l->args[2] = lower; + if (lower > l->args[1]) + return perr_bfr (bfr, "lower has to be less than or equal to upper"); + return 1; +} + +static int32_t +parse_binary_op_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + if (!parse_args (bfr, l, 2)) return 0; + return 1; +} + +static int32_t +parse_ternary_op_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + if (!parse_args (bfr, l, 3)) return 0; + return 1; +} + +static int32_t +check_consth (const char *consth, uint32_t width) +{ + char c; + size_t i, len, req_width; + + len = strlen (consth); + req_width = len * 4; + for (i = 0; i < len; i++) + { + c = consth[i]; + assert (isxdigit (c)); + if (c >= 'A' && c <= 'F') c = tolower (c); + + if (c == '0') + { + req_width -= 4; + continue; + } + c = (c >= '0' && c <= '9') ? c - '0' : c - 'a' + 0xa; + assert (c > 0 && c <= 15); + if (c >> 1 == 0) + req_width -= 3; + else if (c >> 2 == 0) + req_width -= 2; + else if (c >> 3 == 0) + req_width -= 1; + break; + } + if (req_width <= width) return 1; + return 0; +} + +#ifndef NDEBUG +static int32_t +is_bin_str (const char *c) +{ + const char *p; + char ch; + + assert (c != NULL); + + for (p = c; (ch = *p); p++) + if (ch != '0' && ch != '1') return 0; + return 1; +} +#endif + +static const char *digit2const_table[10] = { + "", + "1", + "10", + "11", + "100", + "101", + "110", + "111", + "1000", + "1001", +}; + +static const char * +digit2const (char ch) +{ + assert ('0' <= ch); + assert (ch <= '9'); + + return digit2const_table[ch - '0']; +} + +static const char * +strip_zeroes (const char *a) +{ + assert (a); + while (*a == '0') a++; + return a; +} + +static char * +mult_unbounded_bin_str (const char *a, const char *b) +{ + assert (a); + assert (b); + assert (is_bin_str (a)); + assert (is_bin_str (b)); + + char *res, *r, c, x, y, s, m; + uint32_t alen, blen, rlen, i; + const char *p; + + a = strip_zeroes (a); + if (!*a) return btor2parser_strdup (""); + if (a[0] == '1' && !a[1]) return btor2parser_strdup (b); + + b = strip_zeroes (b); + if (!*b) return btor2parser_strdup (""); + if (b[0] == '1' && !b[1]) return btor2parser_strdup (a); + + alen = strlen (a); + blen = strlen (b); + rlen = alen + blen; + res = (char *)btor2parser_malloc (rlen + 1); + res[rlen] = 0; + + for (r = res; r < res + blen; r++) *r = '0'; + for (p = a; p < a + alen; p++) *r++ = *p; + assert (r == res + rlen); + + for (i = 0; i < alen; i++) + { + m = res[rlen - 1]; + c = '0'; + + if (m == '1') + { + p = b + blen; + r = res + blen; + + while (res < r && b < p) + { + assert (b < p); + x = *--p; + y = *--r; + s = x ^ y ^ c; + c = (x & y) | (x & c) | (y & c); + *r = s; + } + } + + memmove (res + 1, res, rlen - 1); + res[0] = c; + } + + return res; +} + +static char * +add_unbounded_bin_str (const char *a, const char *b) +{ + assert (a); + assert (b); + assert (is_bin_str (a)); + assert (is_bin_str (b)); + + char *res, *r, c, x, y, s, *tmp; + uint32_t alen, blen, rlen; + const char *p, *q; + + a = strip_zeroes (a); + b = strip_zeroes (b); + + if (!*a) return btor2parser_strdup (b); + if (!*b) return btor2parser_strdup (a); + + alen = strlen (a); + blen = strlen (b); + rlen = (alen < blen) ? blen : alen; + rlen++; + + res = (char *)btor2parser_malloc (rlen + 1); + + p = a + alen; + q = b + blen; + + c = '0'; + + r = res + rlen; + *r = 0; + + while (res < r) + { + x = (a < p) ? *--p : '0'; + y = (b < q) ? *--q : '0'; + s = x ^ y ^ c; + c = (x & y) | (x & c) | (y & c); + *--r = s; + } + + p = strip_zeroes (res); + if ((p != res)) + { + tmp = btor2parser_strdup (p); + if (!tmp) + { + free (res); + return 0; + } + free (res); + res = tmp; + } + + return res; +} + +static char * +dec_to_bin_str (const char *str, uint32_t len) +{ + assert (str); + + const char *end, *p; + char *res, *tmp; + + res = btor2parser_strdup (""); + if (!res) return 0; + + end = str + len; + for (p = str; p < end; p++) + { + tmp = mult_unbounded_bin_str (res, "1010"); /* *10 */ + if (!tmp) + { + free (res); + return 0; + } + free (res); + res = tmp; + + tmp = add_unbounded_bin_str (res, digit2const (*p)); + if (!tmp) + { + free (res); + return 0; + } + free (res); + res = tmp; + } + + assert (strip_zeroes (res) == res); + if (strlen (res)) return res; + free (res); + return btor2parser_strdup ("0"); +} + +int32_t +check_constd (const char *str, uint32_t width) +{ + assert (str); + assert (width); + + int32_t is_neg, is_min_val = 0, res; + char *bits; + size_t size_bits, len; + + is_neg = (str[0] == '-'); + len = is_neg ? strlen (str) - 1 : strlen (str); + bits = dec_to_bin_str (is_neg ? str + 1 : str, len); + size_bits = strlen (bits); + if (is_neg) + { + is_min_val = (bits[0] == '1'); + for (size_t i = 1; is_min_val && i < size_bits; i++) + is_min_val = (bits[i] == '0'); + } + res = ((is_neg && !is_min_val) || size_bits <= width) + && (!is_neg || is_min_val || size_bits + 1 <= width); + free (bits); + return res; +} + +static int32_t +parse_constant_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + + if (l->sort.tag != BTOR2_TAG_SORT_bitvec) + return perr_bfr (bfr, "expected bitvec sort for %s", l->name); + + if (l->tag == BTOR2_TAG_one || l->tag == BTOR2_TAG_ones + || l->tag == BTOR2_TAG_zero) + { + return 1; + } + + int32_t ch = getc_bfr (bfr); + if (ch != ' ') return perr_bfr (bfr, "expected space after sort id"); + + bfr->nbuf = 0; + if (l->tag == BTOR2_TAG_const) + { + while ('0' == (ch = getc_bfr (bfr)) || ch == '1') pushc_bfr (bfr, ch); + } + else if (l->tag == BTOR2_TAG_constd) + { + /* allow negative numbers */ + if ((ch = getc_bfr (bfr)) && (ch == '-' || isdigit (ch))) + pushc_bfr (bfr, ch); + while (isdigit ((ch = getc_bfr (bfr)))) pushc_bfr (bfr, ch); + } + else if (l->tag == BTOR2_TAG_consth) + { + while (isxdigit ((ch = getc_bfr (bfr)))) pushc_bfr (bfr, ch); + } + if (!bfr->nbuf) + { + perr_bfr (bfr, "expected number"); + return 0; + } + if (ch != '\n' && ch != ' ') + { + perr_bfr (bfr, "invalid character '%c' in constant definition", ch); + return 0; + } + ungetc_bfr (bfr, ch); + pushc_bfr (bfr, 0); + + if (l->tag == BTOR2_TAG_const && strlen (bfr->buf) != l->sort.bitvec.width) + { + return perr_bfr (bfr, + "constant '%s' does not match bit-vector sort size %u", + bfr->buf, + l->sort.bitvec.width); + } + else if (l->tag == BTOR2_TAG_constd + && !check_constd (bfr->buf, l->sort.bitvec.width)) + { + return perr_bfr (bfr, + "constant '%s' does not match bit-vector sort size %u", + bfr->buf, + l->sort.bitvec.width); + } + else if (l->tag == BTOR2_TAG_consth + && !check_consth (bfr->buf, l->sort.bitvec.width)) + { + return perr_bfr (bfr, + "constant '%s' does not fit into bit-vector of size %u", + bfr->buf, + l->sort.bitvec.width); + } + l->constant = btor2parser_strdup (bfr->buf); + return 1; +} + +static int32_t +parse_input_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + return parse_sort_id_bfr (bfr, &l->sort); +} + +BTOR2_DECLARE_STACK (Btor2Long, int64_t); + +static int32_t +check_state_init (Btor2Parser *bfr, int64_t state_id, int64_t init_id) +{ + assert (state_id > init_id); + (void) state_id; + + int32_t res = 1; + int64_t id; + uint32_t i; + Btor2Line *line; + Btor2LongStack stack; + char *cache; + + line = id2line_bfr (bfr, init_id); + + // 'init_id' is the highest id we will see when traversing down + size_t size = (labs (init_id) + 1) * sizeof (char); + cache = (char *)btor2parser_malloc (size); + memset (cache, 0, size); + + BTOR2_INIT_STACK (stack); + BTOR2_PUSH_STACK (int64_t, stack, init_id); + do + { + id = BTOR2_POP_STACK (stack); + assert (id); + if (id < 0) id = -id; + + // no cycles possible since state_id > init_id + assert (id != state_id); + if (cache[id]) continue; + + cache[id] = 1; + line = id2line_bfr (bfr, id); + + if (line->tag == BTOR2_TAG_input) + { + res = perr_bfr (bfr, + "inputs are not allowed in initialization expressions, " + "use a state instead of input %" PRId64 ".", + id); + break; + } + for (i = 0; i < line->nargs; i++) BTOR2_PUSH_STACK (int64_t, stack, line->args[i]); + } while (!BTOR2_EMPTY_STACK (stack)); + + free (cache); + BTOR2_RELEASE_STACK (stack); + return res; +} + +static int32_t +parse_init_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + Btor2Line *state; + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + if (!parse_args (bfr, l, 2)) return 0; + if (l->args[0] < 0) return perr_bfr (bfr, "invalid negated first argument"); + state = id2line_bfr (bfr, l->args[0]); + if (state->tag != BTOR2_TAG_state) + return perr_bfr (bfr, "expected state as first argument"); + if (l->args[0] < labs (l->args[1])) + return perr_bfr (bfr, "state id must be greater than id of second operand"); + if (!check_state_init (bfr, l->args[0], l->args[1])) return 0; + if (state->init) + return perr_bfr (bfr, "state %" PRId64 " initialized twice", state->id); + state->init = l->args[1]; + return 1; +} + +static int32_t +parse_next_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + Btor2Line *state; + if (!parse_sort_id_bfr (bfr, &l->sort)) return 0; + if (!parse_args (bfr, l, 2)) return 0; + if (l->args[0] < 0) return perr_bfr (bfr, "invalid negated first argument"); + state = id2line_bfr (bfr, l->args[0]); + if (state->tag != BTOR2_TAG_state) + return perr_bfr (bfr, "expected state as first argument"); + if (state->next) + return perr_bfr (bfr, "next for state %" PRId64 " set twice", state->id); + state->next = l->args[1]; + return 1; +} + +static int32_t +parse_constraint_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + /* contraint, bad, justice, fairness do not have a sort id after the tag */ + if (!(l->args[0] = parse_arg_bfr (bfr))) return 0; + Btor2Line *arg = id2line_bfr (bfr, l->args[0]); + if (arg->tag == BTOR2_TAG_sort) + return perr_bfr (bfr, "unexpected sort id after tag"); + l->nargs = 1; + return 1; +} + +static int32_t +parse_justice_bfr (Btor2Parser *bfr, Btor2Line *l) +{ + uint32_t nargs; + if (!parse_pos_number_bfr (bfr, &nargs)) return 0; + l->args = (int64_t *)btor2parser_realloc (l->args, sizeof (int64_t) * nargs); + l->nargs = nargs; + if (!parse_args (bfr, l, nargs)) return 0; + return 1; +} + +#define PARSE(NAME, GENERIC) \ + do \ + { \ + if (!strcmp (tag, #NAME)) \ + { \ + Btor2Line *LINE = \ + new_line_bfr (bfr, id, lineno, #NAME, BTOR2_TAG_##NAME); \ + if (parse_##GENERIC##_bfr (bfr, LINE)) \ + { \ + pusht_bfr (bfr, LINE); \ + assert (bfr->table[id] == LINE); \ + if (!check_sorts_bfr (bfr, LINE) || !parse_opt_symbol_bfr (bfr, LINE)) \ + { \ + return 0; \ + } \ + return 1; \ + } \ + else \ + { \ + return 0; \ + } \ + } \ + } while (0) + +// draft changes: +// 1) allow white spaces at beginning of the line +// 2) allow comments at the end of the line + +static int32_t +readl_bfr (Btor2Parser *bfr) +{ + const char *tag; + int64_t lineno; + int64_t id; + int32_t ch; +START: + // skip white spaces at the beginning of the line + while ((ch = getc_bfr (bfr)) == ' ') + ; + if (ch == EOF) return 0; + if (ch == '\n') goto START; + if (ch == '\t') + return perr_bfr (bfr, "unexpected tab character at start of line"); + if (ch == ';') + { + if (!skip_comment (bfr)) return 0; + goto START; + } + ungetc_bfr (bfr, ch); + if (!parse_id_bfr (bfr, &id)) return 0; + if (getc_bfr (bfr) != ' ') return perr_bfr (bfr, "expected space after id"); + if (id < bfr->ntable) + { + if (id2line_bfr (bfr, id) != 0) return perr_bfr (bfr, "id already defined"); + return perr_bfr (bfr, "id out-of-order"); + } + lineno = bfr->lineno; + tag = parse_tag (bfr); + if (!tag) return 0; + switch (tag[0]) + { + case 'a': + PARSE (add, binary_op); + PARSE (and, binary_op); + break; + case 'b': PARSE (bad, constraint); break; + case 'c': + PARSE (constraint, constraint); + PARSE (concat, binary_op); + PARSE (const, constant); + PARSE (constd, constant); + PARSE (consth, constant); + break; + case 'd': PARSE (dec, unary_op); break; + case 'e': PARSE (eq, binary_op); break; + case 'f': PARSE (fair, constraint); break; + case 'i': + PARSE (implies, binary_op); + PARSE (iff, binary_op); + PARSE (inc, unary_op); + PARSE (init, init); + PARSE (input, input); + PARSE (ite, ternary_op); + break; + case 'j': PARSE (justice, justice); break; + case 'm': PARSE (mul, binary_op); break; + case 'n': + PARSE (nand, binary_op); + PARSE (neq, binary_op); + PARSE (neg, unary_op); + PARSE (next, next); + PARSE (nor, binary_op); + PARSE (not, unary_op); + break; + case 'o': + PARSE (one, constant); + PARSE (ones, constant); + PARSE (or, binary_op); + PARSE (output, constraint); + break; + case 'r': + PARSE (read, binary_op); + PARSE (redand, unary_op); + PARSE (redor, unary_op); + PARSE (redxor, unary_op); + PARSE (rol, binary_op); + PARSE (ror, binary_op); + break; + case 's': + PARSE (saddo, binary_op); + PARSE (sext, ext); + PARSE (sgt, binary_op); + PARSE (sgte, binary_op); + PARSE (sdiv, binary_op); + PARSE (sdivo, binary_op); + PARSE (slice, slice); + PARSE (sll, binary_op); + PARSE (slt, binary_op); + PARSE (slte, binary_op); + PARSE (sort, sort); + PARSE (smod, binary_op); + PARSE (smulo, binary_op); + PARSE (ssubo, binary_op); + PARSE (sra, binary_op); + PARSE (srl, binary_op); + PARSE (srem, binary_op); + PARSE (state, input); + PARSE (sub, binary_op); + break; + case 'u': + PARSE (uaddo, binary_op); + PARSE (udiv, binary_op); + PARSE (uext, ext); + PARSE (ugt, binary_op); + PARSE (ugte, binary_op); + PARSE (ult, binary_op); + PARSE (ulte, binary_op); + PARSE (umulo, binary_op); + PARSE (urem, binary_op); + PARSE (usubo, binary_op); + break; + case 'w': PARSE (write, ternary_op); break; + case 'x': + PARSE (xnor, binary_op); + PARSE (xor, binary_op); + break; + case 'z': PARSE (zero, constant); break; + } + return perr_bfr (bfr, "invalid tag '%s'", tag); +} + +int32_t +btor2parser_read_lines (Btor2Parser *bfr, FILE *file) +{ + reset_bfr (bfr); + bfr->lineno = 1; + bfr->saved = EOF; + bfr->file = file; + while (readl_bfr (bfr)) + ; + return !bfr->error; +} + +const char * +btor2parser_error (Btor2Parser *bfr) +{ + return bfr->error; +} + +static int64_t +find_non_zero_line_bfr (Btor2Parser *bfr, int64_t start) +{ + int64_t res; + for (res = start; res < bfr->ntable; res++) + if (bfr->table[res]) return res; + return 0; +} + +Btor2LineIterator +btor2parser_iter_init (Btor2Parser *bfr) +{ + Btor2LineIterator res; + res.reader = bfr; + if (bfr->error) + res.next = 0; + else + res.next = find_non_zero_line_bfr (bfr, 1); + return res; +} + +Btor2Line * +btor2parser_iter_next (Btor2LineIterator *it) +{ + Btor2Line *res; + if (!it->next) return 0; + assert (0 < it->next); + assert (it->next < it->reader->ntable); + res = it->reader->table[it->next]; + it->next = find_non_zero_line_bfr (it->reader, it->next + 1); + return res; +} + +Btor2Line * +btor2parser_get_line_by_id (Btor2Parser *bfr, int64_t id) +{ + return id2line_bfr (bfr, id); +} + +int64_t +btor2parser_max_id (Btor2Parser *bfr) +{ + return bfr->ntable - 1; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/misc/btor/btor2parser.h b/src/misc/btor/btor2parser.h new file mode 100644 index 000000000..328068997 --- /dev/null +++ b/src/misc/btor/btor2parser.h @@ -0,0 +1,211 @@ +/** + * Btor2Tools: A tool package for the BTOR2 format. + * + * Copyright (c) 2012-2018 Armin Biere. + * Copyright (c) 2017 Mathias Preiner + * Copyright (c) 2017 Aina Niemetz + * + * All rights reserved. + * + * This file is part of the Btor2Tools package. + * See LICENSE.txt for more information on using this software. + */ + +#ifndef btor2parser_h_INCLUDED +#define btor2parser_h_INCLUDED + +/*------------------------------------------------------------------------*/ +/* The BTOR2 format is described in */ +/* "BTOR2, BtorMC and Boolector 3.0" by A. Niemetz, M. Preiner, C. Wolf */ +/* and A. Biere at CAV 2018. */ +/*------------------------------------------------------------------------*/ + +#include +#include + +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +/*------------------------------------------------------------------------*/ + +#define BTOR2_FORMAT_MAXID (((int64_t) 1) << 40) +#define BTOR2_FORMAT_MAXBITWIDTH ((1l << 30) + ((1l << 30) - 1)) + +/*------------------------------------------------------------------------*/ + +typedef struct Btor2Parser Btor2Parser; +typedef struct Btor2Line Btor2Line; +typedef struct Btor2Sort Btor2Sort; +typedef struct Btor2LineIterator Btor2LineIterator; + +/*------------------------------------------------------------------------*/ + +/** + * BTOR2 tags can be used for fast(er) traversal and operations on BTOR2 + * format lines, e.g., in a switch statement in client code. + * Alternatively, client code can use the name of the BTOR2 tag, which is a C + * string (redundantly) contained in the format line. Note that this requires + * string comparisons and is therefore slower even if client code uses an + * additional hash table. + */ +enum Btor2Tag +{ + BTOR2_TAG_add, + BTOR2_TAG_and, + BTOR2_TAG_bad, + BTOR2_TAG_concat, + BTOR2_TAG_const, + BTOR2_TAG_constraint, + BTOR2_TAG_constd, + BTOR2_TAG_consth, + BTOR2_TAG_dec, + BTOR2_TAG_eq, + BTOR2_TAG_fair, + BTOR2_TAG_iff, + BTOR2_TAG_implies, + BTOR2_TAG_inc, + BTOR2_TAG_init, + BTOR2_TAG_input, + BTOR2_TAG_ite, + BTOR2_TAG_justice, + BTOR2_TAG_mul, + BTOR2_TAG_nand, + BTOR2_TAG_neq, + BTOR2_TAG_neg, + BTOR2_TAG_next, + BTOR2_TAG_nor, + BTOR2_TAG_not, + BTOR2_TAG_one, + BTOR2_TAG_ones, + BTOR2_TAG_or, + BTOR2_TAG_output, + BTOR2_TAG_read, + BTOR2_TAG_redand, + BTOR2_TAG_redor, + BTOR2_TAG_redxor, + BTOR2_TAG_rol, + BTOR2_TAG_ror, + BTOR2_TAG_saddo, + BTOR2_TAG_sdiv, + BTOR2_TAG_sdivo, + BTOR2_TAG_sext, + BTOR2_TAG_sgt, + BTOR2_TAG_sgte, + BTOR2_TAG_slice, + BTOR2_TAG_sll, + BTOR2_TAG_slt, + BTOR2_TAG_slte, + BTOR2_TAG_sort, + BTOR2_TAG_smod, + BTOR2_TAG_smulo, + BTOR2_TAG_sra, + BTOR2_TAG_srem, + BTOR2_TAG_srl, + BTOR2_TAG_ssubo, + BTOR2_TAG_state, + BTOR2_TAG_sub, + BTOR2_TAG_uaddo, + BTOR2_TAG_udiv, + BTOR2_TAG_uext, + BTOR2_TAG_ugt, + BTOR2_TAG_ugte, + BTOR2_TAG_ult, + BTOR2_TAG_ulte, + BTOR2_TAG_umulo, + BTOR2_TAG_urem, + BTOR2_TAG_usubo, + BTOR2_TAG_write, + BTOR2_TAG_xnor, + BTOR2_TAG_xor, + BTOR2_TAG_zero, +}; +typedef enum Btor2Tag Btor2Tag; + +enum Btor2SortTag +{ + BTOR2_TAG_SORT_array, + BTOR2_TAG_SORT_bitvec, +}; +typedef enum Btor2SortTag Btor2SortTag; + +/*------------------------------------------------------------------------*/ + +struct Btor2Sort +{ + int64_t id; + Btor2SortTag tag; + const char *name; + union + { + struct + { + int64_t index; + int64_t element; + } array; + struct + { + uint32_t width; + } bitvec; + }; +}; + +struct Btor2Line +{ + int64_t id; /* positive id (non zero) */ + int64_t lineno; /* line number in original file */ + const char *name; /* name in ASCII: "and", "add", ... */ + Btor2Tag tag; /* same as name but encoded as integer */ + Btor2Sort sort; + int64_t init, next; /* non zero if initialized or has next */ + char *constant; /* non zero for const, constd, consth */ + char *symbol; /* optional for: var array state input */ + uint32_t nargs; /* number of arguments */ + int64_t *args; /* non zero ids up to nargs */ +}; + +struct Btor2LineIterator +{ + Btor2Parser *reader; + int64_t next; +}; + +/*------------------------------------------------------------------------*/ +/* Constructor, setting options and destructor: + */ +Btor2Parser *btor2parser_new (); +void btor2parser_delete (Btor2Parser *); + +/*------------------------------------------------------------------------*/ +/* The 'btor2parser_read_lines' function returns zero on failure. In this + * case you can call 'btor2parser_error' to obtain a description of + * the actual read or parse error, which includes the line number where + * the error occurred. + */ +int32_t btor2parser_read_lines (Btor2Parser *, FILE *); +const char *btor2parser_error (Btor2Parser *); + +/*------------------------------------------------------------------------*/ +/* Iterate over all read format lines: + * + * Btor2LineIterator it = btor2parser_iter_init (bfr); + * Btor2Line * l; + * while ((l = btor2parser_iter_next (&it))) + * do_something_with_btor_format_line (l); + */ +Btor2LineIterator btor2parser_iter_init (Btor2Parser *bfr); +Btor2Line *btor2parser_iter_next (Btor2LineIterator *); + +/*------------------------------------------------------------------------*/ +/* The reader maintains a mapping of ids to format lines. This mapping + * can be retrieved with the following function. Note, however, that + * ids might be negative and denote the negation of the actual node. + */ +int64_t btor2parser_max_id (Btor2Parser *); +Btor2Line *btor2parser_get_line_by_id (Btor2Parser *, int64_t id); + +/*------------------------------------------------------------------------*/ + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/misc/btor/btor2stack.h b/src/misc/btor/btor2stack.h new file mode 100644 index 000000000..f265cbf5e --- /dev/null +++ b/src/misc/btor/btor2stack.h @@ -0,0 +1,96 @@ +/** + * Btor2Tools: A tool package for the BTOR format. + * + * Copyright (C) 2007-2009 Robert Daniel Brummayer. + * Copyright (C) 2007-2013 Armin Biere. + * Copyright (C) 2013-2018 Aina Niemetz. + * Copyright (C) 2015-2016 Mathias Preiner. + * + * All rights reserved. + * + * This file is part of the Btor2Tools package. + * See LICENSE.txt for more information on using this software. + */ + +#ifndef BTOR2STACK_H_INCLUDED +#define BTOR2STACK_H_INCLUDED + +#include "btor2mem.h" + +ABC_NAMESPACE_HEADER_START + +#define BTOR2_DECLARE_STACK(name, type) \ + typedef struct name##Stack name##Stack; \ + struct name##Stack \ + { \ + type *start; \ + type *top; \ + type *end; \ + } + +BTOR2_DECLARE_STACK (BtorChar, char); +BTOR2_DECLARE_STACK (BtorCharPtr, char *); +BTOR2_DECLARE_STACK (BtorVoidPtr, void *); + +#define BTOR2_INIT_STACK(stack) \ + do \ + { \ + (stack).start = 0; \ + (stack).top = 0; \ + (stack).end = 0; \ + } while (0) + +#define BTOR2_COUNT_STACK(stack) ((stack).top - (stack).start) +#define BTOR2_SIZE_STACK(stack) ((stack).end - (stack).start) +#define BTOR2_EMPTY_STACK(stack) ((stack).top == (stack).start) +#define BTOR2_FULL_STACK(stack) ((stack).top == (stack).end) +#define BTOR2_RESET_STACK(stack) ((stack).top = (stack).start) + +#define BTOR2_RELEASE_STACK(stack) \ + do \ + { \ + BTOR2_DELETE ((stack).start); \ + BTOR2_INIT_STACK ((stack)); \ + } while (0) + +#define BTOR2_ENLARGE(T, p, o, n) \ + do \ + { \ + size_t internaln = (o) ? 2 * (o) : 1; \ + (p) = (T *) btorsim_realloc ((p), ((internaln) * sizeof (T))); \ + (n) = internaln; \ + } while (0) + +#define BTOR2_ENLARGE_STACK(T, stack) \ + do \ + { \ + size_t old_size = BTOR2_SIZE_STACK (stack), new_size; \ + size_t old_count = BTOR2_COUNT_STACK (stack); \ + BTOR2_ENLARGE (T, (stack).start, old_size, new_size); \ + (stack).top = (stack).start + old_count; \ + (stack).end = (stack).start + new_size; \ + } while (0) + +#define BTOR2_PUSH_STACK(T, stack, elem) \ + do \ + { \ + if (BTOR2_FULL_STACK ((stack))) BTOR2_ENLARGE_STACK (T, (stack)); \ + *((stack).top++) = (elem); \ + } while (0) + +#define BTOR2_POP_STACK(stack) \ + (assert (!BTOR2_EMPTY_STACK (stack)), (*--(stack).top)) + +#define BTOR2_PEEK_STACK(stack, idx) \ + (assert ((idx) < BTOR2_COUNT_STACK (stack)), (stack).start[idx]) + +#define BTOR2_POKE_STACK(stack, idx, elem) \ + do \ + { \ + assert ((idx) < BTOR2_COUNT_STACK (stack)); \ + (stack).start[idx] = (elem); \ + } while (0) + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/misc/btor/catbtor.c b/src/misc/btor/catbtor.c new file mode 100644 index 000000000..89dd16c54 --- /dev/null +++ b/src/misc/btor/catbtor.c @@ -0,0 +1,111 @@ +/** + * Btor2Tools: A tool package for the BTOR format. + * + * Copyright (c) 2012-2015 Armin Biere. + * Copyright (c) 2017 Mathias Preiner. + * Copyright (c) 2017-2018 Aina Niemetz. + * + * All rights reserved. + * + * This file is part of the Btor2Tools package. + * See LICENSE.txt for more information on using this software. + */ + +#include "btor2parser.h" + +#include +#include +#include +#include +#include + +ABC_NAMESPACE_IMPL_START + +/* Parse BTOR2 file and print to stdout. */ + +int32_t +Abc_BtorCat (char* input_name, int verbosity) +{ + FILE* input_file; + + Btor2Parser* reader; + Btor2LineIterator it; + Btor2Line* l; + uint32_t j; + const char* err; + + input_file = fopen (input_name, "r"); + if (!input_file) + { + fprintf (stderr, "*** catbtor: can not open '%s' for reading\n", input_name); + return 1; + } + + if (verbosity) + { + fprintf (stderr, + "; [catbor] simple CAT for BTOR files\n" + "; [catbor] reading '%s'\n", + input_name); + fflush (stderr); + } + reader = btor2parser_new (); + if (!btor2parser_read_lines (reader, input_file)) + { + err = btor2parser_error (reader); + assert (err); + fprintf (stderr, "*** catbtor: parse error in '%s' %s\n", input_name, err); + btor2parser_delete (reader); + fclose (input_file); + return 1; + } + fclose (input_file); + if (verbosity) + { + fprintf (stderr, "; [catbor] finished parsing '%s'\n", input_name); + fflush (stderr); + } + if (verbosity) + { + fprintf (stderr, "; [catbor] starting to dump BTOR model to ''\n"); + fflush (stderr); + } + it = btor2parser_iter_init (reader); + while ((l = btor2parser_iter_next (&it))) + { + printf ("%" PRId64 " %s", l->id, l->name); + if (l->tag == BTOR2_TAG_sort) + { + printf (" %s", l->sort.name); + switch (l->sort.tag) + { + case BTOR2_TAG_SORT_bitvec: printf (" %u", l->sort.bitvec.width); break; + case BTOR2_TAG_SORT_array: + printf (" %" PRId64 " %" PRId64, l->sort.array.index, l->sort.array.element); + break; + default: + fprintf (stderr, "*** catbtor: invalid sort encountered\n"); + btor2parser_delete (reader); + return 1; + } + } + else if (l->sort.id) + printf (" %" PRId64, l->sort.id); + for (j = 0; j < l->nargs; j++) printf (" %" PRId64, l->args[j]); + if (l->tag == BTOR2_TAG_slice) printf (" %" PRId64 " %" PRId64, l->args[1], l->args[2]); + if (l->tag == BTOR2_TAG_sext || l->tag == BTOR2_TAG_uext) + printf (" %" PRId64, l->args[1]); + if (l->constant) printf (" %s", l->constant); + if (l->symbol) printf (" %s", l->symbol); + fputc ('\n', stdout); + } + btor2parser_delete (reader); + if (verbosity) + { + fprintf (stderr, "; [catbor] finished dumping BTOR model to ''\n"); + fflush (stderr); + } + return 0; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/misc/btor/module.make b/src/misc/btor/module.make new file mode 100644 index 000000000..3298c2c42 --- /dev/null +++ b/src/misc/btor/module.make @@ -0,0 +1,2 @@ +SRC += src/misc/btor/btor2parser.c \ + src/misc/btor/catbtor.c