Skip to content

Commit 2d73775

Browse files
tautschnigtautschnig
committed
C library: Refine and improve stdio models
Fixes portability to FreeBSD, which redefines several functions as macros that would only conditionally call that function. Also, ensure that stdin/stdout/stderr point to valid objects when those are fdopen'ed.
1 parent a93cf38 commit 2d73775

6 files changed

Lines changed: 146 additions & 24 deletions

File tree

‎.github/workflows/bsd.yaml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ jobs:
6666
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
6767
echo "Run regression tests"
6868
gmake -C regression/cbmc test
69+
gmake -C regression/cbmc-library test
6970
# gmake -C regression test-parallel JOBS=2
7071
# gmake -C regression/cbmc test-paths-lifo
7172
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
@@ -128,6 +129,10 @@ jobs:
128129
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
129130
echo "Run regression tests"
130131
gmake -C regression/cbmc test
132+
# TODO: fileno and *fprintf tests are failing, requires debugging
133+
# https://github.com/openbsd/src/blob/master/include/stdio.h may be
134+
# useful (likely need to allocate __sF)
135+
gmake -C regression/cbmc-library test || true
131136
# gmake -C regression test-parallel JOBS=2
132137
# gmake -C regression/cbmc test-paths-lifo
133138
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
@@ -193,6 +198,7 @@ jobs:
193198
echo "Run regression tests"
194199
# TODO: we need to model some more library functions
195200
gmake -C regression/cbmc test || true
201+
gmake -C regression/cbmc-library test || true
196202
# gmake -C regression test-parallel JOBS=2
197203
# gmake -C regression/cbmc test-paths-lifo
198204
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2

‎regression/cbmc-library/fileno/main.c‎

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

44
int main()
55
{
6-
// requires initialization of stdin/stdout/stderr
7-
// assert(fileno(stdin) == 0);
8-
// assert(fileno(stdout) == 1);
9-
// assert(fileno(stderr) == 2);
10-
116
int fd;
127
FILE *some_file = fdopen(fd, "");
13-
assert(fileno(some_file) >= -1);
8+
if(some_file)
9+
assert(fileno(some_file) >= -1);
1410

1511
return 0;
1612
}

‎regression/cbmc-library/tolower/main.c‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,12 @@
33

44
int main()
55
{
6+
#if !defined(__FreeBSD__) && !defined(__OpenBSD__) && !defined(__NetBSD__)
7+
// We would need to model conversion tables, where each of the BSDs has their
8+
// peculiar approach.
69
int x;
710
int r = tolower(x);
811
assert(r >= x);
12+
#endif
913
return 0;
1014
}

‎regression/cbmc-library/toupper/main.c‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,12 @@
33

44
int main()
55
{
6+
#if !defined(__FreeBSD__) && !defined(__OpenBSD__) && !defined(__NetBSD__)
7+
// We would need to model conversion tables, where each of the BSDs has their
8+
// peculiar approach.
69
int x;
710
int r = toupper(x);
811
assert(r <= x);
12+
#endif
913
return 0;
1014
}

‎regression/contracts-dfcc/variant_multidimensional_ackermann/main.c‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@ int main()
88
int n = 5;
99
int result = ackermann(m, n);
1010

11-
printf("Result of the Ackermann function: %d\n", result);
11+
// we don't currently have contracts on what printf is assigning to
12+
// printf("Result of the Ackermann function: %d\n", result);
1213
return 0;
1314
}
1415

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

Lines changed: 128 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,7 @@
66
#define __CPROVER_STDIO_H_INCLUDED
77
#endif
88

9-
/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
10-
#if defined(__OpenBSD__)
11-
#undef getchar
129
#undef putchar
13-
#undef getc
14-
#undef feof
15-
#undef ferror
16-
#undef fileno
17-
#endif
1810

1911
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
2012

@@ -237,7 +229,8 @@ __CPROVER_HIDE:;
237229
__CPROVER_set_must(stream, "closed");
238230
#endif
239231
int return_value=__VERIFIER_nondet_int();
240-
free(stream);
232+
if(stream != stdin && stream != stdout && stream != stderr)
233+
free(stream);
241234
return return_value;
242235
}
243236

@@ -253,25 +246,87 @@ __CPROVER_HIDE:;
253246
#define __CPROVER_STDLIB_H_INCLUDED
254247
#endif
255248

