C library: fix and test getopt model

Remove non-determinism from the model to avoid spurious counterexamples.
Also, make _getopt available, which is macOS' renamed version of getopt.

Author: tautschnig

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

@@ -1,9 +1,34 @@
 #include <assert.h>
-#include <getopt.h>
+#ifndef _WIN32
+#  include <getopt.h>
+#else
+extern char *optarg;
+extern int optind;
+int getopt(int argc, char *const argv[], const char *optstring);
+#endif
+#include <stdlib.h>
 
 int main()
 {
-  getopt();
-  assert(0);
+  int argc = 3;
+  char *argv[] = {"my_program", "-t", "10", NULL};
+
+  int opt;
+  int nsecs = 0;
+
+  while((opt = getopt(argc, argv, "t:")) != -1)
+  {
+    switch(opt)
+    {
+    case 't':
+      nsecs = atoi(optarg);
+      break;
+    default: /* '?' */
+      return 1;
+    }
+  }
+
+  assert(nsecs == 10);
+
   return 0;
 }

regression/cbmc-library/getopt-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --unwind 3 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/library/getopt.c

@@ -1,61 +1,94 @@
-/* FUNCTION: getopt */
-
-extern char *optarg;
-extern int optind;
+/* FUNCTION: _getopt */
 
 #ifndef __CPROVER_STRING_H_INCLUDED
 #include <string.h>
 #define __CPROVER_STRING_H_INCLUDED
 #endif
 
+char *optarg = NULL;
+int optind = 1;
+
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 size_t __VERIFIER_nondet_size_t(void);
 
-int getopt(int argc, char *const argv[], const char *optstring)
+int _getopt(int argc, char *const argv[], const char *optstring)
 {
-  __CPROVER_HIDE:;
-  int result=-1;
-
-  if(optind==0)
-    optind=1;
+__CPROVER_HIDE:;
+  // re-init requested by environment, we just reset optind
+  if(optind == 0)
+    optind = 1;
 
-  if(optind>=argc || argv[optind][0]!='-')
+  // test whether all arguments have been processed
+  if(optind >= argc)
+    return -1;
+  char *const arg = argv[optind];
+  if(arg[0] != '-' || arg[1] == '\0' || (arg[1] == '-' && arg[2] == '\0'))
     return -1;
 
-  size_t result_index=__VERIFIER_nondet_size_t();
+  // test whether the option is in optstring at all
+  size_t optstring_len = strlen(optstring);
+  // gcc doesn't know __CPROVER_forall
+#ifndef LIBRARY_CHECK
+  __CPROVER_bool not_found = __CPROVER_forall
+  {
+    size_t i;
+    i<optstring_len ==> optstring[i] != arg[1]
+  };
+  if(not_found)
+    return '?';
+#endif
+
+  // option is in optstring, find the exact index
+  size_t result_index = __VERIFIER_nondet_size_t();
   __CPROVER_assume(
-    result_index<strlen(optstring) && optstring[result_index]!=':');
-  #ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(optstring),
+    result_index < optstring_len && optstring[result_index] == arg[1]);
+#ifdef __CPROVER_STRING_ABSTRACTION
+  __CPROVER_assert(
+    __CPROVER_is_zero_string(optstring),
     "getopt zero-termination of 3rd argument");
-  #endif
+#endif
 
-  __CPROVER_bool found=__VERIFIER_nondet___CPROVER_bool();
-  if(found)
+  // is an argument required?
+  if(result_index + 1 == optstring_len || optstring[result_index + 1] != ':')
   {
-    result=optstring[result_index];
-    __CPROVER_bool skipped=__VERIFIER_nondet___CPROVER_bool();
-    if(skipped)
-      ++optind;
+    optarg = NULL;
+    return arg[1];
   }
 
-  if(result!=-1 && optind<argc && optstring[result_index+1]==':')
+  // test whether a required argument can be found
+  if(arg[2] != '\0')
+  {
+    optarg = &arg[2];
+    return arg[1];
+  }
+  else if(optind + 1 < argc)
   {
-    __CPROVER_bool has_no_arg=__VERIFIER_nondet___CPROVER_bool();
-    if(has_no_arg)
-    {
-      optarg=argv[optind];
-      ++optind;
-    }
-    else
-      optarg=NULL;
+    optarg = argv[optind + 1];
+    ++optind;
+    return arg[1];
   }
+  else
+  {
+    optarg = NULL;
+    return optstring[0] == ':' ? ':' : '?';
+  }
+}
+
+/* FUNCTION: getopt */
+
+int _getopt(int argc, char *const argv[], const char *optstring);
 
-  return result;
+int getopt(int argc, char *const argv[], const char *optstring)
+{
+__CPROVER_HIDE:;
+  return _getopt(argc, argv, optstring);
 }
 
 /* FUNCTION: getopt_long */
 
+#ifndef _WIN32
+// MSVC doesn't provide getopt.h, which we need for struct option
+
 #ifndef __CPROVER_GETOPT_H_INCLUDED
 #include <getopt.h>
 #define __CPROVER_GETOPT_H_INCLUDED
@@ -77,3 +110,5 @@ int getopt_long(
 
   return getopt(argc, argv, optstring);
 }
+
+#endif

src/ansi-c/library_check.sh

@@ -32,6 +32,7 @@ perl -p -i -e 's/^__CPROVER_contracts_library\n//' __functions
 # Some functions are implicitly covered by running on different operating
 # systems:
 perl -p -i -e 's/^_fopen\n//' __functions # fopen, macOS
+perl -p -i -e 's/^_getopt\n//' __functions # getopt, macOS
 perl -p -i -e 's/^_mmap\n//' __functions # mmap, macOS
 perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
 perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS