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.

Author: tautschnig

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

@@ -3,14 +3,10 @@
 
 int main()
 {
-  // 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);
+  if(some_file)
+    assert(fileno(some_file) >= -1);
 
   return 0;
 }

src/ansi-c/library/stdio.c

@@ -6,15 +6,7 @@
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
-#if defined(__OpenBSD__)
-#undef getchar
 #undef putchar
-#undef getc
-#undef feof
-#undef ferror
-#undef fileno
-#endif
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
@@ -213,25 +205,80 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+#ifndef _WIN32
+FILE *stdin;
+FILE *stdout;
+FILE *stderr;
+#endif
+
 FILE *fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)handle;
+    if(handle < 0)
+    {
+      errno = EBADF;
+      return NULL;
+    }
   (void)*mode;
 #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
 #endif
 
-#if !defined(__linux__) || defined(__GLIBC__)
+#ifndef _WIN32
+  FILE **f_alias = NULL;
+  switch(handle)
+  {
+  case 0:
+    f_alias = &stdin;
+    break;
+  case 1:
+    f_alias = &stdout;
+    break;
+  case 2:
+    f_alias = &stderr;
+    break;
+  }
+
+  if(f_alias != NULL && *f_alias != NULL)
+  {
+    __CPROVER_assume(fileno(*f_alias) == handle);
+    return *f_alias;
+  }
+#  if !defined(__linux__) || defined(__GLIBC__)
   FILE *f=malloc(sizeof(FILE));
 #else
-  // libraries need to expose the definition of FILE; this is the
+  // libraries need not expose the definition of FILE; this is the
   // case for musl
   FILE *f=malloc(sizeof(int));
 #endif
+  if(f_alias != NULL)
+    *f_alias = f;
+  __CPROVER_assume(fileno(f) == handle);
 
   return f;
+#else
+  switch(handle)
+  {
+  case 0:
+    return stdin;
+  case 1:
+    return stdout;
+  case 2:
+    return stderr;
+  default:
+  {
+    FILE *f = malloc(sizeof(FILE));
+    __CPROVER_assume(fileno(f) == handle);
+    return f;
+  }
+  }
+#endif
 }
 
 /* FUNCTION: _fdopen */
@@ -251,18 +298,56 @@ FILE *fdopen(int handle, const char *mode)
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 #ifdef __APPLE__
+
+#  ifndef LIBRARY_CHECK
+FILE *stdin;
+FILE *stdout;
+FILE *stderr;
+#  endif
+
 FILE *_fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)handle;
+    if(handle < 0)
+    {
+      errno = EBADF;
+      return NULL;
+    }
   (void)*mode;
 #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
 #endif
 
+  FILE **f_alias = NULL;
+  switch(handle)
+  {
+  case 0:
+    f_alias = &stdin;
+    break;
+  case 1:
+    f_alias = &stdout;
+    break;
+  case 2:
+    f_alias = &stderr;
+    break;
+  }
+
+  if(f_alias != NULL && *f_alias != NULL)
+  {
+    __CPROVER_assume(fileno(*f_alias) == handle);
+    return *f_alias;
+  }
   FILE *f=malloc(sizeof(FILE));
+  if(f_alias != NULL)
+    *f_alias = f;
+  __CPROVER_assume(fileno(f) == handle);
 
   return f;
 }
@@ -466,6 +551,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef feof
+
 int __VERIFIER_nondet_int(void);
 
 int feof(FILE *stream)
@@ -498,6 +585,8 @@ int feof(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef ferror
+
 int __VERIFIER_nondet_int(void);
 
 int ferror(FILE *stream)
@@ -530,6 +619,8 @@ int ferror(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef fileno
+
 int __VERIFIER_nondet_int(void);
 
 int fileno(FILE *stream)
@@ -695,6 +786,8 @@ int fgetc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef getc
+
 int __VERIFIER_nondet_int(void);
 
 int getc(FILE *stream)
@@ -731,6 +824,8 @@ int getc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef getchar
+
 int __VERIFIER_nondet_int(void);
 
 int getchar(void)
@@ -1593,20 +1688,31 @@ int vasprintf(char **ptr, const char *fmt, va_list ap)
 #    define __CPROVER_STDIO_H_INCLUDED
 #  endif
 
+#  ifndef __CPROVER_STDLIB_H_INCLUDED
+#    include <stdlib.h>
+#    define __CPROVER_STDLIB_H_INCLUDED
+#  endif
+
 FILE *__acrt_iob_func(unsigned fd)
 {
-  static FILE stdin_file;
-  static FILE stdout_file;
-  static FILE stderr_file;
+  static FILE *stdin_file;
+  static FILE *stdout_file;
+  static FILE *stderr_file;
 
   switch(fd)
   {
   case 0:
-    return &stdin_file;
+    if(!stdin_file)
+      stdin_file = malloc(sizeof(FILE));
+    return stdin_file;
   case 1:
-    return &stdout_file;
+    if(!stdout_file)
+      stdout_file = malloc(sizeof(FILE));
+    return stdout_file;
   case 2:
-    return &stderr_file;
+    if(!stderr_file)
+      stderr_file = malloc(sizeof(FILE));
+    return stderr_file;
   default:
     return (FILE *)0;
   }