C library header de-duplication

regression/cbmc-library/__builtin_llabs-01/main.c

@@ -1,9 +1,13 @@
 #include <assert.h>
-#include <stdlib.h>
+
+#include <limits.h>
+
+#ifndef __GNUC__
+long long __builtin_llabs(long long);
+#endif
 
 int main()
 {
-  __builtin_llabs();
-  assert(0);
+  assert(__builtin_llabs(LLONG_MIN + 1) == LLONG_MAX);
   return 0;
 }

regression/cbmc-library/__builtin_llabs-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/llabs-01/main.c

@@ -1,9 +1,10 @@
 #include <assert.h>
 #include <stdlib.h>
 
+#include <limits.h>
+
 int main()
 {
-  llabs();
-  assert(0);
+  assert(llabs(LLONG_MIN + 1) == LLONG_MAX);
   return 0;
 }

regression/cbmc-library/llabs-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/cprover_builtin_headers.h

@@ -84,7 +84,7 @@ int __CPROVER_isunorderedd(double f, double g);
 // absolute value
 int __CPROVER_abs(int x);
 long int __CPROVER_labs(long int x);
-long int __CPROVER_llabs(long long int x);
+long long int __CPROVER_llabs(long long int x);
 double __CPROVER_fabs(double x);
 long double __CPROVER_fabsl(long double x);
 float __CPROVER_fabsf(float x);

src/ansi-c/library/cprover.h

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module:
+Module: C library check
 
 Author: Daniel Kroening, kroening@kroening.com
 
@@ -9,170 +9,36 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_LIBRARY_CPROVER_H
 #define CPROVER_ANSI_C_LIBRARY_CPROVER_H
 
+/// \file
+/// CPROVER built-in declarations to perform library checks. This file is only
+/// used by library_check.sh.
+
+// NOLINTNEXTLINE(readability/identifiers)
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
+// NOLINTNEXTLINE(readability/identifiers)
+typedef signed long long __CPROVER_ssize_t;
+
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_new_object;
-extern _Bool __CPROVER_malloc_is_new_array;
+extern __CPROVER_bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 
 extern int __CPROVER_malloc_failure_mode;
 extern __CPROVER_size_t __CPROVER_max_malloc_size;
-extern _Bool __CPROVER_malloc_may_fail;
+extern __CPROVER_bool __CPROVER_malloc_may_fail;
 
 // malloc failure modes
 extern int __CPROVER_malloc_failure_mode_return_null;
 extern int __CPROVER_malloc_failure_mode_assert_then_assume;
 
