Skip to content

Commit 80e2aa8

Browse files
tautschnigtautschnig
committed
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).
1 parent 05af336 commit 80e2aa8

File tree

3 files changed

+114
-66
lines changed

3 files changed

+114
-66
lines changed

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

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

4-
int main()
4+
int main(int argc, char *argv[])
55
{
6-
fprintf();
7-
assert(0);
6+
fprintf(stdout, "some string %s: %d\n", argv[0], 42);
7+
fprintf(stderr, "some other string\n");
88
return 0;
99
}

‎regression/cbmc-library/fprintf-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: 110 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -232,11 +232,14 @@ char *fgets(char *str, int size, FILE *stream)
232232
__CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
233233

234234
(void)size;
235-
#if !defined(__linux__) || defined(__GLIBC__)
236-
(void)*stream;
237-
#else
238-
(void)*(char*)stream;
239-
#endif
235+
if(stream != stdin)
236+
{
237+
#if !defined(__linux__) || defined(__GLIBC__)
238+
(void)*stream;
239+
#else
240+
(void)*(char *)stream;
241+
#endif
242+
}
240243

241244
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
242245
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -290,11 +293,14 @@ inline size_t fread(
290293
size_t bytes=nread*size;
291294
__CPROVER_assume(nread<=nitems);
292295

293-
#if !defined(__linux__) || defined(__GLIBC__)
294-
(void)*stream;
295-
#else
296-
(void)*(char*)stream;
297-
#endif
296+
if(stream != stdin)
297+
{
298+
#if !defined(__linux__) || defined(__GLIBC__)
299+
(void)*stream;
300+
#else
301+
(void)*(char *)stream;
302+
#endif
303+
}
298304

299305
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
300306
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -325,11 +331,14 @@ inline int feof(FILE *stream)
325331
__CPROVER_HIDE:;
326332
int return_value=__VERIFIER_nondet_int();
327333

328-
#if !defined(__linux__) || defined(__GLIBC__)
329-
(void)*stream;
330-
#else
331-
(void)*(char*)stream;
332-
#endif
334+
if(stream != stdin)
335+
{
336+
#if !defined(__linux__) || defined(__GLIBC__)
337+
(void)*stream;
338+
#else
339+
(void)*(char *)stream;
340+
#endif
341+
}
333342

334343
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
335344
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -354,11 +363,14 @@ inline int ferror(FILE *stream)
354363
__CPROVER_HIDE:;
355364
int return_value=__VERIFIER_nondet_int();
356365

357-
#if !defined(__linux__) || defined(__GLIBC__)
358-
(void)*stream;
359-
#else
360-
(void)*(char*)stream;
361-
#endif
366+
if(stream != stdin)
367+
{
368+
#if !defined(__linux__) || defined(__GLIBC__)
369+
(void)*stream;
370+
#else
371+
(void)*(char *)stream;
372+
#endif
373+
}
362374

363375
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
364376
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -379,8 +391,15 @@ int __VERIFIER_nondet_int();
379391

380392
inline int fileno(FILE *stream)
381393
{
382-
// just return nondet
383-
__CPROVER_HIDE:;
394+
// just return nondet
395+
__CPROVER_HIDE:;
396+
if(stream == stdin)
397+
return 0;
398+
else if(stream == stdout)
399+
return 1;
400+
else if(stream == stderr)
401+
return 2;
402+
384403
int return_value=__VERIFIER_nondet_int();
385404

386405
#if !defined(__linux__) || defined(__GLIBC__)
@@ -416,11 +435,14 @@ inline int fputs(const char *s, FILE *stream)
416435
#endif
417436
(void)*s;
418437

419-
#if !defined(__linux__) || defined(__GLIBC__)
420-
(void)*stream;
421-
#else
422-
(void)*(char*)stream;
423-
#endif
438+
if(stream != stdout && stream != stderr)
439+
{
440+
#if !defined(__linux__) || defined(__GLIBC__)
441+
(void)*stream;
442+
#else
443+
(void)*(char *)stream;
444+
#endif
445+
}
424446

425447
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
426448
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -470,11 +492,14 @@ inline int fpurge(FILE *stream)
470492
__CPROVER_HIDE:;
471493
int return_value=__VERIFIER_nondet_int();
472494

473-
#if !defined(__linux__) || defined(__GLIBC__)
474-
(void)*stream;
475-
#else
476-
(void)*(char*)stream;
477-
#endif
495+
if(stream != stdin && stream != stdout && stream != stderr)
496+
{
497+
#if !defined(__linux__) || defined(__GLIBC__)
498+
(void)*stream;
499+
#else
500+
(void)*(char *)stream;
501+
#endif
502+
}
478503

479504
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
480505
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -497,11 +522,16 @@ inline int fgetc(FILE *stream)
497522
{
498523
__CPROVER_HIDE:;
499524
int return_value=__VERIFIER_nondet_int();
500-
#if !defined(__linux__) || defined(__GLIBC__)
501-
(void)*stream;
502-
#else
503-
(void)*(char*)stream;
504-
#endif
525+
526+
if(stream != stdin)
527+
{
528+
#if !defined(__linux__) || defined(__GLIBC__)
529+
(void)*stream;
530+
#else
531+
(void)*(char *)stream;
532+
#endif
533+
}
534+
505535
// it's a byte or EOF (-1)
506536
__CPROVER_assume(return_value>=-1 && return_value<=255);
507537

@@ -529,11 +559,14 @@ inline int getc(FILE *stream)
529559
__CPROVER_HIDE:;
530560
int return_value=__VERIFIER_nondet_int();
531561

532-
#if !defined(__linux__) || defined(__GLIBC__)
533-
(void)*stream;
534-
#else
535-
(void)*(char*)stream;
536-
#endif
562+
if(stream != stdin)
563+
{
564+
#if !defined(__linux__) || defined(__GLIBC__)
565+
(void)*stream;
566+
#else
567+
(void)*(char *)stream;
568+
#endif
569+
}
537570

538571
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
539572
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -581,11 +614,14 @@ inline int getw(FILE *stream)
581614
__CPROVER_HIDE:;
582615
int return_value=__VERIFIER_nondet_int();
583616

584-
#if !defined(__linux__) || defined(__GLIBC__)
585-
(void)*stream;
586-
#else
587-
(void)*(char*)stream;
588-
#endif
617+
if(stream != stdin)
618+
{
619+
#if !defined(__linux__) || defined(__GLIBC__)
620+
(void)*stream;
621+
#else
622+
(void)*(char *)stream;
623+
#endif
624+
}
589625

590626
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
591627
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -698,11 +734,14 @@ size_t fwrite(
698734
(void)*(char*)ptr;
699735
(void)size;
700736

701-
#if !defined(__linux__) || defined(__GLIBC__)
702-
(void)*stream;
703-
#else
704-
(void)*(char*)stream;
705-
#endif
737+
if(stream != stdout && stream != stderr)
738+
{
739+
#if !defined(__linux__) || defined(__GLIBC__)
740+
(void)*stream;
741+
#else
742+
(void)*(char *)stream;
743+
#endif
744+
}
706745

707746
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
708747
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -821,11 +860,16 @@ inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list a
821860
{
822861
__CPROVER_HIDE:;
823862
int result=__VERIFIER_nondet_int();
824-
#if !defined(__linux__) || defined(__GLIBC__)
825-
(void)*stream;
826-
#else
827-
(void)*(char*)stream;
828-
#endif
863+
864+
if(stream != stdin)
865+
{
866+
#if !defined(__linux__) || defined(__GLIBC__)
867+
(void)*stream;
868+
#else
869+
(void)*(char *)stream;
870+
#endif
871+
}
872+
829873
(void)*format;
830874
(void)arg;
831875

@@ -921,11 +965,15 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
921965

922966
int result=__VERIFIER_nondet_int();
923967

924-
#if !defined(__linux__) || defined(__GLIBC__)
925-
(void)*stream;
926-
#else
927-
(void)*(char*)stream;
928-
#endif
968+
if(stream != stdout && stream != stderr)
969+
{
970+
#if !defined(__linux__) || defined(__GLIBC__)
971+
(void)*stream;
972+
#else
973+
(void)*(char *)stream;
974+
#endif
975+
}
976+
929977
(void)*format;
930978
(void)arg;
931979

0 commit comments

Comments
 (0)