CBMC
stdlib.c
Go to the documentation of this file.
1 /* FUNCTION: abs */
2 
3 #ifndef __CPROVER_LIMITS_H_INCLUDED
4 # include <limits.h>
5 # define __CPROVER_LIMITS_H_INCLUDED
6 #endif
7 
8 #undef abs
9 
10 int abs(int i)
11 {
12  // C99 Section 7.20.6.1:
13  // "If the result cannot be represented, the behavior is undefined."
14  __CPROVER_precondition(i != INT_MIN, "argument to abs must not be INT_MIN");
15  return __CPROVER_abs(i);
16 }
17 
18 /* FUNCTION: labs */
19 
20 #ifndef __CPROVER_LIMITS_H_INCLUDED
21 # include <limits.h>
22 # define __CPROVER_LIMITS_H_INCLUDED
23 #endif
24 
25 #undef labs
26 
27 long int labs(long int i)
28 {
29  // C99 Section 7.20.6.1:
30  // "If the result cannot be represented, the behavior is undefined."
32  i != LONG_MIN, "argument to labs must not be LONG_MIN");
33  return __CPROVER_labs(i);
34 }
35 
36 /* FUNCTION: llabs */
37 
38 #ifndef __CPROVER_LIMITS_H_INCLUDED
39 # include <limits.h>
40 # define __CPROVER_LIMITS_H_INCLUDED
41 #endif
42 
43 #undef llabs
44 
45 long long int llabs(long long int i)
46 {
47  // C99 Section 7.20.6.1:
48  // "If the result cannot be represented, the behavior is undefined."
50  i != LLONG_MIN, "argument to llabs must not be LLONG_MIN");
51  return __CPROVER_llabs(i);
52 }
53 
54 /* FUNCTION: imaxabs */
55 
56 #ifndef __CPROVER_INTTYPES_H_INCLUDED
57 # include <inttypes.h>
58 # define __CPROVER_INTTYPES_H_INCLUDED
59 #endif
60 
61 #ifndef __CPROVER_LIMITS_H_INCLUDED
62 # include <limits.h>
63 # define __CPROVER_LIMITS_H_INCLUDED
64 #endif
65 
66 #undef imaxabs
67 
68 intmax_t __CPROVER_imaxabs(intmax_t);
69 
70 intmax_t imaxabs(intmax_t i)
71 {
73  i != INTMAX_MIN, "argument to imaxabs must not be INTMAX_MIN");
74  return __CPROVER_imaxabs(i);
75 }
76 
77 /* FUNCTION: __builtin_abs */
78 
79 int __builtin_abs(int i)
80 {
81  return __CPROVER_abs(i);
82 }
83 
84 /* FUNCTION: __builtin_labs */
85 
86 long int __builtin_labs(long int i)
87 {
88  return __CPROVER_labs(i);
89 }
90 
91 /* FUNCTION: __builtin_llabs */
92 
93 long long int __builtin_llabs(long long int i)
94 {
95  return __CPROVER_llabs(i);
96 }
97 
98 /* FUNCTION: exit */
99 
100 #undef exit
101 
102 void exit(int status)
103 {
104  (void)status;
105  __CPROVER_assume(0);
106 #ifdef LIBRARY_CHECK
108 #endif
109 }
110 
111 /* FUNCTION: _Exit */
112 
113 #undef _Exit
114 
115 void _Exit(int status)
116 {
117  (void)status;
118  __CPROVER_assume(0);
119 #ifdef LIBRARY_CHECK
121 #endif
122 }
123 
124 /* FUNCTION: abort */
125 
126 #undef abort
127 
128 void abort(void)
129 {
130  __CPROVER_assume(0);
131 #ifdef LIBRARY_CHECK
133 #endif
134 }
135 
136 /* FUNCTION: calloc */
137 
138 #undef calloc
139 
140 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
141 #ifndef __GNUC__
143 #endif
144 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
145 
146 void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
147 {
148 __CPROVER_HIDE:;
149  __CPROVER_size_t alloc_size;
150  if(__builtin_mul_overflow(nmemb, size, &alloc_size))
151  return (void *)0;
152 
154  {
155  __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
156  if(
157  alloc_size > __CPROVER_max_malloc_size ||
158  (__CPROVER_malloc_may_fail && should_malloc_fail))
159  {
160  return (void *)0;
161  }
162  }
163  else if(
166  {
168  alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
170 
171  __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
173  !__CPROVER_malloc_may_fail || !should_malloc_fail,
174  "max allocation may fail");
175  __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
176  }
177 
178  void *malloc_res;
179  // realistically, calloc may return NULL,
180  // and __CPROVER_allocate doesn't, but no one cares
181  malloc_res = __CPROVER_allocate(alloc_size, 1);
182 
183  // record the object size for non-determistic bounds checking
184  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
186  record_malloc ? 0 : __CPROVER_malloc_is_new_array;
187 
188  // detect memory leaks
189  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
190  __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
191 
192 #ifdef __CPROVER_STRING_ABSTRACTION
193  __CPROVER_assume(__CPROVER_buffer_size(malloc_res) == alloc_size);
194  __CPROVER_is_zero_string(malloc_res) = 1;
195  __CPROVER_zero_string_length(malloc_res) = 0;
196 #endif
197 
198  return malloc_res;
199 }
200 
201 /* FUNCTION: malloc */
202 
203 #undef malloc
204 
205 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
206 #ifndef LIBRARY_CHECK
207 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
208 #endif
209 
210 // malloc is marked "inline" for the benefit of goto-analyzer. Really,
211 // goto-analyzer should take care of inlining as needed.
212 inline void *malloc(__CPROVER_size_t malloc_size)
213 {
214 // realistically, malloc may return NULL,
215 // but we only do so if `--malloc-may-fail` is set
216 __CPROVER_HIDE:;
217 
219  {
220  __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
221  if(
222  malloc_size > __CPROVER_max_malloc_size ||
223  (__CPROVER_malloc_may_fail && should_malloc_fail))
224  {
225  return (void *)0;
226  }
227  }
228  else if(
231  {
233  malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
235 
236  __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
238  !__CPROVER_malloc_may_fail || !should_malloc_fail,
239  "max allocation may fail");
240  __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
241  }
242 
243  void *malloc_res;
244  malloc_res = __CPROVER_allocate(malloc_size, 0);
245 
246  // record the object size for non-determistic bounds checking
247  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
249  record_malloc ? 0 : __CPROVER_malloc_is_new_array;
250 
251  // detect memory leaks
252  __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
253  __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
254 
255 #ifdef __CPROVER_STRING_ABSTRACTION
256  __CPROVER_assume(__CPROVER_buffer_size(malloc_res) == malloc_size);
257 #endif
258 
259  return malloc_res;
260 }
261 
262 /* FUNCTION: __builtin_alloca */
263 
264 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
265 const void *__CPROVER_alloca_object = 0;
266 #ifndef LIBRARY_CHECK
267 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
268 #endif
269 
270 void *__builtin_alloca(__CPROVER_size_t alloca_size)
271 {
272  __CPROVER_HIDE:;
273  void *res;
274  res = __CPROVER_allocate(alloca_size, 0);
275 
276  // record the object size for non-determistic bounds checking
277  __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
279 
280  // record alloca to detect invalid free
281  __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool();
282  __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object;
283 
284 #ifdef __CPROVER_STRING_ABSTRACTION
285  __CPROVER_assume(__CPROVER_buffer_size(res) == alloca_size);
286 #endif
287 
288  return res;
289 }
290 
291 /* FUNCTION: alloca */
292 
293 #undef alloca
294 
295 void *__builtin_alloca(__CPROVER_size_t alloca_size);
296 
297 void *alloca(__CPROVER_size_t alloca_size)
298 {
299 __CPROVER_HIDE:;
300  return __builtin_alloca(alloca_size);
301 }
302 
303 /* FUNCTION: free */
304 
305 #undef free
306 
307 void __CPROVER_deallocate(void *);
308 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
309 #ifndef LIBRARY_CHECK
310 const void *__CPROVER_alloca_object = 0;
311 #endif
312 const void *__CPROVER_new_object = 0;
313 #ifndef LIBRARY_CHECK
314 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
315 #endif
316 
317 void free(void *ptr)
318 {
319  __CPROVER_HIDE:;
320  // If ptr is NULL, no operation is performed.
322  ptr == 0 || __CPROVER_r_ok(ptr, 0),
323  "free argument must be NULL or valid pointer");
325  "free argument must be dynamic object");
327  "free argument has offset zero");
328 
329  // catch double free
331  "double free");
332 
333  // catch people who try to use free(...) for stuff
334  // allocated with new[]
337  "free called for new[] object");
338 
339  // catch people who try to use free(...) with alloca
341  ptr == 0 || __CPROVER_alloca_object != ptr,
342  "free called for stack-allocated object");
343 
344  if(ptr!=0)
345  {
347 
348  // detect memory leaks
349  if(__CPROVER_memory_leak==ptr)
351  }
352 }
353 
354 /* FUNCTION: strtol */
355 
356 #ifndef __CPROVER_ERRNO_H_INCLUDED
357 #include <errno.h>
358 #define __CPROVER_ERRNO_H_INCLUDED
359 #endif
360 
361 #ifndef __CPROVER_LIMITS_H_INCLUDED
362 #include <limits.h>
363 #define __CPROVER_LIMITS_H_INCLUDED
364 #endif
365 
366 #undef strtol
367 #undef isdigit
368 #undef isspace
369 
370 int isspace(int);
371 int isdigit(int);
372 
373 #ifndef __GNUC__
375 _Bool __builtin_mul_overflow();
376 #endif
377 
378 long strtol(const char *nptr, char **endptr, int base)
379 {
380  __CPROVER_HIDE:;
381  #ifdef __CPROVER_STRING_ABSTRACTION
383  "zero-termination of argument of strtol");
384  #endif
385 
386  if(base==1 || base<0 || base>36)
387  {
388  errno=EINVAL;
389  return 0;
390  }
391 
392  long res=0;
393  _Bool in_number=0;
394  char sign=0;
395 
396  // 32 chars is an arbitrarily chosen limit
397  int i=0;
398  for( ; i<31; ++i)
399  {
400  char ch=nptr[i];
401  char sub=0;
402  if(ch==0)
403  break;
404  else if((base==0 || base==16) && !in_number &&
405  ch=='0' && (nptr[i+1]=='x' || nptr[i+1]=='X'))
406  {
407  base=16;
408  in_number=1;
409  ++i;
410  continue;
411  }
412  else if(base==0 && !in_number && ch=='0')
413  {
414  base=8;
415  in_number=1;
416  continue;
417  }
418  else if(!in_number && !sign && isspace(ch))
419  continue;
420  else if(!in_number && !sign && (ch=='-' || ch=='+'))
421  {
422  sign=ch;
423  continue;
424  }
425  else if(base>10 && ch>='a' && ch-'a'<base-10)
426  sub='a'-10;
427  else if(base>10 && ch>='A' && ch-'A'<base-10)
428  sub='A'-10;
429  else if(isdigit(ch))
430  {
431  sub='0';
432  base=base==0 ? 10 : base;
433  }
434  else
435  break;
436 
437  in_number=1;
438  _Bool overflow = __builtin_mul_overflow(res, (long)base, &res);
439  if(overflow || __builtin_add_overflow(res, (long)(ch - sub), &res))
440  {
441  errno=ERANGE;
442  if(sign=='-')
443  return LONG_MIN;
444  else
445  return LONG_MAX;
446  }
447  }
448 
449  if(endptr!=0)
450  *endptr=(char*)nptr+i;
451 
452  if(sign=='-')
453  res*=-1;
454 
455  return res;
456 }
457 
458 /* FUNCTION: atoi */
459 
460 #undef atoi
461 #undef strtol
462 
463 long strtol(const char *nptr, char **endptr, int base);
464 
465 int atoi(const char *nptr)
466 {
467  __CPROVER_HIDE:;
468  return (int)strtol(nptr, (char **)0, 10);
469 }
470 
471 /* FUNCTION: atol */
472 
473 #undef atol
474 #undef strtol
475 
476 long strtol(const char *nptr, char **endptr, int base);
477 
478 long atol(const char *nptr)
479 {
480  __CPROVER_HIDE:;
481  return strtol(nptr, (char **)0, 10);
482 }
483 
484 /* FUNCTION: getenv */
485 
486 #undef getenv
487 
488 #ifndef __CPROVER_STDDEF_H_INCLUDED
489 # include <stddef.h>
490 # define __CPROVER_STDDEF_H_INCLUDED
491 #endif
492 
493 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
495 
496 char *getenv(const char *name)
497 {
498  __CPROVER_HIDE:;
499 
500  (void)*name;
501  #ifdef __CPROVER_STRING_ABSTRACTION
503  "zero-termination of argument of getenv");
504  #endif
505 
506 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
507  __CPROVER_event("invalidate_pointer", "getenv_result");
508  char *getenv_result;
509  __CPROVER_set_must(getenv_result, "getenv_result");
510  return getenv_result;
511 
512 #else
513 
514  __CPROVER_bool found=__VERIFIER_nondet___CPROVER_bool();
515  if(!found) return 0;
516 
517  ptrdiff_t buf_size = __VERIFIER_nondet_ptrdiff_t();
518 
519  // It's reasonable to assume this won't exceed the signed
520  // range in practice, but in principle, this could exceed
521  // the range.
522 
523  __CPROVER_assume(buf_size >= 1);
524  char *buffer = (char *)__CPROVER_allocate(buf_size * sizeof(char), 0);
525  buffer[buf_size-1]=0;
526 
527 # ifdef __CPROVER_STRING_ABSTRACTION
528  __CPROVER_assume(__CPROVER_buffer_size(buffer) == buf_size);
529  __CPROVER_is_zero_string(buffer) = 1;
530  __CPROVER_zero_string_length(buffer) = buf_size - 1;
531 # endif
532 
533  return buffer;
534 #endif
535 }
536 
537 /* FUNCTION: realloc */
538 
539 void *malloc(__CPROVER_size_t malloc_size);
540 void free(void *ptr);
541 
542 void *realloc(void *ptr, __CPROVER_size_t malloc_size)
543 {
544  __CPROVER_HIDE:;
545 
547  "realloc argument is dynamic object");
548 
549  // if ptr is NULL, this behaves like malloc
550  if(ptr==0)
551  return malloc(malloc_size);
552 
553  // if malloc-size is 0, allocate new minimum sized object
554  // and free original
555  if(malloc_size==0)
556  {
557  free(ptr);
558  return malloc(0);
559  }
560 
561  // this shouldn't move if the new size isn't bigger
562  void *res;
563  res=malloc(malloc_size);
564  if(res != (void *)0)
565  {
566  __CPROVER_array_copy(res, ptr);
567  free(ptr);
568  }
569 
570  return res;
571 }
572 
573 /* FUNCTION: valloc */
574 
575 void *malloc(__CPROVER_size_t malloc_size);
576 
577 void *valloc(__CPROVER_size_t malloc_size)
578 {
579  // The allocated memory is aligned on a page
580  // boundary, which we don't model.
581 
582  __CPROVER_HIDE:;
583  return malloc(malloc_size);
584 }
585 
586 /* FUNCTION: posix_memalign */
587 
588 #ifndef __CPROVER_ERRNO_H_INCLUDED
589 #include <errno.h>
590 #define __CPROVER_ERRNO_H_INCLUDED
591 #endif
592 
593 #undef posix_memalign
594 
595 void *malloc(__CPROVER_size_t malloc_size);
597  void **ptr,
598  __CPROVER_size_t alignment,
599  __CPROVER_size_t size)
600 {
601 __CPROVER_HIDE:;
602 
603  __CPROVER_size_t multiplier = alignment / sizeof(void *);
604  // Modeling the posix_memalign checks on alignment.
605  if(
606  alignment % sizeof(void *) != 0 || ((multiplier) & (multiplier - 1)) != 0 ||
607  alignment == 0)
608  {
609  return EINVAL;
610  }
611  // The address of the allocated memory is supposed to be aligned with
612  // alignment. As cbmc doesn't model address alignment,
613  // assuming MALLOC_ALIGNMENT = MAX_INT_VALUE seems fair.
614  // As _mid_memalign simplifies for alignment <= MALLOC_ALIGNMENT
615  // to a malloc call, it should be sound, if we do it too.
616 
617  void *tmp = malloc(size);
618  if(tmp != (void *)0)
619  {
620  *ptr = tmp;
621  return 0;
622  }
623  return ENOMEM;
624 }
625 
626 /* FUNCTION: random */
627 
629 
630 long random(void)
631 {
632  // We return a non-deterministic value instead of a random one.
633  __CPROVER_HIDE:;
634  long result=__VERIFIER_nondet_long();
635  __CPROVER_assume(result>=0 && result<=2147483647);
636  return result;
637 }
638 
639 /* FUNCTION: rand */
640 
642 
643 int rand(void)
644 {
645 __CPROVER_HIDE:;
646  // We return a non-deterministic value instead of a random one.
647  int result = __VERIFIER_nondet_int();
648  __CPROVER_assume(result >= 0);
649  return result;
650 }
651 
652 /* FUNCTION: rand_r */
653 
654 int __VERIFIER_nondet_int(void);
655 
656 int rand_r(unsigned int *seed)
657 {
658 __CPROVER_HIDE:;
659  // We return a non-deterministic value instead of a random one.
660  (void)*seed;
661  int result = __VERIFIER_nondet_int();
662  __CPROVER_assume(result >= 0);
663  return result;
664 }
665 
666 /* FUNCTION: __CPROVER_deallocate */
667 
668 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
669 
670 void __CPROVER_deallocate(void *ptr)
671 {
673  __CPROVER_deallocated = ptr;
674 }
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_thread_local __CPROVER_size_t __CPROVER_max_malloc_size
int __CPROVER_malloc_failure_mode
int __CPROVER_malloc_failure_mode_return_null
const void * __CPROVER_deallocated
const void * __CPROVER_memory_leak
__CPROVER_bool __CPROVER_malloc_may_fail
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_bool __CPROVER_r_ok(const void *,...)
__CPROVER_size_t __CPROVER_buffer_size(const void *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
long int __CPROVER_labs(long int x)
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
int __CPROVER_abs(int x)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
long long int __CPROVER_llabs(long long int x)
_Bool __CPROVER_is_zero_string(const void *)
void __CPROVER_set_must(const void *, const char *)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
void __CPROVER_assume(__CPROVER_bool assumption)
void __CPROVER_array_copy(const void *dest, const void *src)
void __builtin_unreachable(void)
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
int __VERIFIER_nondet_int(void)
void * realloc(void *ptr, __CPROVER_size_t malloc_size)
Definition: stdlib.c:542
long random(void)
Definition: stdlib.c:630
long atol(const char *nptr)
Definition: stdlib.c:478
_Bool __builtin_mul_overflow()
long int labs(long int i)
Definition: stdlib.c:27
int posix_memalign(void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size)
Definition: stdlib.c:596
long strtol(const char *nptr, char **endptr, int base)
Definition: stdlib.c:378
int rand_r(unsigned int *seed)
Definition: stdlib.c:656
intmax_t __CPROVER_imaxabs(intmax_t)
void * calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
Definition: stdlib.c:146
void * malloc(__CPROVER_size_t malloc_size)
Definition: stdlib.c:212
void exit(int status)
Definition: stdlib.c:102
long int __builtin_labs(long int i)
Definition: stdlib.c:86
void __CPROVER_deallocate(void *)
Definition: stdlib.c:670
const void * __CPROVER_new_object
Definition: stdlib.c:312
int isdigit(int)
Definition: ctype.c:24
void * alloca(__CPROVER_size_t alloca_size)
Definition: stdlib.c:297
void _Exit(int status)
Definition: stdlib.c:115
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
void abort(void)
Definition: stdlib.c:128
intmax_t imaxabs(intmax_t i)
Definition: stdlib.c:70
int isspace(int)
Definition: ctype.c:80
_Bool __builtin_add_overflow()
long long int llabs(long long int i)
Definition: stdlib.c:45
int __builtin_abs(int i)
Definition: stdlib.c:79
const void * __CPROVER_alloca_object
Definition: stdlib.c:265
long long int __builtin_llabs(long long int i)
Definition: stdlib.c:93
__CPROVER_bool __CPROVER_malloc_is_new_array
Definition: stdlib.c:144
char * getenv(const char *name)
Definition: stdlib.c:496
ptrdiff_t __VERIFIER_nondet_ptrdiff_t(void)
int atoi(const char *nptr)
Definition: stdlib.c:465
int rand(void)
Definition: stdlib.c:643
int abs(int i)
Definition: stdlib.c:10
void * __builtin_alloca(__CPROVER_size_t alloca_size)
Definition: stdlib.c:270
void free(void *ptr)
Definition: stdlib.c:317
long __VERIFIER_nondet_long(void)
void * valloc(__CPROVER_size_t malloc_size)
Definition: stdlib.c:577