-void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
-void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
-void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
-void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
-
-_Bool __CPROVER_is_zero_string(const void *);
-__CPROVER_size_t __CPROVER_zero_string_length(const void *);
-__CPROVER_size_t __CPROVER_buffer_size(const void *);
-__CPROVER_bool __CPROVER_r_ok();
-__CPROVER_bool __CPROVER_w_ok();
-__CPROVER_bool __CPROVER_rw_ok();
-
-#if 0
-__CPROVER_bool __CPROVER_equal();
-__CPROVER_bool __CPROVER_same_object(const void *, const void *);
-
-const unsigned __CPROVER_constant_infinity_uint;
-typedef void __CPROVER_integer;
-typedef void __CPROVER_rational;
-void __CPROVER_initialize(void);
-void __CPROVER_cover(__CPROVER_bool condition);
-#endif
-
-void __CPROVER_printf(const char *format, ...);
-void __CPROVER_input(const char *id, ...);
-void __CPROVER_output(const char *id, ...);
-
-// concurrency-related
-void __CPROVER_atomic_begin();
-void __CPROVER_atomic_end();
-void __CPROVER_fence(const char *kind, ...);
-#if 0
-__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
-unsigned long __CPROVER_next_thread_id=0;
-
-// traces
-void CBMC_trace(int lvl, const char *event, ...);
-#endif
-
-// pointers
-unsigned __CPROVER_POINTER_OBJECT(const void *p);
-signed __CPROVER_POINTER_OFFSET(const void *p);
-__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
-#if 0
-extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];
-void __CPROVER_allocated_memory(
-  __CPROVER_size_t address, __CPROVER_size_t extent);
-
-// this is ANSI-C
-extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];
-
-// this is GCC
-extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];
-extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];
-#endif
-
-// float stuff
-int __CPROVER_fpclassify(int, int, int, int, int, ...);
-__CPROVER_bool __CPROVER_isfinite(double f);
-__CPROVER_bool __CPROVER_isinf(double f);
-__CPROVER_bool __CPROVER_isnormal(double f);
-__CPROVER_bool __CPROVER_sign(double f);
-__CPROVER_bool __CPROVER_isnanf(float f);
-__CPROVER_bool __CPROVER_isnand(double f);
-__CPROVER_bool __CPROVER_isnanld(long double f);
-__CPROVER_bool __CPROVER_isfinitef(float f);
-__CPROVER_bool __CPROVER_isfinited(double f);
-__CPROVER_bool __CPROVER_isfiniteld(long double f);
-__CPROVER_bool __CPROVER_isinff(float f);
-__CPROVER_bool __CPROVER_isinfd(double f);
-__CPROVER_bool __CPROVER_isinfld(long double f);
-__CPROVER_bool __CPROVER_isnormalf(float f);
-__CPROVER_bool __CPROVER_isnormald(double f);
-__CPROVER_bool __CPROVER_isnormalld(long double f);
-__CPROVER_bool __CPROVER_signf(float f);
-__CPROVER_bool __CPROVER_signd(double f);
-__CPROVER_bool __CPROVER_signld(long double f);
-double __CPROVER_inf(void);
-float __CPROVER_inff(void);
-long double __CPROVER_infl(void);
-//extern int __CPROVER_thread_local __CPROVER_rounding_mode;
-int __CPROVER_isgreaterd(double f, double g);
-
-// absolute value
-int __CPROVER_abs(int);
-long int __CPROVER_labs(long int);
-long long int __CPROVER_llabs(long long int);
-double __CPROVER_fabs(double);
-long double __CPROVER_fabsl(long double);
-float __CPROVER_fabsf(float);
-
-// modulo and remainder
-double __CPROVER_fmod(double, double);
-float __CPROVER_fmodf(float, float);
-long double __CPROVER_fmodl(long double, long double);
-double __CPROVER_remainder(double, double);
-float __CPROVER_remainderf(float, float);
-long double __CPROVER_remainderl(long double, long double);
-
-// arrays
-//__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
-void __CPROVER_array_copy(const void *dest, const void *src);
-void __CPROVER_array_set(const void *dest, ...);
-void __CPROVER_array_replace(const void *dest, const void *src);
-
-#if 0
-// k-induction
-void __CPROVER_k_induction_hint(unsigned min, unsigned max,
-unsigned step, unsigned loop_free);
-
-// manual specification of predicates
-void __CPROVER_predicate(__CPROVER_bool predicate);
-void __CPROVER_parameter_predicates();
-void __CPROVER_return_predicates();
-#endif
-
-// pipes, write, read, close
 struct __CPROVER_pipet {
   _Bool widowed;
   char data[4];
   short next_avail;
   short next_unread;
 };
-#if 0
-extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
-// offset to make sure we don't collide with other fds
-extern const int __CPROVER_pipe_offset;
-extern unsigned __CPROVER_pipe_count;
-#endif
-
-void __CPROVER_set_must(const void *, const char *);
-void __CPROVER_set_may(const void *, const char *);
-void __CPROVER_clear_must(const void *, const char *);
-void __CPROVER_clear_may(const void *, const char *);
-void __CPROVER_cleanup(const void *, void (*)(void *));
-__CPROVER_bool __CPROVER_get_must(const void *, const char *);
-__CPROVER_bool __CPROVER_get_may(const void *, const char *);
-
-#define __CPROVER_danger_number_of_ops 1
-#define __CPROVER_danger_max_solution_size 1
-#define __CPROVER_danger_number_of_vars 1
-#define __CPROVER_danger_number_of_consts 1
 
