mymemory.cc

   1
   2 #include <stdlib.h>
   3 #include <stdio.h>
   4 #include <dlfcn.h>
   5 #include <unistd.h>
   6 #include <string.h>
   7 #include <new>
   8
   9 #include "mymemory.h"
  10 #include "snapshot.h"
  11 #include "common.h"
  12 #include "threads-model.h"
  13 #include "model.h"
  14 #include "datarace.h"
  15
  16 #define REQUESTS_BEFORE_ALLOC 1024
  17
  18 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
  19 int nextRequest = 0;
  20 int howManyFreed = 0;
  21 mspace sStaticSpace = NULL;
  22
  23 /** Non-snapshotting calloc for our use. */
  24 void *model_calloc(size_t count, size_t size)
  25 {
  26         return mspace_calloc(sStaticSpace, count, size);
  27 }
  28
  29 /** Non-snapshotting malloc for our use. */
  30 void *model_malloc(size_t size)
  31 {
  32         return mspace_malloc(sStaticSpace, size);
  33 }
  34
  35 /** Non-snapshotting malloc for our use. */
  36 void *model_realloc(void *ptr, size_t size)
  37 {
  38         return mspace_realloc(sStaticSpace, ptr, size);
  39 }
  40
  41 /** @brief Snapshotting malloc, for use by model-checker (not user progs) */
  42 void * snapshot_malloc(size_t size)
  43 {
  44         void *tmp = mspace_malloc(model_snapshot_space, size);
  45         ASSERT(tmp);
  46         return tmp;
  47 }
  48
  49 /** @brief Snapshotting calloc, for use by model-checker (not user progs) */
  50 void * snapshot_calloc(size_t count, size_t size)
  51 {
  52         void *tmp = mspace_calloc(model_snapshot_space, count, size);
  53         ASSERT(tmp);
  54         return tmp;
  55 }
  56
  57 /** @brief Snapshotting realloc, for use by model-checker (not user progs) */
  58 void *snapshot_realloc(void *ptr, size_t size)
  59 {
  60         void *tmp = mspace_realloc(model_snapshot_space, ptr, size);
  61         ASSERT(tmp);
  62         return tmp;
  63 }
  64
  65 /** @brief Snapshotting free, for use by model-checker (not user progs) */
  66 void snapshot_free(void *ptr)
  67 {
  68         mspace_free(model_snapshot_space, ptr);
  69 }
  70
  71 /** Non-snapshotting free for our use. */
  72 void model_free(void *ptr)
  73 {
  74         mspace_free(sStaticSpace, ptr);
  75 }
  76
  77 /** Bootstrap allocation. Problem is that the dynamic linker calls require
  78  *  calloc to work and calloc requires the dynamic linker to work. */
  79
  80 #define BOOTSTRAPBYTES 131072
  81 char bootstrapmemory[BOOTSTRAPBYTES];
  82 size_t offset = 0;
  83
  84 void * HandleEarlyAllocationRequest(size_t sz)
  85 {
  86         /* Align to 8 byte boundary */
  87         sz = (sz + 7) & ~7;
  88
  89         if (sz > (BOOTSTRAPBYTES-offset)) {
  90                 model_print("OUT OF BOOTSTRAP MEMORY.  Increase the size of BOOTSTRAPBYTES in mymemory.cc\n");
  91                 exit(EXIT_FAILURE);
  92         }
  93
  94         void *pointer = (void *)&bootstrapmemory[offset];
  95         offset += sz;
  96         return pointer;
  97 }
  98
  99 /** @brief Global mspace reference for the model-checker's snapshotting heap */
 100 mspace model_snapshot_space = NULL;
 101
 102 /** @brief Snapshotting allocation function for use by the Thread class only */
 103 void * Thread_malloc(size_t size)
 104 {
 105         return snapshot_malloc(size);
 106 }
 107
 108 /** @brief Snapshotting free function for use by the Thread class only */
 109 void Thread_free(void *ptr)
 110 {
 111         snapshot_free(ptr);
 112 }
 113
 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;
 118
 119 void init_memory_ops()
 120 {
 121         if (!real_memcpy) {
 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");
 124         }
 125         if (!real_memmove) {
 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");
 128         }
 129         if (!real_memset) {
 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");
 132         }
 133         if (!real_bzero) {
 134                 real_bzero = (void (*)(void * dst, size_t len)) 1;
 135                 real_bzero = (void (*)(void * dst, size_t len))dlsym(RTLD_NEXT, "bzero");
 136         }
 137 }
 138
 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));
 148                         }
 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));
 154                         }
 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));
 160                         }
 161                 } else {
 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));
 166                         }
 167                 }
 168         } else {
 169                 if (((uintptr_t)real_memcpy) < 2) {
 170                         for(uint i=0;i<n;i++) {
 171                                 ((volatile char *)dst)[i] = ((char *)src)[i];
 172                         }
 173                         return dst;
 174                 }
 175
 176                 return real_memcpy(dst, src, n);
 177         }
 178         return dst;
 179 }
 180
 181 void * memmove(void * dst, const void * src, size_t n) {
 182         if (model && !inside_model) {
 183                 thread_id_t tid = thread_current_id();
 184                 if (((uintptr_t)src&7) == 0 && ((uintptr_t)dst&7) == 0 && (n&7) == 0) {
 185                         if (((uintptr_t)dst) < ((uintptr_t)src))
 186                                 for (uint i = 0; i < (n>>3); i++) {
 187                                         raceCheckRead64(tid, (void *)(((uint64_t *)src) + i));
 188                                         ((volatile uint64_t *)dst)[i] = ((uint64_t *)src)[i];
 189                                         raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
 190                                 }
 191                         else
 192                                 for (uint i = (n>>3); i != 0;) {
 193                                         i--;
 194                                         raceCheckRead64(tid, (void *)(((uint64_t *)src) + i));
 195                                         ((volatile uint64_t *)dst)[i] = ((uint64_t *)src)[i];
 196                                         raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
 197                                 }
 198                 } else if (((uintptr_t)src&3) == 0 && ((uintptr_t)dst&3) == 0 && (n&3) == 0) {
 199                         if (((uintptr_t)dst) < ((uintptr_t)src))
 200                                 for (uint i = 0; i < (n>>2); i++) {
 201                                         raceCheckRead32(tid, (void *)(((uint32_t *)src) + i));
 202                                         ((volatile uint32_t *)dst)[i] = ((uint32_t *)src)[i];
 203                                         raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
 204                                 }
 205                         else
 206                                 for (uint i = (n>>2); i != 0;) {
 207                                         i--;
 208                                         raceCheckRead32(tid, (void *)(((uint32_t *)src) + i));
 209                                         ((volatile uint32_t *)dst)[i] = ((uint32_t *)src)[i];
 210                                         raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
 211                                 }
 212                 } else if (((uintptr_t)src&1) == 0 && ((uintptr_t)dst&1) == 0 && (n&1) == 0) {
 213                         if (((uintptr_t)dst) < ((uintptr_t)src))
 214                                 for (uint i = 0; i < (n>>1); i++) {
 215                                         raceCheckRead16(tid, (void *)(((uint16_t *)src) + i));
 216                                         ((volatile uint16_t *)dst)[i] = ((uint16_t *)src)[i];
 217                                         raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
 218                                 }
 219                         else
 220                                 for (uint i = (n>>1); i != 0;) {
 221                                         i--;
 222                                         raceCheckRead16(tid, (void *)(((uint16_t *)src) + i));
 223                                         ((volatile uint16_t *)dst)[i] = ((uint16_t *)src)[i];
 224                                         raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
 225                                 }
 226                 } else {
 227                         if (((uintptr_t)dst) < ((uintptr_t)src))
 228                                 for(uint i = 0; i < n; i++) {
 229                                         raceCheckRead8(tid, (void *)(((char *)src) + i));
 230                                         ((volatile char *)dst)[i] = ((char *)src)[i];
 231                                         raceCheckWrite8(tid, (void *)(((char *)dst) + i));
 232                                 }
 233                         else
 234                                 for(uint i = n; i != 0;) {
 235                                         i--;
 236                                         raceCheckRead8(tid, (void *)(((char *)src) + i));
 237                                         ((volatile char *)dst)[i] = ((char *)src)[i];
 238                                         raceCheckWrite8(tid, (void *)(((char *)dst) + i));
 239                                 }
 240                 }
 241         } else {
 242                 if (((uintptr_t)real_memmove) < 2) {
 243                         if (((uintptr_t)dst) < ((uintptr_t)src))
 244                                 for(uint i=0;i<n;i++) {
 245                                         ((volatile char *)dst)[i] = ((char *)src)[i];
 246                                 }
 247                         else
 248                                 for(uint i=n;i!=0; ) {
 249                                         i--;
 250                                         ((volatile char *)dst)[i] = ((char *)src)[i];
 251                                 }
 252                         return dst;
 253                 }
 254         return real_memmove(dst, src, n);
 255         }
 256         return dst;
 257 }
 258
 259 void * memset(void *dst, int c, size_t n) {
 260         if (model && !inside_model) {
 261                 thread_id_t tid = thread_current_id();
 262                 uint8_t cs = c&0xff;
 263                 if (((uintptr_t)dst&7) == 0 && (n&7) == 0) {
 264                         for (uint i = 0; i < (n>>3); i++) {
 265                     uint16_t cs2 = cs << 8 | cs;
 266                     uint64_t cs3 = cs2 << 16 | cs2;
 267                     uint64_t cs4 = cs3 << 32 | cs3;
 268                                 ((volatile uint64_t *)dst)[i] = cs4;
 269                                 raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
 270                         }
 271                 } else if (((uintptr_t)dst&3) == 0 && (n&3) == 0) {
 272                         for (uint i = 0; i < (n>>2); i++) {
 273                     uint16_t cs2 = cs << 8 | cs;
 274                     uint32_t cs3 = cs2 << 16 | cs2;
 275                                 ((volatile uint32_t *)dst)[i] = cs3;
 276                                 raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
 277                         }
 278                 } else if (((uintptr_t)dst&1) == 0 && (n&1) == 0) {
 279                         for (uint i = 0; i < (n>>1); i++) {
 280                     uint16_t cs2 = cs << 8 | cs;
 281                                 ((volatile uint16_t *)dst)[i] = cs2;
 282                                 raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
 283                         }
 284                 } else {
 285                         for (uint i=0;i<n;i++) {
 286                                 ((volatile char *)dst)[i] = cs;
 287                                 raceCheckWrite8(tid, (void *)(((char *)dst) + i));
 288                         }
 289                 }
 290         } else {
 291                 if (((uintptr_t)real_memset) < 2) {
 292                         //stuck in dynamic linker alloc cycle...
 293                         for(size_t s=0;s<n;s++) {
 294                                 ((volatile char *)dst)[s] = (char) c;
 295                         }
 296                         return dst;
 297                 }
 298                 return real_memset(dst, c, n);
 299         }
 300         return dst;
 301 }
 302
 303 void bzero(void *dst, size_t n) {
 304         if (model && !inside_model) {
 305                 thread_id_t tid = thread_current_id();
 306                 if (((uintptr_t)dst&7) == 0 && (n&7) == 0) {
 307                         for (uint i = 0; i < (n>>3); i++) {
 308                                 ((volatile uint64_t *)dst)[i] = 0;
 309                                 raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
 310                         }
 311                 } else if (((uintptr_t)dst&3) == 0 && (n&3) == 0) {
 312                         for (uint i = 0; i < (n>>2); i++) {
 313                                 ((volatile uint32_t *)dst)[i] = 0;
 314                                 raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
 315                         }
 316                 } else if (((uintptr_t)dst&1) == 0 && (n&1) == 0) {
 317                         for (uint i = 0; i < (n>>1); i++) {
 318                                 ((volatile uint16_t *)dst)[i] = 0;
 319                                 raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
 320                         }
 321                 } else {
 322                         for (uint i=0;i<n;i++) {
 323                                 ((volatile char *)dst)[i] = 0;
 324                                 raceCheckWrite8(tid, (void *)(((char *)dst) + i));
 325                         }
 326                 }
 327         } else {
 328                 if (((uintptr_t)real_bzero) < 2) {
 329                         for(size_t s=0;s<n;s++) {
 330                                 ((volatile char *)dst)[s] = 0;
 331                         }
 332                         return;
 333                 }
 334                 real_bzero(dst, n);
 335         }
 336 }