Skip to content

Commit d0c403a

Browse files
tautschnigtautschnig
authored
Merge pull request #6490 from tautschnig/c-library-cleanup
C library header de-duplication
2 parents fdc7ba5 + 5295845 commit d0c403a

File tree

13 files changed

+55
-161
lines changed

13 files changed

+55
-161
lines changed

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

+7-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
11
#include <assert.h>
2-
#include <stdlib.h>
2+
3+
#include <limits.h>
4+
5+
#ifndef __GNUC__
6+
long long __builtin_llabs(long long);
7+
#endif
38

49
int main()
510
{
6-
__builtin_llabs();
7-
assert(0);
11+
assert(__builtin_llabs(LLONG_MIN + 1) == LLONG_MAX);
812
return 0;
913
}

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
KNOWNBUG
1+
CORE
22
main.c
3-
--pointer-check --bounds-check
3+
--pointer-check --bounds-check --signed-overflow-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

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

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
#include <assert.h>
22
#include <stdlib.h>
33

4+
#include <limits.h>
5+
46
int main()
57
{
6-
llabs();
7-
assert(0);
8+
assert(llabs(LLONG_MIN + 1) == LLONG_MAX);
89
return 0;
910
}

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
KNOWNBUG
1+
CORE
22
main.c
3-
--pointer-check --bounds-check
3+
--pointer-check --bounds-check --signed-overflow-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎src/ansi-c/cprover_builtin_headers.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ int __CPROVER_isunorderedd(double f, double g);
8484
// absolute value
8585
int __CPROVER_abs(int x);
8686
long int __CPROVER_labs(long int x);
87-
long int __CPROVER_llabs(long long int x);
87+
long long int __CPROVER_llabs(long long int x);
8888
double __CPROVER_fabs(double x);
8989
long double __CPROVER_fabsl(long double x);
9090
float __CPROVER_fabsf(float x);

‎src/ansi-c/library/cprover.h