-// detect overflow
-__CPROVER_bool __CPROVER_overflow_minus();
-__CPROVER_bool __CPROVER_overflow_mult();
-__CPROVER_bool __CPROVER_overflow_plus();
-__CPROVER_bool __CPROVER_overflow_shl();
-__CPROVER_bool __CPROVER_overflow_unary_minus();
+#include "../cprover_builtin_headers.h"
 
 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H

src/ansi-c/library/math.c

@@ -758,7 +758,7 @@ float sqrtf(float f)
     case FE_TOWARDZERO :
       return (f - lowerSquare == 0.0f) ? lower : upper; break;
     default:;
-      //assert(0);
+      return __VERIFIER_nondet_float();
     }
 
   }
@@ -835,7 +835,7 @@ double sqrt(double d)
     case FE_TOWARDZERO:
       return (d - lowerSquare == 0.0) ? lower : upper; break;
     default:;
-      //assert(0);
+      return __VERIFIER_nondet_double();
     }
 
   }
@@ -906,7 +906,7 @@ long double sqrtl(long double d)
     case FE_TOWARDZERO:
       return (d - lowerSquare == 0.0l) ? lower : upper; break;
     default:;
-      //assert(0);
+      return __VERIFIER_nondet_long_double();
     }
 
   }

src/ansi-c/library/module_dependencies.txt

@@ -1,2 +1,3 @@
+..
 ansi-c
 ansi-c/library

src/ansi-c/library/pthread_lib.c

@@ -314,6 +314,9 @@ inline void pthread_exit(void *value_ptr)
 #endif
   __CPROVER_threads_exited[__CPROVER_thread_id]=1;
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: pthread_join */

src/ansi-c/library/setjmp.c

@@ -13,6 +13,9 @@ inline void longjmp(jmp_buf env, int val)
   (void)val;
   __CPROVER_assert(0, "longjmp requires instrumentation");
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: _longjmp */
@@ -29,6 +32,9 @@ inline void _longjmp(jmp_buf env, int val)
   (void)val;
   __CPROVER_assert(0, "_longjmp requires instrumentation");
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: siglongjmp */
@@ -47,6 +53,9 @@ inline void siglongjmp(sigjmp_buf env, int val)
   (void)val;
   __CPROVER_assert(0, "siglongjmp requires instrumentation");
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 #endif

src/ansi-c/library/stdio.c

@@ -330,6 +330,7 @@ char *fgets(char *str, int size, FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+char __VERIFIER_nondet_char();
 size_t __VERIFIER_nondet_size_t();
 
 inline size_t fread(
@@ -359,8 +360,7 @@ inline size_t fread(
 
   for(size_t i=0; i<bytes; i++)
   {
-    char nondet_char;
-    ((char *)ptr)[i]=nondet_char;
+    ((char *)ptr)[i] = __VERIFIER_nondet_char();
   }
 
   return nread;

src/ansi-c/library/stdlib.c

@@ -36,6 +36,9 @@ inline void exit(int status)
 {
   (void)status;
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: _Exit */
@@ -46,6 +49,9 @@ inline void _Exit(int status)
 {
   (void)status;
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: abort */
@@ -55,6 +61,9 @@ inline void _Exit(int status)
 inline void abort(void)
 {
   __CPROVER_assume(0);
+#ifdef LIBRARY_CHECK
+  __builtin_unreachable();
+#endif
 }
 
 /* FUNCTION: calloc */

src/ansi-c/library_check.sh

@@ -7,6 +7,7 @@ for f in "$@"; do
     echo "Checking ${f}"
     cp "${f}" __libcheck.c
     perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c
+    perl -p -i -e 's/s(__builtin_unreachable)/$1/' __libcheck.c
     perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c