[infer][PR] Fix getcwd model to allow NULL argument

Summary:
The model for `getcwd` assumes the first argument should be non-null when in fact a NULL pointer is legitimate and results in allocation:

>       As  an  extension to the POSIX.1-2001 standard, glibc's getcwd() allocates the buffer dynamically using mal‐
>       loc(3) if buf is NULL.  In this case, the allocated buffer has the length size unless size is zero, when buf
>       is allocated as big as necessary.  The caller should free(3) the returned buffer.

I suggest this glibc extension be used for the getcwd model to reduce false positives.
Pull Request resolved: https://github.com/facebook/infer/pull/925

Reviewed By: mbouaziz

Differential Revision: D9830450

Pulled By: jvillard

fbshipit-source-id: 95c4862b1

infer/models/c/src/libc_basic.c

@@ -642,6 +642,16 @@ int fputc(int c, FILE* stream) {
 char* getcwd(char* buffer, size_t size) {
   int n;
   int size_buf;
+  char* result;
+
+  if (buffer == NULL) {
+    if (size == 0) {
+      n = __infer_nondet_int();
+    } else {
+      n = size;
+    }
+    return (char*)malloc(n);
+  } else {
     n = __infer_nondet_int();
 
     if (n > 0) {
@@ -649,8 +659,10 @@ char* getcwd(char* buffer, size_t size) {
       size_buf = __get_array_length(buffer);
       INFER_EXCLUDE_CONDITION(size > size_buf);
       return buffer;
-  } else
+    } else {
       return NULL;
+    }
+  }
 }
 
 // return nonteterministically 0 or -1

infer/tests/codetoanalyze/c/errors/issues.exp

@@ -71,6 +71,9 @@ codetoanalyze/c/errors/null_dereference/getc.c, crash_putc, 4, NULL_DEREFERENCE,
 codetoanalyze/c/errors/null_dereference/getc.c, crash_rewind, 4, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/getc.c, crash_ungetc, 5, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/getc.c, crash_vfprintf, 5, NULL_DEREFERENCE, B1
+codetoanalyze/c/errors/null_dereference/getcwd.c, getcwd_no_buf_no_check_bad, 2, NULL_DEREFERENCE, B1
+codetoanalyze/c/errors/null_dereference/getcwd.c, getcwd_no_buf_no_free_bad, 3, MEMORY_LEAK, no_bucket
+codetoanalyze/c/errors/null_dereference/getcwd.c, getcwd_no_check_bad, 3, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref2_bad, 0, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref_bad, 0, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref_bad_FN, 0, PRECONDITION_NOT_MET, no_bucket

infer/tests/codetoanalyze/c/errors/null_dereference/getcwd.c

@@ -0,0 +1,45 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <unistd.h>
+
+#define BUFFER_SIZE 16
+
+char getcwd_ok() {
+  char* cwd = getcwd(NULL, 0);
+  if (cwd != NULL) {
+    char result = cwd[0];
+    free(cwd);
+    return result;
+  }
+  char buf[BUFFER_SIZE];
+  cwd = getcwd(&buf, BUFFER_SIZE);
+  if (cwd != NULL) {
+    return cwd[0];
+  }
+  return 'a';
+}
+
+char getcwd_no_buf_no_check_bad() {
+  char* cwd = getcwd(NULL, 0);
+  char result = cwd[0];
+  free(cwd);
+  return result;
+}
+
+char getcwd_no_buf_no_free_bad() {
+  char* cwd = getcwd(NULL, 0);
+  if (cwd != NULL) {
+    return cwd[0];
+  }
+  return 'a';
+}
+
+char getcwd_no_check_bad() {
+  char buf[BUFFER_SIZE];
+  char* cwd = getcwd(&buf, BUFFER_SIZE);
+  return cwd[0];
+}