+12-146
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
/*******************************************************************\
22
3-
Module:
3+
Module: C library check
44
55
Author: Daniel Kroening, [email protected]
66
@@ -9,170 +9,36 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_ANSI_C_LIBRARY_CPROVER_H
1010
#define CPROVER_ANSI_C_LIBRARY_CPROVER_H
1111

12+
/// \file
13+
/// CPROVER built-in declarations to perform library checks. This file is only
14+
/// used by library_check.sh.
15+
16+
// NOLINTNEXTLINE(readability/identifiers)
1217
typedef __typeof__(sizeof(int)) __CPROVER_size_t;
18+
// NOLINTNEXTLINE(readability/identifiers)
19+
typedef signed long long __CPROVER_ssize_t;
20+
1321
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
1422
extern const void *__CPROVER_deallocated;
1523
extern const void *__CPROVER_new_object;
16-
extern _Bool __CPROVER_malloc_is_new_array;
24+
extern __CPROVER_bool __CPROVER_malloc_is_new_array;
1725
extern const void *__CPROVER_memory_leak;
1826

1927
extern int __CPROVER_malloc_failure_mode;
2028
extern __CPROVER_size_t __CPROVER_max_malloc_size;
21-
extern _Bool __CPROVER_malloc_may_fail;
29+
extern __CPROVER_bool __CPROVER_malloc_may_fail;
2230

2331
// malloc failure modes
2432
extern int __CPROVER_malloc_failure_mode_return_null;
2533
extern int __CPROVER_malloc_failure_mode_assert_then_assume;
2634

27-
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
28-
void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
29-
void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
30-
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
31-
32-
_Bool __CPROVER_is_zero_string(const void *);
33-
__CPROVER_size_t __CPROVER_zero_string_length(const void *);
34-
__CPROVER_size_t __CPROVER_buffer_size(const void *);
35-
__CPROVER_bool __CPROVER_r_ok();
36-
__CPROVER_bool __CPROVER_w_ok();
37-
__CPROVER_bool __CPROVER_rw_ok();
38-
39-
#if 0
40-
__CPROVER_bool __CPROVER_equal();
41-
__CPROVER_bool __CPROVER_same_object(const void *, const void *);
42-
43-
const unsigned __CPROVER_constant_infinity_uint;
44-
typedef void __CPROVER_integer;
45-
typedef void __CPROVER_rational;
46-
void __CPROVER_initialize(void);
47-
void __CPROVER_cover(__CPROVER_bool condition);
48-
#endif
49-
50-
void __CPROVER_printf(const char *format, ...);
51-
void __CPROVER_input(const char *id, ...);
52-
void __CPROVER_output(const char *id, ...);
53-
54-
// concurrency-related
55-
void __CPROVER_atomic_begin();
56-
void __CPROVER_atomic_end();
57-
void __CPROVER_fence(const char *kind, ...);
58-
#if 0
59-
__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;
60-
__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
61-
unsigned long __CPROVER_next_thread_id=0;
62-
63-
// traces
64-
void CBMC_trace(int lvl, const char *event, ...);
65-
#endif
66-
67-
// pointers
68-
unsigned __CPROVER_POINTER_OBJECT(const void *p);
69-
signed __CPROVER_POINTER_OFFSET(const void *p);
70-
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
71-
#if 0
72-
extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];
73-
void __CPROVER_allocated_memory(
74-
__CPROVER_size_t address, __CPROVER_size_t extent);
75-
76-
// this is ANSI-C
77-
extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];
78-
79-
// this is GCC
80-
extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];
81-
extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];
82-
#endif
83-
84-
// float stuff
85-
int __CPROVER_fpclassify(int, int, int, int, int, ...);
86-
__CPROVER_bool __CPROVER_isfinite(double f);
87-
__CPROVER_bool __CPROVER_isinf(double f);
88-
__CPROVER_bool __CPROVER_isnormal(double f);
89-
__CPROVER_bool __CPROVER_sign(double f);
90-
__CPROVER_bool __CPROVER_isnanf(float f);
91-
__CPROVER_bool __CPROVER_isnand(double f);
92-
__CPROVER_bool __CPROVER_isnanld(long double f);
93-
__CPROVER_bool __CPROVER_isfinitef(float f);
94-
__CPROVER_bool __CPROVER_isfinited(double f);
95-
__CPROVER_bool __CPROVER_isfiniteld(long double f);
96-
__CPROVER_bool __CPROVER_isinff(float f);
97-
__CPROVER_bool __CPROVER_isinfd(double f);
98-
__CPROVER_bool __CPROVER_isinfld(long double f);
99-
__CPROVER_bool __CPROVER_isnormalf(float f);
100-
__CPROVER_bool __CPROVER_isnormald(double f);
101-
__CPROVER_bool __CPROVER_isnormalld(long double f);
102-
__CPROVER_bool __CPROVER_signf(float f);
103-
__CPROVER_bool __CPROVER_signd(double f);
104-
__CPROVER_bool __CPROVER_signld(long double f);
105-
double __CPROVER_inf(void);
106-
float __CPROVER_inff(void);
107-
long double __CPROVER_infl(void);
108-
//extern int __CPROVER_thread_local __CPROVER_rounding_mode;
109-
int __CPROVER_isgreaterd(double f, double g);
110-
111-
// absolute value
112-
int __CPROVER_abs(int);
113-
long int __CPROVER_labs(long int);
114-
long long int __CPROVER_llabs(long long int);
115-
double __CPROVER_fabs(double);
116-
long double __CPROVER_fabsl(long double);
117-
float __CPROVER_fabsf(float);
118-
119-
// modulo and remainder
120-
double __CPROVER_fmod(double, double);
121-
float __CPROVER_fmodf(float, float);
122-
long double __CPROVER_fmodl(long double, long double);
123-
double __CPROVER_remainder(double, double);
124-
float __CPROVER_remainderf(float, float);
125-
long double __CPROVER_remainderl(long double, long double);
126-
127-
// arrays
128-
//__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
129-
void __CPROVER_array_copy(const void *dest, const void *src);
130-
void __CPROVER_array_set(const void *dest, ...);
131-
void __CPROVER_array_replace(const void *dest, const void *src);
132-
133-
#if 0
134-
// k-induction
135-
void __CPROVER_k_induction_hint(unsigned min, unsigned max,
136-
unsigned step, unsigned loop_free);
137-
138-
// manual specification of predicates
139-
void __CPROVER_predicate(__CPROVER_bool predicate);
140-
void __CPROVER_parameter_predicates();
141-
void __CPROVER_return_predicates();
142-
#endif
143-
144-
// pipes, write, read, close
14535
struct __CPROVER_pipet {
14636
_Bool widowed;
14737
char data[4];
14838
short next_avail;
14939
short next_unread;
15040
};
151-
#if 0
152-
extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
153-
// offset to make sure we don't collide with other fds
154-
extern const int __CPROVER_pipe_offset;
155-
extern unsigned __CPROVER_pipe_count;
156-
#endif
157-
158-
void __CPROVER_set_must(const void *, const char *);
159-
void __CPROVER_set_may(const void *, const char *);
160-
void __CPROVER_clear_must(const void *, const char *);
161-
void __CPROVER_clear_may(const void *, const char *);
162-
void __CPROVER_cleanup(const void *, void (*)(void *));
163-
__CPROVER_bool __CPROVER_get_must(const void *, const char *);
164-
__CPROVER_bool __CPROVER_get_may(const void *, const char *);
165-
166-
#define __CPROVER_danger_number_of_ops 1
167-
#define __CPROVER_danger_max_solution_size 1
168-
#define __CPROVER_danger_number_of_vars 1
169-
#define __CPROVER_danger_number_of_consts 1
17041

171-
// detect overflow
172-
__CPROVER_bool __CPROVER_overflow_minus();
173-
__CPROVER_bool __CPROVER_overflow_mult();
174-
__CPROVER_bool __CPROVER_overflow_plus();
175-
__CPROVER_bool __CPROVER_overflow_shl();
176-
__CPROVER_bool __CPROVER_overflow_unary_minus();
42+
#include "../cprover_builtin_headers.h"
17743

17844
#endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H

‎src/ansi-c/library/math.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -758,7 +758,7 @@ float sqrtf(float f)
758758
case FE_TOWARDZERO :
759759
return (f - lowerSquare == 0.0f) ? lower : upper; break;
760760
default:;
761-
//assert(0);
761+
return __VERIFIER_nondet_float();
762762
}
763763

764764
}
@@ -835,7 +835,7 @@ double sqrt(double d)
835835
case FE_TOWARDZERO:
836836
return (d - lowerSquare == 0.0) ? lower : upper; break;
837837
default:;
838-
//assert(0);
838+
return __VERIFIER_nondet_double();
839839
}
840840

841841
}
@@ -906,7 +906,7 @@ long double sqrtl(long double d)
906906
case FE_TOWARDZERO:
907907
return (d - lowerSquare == 0.0l) ? lower : upper; break;
908908
default:;
909-
//assert(0);
909+
return __VERIFIER_nondet_long_double();
910910
}
911911

912912
}

‎src/ansi-c/library/module_dependencies.txt

+1
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
1+
..
12
ansi-c
23
ansi-c/library

‎src/ansi-c/library/pthread_lib.c

+3
Original file line numberDiff line numberDiff line change
@@ -314,6 +314,9 @@ inline void pthread_exit(void *value_ptr)
314314
#endif
315315
__CPROVER_threads_exited[__CPROVER_thread_id]=1;
316316
__CPROVER_assume(0);
317+
#ifdef LIBRARY_CHECK
318+
__builtin_unreachable();
319+
#endif
317320
}
318321

319322
/* FUNCTION: pthread_join */

