16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Run Details

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

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

94.12

/src/parser_utils/tstack_internals.h

/*
 * 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/>.
 */

/*
 * INTERNAL/LOW-LEVEL TERM-STACK OPERATIONS
 */

/*
 * Low-level functions that manipulate internal tstack structures
 * are declared here and implemented in term_stack.c.
 *
 * They should be used only for defining new term stack operations or
 * modifying existing term stack operations.
 *
 * To add or change an operation, define two functions
 * - void check_some_op(tstack_t *stack, stack_elem_t *e, uint32_t n)
 * - void eval_some_op((tstack_t *stack, stack_elem_t *e, uint32_t n)
 *
 * then install both in stack using
 *   tstack_add_op(stack, opcode, flag, eval_new_op, check_new_op);
 *
 * - opcode should be an integer constant (cf. term_stack.h)
 * - flag should be true for associative operations, false otherwise.
 */


#ifndef __TSTACK_INTERNALS_H
#define __TSTACK_INTERNALS_H

#include "parser_utils/term_stack2.h"


/*
 * Raise an exception when processing element e
 * - stack->error_pos is set to e->pos
 * - stack->error_op is set to stack->top_op
 * - stack->error_string is set to e's string field if e is a symbol or a binding,
 *   or to NULL otherwise.
 * code is returned to the enclosing exception handler by longjmp
 *
 * NOTE: It's possible to raise exceptions that are not defined in tstack_error_t
 * by using an integer code > TSTACK_YICES_ERROR. This requires that the interrupt
 * handler knows how to deal with such codes.
 */
extern void __attribute__((noreturn)) raise_exception(tstack_t *stack, stack_elem_t *e, int code);


/*
 * Raise an exception when pushing data on the stack
 * - stack->error_pos is set to loc
 * - stack->error_string is set to s (not a copy)
 * then code is returned to the enclosing exception handler by longjmp
 */
extern void __attribute__((noreturn)) push_exception(tstack_t *stack, loc_t *loc, char *s, int code);


/*
 * Raise an exception when a yices function returns NULL_TERM or another error code.
 * - this raises exception TSTACK_YICES_ERROR
 * - stack->error_loc is set to the top-frame's location
 * - stack->error_op is set to the top_operator code
 * - stack->error_string is NULL
 */
extern void __attribute__((noreturn)) report_yices_error(tstack_t *stack);


/*
 * Check whether e->tag is equal to tg
 * - if not raise an exception
 */
extern void check_tag(tstack_t *stack, stack_elem_t *e, tag_t tg);


/*
 * Check whether cond is true (cond should be a constraint on the number of elements
 * on the top frame). If cond is false, raise exception INVALID_FRAME.
 */
extern void check_size(tstack_t *stack, bool cond);


/*
 * Check whether the top operator is equal to op.
 * - if not raise exception INTERNAL_ERROR
 */
extern void check_op(tstack_t *stack, int32_t op);


/*
 * Check whether all elements from e to end have tag tg
 * - if not raise an exception
 *
 * This is equivalent to
 *   for (t = e; t<end; t++) {
 *     check_tag(stack, t, tg);
 *   }
 */
extern void check_all_tags(tstack_t *stack, stack_elem_t *e, stack_elem_t *end, tag_t tg);


/*
 * Check whether all names in a list of variable bindings are distinct
 * - names are in f[0] .. f[n-1]
 * - all must be  bindings (tag == TAG_BINDING)
 * if the test fails, raise exception DUPLICATE_VAR_NAME
 */
extern void check_distinct_binding_names(tstack_t *stack, stack_elem_t *f, uint32_t n);


/*
 * Check whether all names in a list of type variables are distinct
 * - names are in f[0] .. f[n-1]
 * - all must be have tag == TAG_TYPE_BINDING
 * if the test fails, raise exception DUPLICATE_TYPE_VAR_NAME
 */
extern void check_distinct_type_binding_names(tstack_t *stack, stack_elem_t *f, uint32_t n);



/*
 * OPERATORS
 */

