Allocation size computation in calloc must not overflow

calloc guarantees that the requested number of bytes is allocated, or
else NULL is returned. Since an overflowing multiplication would imply
that the requested size can never be allocated, NULL must be returned
(and we should not report an arithmetic overflow error).

Fixes: #4606

Author: tautschnig

regression/cbmc-library/calloc-02/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  char *p = calloc(-1, -1);
+  if(p)
+    assert(p[0] == 0);
+}

regression/cbmc-library/calloc-02/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unsigned-overflow-check --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/stdlib.c

@@ -65,11 +65,20 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
 inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
+__CPROVER_HIDE:;
+#pragma CPROVER check push
+#pragma CPROVER check disable "unsigned-overflow"
+  if(__CPROVER_overflow_mult(nmemb, size))
+    return (void *)0;
+  // This is now safe; still do it within the scope of the pragma to avoid an
+  // unnecessary assertion to be generated.
+  __CPROVER_size_t alloc_size = nmemb * size;
+#pragma CPROVER check pop
+
+  void *malloc_res;
   // realistically, calloc may return NULL,
   // and __CPROVER_allocate doesn't, but no one cares
-  __CPROVER_HIDE:;
-  void *malloc_res;
-  malloc_res = __CPROVER_allocate(nmemb * size, 1);
+  malloc_res = __CPROVER_allocate(alloc_size, 1);
 
   // make sure it's not recorded as deallocated
   __CPROVER_deallocated =
@@ -79,7 +88,7 @@ inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_object =
     record_malloc ? malloc_res : __CPROVER_malloc_object;
-  __CPROVER_malloc_size = record_malloc ? nmemb * size : __CPROVER_malloc_size;
+  __CPROVER_malloc_size = record_malloc ? alloc_size : __CPROVER_malloc_size;
   __CPROVER_malloc_is_new_array =
     record_malloc ? 0 : __CPROVER_malloc_is_new_array;
 

src/ansi-c/library_check.sh

@@ -11,7 +11,8 @@ for f in "$@"; do
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
     "$CC" -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
-    "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
+    "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
+      -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c
     [ "${ec}" -eq 0 ] || exit "${ec}"