1439

Committed 03 Aug 2020 02:23PM UTC coverage: 64.643% (+0.6%) from 64.041%

Build # 1439

Build Type

Pull #283

travis-ci

Committed by

web-flow

Commit Message

<a href="https://github.com/SRI-CSL/yices2/commit/<a class=hub.com/SRI-CSL/yices2/commit/2833713251ded69090478cc90d0f3d4b54476ed1">283371325<a href="https://github.com/SRI-CSL/yices2/commit/2833713251ded69090478cc90d0f3d4b54476ed1">">Merge </a><a class="double-link" href="https://github.com/SRI-CSL/yices2/commit/<a class="double-link" href="https://github.com/SRI-CSL/yices2/commit/e3d1482348ff43b735daa1b32b20dc5c7191f12b">e3d148234</a>">e3d148234</a><a href="https://github.com/SRI-CSL/yices2/commit/2833713251ded69090478cc90d0f3d4b54476ed1"> into b0c8adb93">b0c8adb93</a>

Pull Request Pull Request #283: Adding solving modulo model assumptions

Run Details

1057 of 1057 new or added lines in 29 files covered. (100.0%)

72836 of 112675 relevant lines covered (64.64%)

1447077.09 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

0.0

/src/parser_utils/term_stack_error.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * ERROR MESSAGES/DIAGNOSIS ON EXCEPTION RAISED BY TERM STACK
 */

#if defined(CYGWIN) || defined(MINGW)
#ifndef __YICES_DLLSPEC__
#define __YICES_DLLSPEC__ __declspec(dllexport)
#endif
#endif

#include <stdint.h>
#include <stdbool.h>
#include <inttypes.h>
#include <assert.h>

#include "api/yices_error.h"
#include "frontend/yices/yices_tstack_ops.h"
#include "parser_utils/term_stack_error.h"

#include "yices.h"
#include "yices_exit_codes.h"


/*
 * Error messages
 */
static const char * const code2string[NUM_TSTACK_ERRORS] = {
  "no error",
  "internal error",
  "operation not supported",
  "undefined term",
  "undefined type",
  "undefined type macro",
  "invalid rational format",
  "invalid float format",
  "invalid bitvector binary format",
  "invalid bitvector hexadecimal format",
  "cannot redefine type",
  "cannot redefine term",
  "cannot redefine type macro",
  "duplicate name",
  "duplicate variable name",
  "duplicate type name",
  "invalid operation",
  "wrong number of arguments",
  "constant too large",
  "exponent must be non-negative",
  "constant is not an integer",
  "string required",
  "symbol required",
  "numerical constant required",
  "type required",
  "error in arithmetic operation",
  "division by zero",
  "divisor is not a constant",
  "size must be positive",
  "bitvectors have incompatible sizes",
  "number cannot be converted to a bitvector",
  "error in bitvector arithmetic operation",
  "error in bitvector operation",
  "incompatible types in define",
  "strings are not terms",
  "yices error",
};


/*
 * Translation of term-stack opcodes to string.
 *
 * We use two tables because some operators have a different name in
 * the SMT-LIB notation and in the Yices language.
 */
static const char * const opcode2smt_string[NUM_BASE_OPCODES] = {
  "no_op",

  "define-type",
  "define",

  "bind",
  "var declaration",
  "type-var declaration",  // for SMT2
  "let",

  "bitvector type",
  "scalar type",   // not in SMT
  "tuple type",    // not in SMT
  "function type",
  "macro application",  // for SMT2

  "function application",
  "if-then-else",
  "equality",
  "disequality",
  "distinct",
  "not",
  "or",
  "and",
  "xor",
  "iff",
  "implies",
  "mk-tuple", // not in SMT
  "select",   // not in SMT
  "tuple update", // not in SMT
  "store",
  "forall",
  "exists",
  "lambda",  // not in SMT

  "addition",
  "subtraction",
  "negation",
  "multiplication",
  "division",
  "exponentiation", // not in SMT
  "inequality",
  "inequality",
  "inequality",
  "inequality",

  "bv constant",
  "bvadd",
  "bvsub",
  "bvmul",
  "bvneg",
  "bvpow",   // not in SMT
  "bvudiv",
  "bvurem",
  "bvsdiv",
  "bvsrem",
  "bvsmod",

  "bvnot",
  "bvand",
  "bvor",
  "bvxor",
  "bvnand",
  "bvnor",
  "bvxnor",

  "shift_left0",
  "shift_left1",
  "shift_right0",
  "shift_right1",
  "ashift_right",
  "rotate_left",
  "rotate_right",

  "bvshl",
  "bvlshr",
  "bvashr",

  "extract",
  "concat",
  "repeat",
  "sign_extend",
  "zero_extend",

  "bvredand",
  "bvredor",
  "bvcomp",

  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",

  "bool-to-bv",  // not in SMT
  "bit",         // not in SMT

  "floor",       // not in SMT
  "ceil",        // not in SMT
  "abs",         // not in SMT
  "div",         // not in SMT
  "mod",         // not in SMT
  "divides",     // not in SMT
  "is_int",      // not in SMT

  "build term",
  "build type",
};