/*
 * To implement term annotations/attributes, we need to know the context
 * (i.e., the enclosing operator of an annotated term).
 *
 * For example: (assert (! <term> :named xxx)) must be treated as
 * a named assertion rather than the assertion of a named term.
 * To deal with this, we allow term-stack functions to query the term stack
 * to examine the current top and the enclosing operator:
 * - get_top_op returns the top-level operator (or NO_OP if the stack is empty)
 * - get_enclosing_op returns the previous operator on the stack (or NO_OP
 *   if there's just one frame on the stack).
 *
 * Examples:
 * 1) in (assert (! <term> :named xxx)), the stack will
 *    have two operators: [ASSERT [ADD_ATTRIBUTES <term> ...]].
 *    When we process ADD_ATTRIBUTES:
 *      top_op = ADD_ATTRIBUTES
 *      enclosing_op = ASSERT
 *
 * 2) in (forall ((x T)) (! (P X) :pattern xxx))
 *    The stack will have [FORALL [BINDING ..] [ADD_ATTRIBUTES <term> ...]
 *    When we process ADD_ATTRIBUTES:
 *      top_op = ADD_ATTRIBUTES
 *      enclosing_op = FORALL
 */
static inline int32_t get_top_op(tstack_t *stack) {
  return stack->top_op; // equal to NO_OP if the stack is empty
}

extern int32_t get_enclosing_op(tstack_t *stack);



/*
 * CONVERSION
 */

/*
 * Convert element e to a term or raise an exception if e can't be converted
 */
extern term_t get_term(tstack_t *stack, stack_elem_t *e);


/*
 * Return the integer value of e (e must have rational tag)
 * Raise an exception if e is too large or is not an integer.
 */
extern int32_t get_integer(tstack_t *stack, stack_elem_t *e);


/*
 * Support for division: return a rational constant equal to den
 * provided den is constant and non-zero
 *
 * Raise exception otherwise
 */
extern rational_t *get_divisor(tstack_t *stack, stack_elem_t *den);

/*
 * Check whether e is a non-zero rational constant.
 * If so, store its value in result and return true.
 * If not, leave result unchanged and return false.
 */
extern bool elem_is_nz_constant(stack_elem_t *e, rational_t *result);


/*
 * Convert element e into a signed symbol:
 * This checks whether e has tag TAG_SYMBOL or TAG_NOT_SYMBOL
 * then copy the symbol's name in s->name and the polarity in s->polarity.
 * Polarity true means TAG_SYMBOL. Polarity false means TAG_NOT_SYMBOL.
 *
 * IMPORTANT: this function does not make a copy of the string.
 *
 * Raise an exception if e has another tag.
 */
extern void get_signed_symbol(tstack_t *stack, stack_elem_t *e, signed_symbol_t *s);



/*
 * BUFFER ALLOCATION
 */

/*
 * All operations below return an initialized/empty buffer that can be
 * pushed onto the stack using set_arith_result,
 * set_bvarith64_results, and variants.
 */
extern rba_buffer_t *tstack_get_abuffer(tstack_t *stack);
extern bvarith64_buffer_t *tstack_get_bva64buffer(tstack_t *stack, uint32_t bitsize);
extern bvarith_buffer_t *tstack_get_bvabuffer(tstack_t *stack, uint32_t bitsize);
extern bvlogic_buffer_t *tstack_get_bvlbuffer(tstack_t *stack);


/*
 * Make the auxiliary buffer large enough for n integers
 */
extern void extend_aux_buffer(tstack_t *stack, uint32_t n);

static inline int32_t *get_aux_buffer(tstack_t *stack, uint32_t n) {
  if (stack->aux_size < n) {
    extend_aux_buffer(stack, n);
  }
  return stack->aux_buffer;
}

/*
 * Make the symbol buffer large enough for n symbols
 */
extern void extend_sbuffer(tstack_t *stack, uint32_t n);

static inline signed_symbol_t *get_sbuffer(tstack_t *stack, uint32_t n) {
  if (stack->sbuffer_size < n) {
    extend_sbuffer(stack, n);
  }
  return stack->sbuffer;
}

/*
 * Make the name buffer large enough for n names
 */
extern void extend_name_buffer(tstack_t *stack, uint32_t n);

static inline char **get_name_buffer(tstack_t *stack, uint32_t n) {
  if (stack->name_buffer_size < n) {
    extend_name_buffer(stack, n);
  }
  return stack->name_buffer;
}


/*
 * ARITHMETIC AND BITVECTOR OPERATIONS
 */

/*
 * All operations update a buffer using a stack element e
 * - the functions attempt to convert e to a term or constant of the
 *   right type. then apply the operation to buffer
 */