‎src/ansi-c/library/setjmp.c

+9
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,9 @@ inline void longjmp(jmp_buf env, int val)
1313
(void)val;
1414
__CPROVER_assert(0, "longjmp requires instrumentation");
1515
__CPROVER_assume(0);
16+
#ifdef LIBRARY_CHECK
17+
__builtin_unreachable();
18+
#endif
1619
}
1720

1821
/* FUNCTION: _longjmp */
@@ -29,6 +32,9 @@ inline void _longjmp(jmp_buf env, int val)
2932
(void)val;
3033
__CPROVER_assert(0, "_longjmp requires instrumentation");
3134
__CPROVER_assume(0);
35+
#ifdef LIBRARY_CHECK
36+
__builtin_unreachable();
37+
#endif
3238
}
3339

3440
/* FUNCTION: siglongjmp */
@@ -47,6 +53,9 @@ inline void siglongjmp(sigjmp_buf env, int val)
4753
(void)val;
4854
__CPROVER_assert(0, "siglongjmp requires instrumentation");
4955
__CPROVER_assume(0);
56+
#ifdef LIBRARY_CHECK
57+
__builtin_unreachable();
58+
#endif
5059
}
5160

5261
#endif

‎src/ansi-c/library/stdio.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,7 @@ char *fgets(char *str, int size, FILE *stream)
330330
#define __CPROVER_STDIO_H_INCLUDED
331331
#endif
332332

333+
char __VERIFIER_nondet_char();
333334
size_t __VERIFIER_nondet_size_t();
334335

335336
inline size_t fread(
@@ -359,8 +360,7 @@ inline size_t fread(
359360

360361
for(size_t i=0; i<bytes; i++)
361362
{
362-
char nondet_char;
363-
((char *)ptr)[i]=nondet_char;
363+
((char *)ptr)[i] = __VERIFIER_nondet_char();
364364
}
365365

366366
return nread;

‎src/ansi-c/library/stdlib.c

+9
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,9 @@ inline void exit(int status)
3636
{
3737
(void)status;
3838
__CPROVER_assume(0);
39+
#ifdef LIBRARY_CHECK
40+
__builtin_unreachable();
41+
#endif
3942
}
4043

4144
/* FUNCTION: _Exit */
@@ -46,6 +49,9 @@ inline void _Exit(int status)
4649
{
4750
(void)status;
4851
__CPROVER_assume(0);
52+
#ifdef LIBRARY_CHECK
53+
__builtin_unreachable();
54+
#endif
4955
}
5056

5157
/* FUNCTION: abort */
@@ -55,6 +61,9 @@ inline void _Exit(int status)
5561
inline void abort(void)
5662
{
5763
__CPROVER_assume(0);
64+
#ifdef LIBRARY_CHECK
65+
__builtin_unreachable();
66+
#endif
5867
}
5968

6069
/* FUNCTION: calloc */

‎src/ansi-c/library_check.sh

+1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ for f in "$@"; do
77
echo "Checking ${f}"
88
cp "${f}" __libcheck.c
99
perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c
10+
perl -p -i -e 's/s(__builtin_unreachable)/$1/' __libcheck.c
1011
perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
1112
perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
1213
perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c

0 commit comments

Comments
 (0)