/*
 * Translate opcode to string: Yices version has more opcodes
 */
static const char * const opcode2yices_string[NUM_YICES_OPCODES] = {
  "no_op",

  "define-type",
  "define",

  "bind",
  "var declaration",
  "type-var declaration",  // SMT2 only
  "let",

  "bitvector type",
  "scalar type",
  "tuple type",
  "function type",
  "type-macro application", // SMT2

  "function application",
  "if-then-else",
  "equality",
  "disequality",
  "distinct",
  "not",
  "or",
  "and",
  "xor",
  "<=>",
  "=>",
  "mk-tuple",
  "select",
  "tuple update",
  "update",
  "forall",
  "exists",
  "lambda",

  "addition",
  "subtraction",
  "negation",
  "multiplication",
  "division",
  "exponentiation",
  "inequality",
  "inequality",
  "inequality",
  "inequality",

  "mk-bv",
  "bv-add",
  "bv-sub",
  "bv-mul",
  "bv-neg",
  "bv-pow",
  "bv-udiv",
  "bv-urem",
  "bv-sdiv",
  "bv-srem",
  "bv-smod",

  "bv-not",
  "bv-and",
  "bv-or",
  "bv-xor",
  "bv-nand",
  "bv-nor",
  "bv-xnor",

  "bv-shift-left0",
  "bv-shift-left1",
  "bv-shift-right0",
  "bv-shift-right1",
  "bv-ashift-right",
  "bv-rotate-left",
  "bv-rotate-right",

  "bv-shl",
  "bv-lshr",
  "bv-ashr",

  "bv-extract",
  "bv-concat",
  "bv-repeat",
  "bv-sign-extend",
  "bv-zero-extend",

  "bv-redand",
  "bv-redor",
  "bv-comp",

  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",
  "bitvector inequality",

  "bool-to-bv",
  "bit",

  "floor",
  "ceil",
  "abs",
  "div",
  "mod",
  "divides",
  "is_int",
  "build term",
  "build type",

  // commands in yices_tstack_ops.h
  "define-type",
  "define",
  "exit",
  "assert",
  "check",
  "show-model",
  "eval",
  "push",
  "pop",
  "reset",
  "echo",
  "include",
  "set-param",
  "show-param",
  "show-params",
  "show-stats",
  "reset-stats",
  "set-timeout",
  "show-timeout",
  "help",
  "ef-solve",
  "export-to-dimacs",
  "show-implicant",
  "dump-context",
};




/*
 * BUG in Yices: Print an error message then exit
 */
void report_bug(const char *s) {
  fprintf(stderr, "\n*************************************************************\n");
  fprintf(stderr, "FATAL ERROR: %s\n\n", s);
  fprintf(stderr, "Please report this bug to yices-bugs@csl.sri.com.\n");
  fprintf(stderr, "To help us diagnose this problem, please include the\n"
                  "following information in your bug report:\n\n");
  fprintf(stderr, "  Yices version: %s\n", yices_version);
  fprintf(stderr, "  Build date: %s\n", yices_build_date);
  fprintf(stderr, "  Platform: %s (%s)\n", yices_build_arch, yices_build_mode);
  fprintf(stderr, "\n");
  fprintf(stderr, "Thank you for your help.\n");
  fprintf(stderr, "*************************************************************\n\n");
  fflush(stderr);

  exit(YICES_EXIT_INTERNAL_ERROR);
}




/*
 * Error reported by term_api:
 * - tstack->error_op = operation being executed
 * - tstack->error_loc = location of the argument expression (approximative)
 *   that triggered the error
 * - opcode2string = either opcoode2yicse_string or opecode2smt_string
 */
static void yices_error(FILE *f, const char *name, tstack_t *tstack, const char * const opcode2string[]) {
  if (name != NULL) {
    fprintf(f, "%s: ", name);
  }
  fprintf(f, "error in %s, line %"PRId32", column %"PRId32": ",
          opcode2string[tstack->error_op], tstack->error_loc.line, tstack->error_loc.column);

  print_error(f);
}



