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 * INTERNAL/LOW-LEVEL TERM-STACK OPERATIONS
21 */
22
23 /*
24 * Low-level functions that manipulate internal tstack structures
25 * are declared here and implemented in term_stack.c.
26 *
27 * They should be used only for defining new term stack operations or
28 * modifying existing term stack operations.
29 *
30 * To add or change an operation, define two functions
31 * - void check_some_op(tstack_t *stack, stack_elem_t *e, uint32_t n)
32 * - void eval_some_op((tstack_t *stack, stack_elem_t *e, uint32_t n)
33 *
34 * then install both in stack using
35 * tstack_add_op(stack, opcode, flag, eval_new_op, check_new_op);
36 *
37 * - opcode should be an integer constant (cf. term_stack.h)
38 * - flag should be true for associative operations, false otherwise.
39 */
40
41
42 #ifndef __TSTACK_INTERNALS_H
43 #define __TSTACK_INTERNALS_H
44
45 #include "parser_utils/term_stack2.h"
46
47
48 /*
49 * Raise an exception when processing element e
50 * - stack->error_pos is set to e->pos
51 * - stack->error_op is set to stack->top_op
52 * - stack->error_string is set to e's string field if e is a symbol or a binding,
53 * or to NULL otherwise.
54 * code is returned to the enclosing exception handler by longjmp
55 *
56 * NOTE: It's possible to raise exceptions that are not defined in tstack_error_t
57 * by using an integer code > TSTACK_YICES_ERROR. This requires that the interrupt
58 * handler knows how to deal with such codes.
59 */
60 extern void __attribute__((noreturn)) raise_exception(tstack_t *stack, stack_elem_t *e, int code);
61
62
63 /*
64 * Raise an exception when pushing data on the stack
65 * - stack->error_pos is set to loc
66 * - stack->error_string is set to s (not a copy)
67 * then code is returned to the enclosing exception handler by longjmp
68 */
69 extern void __attribute__((noreturn)) push_exception(tstack_t *stack, loc_t *loc, char *s, int code);
70
71
72 /*
73 * Raise an exception when a yices function returns NULL_TERM or another error code.
74 * - this raises exception TSTACK_YICES_ERROR
75 * - stack->error_loc is set to the top-frame's location
76 * - stack->error_op is set to the top_operator code
77 * - stack->error_string is NULL
78 */
79 extern void __attribute__((noreturn)) report_yices_error(tstack_t *stack);
80
81
82 /*
83 * Check whether e->tag is equal to tg
84 * - if not raise an exception
85 */
86 extern void check_tag(tstack_t *stack, stack_elem_t *e, tag_t tg);
87
88
89 /*
90 * Check whether cond is true (cond should be a constraint on the number of elements
91 * on the top frame). If cond is false, raise exception INVALID_FRAME.
92 */
93 extern void check_size(tstack_t *stack, bool cond);
94
95
96 /*
97 * Check whether the top operator is equal to op.
98 * - if not raise exception INTERNAL_ERROR
99 */
100 extern void check_op(tstack_t *stack, int32_t op);
101
102
103 /*
104 * Check whether all elements from e to end have tag tg
105 * - if not raise an exception
106 *
107 * This is equivalent to
108 * for (t = e; t<end; t++) {
109 * check_tag(stack, t, tg);
110 * }
111 */
112 extern void check_all_tags(tstack_t *stack, stack_elem_t *e, stack_elem_t *end, tag_t tg);
113
114
115 /*
116 * Check whether all names in a list of variable bindings are distinct
117 * - names are in f[0] .. f[n-1]
118 * - all must be bindings (tag == TAG_BINDING)
119 * if the test fails, raise exception DUPLICATE_VAR_NAME
120 */
121 extern void check_distinct_binding_names(tstack_t *stack, stack_elem_t *f, uint32_t n);
122
123
124 /*
125 * Check whether all names in a list of type variables are distinct
126 * - names are in f[0] .. f[n-1]
127 * - all must be have tag == TAG_TYPE_BINDING
128 * if the test fails, raise exception DUPLICATE_TYPE_VAR_NAME
129 */
130 extern void check_distinct_type_binding_names(tstack_t *stack, stack_elem_t *f, uint32_t n);
131
132
133
134 /*
135 * OPERATORS
136 */
137
138 /*
139 * To implement term annotations/attributes, we need to know the context
140 * (i.e., the enclosing operator of an annotated term).
141 *
142 * For example: (assert (! <term> :named xxx)) must be treated as
143 * a named assertion rather than the assertion of a named term.
144 * To deal with this, we allow term-stack functions to query the term stack
145 * to examine the current top and the enclosing operator:
146 * - get_top_op returns the top-level operator (or NO_OP if the stack is empty)
147 * - get_enclosing_op returns the previous operator on the stack (or NO_OP
148 * if there's just one frame on the stack).
149 *
150 * Examples:
151 * 1) in (assert (! <term> :named xxx)), the stack will
152 * have two operators: [ASSERT [ADD_ATTRIBUTES <term> ...]].
153 * When we process ADD_ATTRIBUTES:
154 * top_op = ADD_ATTRIBUTES
155 * enclosing_op = ASSERT
156 *
157 * 2) in (forall ((x T)) (! (P X) :pattern xxx))
158 * The stack will have [FORALL [BINDING ..] [ADD_ATTRIBUTES <term> ...]
159 * When we process ADD_ATTRIBUTES:
160 * top_op = ADD_ATTRIBUTES
161 * enclosing_op = FORALL
162 */
get_top_op(tstack_t * stack)163 static inline int32_t get_top_op(tstack_t *stack) {
164 return stack->top_op; // equal to NO_OP if the stack is empty
165 }
166
167 extern int32_t get_enclosing_op(tstack_t *stack);
168
169
170
171 /*
172 * CONVERSION
173 */
174
175 /*
176 * Convert element e to a term or raise an exception if e can't be converted
177 */
178 extern term_t get_term(tstack_t *stack, stack_elem_t *e);
179
180
181 /*
182 * Return the integer value of e (e must have rational tag)
183 * Raise an exception if e is too large or is not an integer.
184 */
185 extern int32_t get_integer(tstack_t *stack, stack_elem_t *e);
186
187
188 /*
189 * Support for division: return a rational constant equal to den
190 * provided den is constant and non-zero
191 *
192 * Raise exception otherwise
193 */
194 extern rational_t *get_divisor(tstack_t *stack, stack_elem_t *den);
195
196
197 /*
198 * Convert element e into a signed symbol:
199 * This checks whether e has tag TAG_SYMBOL or TAG_NOT_SYMBOL
200 * then copy the symbol's name in s->name and the polarity in s->polarity.
201 * Polarity true means TAG_SYMBOL. Polarity false means TAG_NOT_SYMBOL.
202 *
203 * IMPORTANT: this function does not make a copy of the string.
204 *
205 * Raise an exception if e has another tag.
206 */
207 extern void get_signed_symbol(tstack_t *stack, stack_elem_t *e, signed_symbol_t *s);
208
209
210
211 /*
212 * BUFFER ALLOCATION
213 */
214
215 /*
216 * All operations below return an initialized/empty buffer that can be
217 * pushed onto the stack using set_arith_result,
218 * set_bvarith64_results, and variants.
219 */
220 extern rba_buffer_t *tstack_get_abuffer(tstack_t *stack);
221 extern bvarith64_buffer_t *tstack_get_bva64buffer(tstack_t *stack, uint32_t bitsize);
222 extern bvarith_buffer_t *tstack_get_bvabuffer(tstack_t *stack, uint32_t bitsize);
223 extern bvlogic_buffer_t *tstack_get_bvlbuffer(tstack_t *stack);
224
225
226 /*
227 * Make the auxiliary buffer large enough for n integers
228 */
229 extern void extend_aux_buffer(tstack_t *stack, uint32_t n);
230
get_aux_buffer(tstack_t * stack,uint32_t n)231 static inline int32_t *get_aux_buffer(tstack_t *stack, uint32_t n) {
232 if (stack->aux_size < n) {
233 extend_aux_buffer(stack, n);
234 }
235 return stack->aux_buffer;
236 }
237
238 /*
239 * Make the symbol buffer large enough for n symbols
240 */
241 extern void extend_sbuffer(tstack_t *stack, uint32_t n);
242
get_sbuffer(tstack_t * stack,uint32_t n)243 static inline signed_symbol_t *get_sbuffer(tstack_t *stack, uint32_t n) {
244 if (stack->sbuffer_size < n) {
245 extend_sbuffer(stack, n);
246 }
247 return stack->sbuffer;
248 }
249
250 /*
251 * ARITHMETIC AND BITVECTOR OPERATIONS
252 */
253
254 /*
255 * All operations update a buffer using a stack element e
256 * - the functions attempt to convert e to a term or constant of the
257 * right type. then apply the operation to buffer
258 */
259 // arithmetic
260 extern void add_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
261 extern void sub_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
262 extern void mul_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
263
264 // bitvector arithmetic for size <= 64
265 extern void bva64_add_elem(tstack_t *stack, bvarith64_buffer_t *b, stack_elem_t *e);
266 extern void bva64_sub_elem(tstack_t *stack, bvarith64_buffer_t *b, stack_elem_t *e);
267 extern void bva64_mul_elem(tstack_t *stack, bvarith64_buffer_t *b, stack_elem_t *e);
268
269 // bitvector arithmetic for size > 64
270 extern void bva_add_elem(tstack_t *stack, bvarith_buffer_t *b, stack_elem_t *e);
271 extern void bva_sub_elem(tstack_t *stack, bvarith_buffer_t *b, stack_elem_t *e);
272 extern void bva_mul_elem(tstack_t *stack, bvarith_buffer_t *b, stack_elem_t *e);
273
274
275 // copy e into b
276 extern void bvl_set_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
277
278 // copy e[i..j] into b (must satisfy 0 <= i < j < e's size)
279 extern void bvl_set_slice_elem(tstack_t *stack, bvlogic_buffer_t *b, uint32_t i, uint32_t j, stack_elem_t *e);
280
281 // add e to the right of b (i.e., high-order bits are from b, low-order bits from e)
282 extern void bvconcat_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
283
284 // bitwise operations
285 extern void bvand_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
286 extern void bvor_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
287 extern void bvxor_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
288 extern void bvcomp_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
289
290
291 /*
292 * In place operations: modify e
293 */
294 // replace e by -e. raise an exception if e is not an arithmetic object
295 extern void neg_elem(tstack_t *stack, stack_elem_t *e);
296
297 // negate e (2's complement): raise an exception if e is not bitvector
298 extern void bvneg_elem(tstack_t *stack, stack_elem_t *e);
299
300
301 /*
302 * Check whether e is a bitvector constant
303 */
304 extern bool elem_is_bvconst(stack_elem_t *e);
305
306
307 /*
308 * Copy the constant value of e into c
309 * - e must satisfy elem_is_bvconst(e)
310 */
311 extern void bvconst_set_elem(bvconstant_t *c, stack_elem_t *e);
312
313
314
315 /*
316 * POP_FRAME AND STORE RESULTS
317 */
318
319 /*
320 * Remove the top-frame (except the operator)
321 * - this must be followed by set_xxx_result, which replaces the top
322 * stack element element by a result
323 */
324 extern void tstack_pop_frame(tstack_t *stack);
325
326 /*
327 * Replace the top stack element by a new value
328 * - this keeps the top-element's loc field unchanged
329 */
330 extern void set_term_result(tstack_t *stack, term_t t);
331 extern void set_type_result(tstack_t *stack, type_t tau);
332 extern void set_binding_result(tstack_t *stack, term_t t, char *symbol);
333 extern void set_type_binding_result(tstack_t *stack, type_t, char *symbol);
334 extern void set_bv64_result(tstack_t *stack, uint32_t nbits, uint64_t c);
335 extern void set_bv_result(tstack_t *stack, uint32_t nbits, uint32_t *bv);
336 extern void set_arith_result(tstack_t *stack, rba_buffer_t *b);
337 extern void set_bvarith64_result(tstack_t *stack, bvarith64_buffer_t *b);
338 extern void set_bvarith_result(tstack_t *stack, bvarith_buffer_t *b);
339 extern void set_bvlogic_result(tstack_t *stack, bvlogic_buffer_t *b);
340 extern void set_aval_result(tstack_t *stack, aval_t v);
341
342 // no result: remove the top element
no_result(tstack_t * stack)343 static inline void no_result(tstack_t *stack) {
344 stack->top --;
345 }
346
347 /*
348 * Replace the top stack element by term t and mark it as special.
349 */
350 extern void set_special_term_result(tstack_t *stack, term_t t);
351
352 /*
353 * Check whether element stored in v is a special term:
354 * - v must be a pointer in the current top frame
355 */
tstack_elem_is_special(stack_elem_t * v)356 static inline bool tstack_elem_is_special(stack_elem_t *v) {
357 return v->tag == TAG_SPECIAL_TERM;
358 }
359
360
361
362 /*
363 * Copy v as result in place of the current stack->frame
364 * then remove all elements above the top frame index.
365 * - v must be a pointer in the current top frame
366 * - v's TAG must not be string/symbol.
367 */
368 extern void copy_result_and_pop_frame(tstack_t *stack, stack_elem_t *v);
369
370
371 /*
372 * CALL AN EXISTING OPERATION
373 */
374
375 /*
376 * Call the function check[op] or eval[op] on f[0] .... f[n-1]
377 * - call_tstack_eval removes the top frame and stores the result of
378 * (op f[0] ... f[n-1]) on top of the stack.
379 */
380 extern void call_tstack_check(tstack_t *stack, int32_t op, stack_elem_t *f, uint32_t n);
381 extern void call_tstack_eval(tstack_t *stack, int32_t op, stack_elem_t *f, uint32_t n);
382
383
384
385 /*
386 * BIT-VECTOR OPERATIONS
387 */
388
389 /*
390 * The functions below are exported to help support both Yices-2 and SMT-LIB
391 * notations. The Yices2 and SMT-LIB versions are identical but take arguments
392 * in the opposite order.
393 */
394
395 /*
396 * Build bitvector constant defined by val and size:
397 * - size = number of bits
398 * - val = value
399 * - f = frame index: it's used for error reporting only
400 * Raise an exception if size <= 0 or size > MAX_BV_SIZE or val is not a non-negative
401 * integer.
402 */
403 extern void mk_bv_const_core(tstack_t *stack, stack_elem_t *f, int32_t size, rational_t *val);
404
405
406 /*
407 * Sign-extend and zero-extend:
408 * - bv = stack element expected to contain the bitvector
409 * - idx = stack element expected to contain an integer
410 *
411 * These should be used for MK_BV_SIGN_EXTEND and MK_BV_ZERO_EXTEND,
412 * which require a stack frame with two arguments. One of them
413 * should be bv the other one should be idx.
414 *
415 * These functions check the arguments bv and idx then push the
416 * zero/sign extension bv + idx bits on top of the stack.
417 */
418 extern void mk_bv_sign_extend_core(tstack_t *stack, stack_elem_t *bv, stack_elem_t *idx);
419 extern void mk_bv_zero_extend_core(tstack_t *stack, stack_elem_t *bv, stack_elem_t *idx);
420
421
422 #endif /* __TSTACK_INTERNALS */
423