// arithmetic
extern void add_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
extern void sub_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
extern void mul_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);

// finite field arithmetic
extern void ff_add_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
extern void ff_sub_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);
extern void ff_mul_elem(tstack_t *stack, rba_buffer_t *b, stack_elem_t *e);

// bitvector arithmetic for size <= 64
extern void bva64_add_elem(tstack_t *stack, bvarith64_buffer_t *b, stack_elem_t *e);
extern void bva64_sub_elem(tstack_t *stack, bvarith64_buffer_t *b, stack_elem_t *e);
extern void bva64_mul_elem(tstack_t *stack, bvarith64_buffer_t *b, stack_elem_t *e);

// bitvector arithmetic for size > 64
extern void bva_add_elem(tstack_t *stack, bvarith_buffer_t *b, stack_elem_t *e);
extern void bva_sub_elem(tstack_t *stack, bvarith_buffer_t *b, stack_elem_t *e);
extern void bva_mul_elem(tstack_t *stack, bvarith_buffer_t *b, stack_elem_t *e);


// copy e into b
extern  void bvl_set_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);

// copy e[i..j] into b (must satisfy 0 <= i < j < e's size)
extern void bvl_set_slice_elem(tstack_t *stack, bvlogic_buffer_t *b, uint32_t i, uint32_t j, stack_elem_t *e);

// add e to the right of b (i.e., high-order bits are from b, low-order bits from e)
extern void bvconcat_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);

// bitwise operations
extern void bvand_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
extern void bvor_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
extern void bvxor_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);
extern void bvcomp_elem(tstack_t *stack, bvlogic_buffer_t *b, stack_elem_t *e);


/*
 * In place operations: modify e
 */
// replace e by -e. raise an exception if e is not an arithmetic object
extern void neg_elem(tstack_t *stack, stack_elem_t *e);

// negate e (2's complement): raise an exception if e is not bitvector
extern void bvneg_elem(tstack_t *stack, stack_elem_t *e);


/*
 * Check whether e is a bitvector constant
 */
extern bool elem_is_bvconst(stack_elem_t *e);


/*
 * Copy the constant value of e into c
 * - e must satisfy elem_is_bvconst(e)
 */
extern void bvconst_set_elem(bvconstant_t *c, stack_elem_t *e);



/*
 * POP_FRAME AND STORE RESULTS
 */

/*
 * Remove the top-frame (except the operator)
 * - this must be followed by set_xxx_result, which replaces the top
 *   stack element element by a result
 */
extern void tstack_pop_frame(tstack_t *stack);

/*
 * Replace the top stack element by a new value
 * - this keeps the top-element's loc field unchanged
 */
extern void set_term_result(tstack_t *stack, term_t t);
extern void set_type_result(tstack_t *stack, type_t tau);
extern void set_binding_result(tstack_t *stack, term_t t, char *symbol);
extern void set_type_binding_result(tstack_t *stack, type_t, char *symbol);
extern void set_bv64_result(tstack_t *stack, uint32_t nbits, uint64_t c);
extern void set_bv_result(tstack_t *stack, uint32_t nbits, uint32_t *bv);
extern void set_ff_result(tstack_t *stack, rational_t *r, rational_t *m);
extern void set_arith_result(tstack_t *stack, rba_buffer_t *b);
extern void set_arith_ff_result(tstack_t *stack, rba_buffer_t *b, rational_t *mod);
extern void set_bvarith64_result(tstack_t *stack, bvarith64_buffer_t *b);
extern void set_bvarith_result(tstack_t *stack, bvarith_buffer_t *b);
extern void set_bvlogic_result(tstack_t *stack, bvlogic_buffer_t *b);
extern void set_aval_result(tstack_t *stack, aval_t v);

// no result: remove the top element
static inline void no_result(tstack_t *stack) {
  stack->top --;
}

/*
 * Replace the top stack element by term t and mark it as special.
 */
extern void set_special_term_result(tstack_t *stack, term_t t);

/*
 * Check whether element stored in v is a special term:
 * - v must be a pointer in the current top frame
 */
static inline bool tstack_elem_is_special(stack_elem_t *v) {
  return v->tag == TAG_SPECIAL_TERM;
}



/*
 * Copy v as result in place of the current stack->frame
 * then remove all elements above the top frame index.
 * - v must be a pointer in the current top frame
 * - v's TAG must not be string/symbol.
 */