/*
 * Print an error message for the given exception
 */
static void base_term_stack_error(FILE *f, const char *name, tstack_t *tstack, tstack_error_t exception, const char * const opcode2string[]) {
  assert(exception != TSTACK_NO_ERROR);

  if (exception == TSTACK_YICES_ERROR) {
    yices_error(f, name, tstack, opcode2string);
    return;
  }

  if (name == NULL) {
    fprintf(f, "Error: %s ", code2string[exception]);
  } else {
    fprintf(f, "%s: %s ", name, code2string[exception]);
  }

  switch (exception) {
  case TSTACK_INTERNAL_ERROR:
  case TSTACK_INVALID_OP:
  case TSTACK_NOT_A_SYMBOL:
  case TSTACK_NOT_A_TYPE:
  case TSTACK_STRINGS_ARE_NOT_TERMS:  // should never be raised by the yices or smt1 parser
    fprintf(f, "Internal exception: opcode = %"PRId32"\n", (int32_t) tstack->error_op);
    report_bug("Term-stack error");
    break;

  case TSTACK_INVALID_FRAME:
  case TSTACK_NONPOSITIVE_BVSIZE:
    fprintf(f, "in %s (line %"PRId32", column %"PRId32")\n",
            opcode2string[tstack->error_op], tstack->error_loc.line, tstack->error_loc.column);
    break;

  case TSTACK_OP_NOT_IMPLEMENTED:
    fprintf(f, "(%s)\n", opcode2string[tstack->error_op]);
    break;

  case TSTACK_UNDEF_TERM:
  case TSTACK_UNDEF_TYPE:
  case TSTACK_UNDEF_MACRO:
  case TSTACK_DUPLICATE_SCALAR_NAME:
  case TSTACK_DUPLICATE_VAR_NAME:
  case TSTACK_DUPLICATE_TYPE_VAR_NAME:
  case TSTACK_RATIONAL_FORMAT:
  case TSTACK_FLOAT_FORMAT:
  case TSTACK_BVBIN_FORMAT:
  case TSTACK_BVHEX_FORMAT:
  case TSTACK_TYPENAME_REDEF:
  case TSTACK_TERMNAME_REDEF:
  case TSTACK_MACRO_REDEF:
    fprintf(f, "%s (line %"PRId32", column %"PRId32")\n",
            tstack->error_string, tstack->error_loc.line, tstack->error_loc.column);
    break;

  case TSTACK_INTEGER_OVERFLOW:
  case TSTACK_NEGATIVE_EXPONENT:
  case TSTACK_NOT_AN_INTEGER:
  case TSTACK_NOT_A_STRING:
  case TSTACK_NOT_A_RATIONAL:
  case TSTACK_ARITH_ERROR:
  case TSTACK_DIVIDE_BY_ZERO:
  case TSTACK_NON_CONSTANT_DIVISOR:
  case TSTACK_INVALID_BVCONSTANT:
  case TSTACK_INCOMPATIBLE_BVSIZES:
  case TSTACK_BVARITH_ERROR:
  case TSTACK_BVLOGIC_ERROR:
  case TSTACK_TYPE_ERROR_IN_DEFTERM:
  case TSTACK_VARIABLES_VALUES_NOT_MATCHING:
    fprintf(f, "(line %"PRId32", column %"PRId32")\n",
            tstack->error_loc.line, tstack->error_loc.column);
    break;

  default:
    fprintf(f, "Invalid error code: %"PRId32"\n", (int32_t) exception);
    report_bug("Term-stack error");
    break;
  }
}


/*
 * Error codes defined in yices_types:
 *   0 to  99 --> reserved for basic errors in term/type construction
 * 100 to 299 --> reserved for parser errors
 * 300 to 399 --> reserved for errors in context operations
 * 400 to ... --> other error codes
 *
 * The term_stack should only trigger error codes in the range [0..99]
 * (more exactly in the range [0 .. BAD_TYPE_DECREF].
 * We assign a severity to these errors, as defined below.
 */
#define NUM_YICES_ERRORS (BAD_TYPE_DECREF+1)

/*
 * Severity of an error:
 * - severity 0: means caused by incorrect input
 * - severity 1: means bug in SMT parser or something related
 * - severity 2: means bug in term_stack or Yices parser
 */
