cprover
Loading...
Searching...
No Matches
jsa.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Counterexample-Guided Inductive Synthesis
4
5Author: Daniel Kroening, kroening@kroening.com
6 Pascal Kesseli, pascal.kesseli@cs.ox.ac.uk
7
8\*******************************************************************/
9
12
13/* FUNCTION: __CPROVER_jsa_synthesise */
14
15#ifndef CPROVER_ANSI_C_LIBRARY_JSA_H
16#define CPROVER_ANSI_C_LIBRARY_JSA_H
17
18#ifdef JSA_GENETIC_SYNTHESIS_H_
19#ifndef __CPROVER_jsa_extern
20#define __CPROVER_jsa_extern extern
21#define JSA_SYNTHESIS_H_
22#define __CPROVER_JSA_DEFINE_TRANSFORMERS
23#endif
24#else
25#ifndef __CPROVER_jsa_extern
26#define __CPROVER_jsa_extern
27#endif
28#endif
29
30#ifndef JSA_SYNTHESIS_H_
31#define __CPROVER_JSA_DEFINE_TRANSFORMERS
32#endif
33
34#ifndef __CPROVER
35#include <assert.h>
36#include <string.h>
37#include <setjmp.h>
38extern jmp_buf __CPROVER_jsa_jump_buffer;
39#endif
40#include <stdbool.h>
41
42#ifndef __CPROVER_JSA_MAX_CONCRETE_NODES
43#define __CPROVER_JSA_MAX_CONCRETE_NODES 100u
44#endif
45#ifndef __CPROVER_JSA_MAX_ABSTRACT_NODES
46#define __CPROVER_JSA_MAX_ABSTRACT_NODES __CPROVER_JSA_MAX_CONCRETE_NODES
47#endif
48#ifndef __CPROVER_JSA_MAX_NODES
49#define __CPROVER_JSA_MAX_NODES __CPROVER_JSA_MAX_CONCRETE_NODES+\
50 __CPROVER_JSA_MAX_ABSTRACT_NODES
51#endif
52#ifndef __CPROVER_JSA_MAX_ABSTRACT_RANGES
53#define __CPROVER_JSA_MAX_ABSTRACT_RANGES __CPROVER_JSA_MAX_ABSTRACT_NODES
54#endif
55#ifndef __CPROVER_JSA_MAX_ITERATORS
56#define __CPROVER_JSA_MAX_ITERATORS 100u
57#endif
58#ifndef __CPROVER_JSA_MAX_LISTS
59#define __CPROVER_JSA_MAX_LISTS __CPROVER_JSA_MAX_ITERATORS
60#endif
61#ifndef __CPROVER_JSA_MAX_NODES_PER_CE_LIST
62#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST __CPROVER_JSA_MAX_NODES
63#endif
64#if __CPROVER_JSA_MAX_LISTS < 1
65#error "JSA needs at least one list variable for analysis."
66#endif
67#if __CPROVER_JSA_MAX_ABSTRACT_NODES!=0
68#error "Currently in concrete-mode only."
69#endif
70
71typedef unsigned char __CPROVER_jsa_word_t;
80#define __CPROVER_jsa_null 0xFF
81#define __CPROVER_jsa_word_max 0xFF
82
93
105
115
128
164
165
166#ifdef __CPROVER
167#define __CPROVER_jsa_inline
168#else
169#define __CPROVER_jsa_inline static inline
170#endif
171
172#ifdef __CPROVER
173#define __CPROVER_jsa_assume(c) __CPROVER_assume(c)
174#define __CPROVER_jsa_assert(c, str) __CPROVER_assert(c, str)
175#else
176#define __CPROVER_jsa_assume(c) \
177 do {\
178 if(!(c))\
179 longjmp(__CPROVER_jsa_jump_buffer, 1);\
180 }\
181 while(false)
182#define __CPROVER_jsa_assert(c, str) assert((c) && str)
183#endif
184
185// Heap comparison
186#ifdef __CPROVER
187#define __CPROVER_jsa__internal_are_heaps_equal(lhs, rhs) (*(lhs) == *(rhs))
188#else
190 const __CPROVER_jsa_abstract_heapt *const lhs,
191 const __CPROVER_jsa_abstract_heapt *const rhs)
192{
194#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
195 for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
196 {
197 const __CPROVER_jsa_abstract_nodet lhs_node=lhs->abstract_nodes[i];
198 const __CPROVER_jsa_abstract_nodet rhs_node=rhs->abstract_nodes[i];
199 if(lhs_node.list!=rhs_node.list ||
200 lhs_node.next!=rhs_node.next ||
201 lhs_node.previous!=rhs_node.previous ||
202 lhs_node.value_ref!=rhs_node.value_ref)
203 return false;
204 }
205#endif
206#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
207 for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_RANGES; ++i)
208 {
209 const __CPROVER_jsa_abstract_ranget lhs_range=lhs->abstract_ranges[i];
210 const __CPROVER_jsa_abstract_ranget rhs_range=rhs->abstract_ranges[i];
211 if(lhs_range.max!=rhs_range.max ||
212 lhs_range.min!=rhs_range.min ||
213 lhs_range.size!=rhs_range.size)
214 return false;
215 }
216#endif
217 for(i=0; i < __CPROVER_JSA_MAX_CONCRETE_NODES; ++i)
218 {
219 const __CPROVER_jsa_concrete_nodet lhs_node=lhs->concrete_nodes[i];
220 const __CPROVER_jsa_concrete_nodet rhs_node=rhs->concrete_nodes[i];
221 if(lhs_node.list!=rhs_node.list ||
222 lhs_node.next!=rhs_node.next ||
223 lhs_node.previous!=rhs_node.previous ||
224 lhs_node.value!=rhs_node.value)
225 return false;
226 }
227 if(lhs->iterator_count!=rhs->iterator_count)
228 return false;
229 for(i=0; i < lhs->iterator_count; ++i)
230 {
231 const __CPROVER_jsa_iteratort lhs_it=lhs->iterators[i];
232 const __CPROVER_jsa_iteratort rhs_it=rhs->iterators[i];
233 if(lhs_it.index!=rhs_it.index ||
234 lhs_it.list!=rhs_it.list ||
235 lhs_it.node_id!=rhs_it.node_id ||
236 lhs_it.previous_index!=rhs_it.previous_index ||
237 lhs_it.previous_node_id!=rhs_it.previous_node_id)
238 return false;
239 }
240 if(lhs->list_count!=rhs->list_count)
241 return false;
242 for(i=0; i<lhs->list_count; ++i)
243 if(lhs->list_head_nodes[i]!=rhs->list_head_nodes[i])
244 return false;
245 return true;
246}
247#endif
248
249// Node utility functions
250#define __CPROVER_jsa__internal_get_head_node(heap_ptr, list) \
251 (heap_ptr)->list_head_nodes[list]
252
253#define __CPROVER_jsa__internal_is_concrete_node(node) \
254 (node < __CPROVER_JSA_MAX_CONCRETE_NODES)
255
256#define __CPROVER_jsa__internal_is_abstract_node(node) \
257 (!__CPROVER_jsa__internal_is_concrete_node(node))
258
259#define __CPROVER_jsa__internal_get_abstract_node_index(node) \
260 (node - __CPROVER_JSA_MAX_CONCRETE_NODES)
261
262#define __CPROVER_jsa__internal_get_abstract_node_id(node_index) \
263 (__CPROVER_JSA_MAX_CONCRETE_NODES + node_index)
264
265#define __CPROVER_jsa__internal_get_list(heap_ptr, node) \
266 (__CPROVER_jsa_null == node ? __CPROVER_jsa_null :\
267 __CPROVER_jsa__internal_is_concrete_node(node) ?\
268 (heap_ptr)->concrete_nodes[node].list:(heap_ptr)->abstract_nodes[node].list)
269
271 __CPROVER_jsa_abstract_heapt * const heap,
272 const __CPROVER_jsa_node_id_t node,
273 const __CPROVER_jsa_node_id_t next_node)
274#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
275{
277 {
278 heap->concrete_nodes[node].next=next_node;
279 } else
280 {
281 const __CPROVER_jsa_index_t index=
283 heap->abstract_nodes[index].next=next_node;
284 }
285}
286#else
287;
288#endif
289
290#define __CPROVER_jsa__internal_get_next(heap_ptr, node) \
291 (__CPROVER_jsa__internal_is_concrete_node(node) ?\
292 (heap_ptr)->concrete_nodes[node].next:\
293 (heap_ptr)->abstract_nodes[\
294 __CPROVER_jsa__internal_get_abstract_node_index(node)].next)
295
297 __CPROVER_jsa_abstract_heapt * const heap,
298 const __CPROVER_jsa_node_id_t node,
299 const __CPROVER_jsa_node_id_t previous_node)
300#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
301{
303 {
304 heap->concrete_nodes[node].previous=previous_node;
305 } else
306 {
307 const __CPROVER_jsa_index_t index=
309 heap->abstract_nodes[index].previous=previous_node;
310 }
311}
312#else
313;
314#endif
315
316#define __CPROVER_jsa__internal_get_previous(heap_ptr, node) \
317 (__CPROVER_jsa__internal_is_concrete_node(node) ?\
318 (heap_ptr)->concrete_nodes[node].previous:\
319 (heap_ptr)->abstract_nodes[\
320 __CPROVER_jsa__internal_get_abstract_node_index(node)].previous)
321
323 __CPROVER_jsa_abstract_heapt * const heap,
324 const __CPROVER_jsa_node_id_t node_id_to_remove)
325#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
326{
329 const __CPROVER_jsa_id_t previous_node_id=
330 heap->concrete_nodes[node_id_to_remove].previous;
331 const __CPROVER_jsa_id_t next_node_id=
332 heap->concrete_nodes[node_id_to_remove].next;
335 heap, node_id_to_remove, __CPROVER_jsa_null);
336 if(__CPROVER_jsa_null!=previous_node_id)
338 heap, previous_node_id, next_node_id);
339 else
340 {
341 const __CPROVER_jsa_list_id_t list=
342 __CPROVER_jsa__internal_get_list(heap, node_id_to_remove);
343 heap->list_head_nodes[list]=next_node_id;
344 }
345 if(__CPROVER_jsa_null!=next_node_id)
346 __CPROVER_jsa__internal_set_previous(heap, next_node_id, previous_node_id);
347 heap->concrete_nodes[node_id_to_remove].value=__CPROVER_jsa_null;
348 heap->concrete_nodes[node_id_to_remove].list=__CPROVER_jsa_null;
349 return next_node_id;
350}
351#else
352;
353#endif
354
355// Iterator utility functions
357 __CPROVER_jsa_abstract_heapt * const heap,
359#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
360{
361 heap->iterators[it].index=0;
362 heap->iterators[it].previous_index=0;
365}
366#else
367;
368#endif
369
370// Heap sanity functions
372 const __CPROVER_jsa_node_id_t node_id)
373#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
374{
375 return __CPROVER_jsa_null == node_id || node_id < __CPROVER_JSA_MAX_NODES;
376}
377#else
378;
379#endif
380
382 const __CPROVER_jsa_abstract_heapt * const heap,
383 const __CPROVER_jsa_node_id_t node_id)
384#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
385{
386 const __CPROVER_jsa_list_id_t list=
388 return __CPROVER_jsa_null == list || list < heap->list_count;
389}
390#else
391;
392#endif
393
395 const __CPROVER_jsa_abstract_heapt * const heap,
396 const __CPROVER_jsa_node_id_t node_id,
397 const __CPROVER_jsa_node_id_t prev,
398 const __CPROVER_jsa_node_id_t next)
399#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
400{
402 if(__CPROVER_jsa_null!=prev)
403 {
405 __CPROVER_jsa_assume(prev < node_id);
408 }
409 if(__CPROVER_jsa_null!=next)
410 {
411 __CPROVER_jsa_assume(node_id==
413 __CPROVER_jsa_assume(node_id<next);
416 }
417}
418#else
419;
420#endif
421
423 const __CPROVER_jsa_abstract_heapt * const h,
424 const __CPROVER_jsa_list_id_t list,
425 const __CPROVER_jsa_node_id_t node_id,
426 const __CPROVER_jsa_index_t index)
427#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
428{
430 if(__CPROVER_jsa_null!=node_id)
432 if(__CPROVER_jsa_null == node_id ||
434 __CPROVER_jsa_assume(index == 0);
435 else
436 {
439 const __CPROVER_jsa_id_t value_ref=h->abstract_nodes[idx].value_ref;
440 __CPROVER_jsa_assume(index < h->abstract_ranges[value_ref].size);
441 }
442}
443#else
444;
445#endif
446
448 const __CPROVER_jsa_abstract_heapt * const heap,
449 const __CPROVER_jsa_node_id_t node_id)
450#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
451{
453 return 0;
456 const __CPROVER_jsa_id_t value_ref=heap->abstract_nodes[idx].value_ref;
457 const __CPROVER_jsa_index_t __CPROVER_jsa__internal_get_max_index_result=
458 heap->abstract_ranges[value_ref].size - 1;
459 return __CPROVER_jsa__internal_get_max_index_result;
460}
461#else
462;
463#endif
464
466 const __CPROVER_jsa_abstract_heapt * const heap,
467 const __CPROVER_jsa_node_id_t lhs_node_id,
468 const __CPROVER_jsa_index_t lhs_index,
469 const __CPROVER_jsa_node_id_t rhs_node_id,
470 const __CPROVER_jsa_index_t rhs_index)
471#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
472{
474 {
475 __CPROVER_jsa_assume(lhs_node_id!=rhs_node_id);
476 __CPROVER_jsa_assume(lhs_index == 0 || rhs_index == 0);
477 __CPROVER_jsa_assume(heap->concrete_nodes[lhs_node_id].next==
478 rhs_node_id ||
479 heap->concrete_nodes[lhs_node_id].previous==
480 rhs_node_id);
481 }
482 else if(lhs_node_id == rhs_node_id)
483 {
484 if(lhs_index < rhs_index)
485 __CPROVER_jsa_assume((lhs_index - rhs_index) == 1);
486 else
487 __CPROVER_jsa_assume((rhs_index - lhs_index) == 1);
488 }
489 else
490 {
491 const __CPROVER_jsa_abstract_nodet node=heap->abstract_nodes[lhs_node_id];
492 if(node.next == rhs_node_id)
493 {
494 __CPROVER_jsa_assume(rhs_index == 0);
495 __CPROVER_jsa_assume(lhs_index==
497 heap, lhs_node_id));
498 }
499 else
500 {
501 __CPROVER_jsa_assume(node.previous == rhs_node_id);
502 __CPROVER_jsa_assume(lhs_index == 0);
503 __CPROVER_jsa_assume(rhs_index==
505 heap, rhs_node_id));
506 }
507 }
508}
509#else
510;
511#endif
512
513#ifdef __CPROVER_JSA_DYNAMIC_TEST_RUNNER
514void __CPROVER_jsa_internal__clear_temps(void);
515#endif
516
518 const __CPROVER_jsa_abstract_heapt * const h,
519 const __CPROVER_jsa_list_id_t list)
520#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
521{
522 __CPROVER_jsa_assume(list < h->list_count);
523}
524#else
525;
526#endif
527
529 const __CPROVER_jsa_abstract_heapt * const h,
530 const __CPROVER_jsa_list_id_t list)
531#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
532{
536}
537#else
538;
539#endif
540
542 const __CPROVER_jsa_abstract_heapt * const h,
544#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
545{
546 __CPROVER_jsa_assume(it < h->iterator_count);
547}
548#else
549;
550#endif
551
553 const __CPROVER_jsa_abstract_heapt * const h)
554#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
555{
556 // Lists point to valid head nodes.
557 // Enforce strictly ascending head node ids (unless null).
558 __CPROVER_jsa_id_t max_head_node=0;
560 for(__CPROVER_jsa_list_id_t list=0; list < __CPROVER_JSA_MAX_LISTS; ++list)
561 {
562 const __CPROVER_jsa_id_t head_node=h->list_head_nodes[list];
563 if(list >= h->list_count)
565 else
566 {
568 if(list!=0)
569 {
570 __CPROVER_jsa_assume(head_node > max_head_node);
571 max_head_node=head_node;
572 }
573 if(__CPROVER_jsa_null!=head_node)
576 }
577 }
578 // Next matches previous && prev < id < next.
579 // (Node is part of only one list, no cycles)
580 for(__CPROVER_jsa_id_t cnode=0;
582 ++cnode)
583 {
584 const __CPROVER_jsa_list_id_t node_list=h->concrete_nodes[cnode].list;
585 const __CPROVER_jsa_id_t nxt=h->concrete_nodes[cnode].next;
586 const __CPROVER_jsa_id_t prev=h->concrete_nodes[cnode].previous;
587 if(__CPROVER_jsa_null == node_list)
588 {
592 }
593 else
594 {
596 __CPROVER_jsa_assume(h->list_head_nodes[node_list] == cnode);
600 }
601 }
602#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
605 ++anode)
606 {
607 const __CPROVER_jsa_id_t nxt=h->abstract_nodes[anode].next;
609 const __CPROVER_jsa_id_t prev=h->abstract_nodes[anode].previous;
611 const __CPROVER_jsa_id_t nid=
614 }
615#endif
616#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
619 ++range)
620 {
622 __CPROVER_jsa_assume(r.size >= 1);
623 __CPROVER_jsa_assume(r.min <= r.max);
624 }
625#endif
626 // Iterators point to valid nodes
629 {
630 const __CPROVER_jsa_iteratort val=h->iterators[it];
631 const __CPROVER_jsa_id_t next_node=val.node_id;
632 const __CPROVER_jsa_index_t next_index=val.index;
633 const __CPROVER_jsa_index_t prev_index=val.previous_index;
634 const __CPROVER_jsa_id_t prev_node=val.previous_node_id;
635 const __CPROVER_jsa_list_id_t list=val.list;
636 if(it >= h->iterator_count)
637 {
640 __CPROVER_jsa_assume(next_index == 0);
641 __CPROVER_jsa_assume(prev_index == 0);
643 }
644 else
645 {
646 __CPROVER_jsa_assume(list < h->list_count);
648 h, list, next_node, next_index);
650 h, list, prev_node, prev_index);
651 if(__CPROVER_jsa_null!=next_node && __CPROVER_jsa_null != prev_node)
653 h, next_node, next_index, prev_node, prev_index);
654 }
655 }
656 // Limit list sizes in counterexamples
659 ++listc)
660 {
664 ++cnodec)
665 if(h->concrete_nodes[cnodec].list == listc)
666 ++count;
667#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
670 ++anodec)
671 if(h->abstract_nodes[anodec].list==listc)
672 ++count;
673#endif
675 }
676}
677#else
678;
679#endif
680
683#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
684{
685 const __CPROVER_jsa_index_t new_list=heap->list_count;
687 heap->list_head_nodes[new_list]=__CPROVER_jsa_null;
688 ++heap->list_count;
689 return new_list;
690}
691#else
692;
693#endif
694
696 __CPROVER_jsa_abstract_heapt * const heap,
697 const __CPROVER_jsa_list_id_t list)
698#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
699{
700 const __CPROVER_jsa_index_t new_iterator=heap->iterator_count;
702 ++heap->iterator_count;
703#ifdef __cplusplus
704 const __CPROVER_jsa_iteratort tmp = {
705 /*.node_id=*/__CPROVER_jsa__internal_get_head_node(heap, list),
706 /*.previous_node_id=*/__CPROVER_jsa_null,
707 /*.index=*/0,
708 /*.previous_index=*/0,
709 /*.list=*/list };
710#else
711 const __CPROVER_jsa_iteratort tmp = {
713 .previous_node_id=__CPROVER_jsa_null,
714 .index=0,
715 .previous_index=0,
716 .list=list };
717#endif
718 heap->iterators[new_iterator]=tmp;
719 return new_iterator;
720}
721#else
722;
723#endif
724
725#define __CPROVER_jsa_hasNext(heap, it)\
726 __CPROVER_jsa_null!=(heap)->iterators[it].node_id
727
729 __CPROVER_jsa_abstract_heapt * const heap,
731#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
732{
733 const __CPROVER_jsa_id_t node_id=heap->iterators[it].node_id;
735 const __CPROVER_jsa_data_t result=heap->concrete_nodes[node_id].value;
736 heap->iterators[it].node_id=heap->concrete_nodes[node_id].next;
737 heap->iterators[it].previous_node_id=node_id;
738 return result;
739}
740#else
741;
742#endif
743
745 __CPROVER_jsa_abstract_heapt * const heap,
747#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
748{
749 const __CPROVER_jsa_id_t node_id_to_remove=
750 heap->iterators[it].previous_node_id;
751 heap->iterators[it].node_id=
752 __CPROVER_jsa__internal_remove(heap, node_id_to_remove);
754}
755#else
756;
757#endif
758
760 __CPROVER_jsa_abstract_heapt * const heap,
762 const __CPROVER_jsa_word_t value)
763#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
764{
765 const __CPROVER_jsa_id_t node_id_to_set=heap->iterators[it].previous_node_id;
766 if(__CPROVER_jsa_null!=node_id_to_set)
767 {
770 heap->concrete_nodes[node_id_to_set].value=value;
771 }
772}
773#else
774;
775#endif
776
778 __CPROVER_jsa_abstract_heapt * const heap,
779 const __CPROVER_jsa_list_id_t list,
780 const __CPROVER_jsa_word_t value)
781#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
782{
784 for(new_node=0; new_node < __CPROVER_JSA_MAX_CONCRETE_NODES; ++new_node)
785 if(__CPROVER_jsa_null == heap->concrete_nodes[new_node].list)
786 break;
788 heap->concrete_nodes[new_node].list=list;
789 heap->concrete_nodes[new_node].next=__CPROVER_jsa_null;
790 heap->concrete_nodes[new_node].value=value;
791 const __CPROVER_jsa_node_id_t head_node=
793 if(__CPROVER_jsa_null == head_node)
794 {
795 heap->list_head_nodes[list]=new_node;
797 }
798 else
799 {
800#ifdef __CPROVER
801 const __CPROVER_jsa_node_id_t last_node;
802 __CPROVER_jsa_assume(last_node!=new_node);
805 __CPROVER_jsa__internal_get_list(heap, last_node));
807 __CPROVER_jsa__internal_get_next(heap, last_node));
808#else
809 __CPROVER_jsa_node_id_t last_node=head_node;
811 {
812 const __CPROVER_jsa_node_id_t next_node=
813 __CPROVER_jsa__internal_get_next(heap, last_node);
814 if(__CPROVER_jsa_null==next_node)
815 break;
816 last_node=next_node;
817 }
819 __CPROVER_jsa__internal_get_next(heap, last_node));
820#endif
821 __CPROVER_jsa__internal_set_next(heap, last_node, new_node);
822 heap->concrete_nodes[new_node].previous=last_node;
823 }
824}
825#else
826;
827#endif
828
830 const __CPROVER_jsa_word_t lhs,
831 const __CPROVER_jsa_word_t rhs)
832#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
833{
834 if(lhs>=rhs)
835 return lhs-rhs;
836 return __CPROVER_jsa_word_max-rhs+lhs;
837}
838#else
839;
840#endif
841
843 const __CPROVER_jsa_word_t lhs,
844 const __CPROVER_jsa_word_t rhs)
845#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
846{
847 if(rhs==0)
848 return 0;
849 return lhs % rhs;
850}
851#else
852;
853#endif
854
856 const __CPROVER_jsa_word_t lhs,
857 const __CPROVER_jsa_word_t rhs)
858#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
859{
861 if(diff < rhs)
862 return rhs-diff;
863 return lhs+rhs;
864}
865#else
866;
867#endif
868
870 const __CPROVER_jsa_word_t lhs,
871 const __CPROVER_jsa_word_t rhs)
872#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
873{
874 if(lhs!=0 && __CPROVER_jsa_word_max/lhs!=rhs)
875 {
877 }
878 return lhs * rhs;
879}
880#else
881;
882#endif
883
885 const __CPROVER_jsa_word_t lhs,
886 const __CPROVER_jsa_word_t rhs)
887#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
888{
889 if(rhs==0)
891 return lhs/rhs;
892}
893#else
894;
895#endif
896
898 const __CPROVER_jsa_word_t res,
899 const __CPROVER_jsa_word_t lhs,
900 const __CPROVER_jsa_word_t rhs)
901#ifdef __CPROVER_JSA_DEFINE_TRANSFORMERS
902{
903 if(res!=0)
904 return lhs;
905 return rhs;
906}
907#else
908;
909#endif
910
911// SYNTHESIS
912
913#ifdef JSA_SYNTHESIS_H_
914
915#ifndef __CPROVER_JSA_NUM_PRED_OPS
916#define __CPROVER_JSA_NUM_PRED_OPS 10
917#endif
918#ifndef __CPROVER_JSA_NUM_PRED_RESULT_OPS
919#define __CPROVER_JSA_NUM_PRED_RESULT_OPS __CPROVER_JSA_NUM_PRED_OPS
920#endif
921#ifndef __CPROVER_JSA_MAX_QUERY_SIZE
922#define __CPROVER_JSA_MAX_QUERY_SIZE 10
923#endif
924#ifndef __CPROVER_JSA_MAX_PRED_SIZE
925#define __CPROVER_JSA_MAX_PRED_SIZE (__CPROVER_JSA_MAX_QUERY_SIZE - 1)
926#endif
927#ifndef __CPROVER_JSA_NUM_PREDS
928#define __CPROVER_JSA_NUM_PREDS (__CPROVER_JSA_MAX_QUERY_SIZE - 1)
929#endif
930
932 *__CPROVER_JSA_PRED_OPS[__CPROVER_JSA_NUM_PRED_OPS];
934 *__CPROVER_JSA_PRED_RESULT_OPS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
936 __CPROVER_JSA_MAX_PRED_SIZE_RELAY[__CPROVER_JSA_MAX_PRED_SIZE];
938 __CPROVER_JSA_MAX_QUERY_SIZE_RELAY[__CPROVER_JSA_MAX_QUERY_SIZE];
940 __CPROVER_JSA_MAX_ITERATORS_RELAY[__CPROVER_JSA_MAX_ITERATORS];
942 __CPROVER_JSA_MAX_LISTS_RELAY[__CPROVER_JSA_MAX_LISTS];
943#if 0
945 __CPROVER_JSA_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
947 __CPROVER_JSA_ORG_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
949 __CPROVER_JSA_QUERIED_HEAP_VARS[__CPROVER_JSA_NUM_PRED_RESULT_OPS];
950#endif
951
952typedef __CPROVER_jsa_word_t __CPROVER_jsa_opcodet;
953typedef __CPROVER_jsa_word_t __CPROVER_jsa_opt;
954typedef struct __CPROVER_jsa_pred_instruction
955{
956 __CPROVER_jsa_opcodet opcode;
957 __CPROVER_jsa_opt result_op;
958 __CPROVER_jsa_opt op0;
959 __CPROVER_jsa_opt op1;
960} __CPROVER_jsa_pred_instructiont;
961
963 __CPROVER_JSA_PRED_OPS_COUNT;
965 __CPROVER_JSA_PRED_RESULT_OPS_COUNT;
966__CPROVER_jsa_extern const __CPROVER_jsa_pred_instructiont
967 *__CPROVER_JSA_PREDICATES[__CPROVER_JSA_NUM_PREDS];
969 __CPROVER_JSA_PREDICATE_SIZES[__CPROVER_JSA_NUM_PREDS];
970
971#define __CPROVER_JSA_NUM_PRED_INSTRUCTIONS 8u
972
973typedef __CPROVER_jsa_word_t __CPROVER_jsa_pred_id_t;
974
975__CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_pred(
976 const __CPROVER_jsa_pred_id_t pred_id)
977{
979 __CPROVER_JSA_PRED_OPS_COUNT<=__CPROVER_JSA_NUM_PRED_OPS,
980 "__CPROVER_JSA_PRED_OPS_COUNT <= __CPROVER_JSA_NUM_PRED_OPS");
982 __CPROVER_JSA_PRED_RESULT_OPS_COUNT<=__CPROVER_JSA_NUM_PRED_RESULT_OPS,
983 "__CPROVER_JSA_PRED_RESULT_OPS_COUNT <= __CPROVER_JSA_NUM_PRED_RESULT_OPS");
984
985 __CPROVER_jsa_assume(pred_id < __CPROVER_JSA_NUM_PREDS);
986 const __CPROVER_jsa_pred_instructiont * const pred=
987 __CPROVER_JSA_PREDICATES[pred_id];
989 __CPROVER_JSA_PREDICATE_SIZES[pred_id];
990 __CPROVER_jsa_assume(sz <= __CPROVER_JSA_MAX_PRED_SIZE);
991 for(__CPROVER_jsa__internal_index_t i=0; i < __CPROVER_JSA_MAX_PRED_SIZE; ++i)
992 {
993 if(i>=sz)
994 break;
995 const __CPROVER_jsa_pred_instructiont instr=pred[i];
996 __CPROVER_jsa_assume(instr.op0 < __CPROVER_JSA_NUM_PRED_OPS);
997 __CPROVER_jsa_assume(instr.op1 < __CPROVER_JSA_NUM_PRED_OPS);
998 __CPROVER_jsa_assume(instr.result_op < __CPROVER_JSA_NUM_PRED_RESULT_OPS);
999 __CPROVER_jsa_assume(__CPROVER_JSA_PRED_OPS[instr.op0]);
1000 __CPROVER_jsa_assume(__CPROVER_JSA_PRED_OPS[instr.op1]);
1001 __CPROVER_jsa_assume(__CPROVER_JSA_PRED_RESULT_OPS[instr.result_op]);
1002 switch (instr.opcode)
1003 {
1004 case 0:
1005 break;
1006 case 1:
1007 break;
1008 case 2:
1009 break;
1010 case 3:
1011 __CPROVER_jsa_assume(instr.op0 < instr.op1);
1012 break;
1013 case 4:
1014 break;
1015 case 5:
1016 __CPROVER_jsa_assume(instr.op0 <= instr.op1);
1017 break;
1018 case 6:
1019 __CPROVER_jsa_assume(instr.op0 <= instr.op1);
1020 break;
1021 default:
1022 __CPROVER_jsa_assume(false);
1023 break;
1024 }
1025 }
1026}
1027
1028__CPROVER_jsa_inline __CPROVER_jsa_word_t __CPROVER_jsa_execute_pred(
1029 const __CPROVER_jsa_pred_id_t pred_id)
1030{
1031 const __CPROVER_jsa_pred_instructiont * const pred=
1032 __CPROVER_JSA_PREDICATES[pred_id];
1033 const __CPROVER_jsa__internal_index_t pred_sz=
1034 __CPROVER_JSA_PREDICATE_SIZES[pred_id];
1035 __CPROVER_jsa_word_t result=0;
1036 for(__CPROVER_jsa__internal_index_t i=0; i < __CPROVER_JSA_MAX_PRED_SIZE; ++i)
1037 {
1038 if(i>=pred_sz)
1039 break;
1040 const __CPROVER_jsa_pred_instructiont instr=pred[i];
1041#define __CPROVER_jsa_execute_pred_op0_ptr __CPROVER_JSA_PRED_OPS[instr.op0]
1042#define __CPROVER_jsa_execute_pred_op1_ptr __CPROVER_JSA_PRED_OPS[instr.op1]
1043#define __CPROVER_jsa_execute_pred_result_op_ptr \
1044 __CPROVER_JSA_PRED_RESULT_OPS[instr.result_op]
1045#define __CPROVER_jsa_execute_pred_op0 *__CPROVER_jsa_execute_pred_op0_ptr
1046#define __CPROVER_jsa_execute_pred_op1 *__CPROVER_jsa_execute_pred_op1_ptr
1047#define __CPROVER_jsa_execute_pred_result \
1048 *__CPROVER_jsa_execute_pred_result_op_ptr
1049 switch (instr.opcode)
1050 {
1051 case 0:
1052 __CPROVER_jsa_pred_opcode_0:
1053 __CPROVER_jsa_execute_pred_result=
1054 __CPROVER_jsa_execute_pred_op0<__CPROVER_jsa_execute_pred_op1;
1055 break;
1056 case 1:
1057 __CPROVER_jsa_pred_opcode_1:
1058 __CPROVER_jsa_execute_pred_result=
1059 __CPROVER_jsa_execute_pred_op0<=__CPROVER_jsa_execute_pred_op1;
1060 break;
1061 case 2:
1062 __CPROVER_jsa_pred_opcode_first_2:
1063 __CPROVER_jsa_execute_pred_result=
1065 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1066 __CPROVER_jsa_pred_opcode_last_2:
1067 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1068 break;
1069 case 3:
1070 __CPROVER_jsa_pred_opcode_3:
1071 __CPROVER_jsa_execute_pred_result=
1072 __CPROVER_jsa_execute_pred_op0!=__CPROVER_jsa_execute_pred_op1;
1073 break;
1074 case 4:
1075 __CPROVER_jsa_pred_opcode_first_4:
1076 __CPROVER_jsa_execute_pred_result=
1078 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1079 __CPROVER_jsa_pred_opcode_last_4:
1080 __CPROVER_jsa_execute_pred_result=
1081 __CPROVER_jsa_execute_pred_result;
1082 break;
1083 case 5:
1084 __CPROVER_jsa_pred_opcode_first_5:
1085 __CPROVER_jsa_execute_pred_result=
1087 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1088 __CPROVER_jsa_pred_opcode_last_5:
1089 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1090 break;
1091 case 6:
1092 __CPROVER_jsa_pred_opcode_first_6:
1093 __CPROVER_jsa_execute_pred_result=
1095 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1096 __CPROVER_jsa_pred_opcode_last_6:
1097 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1098 break;
1099 case 7:
1100 __CPROVER_jsa_pred_opcode_first_7:
1101 __CPROVER_jsa_execute_pred_result=
1103 __CPROVER_jsa_execute_pred_op0, __CPROVER_jsa_execute_pred_op1);
1104 __CPROVER_jsa_pred_opcode_last_7:
1105 __CPROVER_jsa_execute_pred_result=__CPROVER_jsa_execute_pred_result;
1106 break;
1107 }
1108 result=__CPROVER_jsa_execute_pred_result;
1109 }
1110#ifdef __CPROVER_JSA_DYNAMIC_TEST_RUNNER
1111 __CPROVER_jsa_internal__clear_temps();
1112#endif
1113 return result;
1114}
1115
1116// Instrumentation adds a lambda variable at program entry. It'll have id 0.
1117#define __CPROVER_jsa__internal_lambda_op_id 0
1118#define FILTER_QUERY_INSTR_ID 0
1119typedef enum {
1120 FILTER = 0,
1121 MAP = 1,
1122 MAP_IN_PLACE = 2
1123} __CPROVER_jsa_query_idt;
1124
1125__CPROVER_jsa_inline void __CPROVER_jsa_stream_op(
1126 __CPROVER_jsa_abstract_heapt * const heap,
1127 const __CPROVER_jsa_list_id_t list,
1129 const __CPROVER_jsa_list_id_t source,
1130 const __CPROVER_jsa_pred_id_t pred_id,
1132{
1133 const __CPROVER_jsa_list_id_t it_list=heap->iterators[it].list;
1136 const __CPROVER_jsa_node_id_t it_range_end=heap->iterators[it].node_id;
1138 for(distance=0; distance < __CPROVER_JSA_MAX_NODES; ++distance)
1139 if(it_node==it_range_end || it_node==__CPROVER_jsa_null)
1140 break;
1141 else
1142 it_node=__CPROVER_jsa__internal_get_next(heap, it_node);
1143
1145 if(__CPROVER_jsa_null == source)
1146 {
1147 const __CPROVER_jsa_node_id_t head_node=
1149 node=head_node;
1151 for(node_count=0; node_count < __CPROVER_JSA_MAX_NODES; ++node_count)
1152 {
1153 if(__CPROVER_jsa_null == node)
1154 break;
1155 else
1156 node=__CPROVER_jsa__internal_get_next(heap, node);
1157 }
1158 node=head_node;
1159 if(node_count > distance)
1160 {
1161 __CPROVER_jsa__internal_index_t skip_distance=node_count - distance;
1162 for(node_count=0; node_count < __CPROVER_JSA_MAX_NODES; ++node_count)
1163 if(node_count>=skip_distance)
1164 break;
1165 else
1166 node=__CPROVER_jsa__internal_get_next(heap, node);
1167 }
1168 }
1169 else
1170 node=__CPROVER_jsa__internal_get_head_node(heap, source);
1172 {
1173 if(i>=distance || __CPROVER_jsa_null==node)
1174 break;
1175 const _Bool is_concrete=__CPROVER_jsa__internal_is_concrete_node(node);
1176 if(is_concrete)
1177 {
1178 const __CPROVER_jsa_word_t value=heap->concrete_nodes[node].value;
1179 *__CPROVER_JSA_PRED_OPS[__CPROVER_jsa__internal_lambda_op_id]=value;
1180 const __CPROVER_jsa_word_t pred_result=
1181 __CPROVER_jsa_execute_pred(pred_id);
1182 switch(id)
1183 {
1184 case FILTER:
1185 if(pred_result == 0)
1186 node=__CPROVER_jsa__internal_remove(heap, node);
1187 else
1188 node=__CPROVER_jsa__internal_get_next(heap, node);
1189 continue;
1190 case MAP:
1191 __CPROVER_jsa_add(heap, list, pred_result);
1192 break;
1193 case MAP_IN_PLACE:
1194 heap->concrete_nodes[node].value=pred_result;
1195 break;
1196 }
1197 }
1198 else
1199 {
1200 // TODO: Implement filtering abstract nodes.
1201 // (Maybe ignore and handle on whole query level?)
1202 }
1203 node=__CPROVER_jsa__internal_get_next(heap, node);
1204 }
1205}
1206
1207typedef struct __CPROVER_jsa_query_instruction
1208{
1209 __CPROVER_jsa_opcodet opcode;
1210 __CPROVER_jsa_opt op0;
1211 __CPROVER_jsa_opt op1;
1212} __CPROVER_jsa_query_instructiont;
1213
1214#define __CPROVER_JSA_NUM_QUERY_INSTRUCTIONS 3u
1215
1216__CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_query(
1217 const __CPROVER_jsa_abstract_heapt * const heap,
1218 const __CPROVER_jsa_query_instructiont * const query,
1219 const __CPROVER_jsa__internal_index_t query_size)
1220{
1221 __CPROVER_jsa_assume(query_size >= 2);
1222 __CPROVER_jsa_assume(query_size <= __CPROVER_JSA_MAX_QUERY_SIZE);
1223 __CPROVER_jsa_assume(query[0].op1 == 0);
1224 __CPROVER_jsa_assume_valid_list(heap, query[0].opcode);
1225 __CPROVER_jsa_assume_valid_iterator(heap, query[0].op0);
1226
1227 for(__CPROVER_jsa__internal_index_t i=1; i<__CPROVER_JSA_MAX_QUERY_SIZE; ++i)
1228 {
1229 if(i>=query_size)
1230 break;
1231 const __CPROVER_jsa_query_instructiont instr=query[i];
1232 __CPROVER_jsa_assume(instr.op0 < __CPROVER_JSA_NUM_PREDS);
1233 switch(instr.opcode)
1234 {
1235 case FILTER:
1237 break;
1238 case MAP:
1239 __CPROVER_jsa_assume_valid_list(heap, instr.op1);
1240 break;
1241 case MAP_IN_PLACE:
1243 break;
1244 default:
1245 __CPROVER_jsa_assume(false);
1246 break;
1247 }
1248 }
1249}
1250
1251__CPROVER_jsa_inline void __CPROVER_jsa_query_execute(
1252 __CPROVER_jsa_abstract_heapt * const heap,
1253 const __CPROVER_jsa_query_instructiont * const query,
1254 const __CPROVER_jsa__internal_index_t query_size)
1255{
1256 __CPROVER_jsa_assume_valid_query(heap, query, query_size);
1257 const __CPROVER_jsa_list_id_t list=query[0].opcode;
1258 const __CPROVER_jsa_iterator_id_t it=query[0].op0;
1259 for(__CPROVER_jsa__internal_index_t i=1; i<__CPROVER_JSA_MAX_QUERY_SIZE; ++i)
1260 {
1261 if(i>=query_size)
1262 break;
1263 const __CPROVER_jsa_query_instructiont instr=query[i];
1264 __CPROVER_jsa_query_opcode_0:
1265 __CPROVER_jsa_stream_op(
1266 heap, list, it, instr.op1, instr.op0, instr.opcode);
1267 }
1268}
1269
1270__CPROVER_jsa_inline void __CPROVER_jsa_full_query_execute(
1271 __CPROVER_jsa_abstract_heapt * const heap,
1272 const __CPROVER_jsa_query_instructiont * const query,
1273 const __CPROVER_jsa__internal_index_t query_size)
1274{
1275 const __CPROVER_jsa_iterator_id_t it=query[0].op0;
1277 __CPROVER_jsa__internal_make_null(heap, it); // Apply query to full list.
1278 __CPROVER_jsa_query_execute(heap, query, query_size);
1279}
1280
1281__CPROVER_jsa_inline void __CPROVER_jsa_verify_synchronise_iterator(
1282 const __CPROVER_jsa_abstract_heapt * const heap,
1283 __CPROVER_jsa_abstract_heapt * const queried_heap,
1285{
1287 queried_heap->iterators[i]=heap->iterators[i];
1288}
1289
1290__CPROVER_jsa_inline void __CPROVER_jsa_synchronise_iterator(
1291 const __CPROVER_jsa_abstract_heapt * const heap,
1292 __CPROVER_jsa_abstract_heapt * const queried_heap,
1293 const __CPROVER_jsa_query_instructiont * const query,
1294 const __CPROVER_jsa__internal_index_t query_size)
1295{
1296 const __CPROVER_jsa_iterator_id_t it=query[0].op0;
1298 __CPROVER_jsa_verify_synchronise_iterator(heap, queried_heap, it);
1299}
1300
1301__CPROVER_jsa_inline _Bool __CPROVER_jsa_verify_invariant_execute(
1302 const __CPROVER_jsa_abstract_heapt * const heap,
1303 const __CPROVER_jsa_abstract_heapt * const queried_heap)
1304{
1305/*#ifdef __CPROVER
1306 const _Bool vars_equal=
1307 __CPROVER_array_equal(
1308 __CPROVER_JSA_HEAP_VARS, __CPROVER_JSA_QUERIED_HEAP_VARS);
1309#else
1310 const _Bool vars_equal=
1311 memcmp(
1312 &__CPROVER_JSA_HEAP_VARS,
1313 &__CPROVER_JSA_QUERIED_HEAP_VARS,
1314 sizeof(__CPROVER_JSA_HEAP_VARS)) == 0;
1315#endif*/
1316 const _Bool heaps_equal=
1317 __CPROVER_jsa__internal_are_heaps_equal(heap, queried_heap);
1318 //return vars_equal && heaps_equal;
1319 return heaps_equal;
1320}
1321
1322typedef struct __CPROVER_jsa_invariant_instruction
1323{
1324 __CPROVER_jsa_opcodet opcode;
1325} __CPROVER_jsa_invariant_instructiont;
1326
1327#define __CPROVER_JSA_NUM_INV_INSTRUCTIONS 1u
1328
1329__CPROVER_jsa_inline _Bool __CPROVER_jsa_invariant_execute(
1330 const __CPROVER_jsa_abstract_heapt * const heap,
1331 const __CPROVER_jsa_abstract_heapt * const queried_heap,
1332 const __CPROVER_jsa_invariant_instructiont * const inv,
1333 const __CPROVER_jsa__internal_index_t inv_size)
1334{
1335 __CPROVER_jsa_assume(inv_size == 1u);
1336 __CPROVER_jsa_assume(inv[0].opcode == 0); // Single instruction
1337 return __CPROVER_jsa_verify_invariant_execute(heap, queried_heap);
1338}
1339
1340__CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_invariant_iterator(
1341 const __CPROVER_jsa_abstract_heapt * const h,
1343{
1344 __CPROVER_jsa_assume(it < h->iterator_count);
1345 // XXX: Debug: Only one iterator, always first list!
1346 __CPROVER_jsa_assume(h->iterators[it].list == 0);
1347}
1348
1349#endif
1350
1351#endif // CPROVER_ANSI_C_LIBRARY_JSA_H
static int8_t r
Definition irep_hash.h:60
static __CPROVER_jsa_word_t __CPROVER_jsa_div(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
Definition jsa.h:884
static void __CPROVER_jsa_add(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_list_id_t list, const __CPROVER_jsa_word_t value)
Definition jsa.h:777
#define __CPROVER_JSA_MAX_ABSTRACT_RANGES
Definition jsa.h:53
#define __CPROVER_JSA_MAX_ITERATORS
Definition jsa.h:56
__CPROVER_jsa_word_t __CPROVER_jsa_data_t
Definition jsa.h:73
static _Bool __CPROVER_jsa__internal_is_valid_node_id(const __CPROVER_jsa_node_id_t node_id)
Definition jsa.h:371
#define __CPROVER_jsa_word_max
Definition jsa.h:81
unsigned char __CPROVER_jsa_word_t
Definition jsa.h:71
static __CPROVER_jsa_node_id_t __CPROVER_jsa__internal_remove(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id_to_remove)
Definition jsa.h:322
__CPROVER_jsa_id_t __CPROVER_jsa_iterator_id_t
Definition jsa.h:79
__CPROVER_jsa_id_t __CPROVER_jsa_node_id_t
Definition jsa.h:77
static void __CPROVER_jsa_assume_new_list(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list)
Definition jsa.h:528
#define __CPROVER_jsa_inline
Definition jsa.h:169
#define __CPROVER_jsa__internal_get_previous(heap_ptr, node)
Definition jsa.h:316
static void __CPROVER_jsa__internal_assume_valid_iterator_linking(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list, const __CPROVER_jsa_node_id_t node_id, const __CPROVER_jsa_index_t index)
Definition jsa.h:422
static __CPROVER_jsa_word_t __CPROVER_jsa_mult(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
Definition jsa.h:869
static void __CPROVER_jsa_assume_valid_iterator(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_iterator_id_t it)
Definition jsa.h:541
static __CPROVER_jsa_index_t __CPROVER_jsa__internal_get_max_index(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id)
Definition jsa.h:447
static __CPROVER_jsa_list_id_t __CPROVER_jsa_create_list(__CPROVER_jsa_abstract_heapt *const heap)
Definition jsa.h:681
__CPROVER_jsa_word_t __CPROVER_jsa_index_t
Definition jsa.h:74
struct __CPROVER_jsa_abstract_heap __CPROVER_jsa_abstract_heapt
static void __CPROVER_jsa__internal_assume_is_neighbour(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t lhs_node_id, const __CPROVER_jsa_index_t lhs_index, const __CPROVER_jsa_node_id_t rhs_node_id, const __CPROVER_jsa_index_t rhs_index)
Definition jsa.h:465
#define __CPROVER_JSA_MAX_ABSTRACT_NODES
Definition jsa.h:46
static __CPROVER_jsa_word_t __CPROVER_jsa_ite(const __CPROVER_jsa_word_t res, const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
Definition jsa.h:897
static void __CPROVER_jsa__internal_make_null(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
Definition jsa.h:356
static void __CPROVER_jsa__internal_set_next(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node, const __CPROVER_jsa_node_id_t next_node)
Definition jsa.h:270
static _Bool __CPROVER_jsa__internal_is_in_valid_list(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id)
Definition jsa.h:381
#define __CPROVER_jsa__internal_get_abstract_node_index(node)
Definition jsa.h:259
#define __CPROVER_JSA_MAX_NODES_PER_CE_LIST
Definition jsa.h:62
#define __CPROVER_JSA_MAX_LISTS
Definition jsa.h:59
#define __CPROVER_jsa__internal_is_concrete_node(node)
Definition jsa.h:253
#define __CPROVER_jsa__internal_get_list(heap_ptr, node)
Definition jsa.h:265
#define __CPROVER_jsa__internal_get_next(heap_ptr, node)
Definition jsa.h:290
#define __CPROVER_jsa_extern
Definition jsa.h:26
#define __CPROVER_jsa_assert(c, str)
Definition jsa.h:182
#define __CPROVER_jsa__internal_get_head_node(heap_ptr, list)
Definition jsa.h:250
#define __CPROVER_jsa_null
Definition jsa.h:80
#define __CPROVER_jsa_assume(c)
Definition jsa.h:176
static __CPROVER_jsa_word_t __CPROVER_jsa_minus(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
Definition jsa.h:829
static void __CPROVER_jsa__internal_set_previous(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node, const __CPROVER_jsa_node_id_t previous_node)
Definition jsa.h:296
static __CPROVER_jsa_word_t __CPROVER_jsa_mod(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
Definition jsa.h:842
static _Bool __CPROVER_jsa__internal_are_heaps_equal(const __CPROVER_jsa_abstract_heapt *const lhs, const __CPROVER_jsa_abstract_heapt *const rhs)
Definition jsa.h:189
#define __CPROVER_jsa__internal_get_abstract_node_id(node_index)
Definition jsa.h:262
__CPROVER_jsa_word_t __CPROVER_jsa__internal_index_t
Definition jsa.h:75
static void __CPROVER_jsa_assume_valid_heap(const __CPROVER_jsa_abstract_heapt *const h)
Definition jsa.h:552
static __CPROVER_jsa_data_t __CPROVER_jsa_next(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
Definition jsa.h:728
char __CPROVER_jsa_signed_word_t
Definition jsa.h:72
struct __CPROVER_jsa_concrete_node __CPROVER_jsa_concrete_nodet
Concrete node with explicit value.
struct __CPROVER_jsa_abstract_node __CPROVER_jsa_abstract_nodet
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget).
static void __CPROVER_jsa_set(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it, const __CPROVER_jsa_word_t value)
Definition jsa.h:759
static __CPROVER_jsa_iterator_id_t __CPROVER_jsa_iterator(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_list_id_t list)
Definition jsa.h:695
static void __CPROVER_jsa_remove(__CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_iterator_id_t it)
Definition jsa.h:744
__CPROVER_jsa_id_t __CPROVER_jsa_list_id_t
Definition jsa.h:78
struct __CPROVER_jsa_iterator __CPROVER_jsa_iteratort
Iterators point to a node and give the relative index within that node.
static void __CPROVER_jsa__internal_assume_linking_correct(const __CPROVER_jsa_abstract_heapt *const heap, const __CPROVER_jsa_node_id_t node_id, const __CPROVER_jsa_node_id_t prev, const __CPROVER_jsa_node_id_t next)
Definition jsa.h:394
#define __CPROVER_JSA_MAX_NODES
Definition jsa.h:49
static void __CPROVER_jsa_assume_valid_list(const __CPROVER_jsa_abstract_heapt *const h, const __CPROVER_jsa_list_id_t list)
Definition jsa.h:517
#define __CPROVER_JSA_MAX_CONCRETE_NODES
Definition jsa.h:43
jmp_buf __CPROVER_jsa_jump_buffer
struct __CPROVER_jsa_abstract_range __CPROVER_jsa_abstract_ranget
Set of pre-defined, possible values for abstract nodes.
__CPROVER_jsa_word_t __CPROVER_jsa_id_t
Definition jsa.h:76
static __CPROVER_jsa_word_t __CPROVER_jsa_plus(const __CPROVER_jsa_word_t lhs, const __CPROVER_jsa_word_t rhs)
Definition jsa.h:855
__CPROVER_jsa_index_t iterator_count
Number of iterators on the heap.
Definition jsa.h:152
__CPROVER_jsa_concrete_nodet concrete_nodes[100u]
Definition jsa.h:131
__CPROVER_jsa_index_t list_count
Number of lists on the heap.
Definition jsa.h:162
__CPROVER_jsa_abstract_nodet abstract_nodes[100u]
Definition jsa.h:135
__CPROVER_jsa_list_id_t list_head_nodes[100u]
Set of node ids which are list heads.
Definition jsa.h:157
__CPROVER_jsa_iteratort iterators[100u]
Definition jsa.h:147
__CPROVER_jsa_abstract_ranget abstract_ranges[100u]
Definition jsa.h:142
Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget).
Definition jsa.h:99
__CPROVER_jsa_node_id_t previous
Definition jsa.h:101
__CPROVER_jsa_id_t value_ref
Definition jsa.h:103
__CPROVER_jsa_node_id_t next
Definition jsa.h:100
__CPROVER_jsa_list_id_t list
Definition jsa.h:102
Set of pre-defined, possible values for abstract nodes.
Definition jsa.h:110
__CPROVER_jsa_index_t size
Definition jsa.h:113
__CPROVER_jsa_data_t min
Definition jsa.h:111
__CPROVER_jsa_data_t max
Definition jsa.h:112
Concrete node with explicit value.
Definition jsa.h:87
__CPROVER_jsa_list_id_t list
Definition jsa.h:90
__CPROVER_jsa_data_t value
Definition jsa.h:91
__CPROVER_jsa_node_id_t previous
Definition jsa.h:89
__CPROVER_jsa_node_id_t next
Definition jsa.h:88
Iterators point to a node and give the relative index within that node.
Definition jsa.h:121
__CPROVER_jsa_node_id_t previous_node_id
Definition jsa.h:123
__CPROVER_jsa_list_id_t list
Definition jsa.h:126
__CPROVER_jsa_index_t index
Definition jsa.h:124
__CPROVER_jsa_index_t previous_index
Definition jsa.h:125
__CPROVER_jsa_node_id_t node_id
Definition jsa.h:122