extern void copy_result_and_pop_frame(tstack_t *stack, stack_elem_t *v);


/*
 * CALL AN EXISTING OPERATION
 */

/*
 * Call the function check[op] or eval[op] on f[0] .... f[n-1]
 * - call_tstack_eval removes the top frame and stores the result of
 *   (op f[0] ... f[n-1]) on top of the stack.
 */
extern void call_tstack_check(tstack_t *stack, int32_t op, stack_elem_t *f, uint32_t n);
extern void call_tstack_eval(tstack_t *stack, int32_t op, stack_elem_t *f, uint32_t n);



/*
 * BIT-VECTOR OPERATIONS
 */

/*
 * The functions below are exported to help support both Yices-2 and SMT-LIB
 * notations. The Yices2 and SMT-LIB versions are identical but take arguments
 * in the opposite order.
 */

/*
 * Build bitvector constant defined by val and size:
 * - size = number of bits
 * - val = value
 * - f = frame index: it's used for error reporting only
 * Raise an exception if size <= 0 or size > MAX_BV_SIZE or val is not a non-negative
 * integer.
 */
extern void mk_bv_const_core(tstack_t *stack, stack_elem_t *f, int32_t size, rational_t *val);


/*
 * Sign-extend and zero-extend:
 * - bv = stack element expected to contain the bitvector
 * - idx = stack element expected to contain an integer
 *
 * These should be used for MK_BV_SIGN_EXTEND and MK_BV_ZERO_EXTEND,
 * which require a stack frame with two arguments. One of them
 * should be bv the other one should be idx.
 *
 * These functions check the arguments bv and idx then push the
 * zero/sign extension bv + idx bits on top of the stack.
 */
extern void mk_bv_sign_extend_core(tstack_t *stack, stack_elem_t *bv, stack_elem_t *idx);
extern void mk_bv_zero_extend_core(tstack_t *stack, stack_elem_t *bv, stack_elem_t *idx);