static const uint8_t severity[NUM_YICES_ERRORS] = {
  2, // NO_ERROR (should never be raised)
  2, // INVALID_TYPE
  2, // INVALID_TERM
  2, // INVALID_CONSTANT_INDEX (bug in scalar-type construction)
  2, // INVALID_VAR_INDEX (bug in declare-var)
  1, // INVALID_TUPLE_INDEX (no tuples in SMT-LIB)
  2, // INVALID_RATIONAL_FORMAT (raised by yices_parse_rational, which is not used in term_stack)
  2, // INVALID_FLOAT_FORMAT (raised by yices_parse_float, which is not used in term_stack)
  2, // INVALID_BVBIN_FORMAT (raised by yices_parse_bvbin)
  2, // INVALID_BVHEX_FORMAT (raised by yices_parse_bvhex)
  0, // INVALID_BITSHIFT
  0, // INVALID_BVEXTRACT
  0, // INVALID_BITEXTRACT
  0, // TOO_MANY_ARGUMENTS
  0, // TOO_MANY_VARS,
  0, // MAX_BVSIZE_EXCEEDED
  0, // DEGREE_OVERFLOW
  0, // DIVISION_BY_ZERO
  0, // POS_INT_REQUIRED
  0, // NONNEG_INT_REQUIREF
  2, // SCALAR_OR_UTYPE_REQUIRED (bug in scalar-type construction)
  0, // FUNCTION_REQUIRED
  1, // TUPLE_REQUIRED (no tuples in SMT-LIB)
  2, // VARIABLE_REQUIRED (bug in term_stack)
  0, // ARITHTERM_REQUIRED
  0, // BITVECTOR_REQUIRED
  0, // SCALAR_TERM_REQUIRED
  0, // WRONG_NUMBER_OF_ARGUMENTS
  0, // TYPE_MISMATCH
  0, // INCOMPATIBLE_TYPES
  2, // DUPLICATE_VARIABLE (bug in term_stack).
  0, // INCOMPATIBLE_BVSIZES
  2, // EMPTY_BITVECTOR
  2, // ARITHCONSTANT_REQUIRED (should never be raised by term stack, see eval_mk_div)
  2, // INVALID_MACRO (bug in term_stack)
  0, // TOO_MANY_MACRO_PARAMS (used for SMT-LIB 2)
  2, // TYPE_VAR_REQUIRED (bug in term_stack)
  0, // DUPLICATE_TYPE_VAR (used in SMT-LIB 2)
  2, // BVTYPE_REQUIRED (not used anywhere)
  2, // BAD_TERM_DECREF (not used by term_stack)
  2, // BAD_TYPE_DECREF (not used by term_stack)
};


/*
 * Check for fatal errors in YICES
 * - return true if the error is a bug
 */
static inline bool fatal_error(error_code_t error) {
  return severity[error] >= 2;
}

/*
 * Check for fatal errors in SMT-LIB
 * - return true if the error involve operations that do not exist in SMT-LIB
 */
static inline bool fatal_smt_error(error_code_t error) {
  return severity[error] >= 1;
}



/*
 * Print an error message on stream f for the given exception.
 * - if name is non- NULL, the error message is
 *   'name: message ...'
 * - if name is NULL the error message is
 *   'Error: message ...'
 * The term-stack location, top-operator, etc. are used to help locate the error.
 *
 * Abort and print a request for a bug report if the error is
 * internal to Yices.
 */
void term_stack_error(FILE *f, const char *name, tstack_t *tstack, tstack_error_t exception) {
  base_term_stack_error(f, name, tstack, exception, opcode2yices_string);
  if (exception == TSTACK_YICES_ERROR && fatal_error(yices_error_code())) {
    report_bug("Internal error");
  }
}


/*
 * Same thing but also abort for exceptions that should not occur in
 * SMT-LIB input (e.g., error codes involving tuples).
 */
