12 #include "threads-model.h"
16 #define REQUESTS_BEFORE_ALLOC 1024
18 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
21 mspace sStaticSpace = NULL;
23 /** Non-snapshotting calloc for our use. */
24 void *model_calloc(size_t count, size_t size)
26 return mspace_calloc(sStaticSpace, count, size);
29 /** Non-snapshotting malloc for our use. */
30 void *model_malloc(size_t size)
32 return mspace_malloc(sStaticSpace, size);
35 /** Non-snapshotting malloc for our use. */
36 void *model_realloc(void *ptr, size_t size)
38 return mspace_realloc(sStaticSpace, ptr, size);
41 /** @brief Snapshotting malloc, for use by model-checker (not user progs) */
42 void * snapshot_malloc(size_t size)
44 void *tmp = mspace_malloc(model_snapshot_space, size);
49 /** @brief Snapshotting calloc, for use by model-checker (not user progs) */
50 void * snapshot_calloc(size_t count, size_t size)
52 void *tmp = mspace_calloc(model_snapshot_space, count, size);
57 /** @brief Snapshotting realloc, for use by model-checker (not user progs) */
58 void *snapshot_realloc(void *ptr, size_t size)
60 void *tmp = mspace_realloc(model_snapshot_space, ptr, size);
65 /** @brief Snapshotting free, for use by model-checker (not user progs) */
66 void snapshot_free(void *ptr)
68 mspace_free(model_snapshot_space, ptr);
71 /** Non-snapshotting free for our use. */
72 void model_free(void *ptr)
74 mspace_free(sStaticSpace, ptr);
77 /** Bootstrap allocation. Problem is that the dynamic linker calls require
78 * calloc to work and calloc requires the dynamic linker to work. */
80 #define BOOTSTRAPBYTES 131072
81 char bootstrapmemory[BOOTSTRAPBYTES];
84 void * HandleEarlyAllocationRequest(size_t sz)
86 /* Align to 8 byte boundary */
89 if (sz > (BOOTSTRAPBYTES-offset)) {
90 model_print("OUT OF BOOTSTRAP MEMORY. Increase the size of BOOTSTRAPBYTES in mymemory.cc\n");
94 void *pointer = (void *)&bootstrapmemory[offset];
99 /** @brief Global mspace reference for the model-checker's snapshotting heap */
100 mspace model_snapshot_space = NULL;
102 /** @brief Snapshotting allocation function for use by the Thread class only */
103 void * Thread_malloc(size_t size)
105 return snapshot_malloc(size);
108 /** @brief Snapshotting free function for use by the Thread class only */
109 void Thread_free(void *ptr)
114 void * (*volatile real_memcpy)(void * dst, const void *src, size_t n) = NULL;
115 void * (*volatile real_memmove)(void * dst, const void *src, size_t len) = NULL;
116 void (*volatile real_bzero)(void * dst, size_t len) = NULL;
117 void * (*volatile real_memset)(void * dst, int c, size_t len) = NULL;
119 void init_memory_ops()
122 real_memcpy = (void * (*)(void * dst, const void *src, size_t n)) 1;
123 real_memcpy = (void * (*)(void * dst, const void *src, size_t n))dlsym(RTLD_NEXT, "memcpy");
126 real_memmove = (void * (*)(void * dst, const void *src, size_t n)) 1;
127 real_memmove = (void * (*)(void * dst, const void *src, size_t n))dlsym(RTLD_NEXT, "memmove");
130 real_memset = (void * (*)(void * dst, int c, size_t n)) 1;
131 real_memset = (void * (*)(void * dst, int c, size_t n))dlsym(RTLD_NEXT, "memset");
134 real_bzero = (void (*)(void * dst, size_t len)) 1;
135 real_bzero = (void (*)(void * dst, size_t len))dlsym(RTLD_NEXT, "bzero");
139 void * memcpy(void * dst, const void * src, size_t n) {
140 if (model && !inside_model) {
141 //model_print("memcpy intercepted\n");
142 thread_id_t tid = thread_current_id();
143 if (((uintptr_t)src&7) == 0 && ((uintptr_t)dst&7) == 0 && (n&7) == 0) {
144 for (uint i = 0; i < (n>>3); i++) {
145 raceCheckRead64(tid, (void *)(((uint64_t *)src) + i));
146 ((volatile uint64_t *)dst)[i] = ((uint64_t *)src)[i];
147 raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
149 } else if (((uintptr_t)src&3) == 0 && ((uintptr_t)dst&3) == 0 && (n&3) == 0) {
150 for (uint i = 0; i < (n>>2); i++) {
151 raceCheckRead32(tid, (void *)(((uint32_t *)src) + i));
152 ((volatile uint32_t *)dst)[i] = ((uint32_t *)src)[i];
153 raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
155 } else if (((uintptr_t)src&1) == 0 && ((uintptr_t)dst&1) == 0 && (n&1) == 0) {
156 for (uint i = 0; i < (n>>1); i++) {
157 raceCheckRead16(tid, (void *)(((uint16_t *)src) + i));
158 ((volatile uint16_t *)dst)[i] = ((uint16_t *)src)[i];
159 raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
162 for(uint i=0;i<n;i++) {
163 raceCheckRead8(tid, (void *)(((char *)src) + i));
164 ((volatile char *)dst)[i] = ((char *)src)[i];
165 raceCheckWrite8(tid, (void *)(((char *)dst) + i));
169 if (((uintptr_t)real_memcpy) < 2) {
170 for(uint i=0;i<n;i++) {
171 ((volatile char *)dst)[i] = ((char *)src)[i];
176 return real_memcpy(dst, src, n);
181 void * memset(void *dst, int c, size_t n) {
182 if (model && !inside_model) {
183 thread_id_t tid = thread_current_id();
185 if (((uintptr_t)dst&7) == 0 && (n&7) == 0) {
186 for (uint i = 0; i < (n>>3); i++) {
187 uint16_t cs2 = cs << 8 | cs;
188 uint64_t cs3 = cs2 << 16 | cs2;
189 uint64_t cs4 = cs3 << 32 | cs3;
190 ((volatile uint64_t *)dst)[i] = cs4;
191 raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
193 } else if (((uintptr_t)dst&3) == 0 && (n&3) == 0) {
194 for (uint i = 0; i < (n>>2); i++) {
195 uint16_t cs2 = cs << 8 | cs;
196 uint32_t cs3 = cs2 << 16 | cs2;
197 ((volatile uint32_t *)dst)[i] = cs3;
198 raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
200 } else if (((uintptr_t)dst&1) == 0 && (n&1) == 0) {
201 for (uint i = 0; i < (n>>1); i++) {
202 uint16_t cs2 = cs << 8 | cs;
203 ((volatile uint16_t *)dst)[i] = cs2;
204 raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
207 for (uint i=0;i<n;i++) {
208 ((volatile char *)dst)[i] = cs;
209 raceCheckWrite8(tid, (void *)(((char *)dst) + i));
213 if (((uintptr_t)real_memset) < 2) {
214 //stuck in dynamic linker alloc cycle...
215 for(size_t s=0;s<n;s++) {
216 ((volatile char *)dst)[s] = (char) c;
220 return real_memset(dst, c, n);