From 80e2aa88508f9865ba835d900f4313a55b2d81e9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 Feb 2019 21:49:36 +0000 Subject: [PATCH 1/4] C library: Do not require stdin, stdout, stderr to be initialised vfprintf and several other library functions dereference a FILE*-typed stream parameter to make sure pointer checks and bounds checks are triggered. As we do not set up stdin, stdout, stderr to point to valid FILE-typed objects, make sure we never attempt such dereferencing if the stream argument is stdin/stdout/stderr (unless the use of any of those would in itself constitute an error, as is the case in fseek, for example). --- regression/cbmc-library/fprintf-01/main.c | 6 +- regression/cbmc-library/fprintf-01/test.desc | 2 +- src/ansi-c/library/stdio.c | 172 ++++++++++++------- 3 files changed, 114 insertions(+), 66 deletions(-) diff --git a/regression/cbmc-library/fprintf-01/main.c b/regression/cbmc-library/fprintf-01/main.c index 264c8ae7b19..6eed023d694 100644 --- a/regression/cbmc-library/fprintf-01/main.c +++ b/regression/cbmc-library/fprintf-01/main.c @@ -1,9 +1,9 @@ #include #include -int main() +int main(int argc, char *argv[]) { - fprintf(); - assert(0); + fprintf(stdout, "some string %s: %d\n", argv[0], 42); + fprintf(stderr, "some other string\n"); return 0; } diff --git a/regression/cbmc-library/fprintf-01/test.desc b/regression/cbmc-library/fprintf-01/test.desc index 9542d988e8d..96c9b4bcd7b 100644 --- a/regression/cbmc-library/fprintf-01/test.desc +++ b/regression/cbmc-library/fprintf-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index 12a387deb83..47e75ede579 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -232,11 +232,14 @@ char *fgets(char *str, int size, FILE *stream) __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); (void)size; - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -290,11 +293,14 @@ inline size_t fread( size_t bytes=nread*size; __CPROVER_assume(nread<=nitems); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -325,11 +331,14 @@ inline int feof(FILE *stream) __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -354,11 +363,14 @@ inline int ferror(FILE *stream) __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -379,8 +391,15 @@ int __VERIFIER_nondet_int(); inline int fileno(FILE *stream) { - // just return nondet - __CPROVER_HIDE:; +// just return nondet +__CPROVER_HIDE:; + if(stream == stdin) + return 0; + else if(stream == stdout) + return 1; + else if(stream == stderr) + return 2; + int return_value=__VERIFIER_nondet_int(); #if !defined(__linux__) || defined(__GLIBC__) @@ -416,11 +435,14 @@ inline int fputs(const char *s, FILE *stream) #endif (void)*s; - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdout && stream != stderr) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -470,11 +492,14 @@ inline int fpurge(FILE *stream) __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin && stream != stdout && stream != stderr) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -497,11 +522,16 @@ inline int fgetc(FILE *stream) { __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } + // it's a byte or EOF (-1) __CPROVER_assume(return_value>=-1 && return_value<=255); @@ -529,11 +559,14 @@ inline int getc(FILE *stream) __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -581,11 +614,14 @@ inline int getw(FILE *stream) __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -698,11 +734,14 @@ size_t fwrite( (void)*(char*)ptr; (void)size; - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdout && stream != stderr) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -821,11 +860,16 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a { __CPROVER_HIDE:; int result=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + + if(stream != stdin) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } + (void)*format; (void)arg; @@ -921,11 +965,15 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) int result=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) - (void)*stream; - #else - (void)*(char*)stream; - #endif + if(stream != stdout && stream != stderr) + { +#if !defined(__linux__) || defined(__GLIBC__) + (void)*stream; +#else + (void)*(char *)stream; +#endif + } + (void)*format; (void)arg; From 3f1ea297821f2d05449771db2d904dba7cf0d38f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 Feb 2019 21:59:41 +0000 Subject: [PATCH 2/4] clang-format compatible preprocessor instructions --- src/ansi-c/library/stdio.c | 144 ++++++++++++++++++------------------- 1 file changed, 72 insertions(+), 72 deletions(-) diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index 47e75ede579..d1ef15bdc9e 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -75,27 +75,27 @@ inline FILE *fopen(const char *filename, const char *mode) __CPROVER_HIDE:; (void)*filename; (void)*mode; - #ifdef __CPROVER_STRING_ABSTRACTION +#ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_assert(__CPROVER_is_zero_string(filename), "fopen zero-termination of 1st argument"); __CPROVER_assert(__CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument"); - #endif +#endif FILE *fopen_result; __CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool(); - #if !defined(__linux__) || defined(__GLIBC__) +#if !defined(__linux__) || defined(__GLIBC__) fopen_result=fopen_error?NULL:malloc(sizeof(FILE)); - #else +#else // libraries need to expose the definition of FILE; this is the // case for musl fopen_result=fopen_error?NULL:malloc(sizeof(int)); - #endif +#endif - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_set_must(fopen_result, "open"); __CPROVER_cleanup(fopen_result, fclose_cleanup); - #endif +#endif return fopen_result; } @@ -112,11 +112,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f) __CPROVER_HIDE:; (void)*filename; (void)*mode; - #if !defined(__linux__) || defined(__GLIBC__) +#if !defined(__linux__) || defined(__GLIBC__) (void)*f; - #else +#else (void)*(char*)f; - #endif +#endif return f; } @@ -137,13 +137,13 @@ int __VERIFIER_nondet_int(); inline int fclose(FILE *stream) { - __CPROVER_HIDE:; - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +__CPROVER_HIDE:; +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "fclose file must be open"); __CPROVER_clear_must(stream, "open"); __CPROVER_set_must(stream, "closed"); - #endif +#endif int return_value=__VERIFIER_nondet_int(); free(stream); return return_value; @@ -166,18 +166,18 @@ inline FILE *fdopen(int handle, const char *mode) __CPROVER_HIDE:; (void)handle; (void)*mode; - #ifdef __CPROVER_STRING_ABSTRACTION +#ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_assert(__CPROVER_is_zero_string(mode), "fdopen zero-termination of 2nd argument"); - #endif +#endif - #if !defined(__linux__) || defined(__GLIBC__) +#if !defined(__linux__) || defined(__GLIBC__) FILE *f=malloc(sizeof(FILE)); - #else +#else // libraries need to expose the definition of FILE; this is the // case for musl FILE *f=malloc(sizeof(int)); - #endif +#endif return f; } @@ -205,10 +205,10 @@ inline FILE *_fdopen(int handle, const char *mode) __CPROVER_HIDE:; (void)handle; (void)*mode; - #ifdef __CPROVER_STRING_ABSTRACTION +#ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_assert(__CPROVER_is_zero_string(mode), "fdopen zero-termination of 2nd argument"); - #endif +#endif FILE *f=malloc(sizeof(FILE)); @@ -241,12 +241,12 @@ char *fgets(char *str, int size, FILE *stream) #endif } - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "fgets file must be open"); - #endif +#endif - #ifdef __CPROVER_STRING_ABSTRACTION +#ifdef __CPROVER_STRING_ABSTRACTION int resulting_size; __CPROVER_assert(__CPROVER_buffer_size(str)>=size, "buffer-overflow in fgets"); if(size>0) @@ -255,7 +255,7 @@ char *fgets(char *str, int size, FILE *stream) __CPROVER_is_zero_string(str)=!error; __CPROVER_zero_string_length(str)=resulting_size; } - #else +#else if(size>0) { int str_length=__VERIFIER_nondet_int(); @@ -268,7 +268,7 @@ char *fgets(char *str, int size, FILE *stream) if(!error) str[str_length]='\0'; } - #endif +#endif return error?0:str; } @@ -302,10 +302,10 @@ inline size_t fread( #endif } - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "fread file must be open"); - #endif +#endif for(size_t i=0; i=-1 && return_value<=255); @@ -623,10 +623,10 @@ inline int getw(FILE *stream) #endif } - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "getw file must be open"); - #endif +#endif __CPROVER_input("getw", return_value); @@ -648,18 +648,18 @@ inline int fseek(FILE *stream, long offset, int whence) __CPROVER_HIDE:; int return_value=__VERIFIER_nondet_int(); - #if !defined(__linux__) || defined(__GLIBC__) +#if !defined(__linux__) || defined(__GLIBC__) (void)*stream; - #else +#else (void)*(char*)stream; - #endif +#endif (void)offset; (void)whence; - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "fseek file must be open"); - #endif +#endif return return_value; } @@ -678,16 +678,16 @@ inline long ftell(FILE *stream) __CPROVER_HIDE:; long return_value=__VERIFIER_nondet_long(); - #if !defined(__linux__) || defined(__GLIBC__) +#if !defined(__linux__) || defined(__GLIBC__) (void)*stream; - #else +#else (void)*(char*)stream; - #endif +#endif - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "ftell file must be open"); - #endif +#endif return return_value; } @@ -701,18 +701,18 @@ inline long ftell(FILE *stream) void rewind(FILE *stream) { - __CPROVER_HIDE: +__CPROVER_HIDE: - #if !defined(__linux__) || defined(__GLIBC__) +#if !defined(__linux__) || defined(__GLIBC__) (void)*stream; - #else +#else (void)*(char*)stream; - #endif +#endif - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "rewind file must be open"); - #endif +#endif } /* FUNCTION: fwrite */ @@ -743,10 +743,10 @@ size_t fwrite( #endif } - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "fwrite file must be open"); - #endif +#endif size_t nwrite=__VERIFIER_nondet_size_t(); __CPROVER_assume(nwrite<=nitems); @@ -873,10 +873,10 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a (void)*format; (void)arg; - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "vfscanf file must be open"); - #endif +#endif return result; } @@ -977,10 +977,10 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) (void)*format; (void)arg; - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "vfprintf file must be open"); - #endif +#endif return result; } From c02cd7858c89f73451d817a604f65e6a06f5bbb3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 Feb 2019 08:53:59 +0000 Subject: [PATCH 3/4] C library: Constrain the return value of fileno and test it The earlier commit made sure it returns 0/1/2 for stdin/stdout/stderr. --- regression/cbmc-library/fileno-01/main.c | 11 +++++++++-- regression/cbmc-library/fileno-01/test.desc | 2 +- src/ansi-c/library/stdio.c | 2 +- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-library/fileno-01/main.c b/regression/cbmc-library/fileno-01/main.c index a4d6d01dc37..c186de1b88d 100644 --- a/regression/cbmc-library/fileno-01/main.c +++ b/regression/cbmc-library/fileno-01/main.c @@ -3,7 +3,14 @@ int main() { - fileno(); - assert(0); + // requires initialization of stdin/stdout/stderr + // assert(fileno(stdin) == 0); + // assert(fileno(stdout) == 1); + // assert(fileno(stderr) == 2); + + int fd; + FILE *some_file = fdopen(fd, ""); + assert(fileno(some_file) >= -1); + return 0; } diff --git a/regression/cbmc-library/fileno-01/test.desc b/regression/cbmc-library/fileno-01/test.desc index 9542d988e8d..96c9b4bcd7b 100644 --- a/regression/cbmc-library/fileno-01/test.desc +++ b/regression/cbmc-library/fileno-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index d1ef15bdc9e..da620a9d6a9 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -391,7 +391,6 @@ int __VERIFIER_nondet_int(); inline int fileno(FILE *stream) { -// just return nondet __CPROVER_HIDE:; if(stream == stdin) return 0; @@ -401,6 +400,7 @@ __CPROVER_HIDE:; return 2; int return_value=__VERIFIER_nondet_int(); + __CPROVER_assume(return_value >= -1); #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; From 92a38027fbef9ba7ea6bd727ac1503e318a6304d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 Feb 2019 09:53:55 +0000 Subject: [PATCH 4/4] Fix typo: __CPOVER_HIDE -> __CPROVER_HIDE Note the missing "R". --- src/ansi-c/library/stdio.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index da620a9d6a9..8caec8fb5c2 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -790,7 +790,7 @@ void perror(const char *s) inline int fscanf(FILE *restrict stream, const char *restrict format, ...) { - __CPOVER_HIDE:; +__CPROVER_HIDE:; va_list list; va_start(list, format); int result=vfscanf(stream, format, list); @@ -812,7 +812,7 @@ inline int fscanf(FILE *restrict stream, const char *restrict format, ...) inline int scanf(const char *restrict format, ...) { - __CPOVER_HIDE:; +__CPROVER_HIDE:; va_list list; va_start(list, format); int result=vfscanf(stdin, format, list); @@ -834,7 +834,7 @@ inline int scanf(const char *restrict format, ...) inline int sscanf(const char *restrict s, const char *restrict format, ...) { - __CPOVER_HIDE:; +__CPROVER_HIDE:; va_list list; va_start(list, format); int result=vsscanf(s, format, list);