void term_stack_smt_error(FILE *f, const char *name, tstack_t *tstack, tstack_error_t exception) {
  base_term_stack_error(f, name, tstack, exception, opcode2smt_string);
  if (exception == TSTACK_YICES_ERROR && fatal_smt_error(yices_error_code())) {
    report_bug("Internal error (SMT-LIB)");
  }
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* ERROR MESSAGES/DIAGNOSIS ON EXCEPTION RAISED BY TERM STACK
21	*/
22
23	#if defined(CYGWIN) \|\| defined(MINGW)
24	#ifndef __YICES_DLLSPEC__
25	#define __YICES_DLLSPEC__ __declspec(dllexport)
26	#endif
27	#endif
28
29	#include <stdint.h>
30	#include <stdbool.h>
31	#include <inttypes.h>
32	#include <assert.h>
33
34	#include "api/yices_error.h"
35	#include "frontend/yices/yices_tstack_ops.h"
36	#include "parser_utils/term_stack_error.h"
37
38	#include "yices.h"
39	#include "yices_exit_codes.h"
40
41
42	/*
43	* Error messages
44	*/
45	static const char * const code2string[NUM_TSTACK_ERRORS] = {
46	"no error",
47	"internal error",
48	"operation not supported",
49	"undefined term",
50	"undefined type",
51	"undefined type macro",
52	"invalid rational format",
53	"invalid float format",
54	"invalid bitvector binary format",
55	"invalid bitvector hexadecimal format",
56	"cannot redefine type",
57	"cannot redefine term",
58	"cannot redefine type macro",
59	"duplicate name",
60	"duplicate variable name",
61	"duplicate type name",
62	"invalid operation",
63	"wrong number of arguments",
64	"constant too large",
65	"exponent must be non-negative",
66	"constant is not an integer",
67	"string required",
68	"symbol required",
69	"numerical constant required",
70	"type required",
71	"error in arithmetic operation",
72	"division by zero",
73	"divisor is not a constant",
74	"size must be positive",
75	"bitvectors have incompatible sizes",
76	"number cannot be converted to a bitvector",
77	"error in bitvector arithmetic operation",
78	"error in bitvector operation",
79	"incompatible types in define",
80	"strings are not terms",
81	"yices error",
82	};
83
84
85	/*
86	* Translation of term-stack opcodes to string.
87	*
88	* We use two tables because some operators have a different name in
89	* the SMT-LIB notation and in the Yices language.
90	*/
91	static const char * const opcode2smt_string[NUM_BASE_OPCODES] = {
92	"no_op",
93
94	"define-type",
95	"define",
96
97	"bind",
98	"var declaration",
99	"type-var declaration", // for SMT2
100	"let",
101
102	"bitvector type",
103	"scalar type", // not in SMT
104	"tuple type", // not in SMT
105	"function type",
106	"macro application", // for SMT2
107
108	"function application",
109	"if-then-else",
110	"equality",
111	"disequality",
112	"distinct",
113	"not",
114	"or",
115	"and",
116	"xor",
117	"iff",
118	"implies",
119	"mk-tuple", // not in SMT
120	"select", // not in SMT
121	"tuple update", // not in SMT
122	"store",
123	"forall",
124	"exists",
125	"lambda", // not in SMT
126
127	"addition",
128	"subtraction",
129	"negation",
130	"multiplication",
131	"division",
132	"exponentiation", // not in SMT
133	"inequality",
134	"inequality",
135	"inequality",
136	"inequality",
137
138	"bv constant",
139	"bvadd",
140	"bvsub",
141	"bvmul",
142	"bvneg",
143	"bvpow", // not in SMT
144	"bvudiv",
145	"bvurem",
146	"bvsdiv",
147	"bvsrem",
148	"bvsmod",
149
150	"bvnot",
151	"bvand",
152	"bvor",
153	"bvxor",
154	"bvnand",
155	"bvnor",
156	"bvxnor",
157
158	"shift_left0",
159	"shift_left1",
160	"shift_right0",
161	"shift_right1",
162	"ashift_right",
163	"rotate_left",
164	"rotate_right",
165
166	"bvshl",
167	"bvlshr",
168	"bvashr",
169
170	"extract",
171	"concat",
172	"repeat",
173	"sign_extend",
174	"zero_extend",
175
176	"bvredand",
177	"bvredor",
178	"bvcomp",
179
180	"bitvector inequality",
181	"bitvector inequality",
182	"bitvector inequality",
183	"bitvector inequality",
184	"bitvector inequality",
185	"bitvector inequality",
186	"bitvector inequality",
187	"bitvector inequality",
188
189	"bool-to-bv", // not in SMT
190	"bit", // not in SMT
191
192	"floor", // not in SMT
193	"ceil", // not in SMT
194	"abs", // not in SMT
195	"div", // not in SMT
196	"mod", // not in SMT
197	"divides", // not in SMT
198	"is_int", // not in SMT
199
200	"build term",
201	"build type",
202	};
203
204
205
206	/*
207	* Translate opcode to string: Yices version has more opcodes
208	*/
209	static const char * const opcode2yices_string[NUM_YICES_OPCODES] = {
210	"no_op",
211
212	"define-type",
213	"define",
214
215	"bind",
216	"var declaration",
217	"type-var declaration", // SMT2 only
218	"let",
219
220	"bitvector type",
221	"scalar type",
222	"tuple type",
223	"function type",
224	"type-macro application", // SMT2
225
226	"function application",
227	"if-then-else",
228	"equality",
229	"disequality",
230	"distinct",
231	"not",
232	"or",
233	"and",
234	"xor",
235	"<=>",
236	"=>",
237	"mk-tuple",
238	"select",
239	"tuple update",
240	"update",
241	"forall",
242	"exists",
243	"lambda",
244
245	"addition",
246	"subtraction",
247	"negation",
248	"multiplication",
249	"division",
250	"exponentiation",
251	"inequality",
252	"inequality",
253	"inequality",
254	"inequality",
255
256	"mk-bv",
257	"bv-add",
258	"bv-sub",
259	"bv-mul",
260	"bv-neg",
261	"bv-pow",
262	"bv-udiv",
263	"bv-urem",
264	"bv-sdiv",
265	"bv-srem",
266	"bv-smod",
267
268	"bv-not",
269	"bv-and",
270	"bv-or",
271	"bv-xor",
272	"bv-nand",
273	"bv-nor",
274	"bv-xnor",
275
276	"bv-shift-left0",
277	"bv-shift-left1",
278	"bv-shift-right0",
279	"bv-shift-right1",
280	"bv-ashift-right",
281	"bv-rotate-left",
282	"bv-rotate-right",
283
284	"bv-shl",
285	"bv-lshr",
286	"bv-ashr",
287
288	"bv-extract",
289	"bv-concat",
290	"bv-repeat",
291	"bv-sign-extend",
292	"bv-zero-extend",
293
294	"bv-redand",
295	"bv-redor",
296	"bv-comp",
297
298	"bitvector inequality",
299	"bitvector inequality",
300	"bitvector inequality",
301	"bitvector inequality",
302	"bitvector inequality",
303	"bitvector inequality",
304	"bitvector inequality",
305	"bitvector inequality",
306
307	"bool-to-bv",
308	"bit",
309
310	"floor",
311	"ceil",
312	"abs",
313	"div",
314	"mod",
315	"divides",
316	"is_int",
317	"build term",
318	"build type",
319
320	// commands in yices_tstack_ops.h
321	"define-type",
322	"define",
323	"exit",
324	"assert",
325	"check",
326	"show-model",
327	"eval",
328	"push",
329	"pop",
330	"reset",
331	"echo",
332	"include",
333	"set-param",
334	"show-param",
335	"show-params",
336	"show-stats",
337	"reset-stats",
338	"set-timeout",
339	"show-timeout",
340	"help",
341	"ef-solve",
342	"export-to-dimacs",
343	"show-implicant",
344	"dump-context",
345	};
346
347
348
349
350	/*
351	* BUG in Yices: Print an error message then exit
352	*/
353	void report_bug(const char *s) {	×
354	fprintf(stderr, "\n*************************************************************\n");	×
355	fprintf(stderr, "FATAL ERROR: %s\n\n", s);	×
356	fprintf(stderr, "Please report this bug to yices-bugs@csl.sri.com.\n");	×
357	fprintf(stderr, "To help us diagnose this problem, please include the\n"	×
358	"following information in your bug report:\n\n");
359	fprintf(stderr, " Yices version: %s\n", yices_version);	×
360	fprintf(stderr, " Build date: %s\n", yices_build_date);	×
361	fprintf(stderr, " Platform: %s (%s)\n", yices_build_arch, yices_build_mode);	×
362	fprintf(stderr, "\n");	×
363	fprintf(stderr, "Thank you for your help.\n");	×
364	fprintf(stderr, "*************************************************************\n\n");	×
365	fflush(stderr);	×
366
367	exit(YICES_EXIT_INTERNAL_ERROR);	×
368	}
369
370
371
372
373	/*
374	* Error reported by term_api:
375	* - tstack->error_op = operation being executed
376	* - tstack->error_loc = location of the argument expression (approximative)
377	* that triggered the error
378	* - opcode2string = either opcoode2yicse_string or opecode2smt_string
379	*/
380	static void yices_error(FILE f, const char name, tstack_t tstack, const char const opcode2string[]) {	×
381	if (name != NULL) {	×
382	fprintf(f, "%s: ", name);	×
383	}
384	fprintf(f, "error in %s, line %"PRId32", column %"PRId32": ",	×
385	opcode2string[tstack->error_op], tstack->error_loc.line, tstack->error_loc.column);	×
386
387	print_error(f);	×
388	}	×
389
390
391
392	/*
393	* Print an error message for the given exception
394	*/
395	static void base_term_stack_error(FILE f, const char name, tstack_t tstack, tstack_error_t exception, const char const opcode2string[]) {	×
396	assert(exception != TSTACK_NO_ERROR);
397
398	if (exception == TSTACK_YICES_ERROR) {	×
399	yices_error(f, name, tstack, opcode2string);	×
400	return;	×
401	}
402
403	if (name == NULL) {	×
404	fprintf(f, "Error: %s ", code2string[exception]);	×
405	} else {
406	fprintf(f, "%s: %s ", name, code2string[exception]);	×
407	}
408
409	switch (exception) {	×
410	case TSTACK_INTERNAL_ERROR:
411	case TSTACK_INVALID_OP:
412	case TSTACK_NOT_A_SYMBOL:
413	case TSTACK_NOT_A_TYPE:
414	case TSTACK_STRINGS_ARE_NOT_TERMS: // should never be raised by the yices or smt1 parser
415	fprintf(f, "Internal exception: opcode = %"PRId32"\n", (int32_t) tstack->error_op);	×
416	report_bug("Term-stack error");	×
417	break;
418
419	case TSTACK_INVALID_FRAME:
420	case TSTACK_NONPOSITIVE_BVSIZE:
421	fprintf(f, "in %s (line %"PRId32", column %"PRId32")\n",	×
422	opcode2string[tstack->error_op], tstack->error_loc.line, tstack->error_loc.column);	×
423	break;	×
424
425	case TSTACK_OP_NOT_IMPLEMENTED:
426	fprintf(f, "(%s)\n", opcode2string[tstack->error_op]);	×
427	break;	×
428
429	case TSTACK_UNDEF_TERM:
430	case TSTACK_UNDEF_TYPE:
431	case TSTACK_UNDEF_MACRO:
432	case TSTACK_DUPLICATE_SCALAR_NAME:
433	case TSTACK_DUPLICATE_VAR_NAME:
434	case TSTACK_DUPLICATE_TYPE_VAR_NAME:
435	case TSTACK_RATIONAL_FORMAT:
436	case TSTACK_FLOAT_FORMAT:
437	case TSTACK_BVBIN_FORMAT:
438	case TSTACK_BVHEX_FORMAT:
439	case TSTACK_TYPENAME_REDEF:
440	case TSTACK_TERMNAME_REDEF:
441	case TSTACK_MACRO_REDEF:
442	fprintf(f, "%s (line %"PRId32", column %"PRId32")\n",	×
443	tstack->error_string, tstack->error_loc.line, tstack->error_loc.column);
444	break;	×
445
446	case TSTACK_INTEGER_OVERFLOW:
447	case TSTACK_NEGATIVE_EXPONENT:
448	case TSTACK_NOT_AN_INTEGER:
449	case TSTACK_NOT_A_STRING:
450	case TSTACK_NOT_A_RATIONAL:
451	case TSTACK_ARITH_ERROR:
452	case TSTACK_DIVIDE_BY_ZERO:
453	case TSTACK_NON_CONSTANT_DIVISOR:
454	case TSTACK_INVALID_BVCONSTANT:
455	case TSTACK_INCOMPATIBLE_BVSIZES:
456	case TSTACK_BVARITH_ERROR:
457	case TSTACK_BVLOGIC_ERROR:
458	case TSTACK_TYPE_ERROR_IN_DEFTERM:
459	case TSTACK_VARIABLES_VALUES_NOT_MATCHING:
460	fprintf(f, "(line %"PRId32", column %"PRId32")\n",	×
461	tstack->error_loc.line, tstack->error_loc.column);
462	break;	×
463
464	default:
465	fprintf(f, "Invalid error code: %"PRId32"\n", (int32_t) exception);	×
466	report_bug("Term-stack error");	×
467	break;
468	}
469	}
470
471
472	/*
473	* Error codes defined in yices_types:
474	* 0 to 99 --> reserved for basic errors in term/type construction
475	* 100 to 299 --> reserved for parser errors
476	* 300 to 399 --> reserved for errors in context operations
477	* 400 to ... --> other error codes
478	*
479	* The term_stack should only trigger error codes in the range [0..99]
480	* (more exactly in the range [0 .. BAD_TYPE_DECREF].
481	* We assign a severity to these errors, as defined below.
482	*/
483	#define NUM_YICES_ERRORS (BAD_TYPE_DECREF+1)
484
485	/*
486	* Severity of an error:
487	* - severity 0: means caused by incorrect input
488	* - severity 1: means bug in SMT parser or something related
489	* - severity 2: means bug in term_stack or Yices parser
490	*/
491	static const uint8_t severity[NUM_YICES_ERRORS] = {
492	2, // NO_ERROR (should never be raised)
493	2, // INVALID_TYPE
494	2, // INVALID_TERM
495	2, // INVALID_CONSTANT_INDEX (bug in scalar-type construction)
496	2, // INVALID_VAR_INDEX (bug in declare-var)
497	1, // INVALID_TUPLE_INDEX (no tuples in SMT-LIB)
498	2, // INVALID_RATIONAL_FORMAT (raised by yices_parse_rational, which is not used in term_stack)
499	2, // INVALID_FLOAT_FORMAT (raised by yices_parse_float, which is not used in term_stack)
500	2, // INVALID_BVBIN_FORMAT (raised by yices_parse_bvbin)
501	2, // INVALID_BVHEX_FORMAT (raised by yices_parse_bvhex)
502	0, // INVALID_BITSHIFT
503	0, // INVALID_BVEXTRACT
504	0, // INVALID_BITEXTRACT
505	0, // TOO_MANY_ARGUMENTS
506	0, // TOO_MANY_VARS,
507	0, // MAX_BVSIZE_EXCEEDED
508	0, // DEGREE_OVERFLOW
509	0, // DIVISION_BY_ZERO
510	0, // POS_INT_REQUIRED
511	0, // NONNEG_INT_REQUIREF
512	2, // SCALAR_OR_UTYPE_REQUIRED (bug in scalar-type construction)
513	0, // FUNCTION_REQUIRED
514	1, // TUPLE_REQUIRED (no tuples in SMT-LIB)
515	2, // VARIABLE_REQUIRED (bug in term_stack)
516	0, // ARITHTERM_REQUIRED
517	0, // BITVECTOR_REQUIRED
518	0, // SCALAR_TERM_REQUIRED
519	0, // WRONG_NUMBER_OF_ARGUMENTS
520	0, // TYPE_MISMATCH
521	0, // INCOMPATIBLE_TYPES
522	2, // DUPLICATE_VARIABLE (bug in term_stack).
523	0, // INCOMPATIBLE_BVSIZES
524	2, // EMPTY_BITVECTOR
525	2, // ARITHCONSTANT_REQUIRED (should never be raised by term stack, see eval_mk_div)
526	2, // INVALID_MACRO (bug in term_stack)
527	0, // TOO_MANY_MACRO_PARAMS (used for SMT-LIB 2)
528	2, // TYPE_VAR_REQUIRED (bug in term_stack)
529	0, // DUPLICATE_TYPE_VAR (used in SMT-LIB 2)
530	2, // BVTYPE_REQUIRED (not used anywhere)
531	2, // BAD_TERM_DECREF (not used by term_stack)
532	2, // BAD_TYPE_DECREF (not used by term_stack)
533	};
534
535
536	/*
537	* Check for fatal errors in YICES
538	* - return true if the error is a bug
539	*/
540	static inline bool fatal_error(error_code_t error) {	×
541	return severity[error] >= 2;	×
542	}
543
544	/*
545	* Check for fatal errors in SMT-LIB
546	* - return true if the error involve operations that do not exist in SMT-LIB
547	*/
548	static inline bool fatal_smt_error(error_code_t error) {	×
549	return severity[error] >= 1;	×
550	}
551
552
553
554	/*
555	* Print an error message on stream f for the given exception.
556	* - if name is non- NULL, the error message is
557	* 'name: message ...'
558	* - if name is NULL the error message is
559	* 'Error: message ...'
560	* The term-stack location, top-operator, etc. are used to help locate the error.
561	*
562	* Abort and print a request for a bug report if the error is
563	* internal to Yices.
564	*/
565	void term_stack_error(FILE f, const char name, tstack_t *tstack, tstack_error_t exception) {	×
566	base_term_stack_error(f, name, tstack, exception, opcode2yices_string);	×
567	if (exception == TSTACK_YICES_ERROR && fatal_error(yices_error_code())) {	×
568	report_bug("Internal error");	×
569	}
570	}	×
571
572
573	/*
574	* Same thing but also abort for exceptions that should not occur in
575	* SMT-LIB input (e.g., error codes involving tuples).
576	*/
577	void term_stack_smt_error(FILE f, const char name, tstack_t *tstack, tstack_error_t exception) {	×
578	base_term_stack_error(f, name, tstack, exception, opcode2smt_string);	×
579	if (exception == TSTACK_YICES_ERROR && fatal_smt_error(yices_error_code())) {	×
580	report_bug("Internal error (SMT-LIB)");	×
581	}
582	}	×

SRI-CSL / yices2 / 1439

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous