[vector] model beginPtr and endPtr separately

Summary:
We keep track of both `beginPtr` and `endPtr` but the modelling was mostly
about `beginPtr` as some sort of approximation I guess. This shouldn't change
much but will be useful later when doing more iterator stuff.

Reviewed By: mbouaziz

Differential Revision: D5255772

fbshipit-source-id: 0f6e3e8

infer/models/cpp/include/infer_model/vector.h

@@ -53,6 +53,8 @@ struct vector_ref<bool> {
   typedef bool_ref ref;
 };
 
+int __infer_skip__get_int_val();
+
 // this function will be treated as SKIP by infer
 template <class T>
 T* __infer_skip__get_nondet_val() {}
@@ -89,7 +91,7 @@ class vector {
   value_type* endPtr = nullptr;
   value_type* __ignore;
 
-  value_type* get() const {
+  value_type* _get_begin() const {
     // we have to resort to that hack so that infer can truly dereference
     // beginPtr.
     // Another way to model that would be 'auto tmp = *beginPtr' but that will
@@ -98,11 +100,23 @@ class vector {
     return beginPtr;
   }
 
+  value_type* _get_end() const {
+    __infer_deref_first_arg(beginPtr);
+    __infer_deref_first_arg(endPtr);
+    return endPtr;
+  }
+
+  value_type* _get_index(size_type __n) const {
+    __infer_deref_first_arg(beginPtr);
+    return __infer_skip__get_nondet_val<value_type>();
+  }
+
   void allocate(size_type size) {
     // assume that allocation will produce non-empty vector regardless of the
     // size
     // if (size > 0) {
     beginPtr = __infer_skip__get_nondet_val<value_type>();
+    endPtr = __infer_skip__get_nondet_val<value_type>();
     //} else {
     //  deallocate();
     //}
@@ -233,14 +247,20 @@ class vector {
   reference at(size_type __n);
   const_reference at(size_type __n) const;
 
-  reference front() { return (reference)*get(); }
-  const_reference front() const { return (const_reference)*get(); }
-  reference back() { return (reference)*get(); }
-  const_reference back() const { return (const_reference)*get(); }
+  reference front() { return (reference)*_get_begin(); }
+  const_reference front() const { return (const_reference)*_get_begin(); }
+  reference back() {
+    size_t last_element = __infer_skip__get_int_val();
+    return (reference)*_get_index(last_element);
+  }
+  const_reference back() const {
+    size_t last_element = __infer_skip__get_int_val();
+    return (const_reference)*_get_index(last_element);
+  }
 
-  value_type* data() noexcept { return get(); }
+  value_type* data() noexcept { return _get_begin(); }
 
-  const value_type* data() const noexcept { return get(); }
+  const value_type* data() const noexcept { return _get_begin(); }
 
   void push_back(const_reference __x);
   void push_back(value_type&& __x);
@@ -445,25 +465,25 @@ vector<_Tp, _Allocator>::end() const noexcept {
 template <class _Tp, class _Allocator>
 inline typename vector<_Tp, _Allocator>::reference vector<_Tp, _Allocator>::
 operator[](size_type __n) {
-  return (reference)*get();
+  return (reference)*_get_index(__n);
 }
 
 template <class _Tp, class _Allocator>
 inline typename vector<_Tp, _Allocator>::const_reference
     vector<_Tp, _Allocator>::operator[](size_type __n) const {
-  return (const_reference)*get();
+  return (const_reference)*_get_index(__n);
 }
 
 template <class _Tp, class _Allocator>
 typename vector<_Tp, _Allocator>::reference vector<_Tp, _Allocator>::at(
     size_type __n) {
-  return (reference)*get();
+  return (reference)*_get_index(__n);
 }
 
 template <class _Tp, class _Allocator>
 typename vector<_Tp, _Allocator>::const_reference vector<_Tp, _Allocator>::at(
     size_type __n) const {
-  return (const_reference)*get();
+  return (const_reference)*_get_index(__n);
 }
 
 template <class _Tp, class _Allocator>

infer/src/backend/errdesc.ml

@@ -846,7 +846,8 @@ let create_dereference_desc tenv
       | Some (DExp.Ddot (dexp, fieldname)) ->
           if is_special_field mutex_matcher (Some "null_if_locked") fieldname then
             Localise.desc_double_lock None (DExp.to_string dexp) loc
-          else if is_special_field vector_matcher (Some "beginPtr") fieldname then
+          else if is_special_field vector_matcher (Some "beginPtr") fieldname
+               || is_special_field vector_matcher (Some "endPtr") fieldname then
             Localise.desc_empty_vector_access None (DExp.to_string dexp) loc
           else
             desc

infer/tests/clang.make

@@ -9,7 +9,7 @@ ROOT_DIR = $(TESTS_DIR)/../..
 
 CLEAN_EXTRA += duplicates.txt
 
-OBJECTS = $(foreach source,$(SOURCES),$(basename $(source)).o)
+OBJECTS = $(foreach source,$(filter %.c %.cpp %.m %.mm,$(SOURCES)),$(basename $(source)).o)
 
 include $(TESTS_DIR)/infer.make
 include $(TESTS_DIR)/clang-base.make

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

@@ -146,6 +146,8 @@ codetoanalyze/cpp/errors/vector/access_field_later.cpp, getWithoutCopy, 2, EMPTY
 codetoanalyze/cpp/errors/vector/access_field_later.cpp, getWithoutCopyPtr, 1, RETURN_VALUE_IGNORED, [start of procedure getWithoutCopyPtr()]
 codetoanalyze/cpp/errors/vector/access_field_later.cpp, getWithoutCopyPtr, 2, EMPTY_VECTOR_ACCESS, [start of procedure getWithoutCopyPtr()]
 codetoanalyze/cpp/errors/vector/empty_access.cpp, access_empty, 2, EMPTY_VECTOR_ACCESS, [start of procedure access_empty()]
+codetoanalyze/cpp/errors/vector/empty_access.cpp, access_empty_back_bad, 2, EMPTY_VECTOR_ACCESS, [start of procedure access_empty_back_bad()]
+codetoanalyze/cpp/errors/vector/empty_access.cpp, access_empty_front_bad, 2, EMPTY_VECTOR_ACCESS, [start of procedure access_empty_front_bad()]
 codetoanalyze/cpp/errors/vector/empty_access.cpp, assign_empty, 4, EMPTY_VECTOR_ACCESS, [start of procedure assign_empty()]
 codetoanalyze/cpp/errors/vector/empty_access.cpp, clear_empty, 3, EMPTY_VECTOR_ACCESS, [start of procedure clear_empty()]
 codetoanalyze/cpp/errors/vector/empty_access.cpp, copy_empty, 3, EMPTY_VECTOR_ACCESS, [start of procedure copy_empty()]

infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp

@@ -14,6 +14,16 @@ int access_empty() {
   return vec[0];
 }
 
+int access_empty_front_bad() {
+  const std::vector<int> vec;
+  return vec.front();
+}
+
+int access_empty_back_bad() {
+  const std::vector<int> vec;
+  return vec.back();
+}
+
 int access_nonempty() {
   const std::vector<int> vec(1);
   return vec[0];