Skip to content

Commit a021bf6

Browse files
tautschnigtautschnig
authored
Merge pull request #7904 from tautschnig/features/chk
C library: model and test several __*_chk variants
2 parents 801fa73 + d95917d commit a021bf6

File tree

15 files changed

+305
-34
lines changed

15 files changed

+305
-34
lines changed

‎regression/cbmc-library/fgets-01/__fgets_chk.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
KNOWNBUG
2+
main.c
3+
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 --unwindset fgets:0
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[main.assertion.3\] line 16 assertion p\[1\] == 'b': FAILURE
8+
\*\* 1 of \d+ failed
9+
--
10+
^\*\*\*\* WARNING: no body for function __fgets_chk
11+
^warning: ignoring
12+
--
13+
Our asm renaming results in fgets and its alias being one and the same function
14+
to us, so we end up recursing in glibc's fgets wrapper.

‎regression/cbmc-library/fprintf-01/__fprintf_chk.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^\*\*\*\* WARNING: no body for function __fprintf_chk
9+
^warning: ignoring

‎regression/cbmc-library/fread-01/__fread_chk.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 --unwindset fread:0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^\*\*\*\* WARNING: no body for function __fread_chk
9+
^warning: ignoring

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

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,15 @@
33

44
int main()
55
{
6-
fread();
7-
assert(0);
6+
FILE *f = fdopen(0, "r");
7+
if(!f)
8+
return 1;
9+
10+
char buffer[3];
11+
size_t result = fread(buffer, 3, 1, f);
12+
assert(result <= 3);
13+
14+
fclose(f);
15+
816
return 0;
917
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

‎regression/cbmc-library/printf-01/__printf_chk.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\*\* 1 of \d+ failed
7+
^VERIFICATION FAILED$
8+
--
9+
^\*\*\*\* WARNING: no body for function __printf_chk
10+
^warning: ignoring

‎regression/cbmc-library/syslog-01/__syslog_chk.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^\*\*\*\* WARNING: no body for function __syslog_chk
9+
^warning: ignoring

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

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
11
#include <assert.h>
2-
#include <syslog.h>
2+
#ifndef _WIN32
3+
# include <syslog.h>
4+
#else
5+
void syslog(int priority, const char *format, ...);
6+
#endif
37

4-
int main()
8+
int main(int argc, char *argv[])
59
{
6-
syslog();
7-
assert(0);
10+
int some_priority;
11+
syslog(some_priority, "%d\n", argc);
812
return 0;
913
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

‎regression/cbmc-library/vfprintf-01/__vfprintf_chk.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^\*\*\*\* WARNING: no body for function __vfprintf_chk
9+
^warning: ignoring

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

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,17 @@
1-
#include <assert.h>
1+
#include <stdarg.h>
22
#include <stdio.h>
33

4+
int xprintf(const char *format, ...)
5+
{
6+
va_list list;
7+
va_start(list, format);
8+
int result = vfprintf(stdout, format, list);
9+
va_end(list);
10+
return result;
11+
}
12+
413
int main()
514
{
6-
vfprintf();
7-
assert(0);
15+
xprintf("%d\n", 42);
816
return 0;
917
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

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

Lines changed: 198 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -280,7 +280,7 @@ int __VERIFIER_nondet_int(void);
280280

281281
char *fgets(char *str, int size, FILE *stream)
282282
{
283-
__CPROVER_HIDE:;
283+
__CPROVER_HIDE:;
284284
__CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
285285

286286
(void)size;
@@ -323,6 +323,63 @@ char *fgets(char *str, int size, FILE *stream)
323323
return error?0:str;
324324
}
325325

326+
/* FUNCTION: __fgets_chk */
327+
328+
#ifndef __CPROVER_STDIO_H_INCLUDED
329+
# include <stdio.h>
330+
# define __CPROVER_STDIO_H_INCLUDED
331+
#endif
332+
333+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
334+
int __VERIFIER_nondet_int(void);
335+
336+
char *__fgets_chk(char *str, __CPROVER_size_t bufsize, int size, FILE *stream)
337+
{
338+
__CPROVER_HIDE:;
339+
(void)bufsize;
340+
__CPROVER_bool error = __VERIFIER_nondet___CPROVER_bool();
341+
342+
(void)size;
343+
if(stream != stdin)
344+
{
345+
#if !defined(__linux__) || defined(__GLIBC__)
346+
(void)*stream;
347+
#else
348+
(void)*(char *)stream;
349+
#endif
350+
}
351+
352+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
353+
__CPROVER_assert(
354+
__CPROVER_get_must(stream, "open"), "fgets file must be open");
355+
#endif
356+
357+
#ifdef __CPROVER_STRING_ABSTRACTION
358+
int resulting_size;
359+
__CPROVER_assert(
360+
__CPROVER_buffer_size(str) >= size, "buffer-overflow in fgets");
361+
if(size > 0)
362+
{
363+
__CPROVER_assume(resulting_size < size);
364+
__CPROVER_is_zero_string(str) = !error;
365+
__CPROVER_zero_string_length(str) = resulting_size;
366+
}
367+
#else
368+
if(size > 0)
369+
{
370+
int str_length = __VERIFIER_nondet_int();
371+
__CPROVER_assume(str_length >= 0 && str_length < size);
372+
__CPROVER_precondition(__CPROVER_w_ok(str, size), "fgets buffer writable");
373+
char contents_nondet[str_length];
374+
__CPROVER_array_replace(str, contents_nondet);
375+
if(!error)
376+
str[str_length] = '\0';
377+
}
378+
#endif
379+
380+
return error ? 0 : str;
381+
}
382+
326383
/* FUNCTION: fread */
327384

328385
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -335,10 +392,10 @@ size_t __VERIFIER_nondet_size_t(void);
335392

336393
size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
337394
{
338-
__CPROVER_HIDE:;
339-
size_t nread=__VERIFIER_nondet_size_t();
340-
size_t bytes=nread*size;
341-
__CPROVER_assume(nread<=nitems);
395+
__CPROVER_HIDE:;
396+
size_t bytes_read = __VERIFIER_nondet_size_t();
397+
size_t upper_bound = nitems * size;
398+
__CPROVER_assume(bytes_read <= upper_bound);
342399

343400
if(stream != stdin)
344401
{
@@ -354,12 +411,52 @@ size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
354411
"fread file must be open");
355412
#endif
356413

357-
for(size_t i=0; i<bytes; i++)
414+
for(size_t i = 0; i < bytes_read && i < upper_bound; i++)
415+
{
416+
((char *)ptr)[i] = __VERIFIER_nondet_char();
417+
}
418+
419+
return bytes_read / size;
420+
}
421+
422+
/* FUNCTION: __fread_chk */
423+
424+
#ifndef __CPROVER_STDIO_H_INCLUDED
425+
# include <stdio.h>
426+
# define __CPROVER_STDIO_H_INCLUDED
427+
#endif
428+
429+
char __VERIFIER_nondet_char(void);
430+
size_t __VERIFIER_nondet_size_t(void);
431+
432+
size_t
433+
__fread_chk(void *ptr, size_t ptrlen, size_t size, size_t nitems, FILE *stream)
434+
{
435+
__CPROVER_HIDE:;
436+
size_t bytes_read = __VERIFIER_nondet_size_t();
437+
size_t upper_bound = nitems * size;
438+
__CPROVER_assume(bytes_read <= upper_bound);
439+
440+
if(stream != stdin)
441+
{
442+
#if !defined(__linux__) || defined(__GLIBC__)
443+
(void)*stream;
444+
#else
445+
(void)*(char *)stream;
446+
#endif
447+
}
448+
449+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
450+
__CPROVER_assert(
451+
__CPROVER_get_must(stream, "open"), "fread file must be open");
452+
#endif
453+
454+
for(size_t i = 0; i < bytes_read && i < upper_bound && i < ptrlen; i++)
358455
{
359456
((char *)ptr)[i] = __VERIFIER_nondet_char();
360457
}
361458

362-
return nread;
459+
return bytes_read / size;
363460
}
364461

365462
/* FUNCTION: feof */
@@ -1287,6 +1384,32 @@ __CPROVER_HIDE:;
12871384
return result;
12881385
}
12891386

1387+
/* FUNCTION: __printf_chk */
1388+
1389+
#ifndef __CPROVER_STDIO_H_INCLUDED
1390+
# include <stdio.h>
1391+
# define __CPROVER_STDIO_H_INCLUDED
1392+
#endif
1393+
1394+
#ifndef __CPROVER_STDARG_H_INCLUDED
1395+
# include <stdarg.h>
1396+
# define __CPROVER_STDARG_H_INCLUDED
1397+
#endif
1398+
1399+
int __VERIFIER_nondet_int(void);
1400+
1401+
int __printf_chk(int flag, const char *format, ...)
1402+
{
1403+
__CPROVER_HIDE:;
1404+
(void)flag;
1405+
int result = __VERIFIER_nondet_int();
1406+
va_list list;
1407+
va_start(list, format);
1408+
__CPROVER_printf(format, list);
1409+
va_end(list);
1410+
return result;
1411+
}
1412+
12901413
/* FUNCTION: fprintf */
12911414

12921415
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1309,6 +1432,29 @@ int fprintf(FILE *stream, const char *restrict format, ...)
13091432
return result;
13101433
}
13111434

1435+
/* FUNCTION: __fprintf_chk */
1436+
1437+
#ifndef __CPROVER_STDIO_H_INCLUDED
1438+
# include <stdio.h>
1439+
# define __CPROVER_STDIO_H_INCLUDED
1440+
#endif
1441+
1442+
#ifndef __CPROVER_STDARG_H_INCLUDED
1443+
# include <stdarg.h>
1444+
# define __CPROVER_STDARG_H_INCLUDED
1445+
#endif
1446+
1447+
int __fprintf_chk(FILE *stream, int flag, const char *restrict format, ...)
1448+
{
1449+
__CPROVER_HIDE:;
1450+
(void)flag;
1451+
va_list list;
1452+
va_start(list, format);
1453+
int result = vfprintf(stream, format, list);
1454+
va_end(list);
1455+
return result;
1456+
}
1457+
13121458
/* FUNCTION: vfprintf */
13131459

13141460
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1349,6 +1495,51 @@ int vfprintf(FILE *stream, const char *restrict format, va_list arg)
13491495
return result;
13501496
}
13511497

