1 /*----------------------------------------------------------------------- 2 3 File : clb_plocalstacks.h 4 5 Author: Martin Möhrmann 6 7 Contents 8 9 Stack implementation with macros that use local variables. 10 11 Copyright 2016 by the author. 12 This code is released under the GNU General Public Licence and 13 the GNU Lesser General Public License. 14 See the file COPYING in the main E directory for details.. 15 Run "eprover -h" for contact information. 16 17 -----------------------------------------------------------------------*/ 18 19 #ifndef CLB_PLOCALSTACKS 20 21 #define CLB_PLOCALSTACKS 22 23 #include <clb_memory.h> 24 25 26 #define PLOCALSTACK_DEFAULT_SIZE 64 27 28 29 #define PLocalStackInit(stack) PLocalStackInitWithSize(stack, PLOCALSTACK_DEFAULT_SIZE) 30 31 #define PLocalStackInitWithSize(stack, num) size_t stack##_##size = num; \ 32 void* *stack##_##data = SizeMalloc(stack##_##size * sizeof(void*)); \ 33 size_t stack##_##current = 0 34 35 #define PLocalStackFree(junk) SizeFree(junk##_##data, junk##_##size * sizeof(void*)); 36 37 #define PLocalStackEnsureSpace(stack, space) do{ \ 38 if(UNLIKELY((stack##_##current+space) >= stack##_##size)) \ 39 { \ 40 stack##_##size = PLocalStackGrow(&stack##_##data, stack##_##size, space); \ 41 } \ 42 }while(0) 43 44 #define PLocalStackEmpty(stack) (stack##_##current == 0) 45 #define PLocalStackPop(stack) (stack##_##data[--stack##_##current]) 46 #define PLocalStackPush(stack, val) (stack##_##data[stack##_##current++] = val) 47 48 #define PLocalStackPushTermArgsReversed(stack, term) do{ \ 49 PLocalStackEnsureSpace(stack,term->arity); \ 50 for(long i = term->arity-1; i>=0; i--) \ 51 { \ 52 PLocalStackPush(stack, term->args[i]); \ 53 } \ 54 }while(0) 55 56 #define PLocalStackPushTermArgs(stack, term) do{ \ 57 PLocalStackEnsureSpace(stack,term->arity); \ 58 for(size_t i = 0; i < term->arity; i++) \ 59 { \ 60 PLocalStackPush(stack, term->args[i]); \ 61 } \ 62 }while(0) 63 64 #define PLOCALSTACK_TAG_BITS 2 65 #define PLOCALSTACK_TAG_MASK (uintptr_t)((1<<PLOCALSTACK_TAG_BITS)-1) 66 #define PLOCALSTACK_VAL_MASK (uintptr_t)(~PLOCALSTACK_TAG_MASK) 67 68 #define PLocalTaggedStackInit(stack) PLocalStackInit(stack) 69 #define PLocalTaggedStackFree(junk) PLocalStackFree(junk) 70 #define PLocalTaggedStackEmpty(stack) PLocalStackEmpty(stack) 71 72 #define PLocalTaggedStackPushTermArgsReversed(stack, term, tag) do{ \ 73 const long arity = term->arity; \ 74 PLocalTaggedStackEnsureSpace(stack,arity); \ 75 for(long i = arity-1; i>=0; i--) \ 76 { \ 77 PLocalTaggedStackPush(stack, term->args[i], tag); \ 78 } \ 79 }while(0) 80 81 #define PLocalTaggedStackPushTermArgs(stack, term, tag) do{ \ 82 const long arity = term->arity; \ 83 PLocalTaggedStackEnsureSpace(stack, arity); \ 84 for(size_t i = 0; i < arity; i++) \ 85 { \ 86 PLocalTaggedStackPush(stack, term->args[i], tag); \ 87 } \ 88 }while(0) 89 90 #ifdef TAGGED_POINTERS 91 92 #define PLocalTaggedStackEnsureSpace(stack, space) PLocalStackEnsureSpace(stack, space) 93 94 #define PLocalTaggedStackPop(stack, val, tag) do{ \ 95 val = stack##_##data[--stack##_##current]; \ 96 tag = (uintptr_t)val & PLOCALSTACK_TAG_MASK; \ 97 val = (void*)((uintptr_t)val & PLOCALSTACK_VAL_MASK); \ 98 }while(0) 99 100 #define PLocalTaggedStackPush(stack, val, tag) do{ \ 101 assert(((void*)((uintptr_t)val&PLOCALSTACK_VAL_MASK)) == val); \ 102 assert(((uintptr_t)tag&PLOCALSTACK_TAG_MASK) == tag); \ 103 stack##_##data[stack##_##current++] = (void*)(((uintptr_t)val) | tag); \ 104 }while(0) \ 105 106 #else 107 108 #define PLocalTaggedStackEnsureSpace(stack, space) PLocalStackEnsureSpace(stack, (2*(space))) 109 110 #define PLocalTaggedStackPop(stack, val, tag) do{ \ 111 tag = (__typeof__(tag))stack##_##data[--stack##_##current]; \ 112 val = stack##_##data[--stack##_##current]; \ 113 }while(0) 114 115 #define PLocalTaggedStackPush(stack, val, tag) do{ \ 116 assert(sizeof(tag) =< sizeof(void*)); \ 117 assert(((__typeof__(tag))((void*)tag)) == tag); \ 118 stack##_##data[stack##_##current++] = val; \ 119 stack##_##data[stack##_##current++] = (void*)tag; \ 120 }while(0) 121 122 #endif 123 124 __attribute__ ((noinline)) size_t PLocalStackGrow(void** *data, size_t size, size_t space); 125 126 #endif 127 128 /*---------------------------------------------------------------------*/ 129 /* End of File */ 130 /*---------------------------------------------------------------------*/ 131