[pulse] a directory stream created by fdopendir owns its descriptor

infer/src/pulse/PulseModelsC.ml

@@ -306,6 +306,16 @@ include struct
     @@ fun () -> check_valid mode @@> Basic.free FClose fd @@> ret_alloc_or_null FileDescriptor
 
 
+  (* the returned stream owns [fd] and [closedir] releases it, but a failure leaves [fd] with the
+     caller *)
+  let fdopendir fd : model =
+    start_model
+    @@ fun () ->
+    disj
+      [ assign_ret @= null
+      ; Basic.free FClose fd @@> Basic.return_alloc_not_null FileDescriptor None ~initialize:true ]
+
+
   let opendir path : model =
     start_model @@ fun () -> check_valid path @@> ret_alloc_or_null FileDescriptor
 
@@ -638,6 +648,7 @@ let matchers : matcher list =
     $--> compose1 (ignore_arg @@ start_model @@ null_or_nonneg_non_det_ret) taint_ret_from_arg
   ; -"fclose" <>$ capt_arg $--> fclose
   ; -"fdopen" <>$ capt_arg $+ capt_arg_payload $--> fdopen
+  ; -"fdopendir" <>$ capt_arg $--> fdopendir
   ; -"feof" <>$ capt_arg_payload $--> compose1 valid_arg (ignore_arg non_det_ret)
   ; -"ferror" <>$ capt_arg_payload $--> compose1 valid_arg (ignore_arg non_det_ret)
   ; -"fgetc" <>$ capt_arg_payload

infer/tests/codetoanalyze/c/pulse/fdopendir.c

@@ -0,0 +1,63 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <dirent.h>
+#include <fcntl.h>
+#include <unistd.h>
+
+// the stream returned by fdopendir() owns the descriptor, and closedir()
+// releases it, so there is nothing left to close here
+int fdopendirClosed_ok() {
+  int fd = open("mydir", O_RDONLY);
+  if (fd < 0) {
+    return -1;
+  }
+  DIR* dir = fdopendir(fd);
+  if (!dir) {
+    close(fd);
+    return -1;
+  }
+  closedir(dir);
+  return 0;
+}
+
+// the new owner of the descriptor is dropped without being closed
+int fdopendirNotClosed_bad() {
+  int fd = open("mydir", O_RDONLY);
+  if (fd < 0) {
+    return -1;
+  }
+  DIR* dir = fdopendir(fd);
+  if (!dir) {
+    close(fd);
+    return -1;
+  }
+  return 0;
+}
+
+// fdopendir() failed, so the descriptor is still the caller's to close
+int fdopendirFailed_bad() {
+  int fd = open("mydir", O_RDONLY);
+  if (fd < 0) {
+    return -1;
+  }
+  DIR* dir = fdopendir(fd);
+  if (!dir) {
+    return -1;
+  }
+  closedir(dir);
+  return 0;
+}
+
+// no stream is involved at all
+int fdopendirDescriptorLeaked_bad() {
+  int fd = open("mydir", O_RDONLY);
+  if (fd < 0) {
+    return -1;
+  }
+  return 0;
+}

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

@@ -45,6 +45,9 @@ codetoanalyze/c/pulse/eternal-even.c, FN_inf_rec_deep_bad, 4, MUTUAL_RECURSION_C
 codetoanalyze/c/pulse/eternal-even.c, inf_rec_deep_ok, 2, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`inf_rec_deep_ok` makes a recursive call to `inf_rec_deep_ok`]
 codetoanalyze/c/pulse/eternal-list.c, FP_xmlListSize_ok, 6, INFINITE_LOOP, no_bucket, WARNING, [in loop]
 codetoanalyze/c/pulse/exit_example.c, exit_example_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/fdopendir.c, fdopendirNotClosed_bad, 6, PULSE_RESOURCE_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `fopen()` here,file descriptor becomes unreachable here]
+codetoanalyze/c/pulse/fdopendir.c, fdopendirFailed_bad, 5, PULSE_RESOURCE_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `fopen()` here,file descriptor becomes unreachable here]
+codetoanalyze/c/pulse/fdopendir.c, fdopendirDescriptorLeaked_bad, 2, PULSE_RESOURCE_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `fopen()` here,file descriptor becomes unreachable here]
 codetoanalyze/c/pulse/field_taint.c, test_taint_field_bad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: field `manipulated` of value passed as argument `#0` to `taint_manipulated` with kind `Simple`,flows to this sink: value passed as argument `#0` to `sink_int` with kind `Simple`], source: taint_manipulated, sink: sink_int, tainted expression: s.manipulated
 codetoanalyze/c/pulse/field_taint.c, test_sink_field_bad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `int_source` with kind `Simple`,flows to this sink: field `manipulated` of value passed as argument `#0` to `sink_manipulated` with kind `Simple`], source: int_source, sink: sink_manipulated, tainted expression: s.manipulated
 codetoanalyze/c/pulse/field_taint.c, test_sanitize_field_bad, 10, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#0` to `taint_structure` with kind `Simple`,flows to this sink: value passed as argument `#0` to `sink_int` with kind `Simple`], source: taint_structure, sink: sink_int, tainted expression: s.other