From c473f21f8101544582fbe518ff9641ae662a47a0 Mon Sep 17 00:00:00 2001
From: Andrzej Kotulski <akotulski@fb.com>
Date: Wed, 2 Aug 2017 11:51:24 -0700
Subject: [PATCH] [C++] fix std::vector::empty model

Summary:
With current model, there are issues with cxx range loop. It looks like
it comes from std::vector::size model.

example of such FP:
```
int t = vec.size();
for(auto& elem : vec) {
  auto x = elem
}
```

Reviewed By: jvillard

Differential Revision: D5545914

fbshipit-source-id: fbe55b3
---
 infer/models/cpp/include/infer_model/vector.h | 13 +++++-
 .../tests/codetoanalyze/cpp/errors/issues.exp |  1 +
 .../codetoanalyze/cpp/errors/vector/loop.cpp  | 43 +++++++++++++++++++
 3 files changed, 56 insertions(+), 1 deletion(-)
 create mode 100644 infer/tests/codetoanalyze/cpp/errors/vector/loop.cpp

diff --git a/infer/models/cpp/include/infer_model/vector.h b/infer/models/cpp/include/infer_model/vector.h
index e522a403d..a25fcef6f 100644
--- a/infer/models/cpp/include/infer_model/vector.h
+++ b/infer/models/cpp/include/infer_model/vector.h
@@ -59,6 +59,10 @@ T* __infer_skip__get_nondet_val() {}
 template <class T>
 void __infer_deref_first_arg(T* ptr) INFER_MODEL_AS_DEREF_FIRST_ARG;
 
+#define INFER_EXCLUDE_CONDITION(cond) \
+  if (cond)                           \
+    while (1)
+
 // WARNING: do not add any new fields to std::vector model. sizeof(std::vector)
 // = 24 !!
 #ifdef INFER_USE_LIBCPP
@@ -241,7 +245,14 @@ class vector {
 
   size_type capacity() const noexcept {}
 
-  bool empty() const noexcept { return beginPtr == nullptr; }
+  bool empty() const noexcept {
+    if (beginPtr == nullptr) {
+      // prune branch where beginPtr is nullptr and endPtr isn't
+      INFER_EXCLUDE_CONDITION(endPtr != nullptr);
+      return true;
+    }
+    return false;
+  }
   size_type max_size() const noexcept;
   void reserve(size_type __n);
   void shrink_to_fit() noexcept;
diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp
index 2157422c6..3c78eb05e 100644
--- a/infer/tests/codetoanalyze/cpp/errors/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp
@@ -208,6 +208,7 @@ codetoanalyze/cpp/errors/vector/iterator_cmp.cpp, iterator_compare::empty_deref1
 codetoanalyze/cpp/errors/vector/iterator_cmp.cpp, iterator_compare::empty_deref2_bad, 4, NULL_DEREFERENCE, [start of procedure iterator_compare::empty_deref2_bad(),start of procedure iterator_compare::not_empty(),return from a call to iterator_compare::not_empty,Condition is false,Condition is true]
 codetoanalyze/cpp/errors/vector/iterator_cmp.cpp, iterator_compare::not_empty_deref1_bad, 4, NULL_DEREFERENCE, [start of procedure iterator_compare::not_empty_deref1_bad(),Skipped call: function or method not found,start of procedure iterator_compare::is_empty(),return from a call to iterator_compare::is_empty,Condition is false,Condition is true]
 codetoanalyze/cpp/errors/vector/iterator_cmp.cpp, iterator_compare::not_empty_deref2_bad, 4, NULL_DEREFERENCE, [start of procedure iterator_compare::not_empty_deref2_bad(),Skipped call: function or method not found,start of procedure iterator_compare::not_empty(),return from a call to iterator_compare::not_empty,Condition is true]
+codetoanalyze/cpp/errors/vector/loop.cpp, non_empty_vector_loop_bad, 4, NULL_DEREFERENCE, [start of procedure non_empty_vector_loop_bad(),Condition is true]
 codetoanalyze/cpp/shared/attributes/annotate.cpp, derefFirstArg2_null_deref, 2, NULL_DEREFERENCE, [start of procedure derefFirstArg2_null_deref()]
 codetoanalyze/cpp/shared/attributes/annotate.cpp, derefFirstArg3_null_deref, 2, NULL_DEREFERENCE, [start of procedure derefFirstArg3_null_deref(),start of procedure derefFirstArg3()]
 codetoanalyze/cpp/shared/attributes/annotate.cpp, derefFirstArg_null_deref, 2, NULL_DEREFERENCE, [start of procedure derefFirstArg_null_deref()]
diff --git a/infer/tests/codetoanalyze/cpp/errors/vector/loop.cpp b/infer/tests/codetoanalyze/cpp/errors/vector/loop.cpp
new file mode 100644
index 000000000..653c9b9d6
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/errors/vector/loop.cpp
@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#include <vector>
+
+void foreach_access_ok(std::vector<int>& vec) {
+  if (vec.empty()) {
+    // do nothing
+  }
+  for (const auto& elem : vec) {
+    auto r = elem;
+  }
+}
+
+void iterator_for_access_ok(std::vector<int>& vec) {
+  if (vec.empty()) {
+    // do nothing
+  }
+  for (auto it = vec.begin(); it != vec.end(); ++it) {
+    auto r = *it;
+  }
+}
+
+void empty_vector_loop_ok() {
+  std::vector<int> vec;
+  int* ptr = nullptr;
+  for (const auto& elem : vec) {
+    *ptr = elem; // this is unreachable
+  }
+}
+
+void non_empty_vector_loop_bad(std::vector<int>& vec) {
+  std::vector<int> x;
+  int* ptr = nullptr;
+  for (const auto& elem : vec) {
+    *ptr = elem; // this is reachable
+  }
+}