1498+
/* FUNCTION: __vfprintf_chk */
1499+
1500+
#ifndef __CPROVER_STDIO_H_INCLUDED
1501+
# include <stdio.h>
1502+
# define __CPROVER_STDIO_H_INCLUDED
1503+
#endif
1504+
1505+
#ifndef __CPROVER_STDARG_H_INCLUDED
1506+
# include <stdarg.h>
1507+
# define __CPROVER_STDARG_H_INCLUDED
1508+
#endif
1509+
1510+
int __VERIFIER_nondet_int(void);
1511+
1512+
int __vfprintf_chk(
1513+
FILE *stream,
1514+
int flag,
1515+
const char *restrict format,
1516+
va_list arg)
1517+
{
1518+
__CPROVER_HIDE:;
1519+
(void)flag;
1520+
1521+
int result = __VERIFIER_nondet_int();
1522+
1523+
if(stream != stdout && stream != stderr)
1524+
{
1525+
#if !defined(__linux__) || defined(__GLIBC__)
1526+
(void)*stream;
1527+
#else
1528+
(void)*(char *)stream;
1529+
#endif
1530+
}
1531+
1532+
(void)*format;
1533+
(void)arg;
1534+
1535+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1536+
__CPROVER_assert(
1537+
__CPROVER_get_must(stream, "open"), "vfprintf file must be open");
1538+
#endif
1539+
1540+
return result;
1541+
}
1542+
13521543
/* FUNCTION: vasprintf */
13531544

13541545
#ifndef __CPROVER_STDIO_H_INCLUDED

0 commit comments

Comments
 (0)