Merge pull request #1167 from tautschnig/c-library-ext

C library modelling: fgets, getopt, vasprintf

Author: kroening

regression/cbmc/fgets1/main.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  char buffer[3]={'a', 'b', '\0'};
+  FILE *f=fdopen(0, "r");
+  if(!f)
+    return 1;
+
+  char *p=fgets(buffer, 3, f);
+  if(p)
+  {
+    assert(buffer[1]==p[1]);
+    assert(buffer[2]=='\0');
+    assert(p[1]=='b'); // expected to fail
+  }
+
+  fclose(f);
+
+  return 0;
+}

regression/cbmc/fgets1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
+\*\* 1 of 38 failed \(2 iterations\)
+--
+^warning: ignoring

src/ansi-c/library/getopt.c

@@ -3,22 +3,67 @@
 extern char *optarg;
 extern int optind;
 
+#ifndef __CPROVER_STRING_H_INCLUDED
+#include <string.h>
+#define __CPROVER_STRING_H_INCLUDED
+#endif
+
 inline int getopt(int argc, char * const argv[],
                   const char *optstring)
 {
   __CPROVER_HIDE:;
-  int result_index;
-  __CPROVER_assume(result_index>=0);
-  (void)*optstring;
-  if(optind>=argc)
+  int result=-1;
+
+  if(optind==0)
+    optind=1;
+
+  if(optind>=argc || argv[optind][0]!='-')
     return -1;
-  __CPROVER_assume(result_index<argc && result_index>=optind);
+
+  size_t result_index;
+  __CPROVER_assume(
+    result_index<strlen(optstring) && optstring[result_index]!=':');
   #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(optstring),
     "getopt zero-termination of 3rd argument");
   #endif
-  optarg = argv[result_index];
-  optind = result_index+1;
-  int retval;
-  return retval;
+
+  _Bool found;
+  if(found)
+  {
+    result=optstring[result_index];
+    if(skipped)
+      ++optind;
+  }
+
+  if(result!=-1 && optind<argc && optstring[result_index+1]==':')
+  {
+    _Bool has_no_arg;
+    if(has_no_arg)
+    {
+      optarg=argv[optind];
+      ++optind;
+    }
+    else
+      optarg=NULL;
+  }
+
+  return result;
+}
+
+/* FUNCTION: getopt_long */
+
+int getopt(int argc, char * const argv[], const char *optstring);
+
+inline int getopt_long(int argc, char * const argv[], const char *optstring,
+                const struct option *longopts, int *longindex)
+{
+  // trigger valid-pointer checks (if enabled), even though we don't
+  // use the parameter in this model
+  (void)*longopts;
+  // avoid unused-parameter warnings when compiling using GCC (for
+  // internal library syntax checks)
+  (void)longindex;
+
+  return getopt(argc, argv, optstring);
 }

src/ansi-c/library/stdio.c

@@ -65,7 +65,14 @@ inline FILE *fopen(const char *filename, const char *mode)
   FILE *fopen_result;
 
   _Bool fopen_error;
+
+  #if !defined(__linux__) || defined(__GLIBC__)
   fopen_result=fopen_error?NULL:malloc(sizeof(FILE));
+  #else
+  // libraries need to expose the definition of FILE; this is the
+  // case for musl
+  fopen_result=fopen_error?NULL:malloc(sizeof(int));
+  #endif
 
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_set_must(fopen_result, "open");
@@ -99,6 +106,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
 inline int fclose(FILE *stream)
 {
   __CPROVER_HIDE:;
@@ -135,19 +147,56 @@ inline FILE *fdopen(int handle, const char *mode)
     "fdopen zero-termination of 2nd argument");
   #endif
 
+  #if !defined(__linux__) || defined(__GLIBC__)
   FILE *f=malloc(sizeof(FILE));
+  #else
+  // libraries need to expose the definition of FILE; this is the
+  // case for musl
+  FILE *f=malloc(sizeof(int));
+  #endif
 
   return f;
 }
 
+/* FUNCTION: _fdopen */
+
+// This is for Apple
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#include <stdio.h>
+#define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+#ifdef __APPLE__
+inline FILE *_fdopen(int handle, const char *mode)
+{
+  __CPROVER_HIDE:;
+  (void)handle;
+  (void)*mode;
+  #ifdef __CPROVER_STRING_ABSTRACTION
+  __CPROVER_assert(__CPROVER_is_zero_string(mode),
+    "fdopen zero-termination of 2nd argument");
+  #endif
+
+  FILE *f=malloc(sizeof(FILE));
+
+  return f;
+}
+#endif
+
 /* FUNCTION: fgets */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
 #include <stdio.h>
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-inline char *fgets(char *str, int size, FILE *stream)
+char *fgets(char *str, int size, FILE *stream)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error;
@@ -169,6 +218,16 @@ inline char *fgets(char *str, int size, FILE *stream)
     __CPROVER_is_zero_string(str)=!error;
     __CPROVER_zero_string_length(str)=resulting_size;
   }
+  #else
+  if(size>0)
+  {
+    int str_length;
+    __CPROVER_assume(str_length>=0 && str_length<size);
+    char contents_nondet[str_length];
+    __CPROVER_array_replace(str, contents_nondet);
+    if(!error)
+      str[str_length]='\0';
+  }
   #endif
 
   return error?0:str;
@@ -735,3 +794,43 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg)
 
   return result;
 }
+
+/* FUNCTION: vasprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#include <stdio.h>
+#define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#include <stdarg.h>
+#define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+inline int vasprintf(char **ptr, const char *fmt, va_list ap)
+{
+  (void)*fmt;
+  (void)ap;
+
+  int result_buffer_size;
+  if(result_buffer_size<=0)
+    return -1;
+
+  *ptr=malloc(result_buffer_size);
+  for(int i=0; i<result_buffer_size; ++i)
+  {
+    char c;
+    (*ptr)[i]=c;
+    if(c=='\0')
+      break;
+  }
+
+  __CPROVER_assume(i<result_buffer_size);
+
+  return i;
+}