#endif /* __TSTACK_INTERNALS */

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	*/
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	* Check whether e is a non-zero rational constant.
198	* If so, store its value in result and return true.
199	* If not, leave result unchanged and return false.
200	*/
201	extern bool elem_is_nz_constant(stack_elem_t e, rational_t result);
202
203
204	/*
205	* Convert element e into a signed symbol:
206	* This checks whether e has tag TAG_SYMBOL or TAG_NOT_SYMBOL
207	* then copy the symbol's name in s->name and the polarity in s->polarity.
208	* Polarity true means TAG_SYMBOL. Polarity false means TAG_NOT_SYMBOL.
209	*
210	* IMPORTANT: this function does not make a copy of the string.
211	*
212	* Raise an exception if e has another tag.
213	*/
214	extern void get_signed_symbol(tstack_t stack, stack_elem_t e, signed_symbol_t *s);
215
216
217
218	/*
219	* BUFFER ALLOCATION
220	*/
221
222	/*
223	* All operations below return an initialized/empty buffer that can be
224	* pushed onto the stack using set_arith_result,
225	* set_bvarith64_results, and variants.
226	*/
227	extern rba_buffer_t tstack_get_abuffer(tstack_t stack);
228	extern bvarith64_buffer_t tstack_get_bva64buffer(tstack_t stack, uint32_t bitsize);
229	extern bvarith_buffer_t tstack_get_bvabuffer(tstack_t stack, uint32_t bitsize);
230	extern bvlogic_buffer_t tstack_get_bvlbuffer(tstack_t stack);
231
232
233	/*
234	* Make the auxiliary buffer large enough for n integers
235	*/
236	extern void extend_aux_buffer(tstack_t *stack, uint32_t n);
237
238	static inline int32_t get_aux_buffer(tstack_t stack, uint32_t n) {	269,404✔
239	if (stack->aux_size < n) {	269,404✔
240	extend_aux_buffer(stack, n);	33✔
241	}
242	return stack->aux_buffer;	269,404✔
243	}
244
245	/*
246	* Make the symbol buffer large enough for n symbols
247	*/
248	extern void extend_sbuffer(tstack_t *stack, uint32_t n);
249
250	static inline signed_symbol_t get_sbuffer(tstack_t stack, uint32_t n) {	1✔
251	if (stack->sbuffer_size < n) {	1✔
252	extend_sbuffer(stack, n);	×
253	}
254	return stack->sbuffer;	1✔
255	}
256
257	/*
258	* Make the name buffer large enough for n names
259	*/
260	extern void extend_name_buffer(tstack_t *stack, uint32_t n);
261
262	static inline char *get_name_buffer(tstack_t stack, uint32_t n) {	125,825✔
263	if (stack->name_buffer_size < n) {	125,825✔
264	extend_name_buffer(stack, n);	693✔
265	}
266	return stack->name_buffer;	125,825✔
267	}
268
269
270	/*
271	* ARITHMETIC AND BITVECTOR OPERATIONS
272	*/
273
274	/*
275	* All operations update a buffer using a stack element e
276	* - the functions attempt to convert e to a term or constant of the
277	* right type. then apply the operation to buffer
278	*/
279	// arithmetic
280	extern void add_elem(tstack_t stack, rba_buffer_t b, stack_elem_t *e);
281	extern void sub_elem(tstack_t stack, rba_buffer_t b, stack_elem_t *e);
282	extern void mul_elem(tstack_t stack, rba_buffer_t b, stack_elem_t *e);
283
284	// finite field arithmetic
285	extern void ff_add_elem(tstack_t stack, rba_buffer_t b, stack_elem_t *e);
286	extern void ff_sub_elem(tstack_t stack, rba_buffer_t b, stack_elem_t *e);
287	extern void ff_mul_elem(tstack_t stack, rba_buffer_t b, stack_elem_t *e);
288
289	// bitvector arithmetic for size <= 64
290	extern void bva64_add_elem(tstack_t stack, bvarith64_buffer_t b, stack_elem_t *e);
291	extern void bva64_sub_elem(tstack_t stack, bvarith64_buffer_t b, stack_elem_t *e);
292	extern void bva64_mul_elem(tstack_t stack, bvarith64_buffer_t b, stack_elem_t *e);
293
294	// bitvector arithmetic for size > 64
295	extern void bva_add_elem(tstack_t stack, bvarith_buffer_t b, stack_elem_t *e);
296	extern void bva_sub_elem(tstack_t stack, bvarith_buffer_t b, stack_elem_t *e);
297	extern void bva_mul_elem(tstack_t stack, bvarith_buffer_t b, stack_elem_t *e);
298
299
300	// copy e into b
301	extern void bvl_set_elem(tstack_t stack, bvlogic_buffer_t b, stack_elem_t *e);
302
303	// copy e[i..j] into b (must satisfy 0 <= i < j < e's size)
304	extern void bvl_set_slice_elem(tstack_t stack, bvlogic_buffer_t b, uint32_t i, uint32_t j, stack_elem_t *e);
305
306	// add e to the right of b (i.e., high-order bits are from b, low-order bits from e)
307	extern void bvconcat_elem(tstack_t stack, bvlogic_buffer_t b, stack_elem_t *e);
308
309	// bitwise operations
310	extern void bvand_elem(tstack_t stack, bvlogic_buffer_t b, stack_elem_t *e);
311	extern void bvor_elem(tstack_t stack, bvlogic_buffer_t b, stack_elem_t *e);
312	extern void bvxor_elem(tstack_t stack, bvlogic_buffer_t b, stack_elem_t *e);
313	extern void bvcomp_elem(tstack_t stack, bvlogic_buffer_t b, stack_elem_t *e);
314
315
316	/*
317	* In place operations: modify e
318	*/
319	// replace e by -e. raise an exception if e is not an arithmetic object
320	extern void neg_elem(tstack_t stack, stack_elem_t e);
321
322	// negate e (2's complement): raise an exception if e is not bitvector
323	extern void bvneg_elem(tstack_t stack, stack_elem_t e);
324
325
326	/*
327	* Check whether e is a bitvector constant
328	*/
329	extern bool elem_is_bvconst(stack_elem_t *e);
330
331
332	/*
333	* Copy the constant value of e into c
334	* - e must satisfy elem_is_bvconst(e)
335	*/
336	extern void bvconst_set_elem(bvconstant_t c, stack_elem_t e);
337
338
339
340	/*
341	* POP_FRAME AND STORE RESULTS
342	*/
343
344	/*
345	* Remove the top-frame (except the operator)
346	* - this must be followed by set_xxx_result, which replaces the top
347	* stack element element by a result
348	*/
349	extern void tstack_pop_frame(tstack_t *stack);
350
351	/*
352	* Replace the top stack element by a new value
353	* - this keeps the top-element's loc field unchanged
354	*/
355	extern void set_term_result(tstack_t *stack, term_t t);
356	extern void set_type_result(tstack_t *stack, type_t tau);
357	extern void set_binding_result(tstack_t stack, term_t t, char symbol);
358	extern void set_type_binding_result(tstack_t stack, type_t, char symbol);
359	extern void set_bv64_result(tstack_t *stack, uint32_t nbits, uint64_t c);
360	extern void set_bv_result(tstack_t stack, uint32_t nbits, uint32_t bv);
361	extern void set_ff_result(tstack_t stack, rational_t r, rational_t *m);
362	extern void set_arith_result(tstack_t stack, rba_buffer_t b);
363	extern void set_arith_ff_result(tstack_t stack, rba_buffer_t b, rational_t *mod);
364	extern void set_bvarith64_result(tstack_t stack, bvarith64_buffer_t b);
365	extern void set_bvarith_result(tstack_t stack, bvarith_buffer_t b);
366	extern void set_bvlogic_result(tstack_t stack, bvlogic_buffer_t b);
367	extern void set_aval_result(tstack_t *stack, aval_t v);
368
369	// no result: remove the top element
370	static inline void no_result(tstack_t *stack) {	112,468✔
371	stack->top --;	112,468✔
372	}	112,468✔
373
374	/*
375	* Replace the top stack element by term t and mark it as special.
376	*/
377	extern void set_special_term_result(tstack_t *stack, term_t t);
378
379	/*
380	* Check whether element stored in v is a special term:
381	* - v must be a pointer in the current top frame
382	*/
383	static inline bool tstack_elem_is_special(stack_elem_t *v) {	12,166✔
384	return v->tag == TAG_SPECIAL_TERM;	12,166✔
385	}
386
387
388
389	/*
390	* Copy v as result in place of the current stack->frame
391	* then remove all elements above the top frame index.
392	* - v must be a pointer in the current top frame
393	* - v's TAG must not be string/symbol.
394	*/
395	extern void copy_result_and_pop_frame(tstack_t stack, stack_elem_t v);
396
397
398	/*
399	* CALL AN EXISTING OPERATION
400	*/
401
402	/*
403	* Call the function check[op] or eval[op] on f[0] .... f[n-1]
404	* - call_tstack_eval removes the top frame and stores the result of
405	* (op f[0] ... f[n-1]) on top of the stack.
406	*/
407	extern void call_tstack_check(tstack_t stack, int32_t op, stack_elem_t f, uint32_t n);
408	extern void call_tstack_eval(tstack_t stack, int32_t op, stack_elem_t f, uint32_t n);
409
410
411
412	/*
413	* BIT-VECTOR OPERATIONS
414	*/
415
416	/*
417	* The functions below are exported to help support both Yices-2 and SMT-LIB
418	* notations. The Yices2 and SMT-LIB versions are identical but take arguments
419	* in the opposite order.
420	*/
421
422	/*
423	* Build bitvector constant defined by val and size:
424	* - size = number of bits
425	* - val = value
426	* - f = frame index: it's used for error reporting only
427	* Raise an exception if size <= 0 or size > MAX_BV_SIZE or val is not a non-negative
428	* integer.
429	*/
430	extern void mk_bv_const_core(tstack_t stack, stack_elem_t f, int32_t size, rational_t *val);
431
432
433	/*
434	* Sign-extend and zero-extend:
435	* - bv = stack element expected to contain the bitvector
436	* - idx = stack element expected to contain an integer
437	*
438	* These should be used for MK_BV_SIGN_EXTEND and MK_BV_ZERO_EXTEND,
439	* which require a stack frame with two arguments. One of them
440	* should be bv the other one should be idx.
441	*
442	* These functions check the arguments bv and idx then push the
443	* zero/sign extension bv + idx bits on top of the stack.
444	*/
445	extern void mk_bv_sign_extend_core(tstack_t stack, stack_elem_t bv, stack_elem_t *idx);
446	extern void mk_bv_zero_extend_core(tstack_t stack, stack_elem_t bv, stack_elem_t *idx);
447
448
449	#endif /* __TSTACK_INTERNALS */

SRI-CSL / yices2 / 16032530443

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