249+
#ifndef __CPROVER_ERRNO_H_INCLUDED
250+
# include <errno.h>
251+
# define __CPROVER_ERRNO_H_INCLUDED
252+
#endif
253+
256254
FILE *fdopen(int handle, const char *mode)
257255
{
258256
__CPROVER_HIDE:;
259-
(void)handle;
257+
if(handle < 0)
258+
{
259+
errno = EBADF;
260+
return NULL;
261+
}
260262
(void)*mode;
261263
#ifdef __CPROVER_STRING_ABSTRACTION
262264
__CPROVER_assert(__CPROVER_is_zero_string(mode),
263265
"fdopen zero-termination of 2nd argument");
264266
#endif
265267

266-
#if !defined(__linux__) || defined(__GLIBC__)
267-
FILE *f=malloc(sizeof(FILE));
268+
#if defined(_WIN32) || defined(__OpenBSD__) || defined(__NetBSD__)
269+
switch(handle)
270+
{
271+
case 0:
272+
return stdin;
273+
case 1:
274+
return stdout;
275+
case 2:
276+
return stderr;
277+
default:
278+
{
279+
FILE *f = malloc(sizeof(FILE));
280+
if(f == NULL)
281+
return NULL;
282+
__CPROVER_assume(fileno(f) == handle);
283+
return f;
284+
}
285+
}
268286
#else
269-
// libraries need to expose the definition of FILE; this is the
287+
# if !defined(__linux__) || defined(__GLIBC__)
288+
static FILE stdin_file;
289+
static FILE stdout_file;
290+
static FILE stderr_file;
291+
# else
292+
// libraries need not expose the definition of FILE; this is the
270293
// case for musl
271-
FILE *f=malloc(sizeof(int));
272-
#endif
294+
static int stdin_file;
295+
static int stdout_file;
296+
static int stderr_file;
297+
# endif
298+
299+
FILE *f = NULL;
300+
switch(handle)
301+
{
302+
case 0:
303+
stdin = &stdin_file;
304+
__CPROVER_havoc_object(&stdin_file);
305+
f = &stdin_file;
306+
break;
307+
case 1:
308+
stdout = &stdout_file;
309+
__CPROVER_havoc_object(&stdout_file);
310+
f = &stdout_file;
311+
break;
312+
case 2:
313+
stderr = &stderr_file;
314+
__CPROVER_havoc_object(&stderr_file);
315+
f = &stderr_file;
316+
break;
317+
default:
318+
# if !defined(__linux__) || defined(__GLIBC__)
319+
f = malloc(sizeof(FILE));
320+
# else
321+
f = malloc(sizeof(int));
322+
# endif
323+
}
273324

325+
if(f == NULL)
326+
return NULL;
327+
__CPROVER_assume(fileno(f) == handle);
274328
return f;
329+
#endif
275330
}
276331

277332
/* FUNCTION: _fdopen */
@@ -291,19 +346,62 @@ FILE *fdopen(int handle, const char *mode)
291346
#define __CPROVER_STDLIB_H_INCLUDED
292347
#endif
293348

349+
#ifndef __CPROVER_ERRNO_H_INCLUDED
350+
# include <errno.h>
351+
# define __CPROVER_ERRNO_H_INCLUDED
352+
#endif
353+
294354
#ifdef __APPLE__
355+
356+
# ifndef LIBRARY_CHECK
357+
FILE *stdin;
358+
FILE *stdout;
359+
FILE *stderr;
360+
# endif
361+
295362
FILE *_fdopen(int handle, const char *mode)
296363
{
297364
__CPROVER_HIDE:;
298-
(void)handle;
365+
if(handle < 0)
366+
{
367+
errno = EBADF;
368+
return NULL;
369+
}
299370
(void)*mode;
300371
#ifdef __CPROVER_STRING_ABSTRACTION
301372
__CPROVER_assert(__CPROVER_is_zero_string(mode),
302373
"fdopen zero-termination of 2nd argument");
303374
#endif
304375

305-
FILE *f=malloc(sizeof(FILE));
376+
static FILE stdin_file;
377+
static FILE stdout_file;
378+
static FILE stderr_file;
379+
380+
FILE *f = NULL;
381+
switch(handle)
382+
{
383+
case 0:
384+
stdin = &stdin_file;
385+
__CPROVER_havoc_object(&stdin_file);
386+
f = &stdin_file;
387+
break;
388+
case 1:
389+
stdout = &stdout_file;
390+
__CPROVER_havoc_object(&stdout_file);
391+
f = &stdout_file;
392+
break;
393+
case 2:
394+
stderr = &stderr_file;
395+
__CPROVER_havoc_object(&stderr_file);
396+
f = &stderr_file;
397+
break;
398+
default:
399+
f = malloc(sizeof(FILE));
400+
}
306401

402+
if(f == NULL)
403+
return NULL;
404+
__CPROVER_assume(fileno(f) == handle);
307405
return f;
308406
}
309407
#endif
@@ -506,6 +604,8 @@ __CPROVER_HIDE:;
506604
#define __CPROVER_STDIO_H_INCLUDED
507605
#endif
508606

607+
#undef feof
608+
509609
int __VERIFIER_nondet_int(void);
510610

511611
int feof(FILE *stream)
@@ -538,6 +638,8 @@ int feof(FILE *stream)
538638
#define __CPROVER_STDIO_H_INCLUDED
539639
#endif
540640

641+
#undef ferror
642+
541643
int __VERIFIER_nondet_int(void);
542644

543645
int ferror(FILE *stream)
@@ -570,6 +672,8 @@ int ferror(FILE *stream)
570672
#define __CPROVER_STDIO_H_INCLUDED
571673
#endif
572674

675+
#undef fileno
676+
573677
int __VERIFIER_nondet_int(void);
574678

575679
int fileno(FILE *stream)
@@ -735,6 +839,8 @@ int fgetc(FILE *stream)
735839
#define __CPROVER_STDIO_H_INCLUDED
736840
#endif
737841

842+
#undef getc
843+
738844
int __VERIFIER_nondet_int(void);
739845

740846
int getc(FILE *stream)
@@ -771,6 +877,8 @@ int getc(FILE *stream)
771877
#define __CPROVER_STDIO_H_INCLUDED
772878
#endif
773879

880+
#undef getchar
881+
774882
int __VERIFIER_nondet_int(void);
775883

776884
int getchar(void)
@@ -1939,10 +2047,13 @@ FILE *__acrt_iob_func(unsigned fd)
19392047
switch(fd)
19402048
{
19412049
case 0:
2050+
__CPROVER_havoc_object(&stdin_file);
19422051
return &stdin_file;
19432052
case 1:
2053+
__CPROVER_havoc_object(&stdout_file);
19442054
return &stdout_file;
19452055
case 2:
2056+
__CPROVER_havoc_object(&stderr_file);
19462057
return &stderr_file;
19472058
default:
19482059
return (FILE *)0;

0 commit comments

Comments
 (0)