1 /*  Boolector: Satisfiability Modulo Theories (SMT) solver.
2  *
3  *  Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4  *
5  *  This file is part of Boolector.
6  *  See COPYING for more information on using this software.
7  */
8 
9 /*------------------------------------------------------------------------*/
10 #ifndef NDEBUG
11 /*------------------------------------------------------------------------*/
12 
13 #include "btordbg.h"
14 
15 #include <limits.h>
16 #include "btorlog.h"
17 #include "utils/btorhashptr.h"
18 #include "utils/btorutil.h"
19 
20 /*------------------------------------------------------------------------*/
21 /* core                                                                   */
22 /*------------------------------------------------------------------------*/
23 
24 bool
btor_dbg_check_lambdas_static_rho_proxy_free(const Btor * btor)25 btor_dbg_check_lambdas_static_rho_proxy_free (const Btor *btor)
26 {
27   BtorNode *cur, *data, *key;
28   BtorPtrHashTableIterator it, iit;
29   BtorPtrHashTable *static_rho;
30 
31   btor_iter_hashptr_init (&it, btor->lambdas);
32   while (btor_iter_hashptr_has_next (&it))
33   {
34     cur        = btor_iter_hashptr_next (&it);
35     static_rho = btor_node_lambda_get_static_rho (cur);
36     if (!static_rho) continue;
37 
38     btor_iter_hashptr_init (&iit, static_rho);
39     while (btor_iter_hashptr_has_next (&iit))
40     {
41       data = iit.bucket->data.as_ptr;
42       key  = btor_iter_hashptr_next (&iit);
43       assert (data);
44       if (btor_node_is_proxy (data)) return false;
45       if (btor_node_is_proxy (key)) return false;
46     }
47   }
48   return true;
49 }
50 
51 bool
btor_dbg_check_unique_table_children_proxy_free(const Btor * btor)52 btor_dbg_check_unique_table_children_proxy_free (const Btor *btor)
53 {
54   uint32_t i, j;
55   BtorNode *cur;
56 
57   for (i = 0; i < btor->nodes_unique_table.size; i++)
58     for (cur = btor->nodes_unique_table.chains[i]; cur; cur = cur->next)
59       for (j = 0; j < cur->arity; j++)
60         if (btor_node_is_proxy (cur->e[j]))
61         {
62           BTORLOG (1,
63                    "found proxy node in unique table: %s (parent: %s)",
64                    btor_util_node2string (cur->e[j]),
65                    btor_util_node2string (cur));
66           return false;
67         }
68   return true;
69 }
70 
71 bool
btor_dbg_check_hash_table_proxy_free(BtorPtrHashTable * table)72 btor_dbg_check_hash_table_proxy_free (BtorPtrHashTable *table)
73 {
74   BtorPtrHashTableIterator it;
75   BtorNode *cur;
76 
77   btor_iter_hashptr_init (&it, table);
78   while (btor_iter_hashptr_has_next (&it))
79   {
80     cur = btor_iter_hashptr_next (&it);
81     if (btor_node_is_proxy (cur)) return false;
82   }
83   return true;
84 }
85 
86 bool
btor_dbg_check_all_hash_tables_proxy_free(const Btor * btor)87 btor_dbg_check_all_hash_tables_proxy_free (const Btor *btor)
88 {
89   if (!btor_dbg_check_hash_table_proxy_free (btor->embedded_constraints))
90     return false;
91   if (!btor_dbg_check_hash_table_proxy_free (btor->unsynthesized_constraints))
92     return false;
93   if (!btor_dbg_check_hash_table_proxy_free (btor->synthesized_constraints))
94     return false;
95   return true;
96 }
97 
98 bool
btor_dbg_check_hash_table_simp_free(BtorPtrHashTable * table)99 btor_dbg_check_hash_table_simp_free (BtorPtrHashTable *table)
100 {
101   BtorPtrHashTableIterator it;
102   btor_iter_hashptr_init (&it, table);
103   while (btor_iter_hashptr_has_next (&it))
104     if (btor_node_is_simplified (btor_iter_hashptr_next (&it)))
105       return false;
106   return true;
107 }
108 
109 bool
btor_dbg_check_unique_table_rebuild(const Btor * btor)110 btor_dbg_check_unique_table_rebuild (const Btor *btor)
111 {
112   uint32_t i;
113   BtorNode *cur;
114 
115   for (i = 0; i < btor->nodes_unique_table.size; i++)
116     for (cur = btor->nodes_unique_table.chains[i]; cur; cur = cur->next)
117     {
118       if (cur->rebuild)
119       {
120         BTORLOG (1,
121                  "found node with rebuild flag enabled: %s",
122                  btor_util_node2string (cur));
123         return false;
124       }
125     }
126   return true;
127 }
128 
129 bool
btor_dbg_check_all_hash_tables_simp_free(const Btor * btor)130 btor_dbg_check_all_hash_tables_simp_free (const Btor *btor)
131 {
132   if (!btor_dbg_check_hash_table_simp_free (btor->embedded_constraints))
133     return false;
134   if (!btor_dbg_check_hash_table_simp_free (btor->unsynthesized_constraints))
135     return false;
136   if (!btor_dbg_check_hash_table_simp_free (btor->synthesized_constraints))
137     return false;
138   return true;
139 }
140 
141 bool
btor_dbg_check_constraints_not_const(const Btor * btor)142 btor_dbg_check_constraints_not_const (const Btor *btor)
143 {
144   BtorNode *cur;
145   BtorPtrHashTableIterator it;
146 
147   btor_iter_hashptr_init (&it, btor->unsynthesized_constraints);
148   while (btor_iter_hashptr_has_next (&it))
149   {
150     cur = btor_iter_hashptr_next (&it);
151     assert (cur);
152     if (btor_node_is_bv_const (cur)) return false;
153   }
154 
155   btor_iter_hashptr_init (&it, btor->synthesized_constraints);
156   while (btor_iter_hashptr_has_next (&it))
157   {
158     cur = btor_iter_hashptr_next (&it);
159     assert (cur);
160     if (btor_node_is_bv_const (cur)) return false;
161   }
162   return true;
163 }
164 
165 bool
btor_dbg_check_assumptions_simp_free(const Btor * btor)166 btor_dbg_check_assumptions_simp_free (const Btor *btor)
167 {
168   BtorPtrHashTableIterator it;
169   btor_iter_hashptr_init (&it, btor->assumptions);
170   while (btor_iter_hashptr_has_next (&it))
171     if (btor_node_is_simplified (btor_iter_hashptr_next (&it)))
172       return false;
173   return true;
174 }
175 
176 bool
btor_dbg_check_nodes_simp_free(Btor * btor,BtorNode * nodes[],size_t nnodes)177 btor_dbg_check_nodes_simp_free (Btor *btor, BtorNode *nodes[], size_t nnodes)
178 {
179   size_t i;
180   int32_t id;
181   BtorNode *cur;
182   BtorPtrHashTableIterator it;
183   BtorIntHashTable *cache;
184   BtorPtrHashTable *rho;
185   BtorNodePtrStack visit;
186   bool opt_nondestr_subst;
187 
188   BTOR_INIT_STACK (btor->mm, visit);
189   cache              = btor_hashint_table_new (btor->mm);
190   opt_nondestr_subst = btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST) == 1;
191 
192   for (i = 0; i < nnodes; i++)
193   {
194     BTOR_PUSH_STACK (visit, nodes[i]);
195     BTORLOG (3, "  root: %s", btor_util_node2string (nodes[i]));
196   }
197 
198   while (!BTOR_EMPTY_STACK (visit))
199   {
200     cur = btor_node_real_addr (BTOR_POP_STACK (visit));
201     id  = btor_node_get_id (cur);
202     BTORLOG (3, "check simp free: %s", btor_util_node2string (cur));
203     if (opt_nondestr_subst && btor_node_is_synth (cur))
204     {
205       continue;
206     }
207     if (btor_node_is_simplified (cur))
208     {
209       BTORLOG (3,
210                "  simplified: %s",
211                btor_util_node2string (btor_node_get_simplified (btor, cur)));
212     }
213     assert (!btor_node_is_simplified (cur));
214 
215     if (btor_hashint_table_contains (cache, id)) continue;
216 
217     if (btor_node_is_lambda (cur)
218         && (rho = btor_node_lambda_get_static_rho (cur)))
219     {
220       btor_iter_hashptr_init (&it, rho);
221       while (btor_iter_hashptr_has_next (&it))
222       {
223         BTOR_PUSH_STACK (visit, it.bucket->data.as_ptr);
224         BTOR_PUSH_STACK (visit, btor_iter_hashptr_next (&it));
225       }
226     }
227 
228     btor_hashint_table_add (cache, id);
229     for (i = 0; i < cur->arity; i++)
230     {
231       BTOR_PUSH_STACK (visit, cur->e[i]);
232     }
233   }
234 
235   BTOR_RELEASE_STACK (visit);
236   btor_hashint_table_delete (cache);
237   return true;
238 }
239 
240 bool
btor_dbg_check_constraints_simp_free(Btor * btor)241 btor_dbg_check_constraints_simp_free (Btor *btor)
242 {
243   BtorNode *cur;
244   BtorNodePtrStack nodes;
245   BtorPtrHashTableIterator it;
246 
247   BTOR_INIT_STACK (btor->mm, nodes);
248 
249   btor_iter_hashptr_init (&it, btor->unsynthesized_constraints);
250   btor_iter_hashptr_queue (&it, btor->synthesized_constraints);
251   btor_iter_hashptr_queue (&it, btor->assumptions);
252   while (btor_iter_hashptr_has_next (&it))
253   {
254     cur = btor_iter_hashptr_next (&it);
255     BTOR_PUSH_STACK (nodes, cur);
256   }
257 
258   btor_dbg_check_nodes_simp_free (btor, nodes.start, BTOR_COUNT_STACK (nodes));
259   BTOR_RELEASE_STACK (nodes);
260   return true;
261 }
262 
263 /*------------------------------------------------------------------------*/
264 /* exp                                                                    */
265 /*------------------------------------------------------------------------*/
266 
267 bool
btor_dbg_precond_slice_exp(Btor * btor,const BtorNode * exp,uint32_t upper,uint32_t lower)268 btor_dbg_precond_slice_exp (Btor *btor,
269                             const BtorNode *exp,
270                             uint32_t upper,
271                             uint32_t lower)
272 {
273   assert (btor);
274   assert (exp);
275   assert (!btor_node_is_simplified (exp));
276   assert (!btor_node_is_fun (exp));
277   assert (upper >= lower);
278   assert (upper < btor_node_bv_get_width (btor, exp));
279   assert (btor_node_real_addr (exp)->btor == btor);
280   return true;
281 }
282 
283 bool
btor_dbg_precond_ext_exp(Btor * btor,const BtorNode * exp)284 btor_dbg_precond_ext_exp (Btor *btor, const BtorNode *exp)
285 {
286   assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
287   return true;
288 }
289 
290 bool
btor_dbg_precond_regular_unary_bv_exp(Btor * btor,const BtorNode * exp)291 btor_dbg_precond_regular_unary_bv_exp (Btor *btor, const BtorNode *exp)
292 {
293   assert (btor);
294   assert (exp);
295   assert (!btor_node_is_simplified (exp));
296   assert (!btor_node_is_fun (exp));
297   assert (btor_node_real_addr (exp)->btor == btor);
298   return true;
299 }
300 
301 bool
btor_dbg_precond_eq_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)302 btor_dbg_precond_eq_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1)
303 {
304   BtorNode *real_e0, *real_e1;
305 
306   assert (btor);
307   assert (e0);
308   assert (e1);
309 
310   real_e0 = btor_node_real_addr (e0);
311   real_e1 = btor_node_real_addr (e1);
312 
313   assert (real_e0);
314   assert (real_e1);
315   assert (real_e0->btor == btor);
316   assert (real_e1->btor == btor);
317   assert (!btor_node_is_simplified (real_e0));
318   assert (!btor_node_is_simplified (real_e1));
319   assert (btor_node_get_sort_id (real_e0) == btor_node_get_sort_id (real_e1));
320   assert (real_e0->is_array == real_e1->is_array);
321   assert (!btor_node_is_fun (real_e0)
322           || (btor_node_is_regular (e0) && btor_node_is_regular (e1)));
323   return true;
324 }
325 
326 bool
btor_dbg_precond_concat_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)327 btor_dbg_precond_concat_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1)
328 {
329   assert (btor);
330   assert (e0);
331   assert (e1);
332   assert (!btor_node_is_simplified (e0));
333   assert (!btor_node_is_simplified (e1));
334   assert (!btor_node_is_fun (e0));
335   assert (!btor_node_is_fun (e1));
336   assert (btor_node_bv_get_width (btor, e0)
337           <= INT32_MAX - btor_node_bv_get_width (btor, e1));
338   assert (btor_node_real_addr (e0)->btor == btor);
339   assert (btor_node_real_addr (e1)->btor == btor);
340   return true;
341 }
342 
343 bool
btor_dbg_precond_shift_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)344 btor_dbg_precond_shift_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1)
345 {
346   assert (btor);
347   assert (e0);
348   assert (e1);
349   assert (!btor_node_is_simplified (e0));
350   assert (!btor_node_is_simplified (e1));
351   assert (!btor_node_is_fun (e0));
352   assert (!btor_node_is_fun (e1));
353   assert (btor_node_bv_get_width (btor, e0)
354           == btor_node_bv_get_width (btor, e1));
355   assert (btor_node_real_addr (e0)->btor == btor);
356   assert (btor_node_real_addr (e1)->btor == btor);
357   return true;
358 }
359 
360 bool
btor_dbg_precond_regular_binary_bv_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)361 btor_dbg_precond_regular_binary_bv_exp (Btor *btor,
362                                         const BtorNode *e0,
363                                         const BtorNode *e1)
364 {
365   assert (btor);
366   assert (e0);
367   assert (e1);
368   assert (!btor_node_is_simplified (e0));
369   assert (!btor_node_is_simplified (e1));
370   assert (!btor_node_is_fun (e0));
371   assert (!btor_node_is_fun (e1));
372   assert (btor_node_get_sort_id (e0) == btor_node_get_sort_id (e1));
373   assert (btor_node_real_addr (e0)->btor == btor);
374   assert (btor_node_real_addr (e1)->btor == btor);
375   return true;
376 }
377 
378 bool
btor_dbg_precond_read_exp(Btor * btor,const BtorNode * e_array,const BtorNode * e_index)379 btor_dbg_precond_read_exp (Btor *btor,
380                            const BtorNode *e_array,
381                            const BtorNode *e_index)
382 {
383   assert (btor);
384   assert (e_array);
385   assert (e_index);
386   assert (btor_node_is_regular (e_array));
387   assert (btor_node_is_fun (e_array));
388   assert (!btor_node_is_simplified (e_array));
389   assert (!btor_node_is_simplified (e_index));
390   assert (!btor_node_is_fun (e_index));
391   assert (btor_sort_array_get_index (btor, btor_node_get_sort_id (e_array))
392           == btor_node_get_sort_id (e_index));
393   assert (btor_node_real_addr (e_array)->btor == btor);
394   assert (btor_node_real_addr (e_index)->btor == btor);
395   assert (e_array->is_array);
396   return true;
397 }
398 
399 bool
btor_dbg_precond_write_exp(Btor * btor,const BtorNode * e_array,const BtorNode * e_index,const BtorNode * e_value)400 btor_dbg_precond_write_exp (Btor *btor,
401                             const BtorNode *e_array,
402                             const BtorNode *e_index,
403                             const BtorNode *e_value)
404 {
405   assert (btor);
406   assert (e_array);
407   assert (e_index);
408   assert (e_value);
409   assert (btor_node_is_regular (e_array));
410   assert (btor_node_is_fun (e_array));
411   assert (!btor_node_is_simplified (e_array));
412   assert (!btor_node_is_simplified (e_index));
413   assert (!btor_node_is_simplified (e_value));
414   assert (!btor_node_is_fun (e_index));
415   assert (!btor_node_is_fun (e_value));
416   assert (btor_sort_array_get_index (btor, btor_node_get_sort_id (e_array))
417           == btor_node_get_sort_id (e_index));
418   assert (btor_sort_array_get_element (btor, btor_node_get_sort_id (e_array))
419           == btor_node_get_sort_id (e_value));
420   assert (btor_node_real_addr (e_array)->btor == btor);
421   assert (btor_node_real_addr (e_index)->btor == btor);
422   assert (btor_node_real_addr (e_value)->btor == btor);
423   assert (e_array->is_array);
424   return true;
425 }
426 
427 bool
btor_dbg_precond_cond_exp(Btor * btor,const BtorNode * e_cond,const BtorNode * e_if,const BtorNode * e_else)428 btor_dbg_precond_cond_exp (Btor *btor,
429                            const BtorNode *e_cond,
430                            const BtorNode *e_if,
431                            const BtorNode *e_else)
432 {
433   assert (btor);
434   assert (e_cond);
435   assert (e_if);
436   assert (e_else);
437   assert (!btor_node_is_simplified (e_cond));
438   assert (btor_node_bv_get_width (btor, e_cond) == 1);
439 
440   BtorNode *real_e_if, *real_e_else;
441 
442   real_e_if   = btor_node_real_addr (e_if);
443   real_e_else = btor_node_real_addr (e_else);
444 
445   assert (!btor_node_is_simplified (real_e_if));
446   assert (!btor_node_is_simplified (real_e_else));
447   assert (btor_node_get_sort_id (real_e_if)
448           == btor_node_get_sort_id (real_e_else));
449   assert (btor_node_real_addr (e_cond)->btor == btor);
450   assert (real_e_if->btor == btor);
451   assert (real_e_else->btor == btor);
452   assert (real_e_if->is_array == real_e_else->is_array);
453   return true;
454 }
455 
456 bool
btor_dbg_precond_apply_exp(Btor * btor,const BtorNode * fun,const BtorNode * args)457 btor_dbg_precond_apply_exp (Btor *btor,
458                             const BtorNode *fun,
459                             const BtorNode *args)
460 {
461   assert (btor);
462   assert (fun);
463   assert (args);
464   assert (btor_node_is_regular (fun));
465   assert (btor_node_is_regular (args));
466   assert (btor_node_is_fun (fun));
467   assert (btor_node_is_args (args));
468   assert (btor_sort_fun_get_domain (btor, btor_node_get_sort_id (fun))
469           == btor_node_get_sort_id (args));
470   return true;
471 }
472 
473 /*------------------------------------------------------------------------*/
474 #endif
475 /*------------------------------------------------------------------------*/
476