From 058f4455dcfffc3ac3fe23597973de0ff9d115b5 Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Mon, 23 May 2016 02:59:53 -0700 Subject: [PATCH] Modify model of std::vector Summary: Turns out, analyzer was getting confused with complicated model and it was reporting empty access in places it shouldn't. Fixing backend is not trivial (tracing mode is the answer), but the model can be simplified. It introduces the problem that get() method doesn't return fresh value every time, but we should be able to change backend later to deal with it. Reviewed By: sblackshear Differential Revision: D3328228 fbshipit-source-id: dddbaf8 --- infer/models/cpp/include/infer_model/vector.h | 48 ++++++++----------- .../cpp/errors/vector/empty_access.cpp | 14 ++++++ .../endtoend/cpp/VectorEmptyAccessTest.java | 1 + 3 files changed, 35 insertions(+), 28 deletions(-) diff --git a/infer/models/cpp/include/infer_model/vector.h b/infer/models/cpp/include/infer_model/vector.h index 90ed3a26b..fa7cd7902 100644 --- a/infer/models/cpp/include/infer_model/vector.h +++ b/infer/models/cpp/include/infer_model/vector.h @@ -76,27 +76,19 @@ class vector { typedef std::reverse_iterator const_reverse_iterator; /* INFER SPECIFIC HELPER FUNCTIONS */ - bool isEmpty = true; // required to keep sizeof(std::vector) same as in standard value_type* beginPtr = nullptr; value_type* endPtr = nullptr; + value_type* __ignore; - value_type* get() const { - if (isEmpty) { - return nullptr; - } - // infer will angelically assume that __infer_skip__get_nondet_val - // returns non-null with unknown value which means there will be no - // null dereference - return __infer_skip__get_nondet_val(); - } + value_type* get() const { return beginPtr; } void allocate(size_type size) { if (size > 0) { - isEmpty = false; + beginPtr = __infer_skip__get_nondet_val(); } else { - isEmpty = true; + beginPtr = nullptr; } } @@ -200,7 +192,7 @@ class vector { const_reverse_iterator crend() const noexcept { return rend(); } size_type size() const noexcept { - if (!isEmpty) { + if (beginPtr) { return 10; } return 0; @@ -208,7 +200,7 @@ class vector { size_type capacity() const noexcept {} - bool empty() const noexcept { return isEmpty; } + bool empty() const noexcept { return beginPtr == nullptr; } size_type max_size() const noexcept; void reserve(size_type __n); void shrink_to_fit() noexcept; @@ -259,7 +251,7 @@ class vector { iterator erase(const_iterator __position); iterator erase(const_iterator __first, const_iterator __last); - void clear() noexcept { isEmpty = true; } + void clear() noexcept { allocate(0); } void resize(size_type __sz); void resize(size_type __sz, const_reference __x); @@ -326,25 +318,25 @@ vector<_Tp, _Allocator>::vector( template vector<_Tp, _Allocator>::vector(const vector& __x) { - isEmpty = __x.isEmpty; + beginPtr = __x.beginPtr; } template vector<_Tp, _Allocator>::vector(const vector& __x, const allocator_type& __a) { - isEmpty = __x.isEmpty; + beginPtr = __x.beginPtr; } template inline vector<_Tp, _Allocator>::vector(vector&& __x) noexcept { - isEmpty = __x.isEmpty; - __x.isEmpty = true; + beginPtr = __x.beginPtr; + __x.beginPtr = nullptr; } template inline vector<_Tp, _Allocator>::vector(vector&& __x, const allocator_type& __a) { - isEmpty = __x.isEmpty; - __x.isEmpty = true; + beginPtr = __x.beginPtr; + __x.beginPtr = nullptr; } template @@ -363,15 +355,15 @@ inline vector<_Tp, _Allocator>& vector<_Tp, _Allocator>::operator=( vector&& __x) noexcept /*((__noexcept_move_assign_container<_Allocator, __alloc_traits>::value)) */ { - isEmpty = __x.isEmpty; - __x.isEmpty = true; + beginPtr = __x.beginPtr; + __x.beginPtr = nullptr; return *this; } template inline vector<_Tp, _Allocator>& vector<_Tp, _Allocator>::operator=( const vector& __x) { - isEmpty = __x.isEmpty; + beginPtr = __x.beginPtr; return *this; } @@ -516,7 +508,7 @@ typename vector<_Tp, _Allocator>::iterator vector<_Tp, _Allocator>::emplace( template typename vector<_Tp, _Allocator>::iterator vector<_Tp, _Allocator>::insert( const_iterator __position, size_type __n, const_reference __x) { - if (isEmpty) { + if (empty()) { allocate(__n); } } @@ -545,9 +537,9 @@ void vector<_Tp, _Allocator>::resize(size_type __sz, const_reference __x) { template void vector<_Tp, _Allocator>::swap(vector& __x) { - bool tmp = __x.isEmpty; - __x.isEmpty = isEmpty; - isEmpty = tmp; + value_type* tmp = __x.beginPtr; + __x.beginPtr = beginPtr; + beginPtr = tmp; } template diff --git a/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp b/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp index 4ba8e9f16..78fd14ba7 100644 --- a/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp @@ -108,3 +108,17 @@ int size_check1_nonempty() { } return 1; } + +int vector_param_access(std::vector& v) { + return v.back(); // shouldn't report anything here +} + +int vector_as_param_empty() { + std::vector v; + return vector_param_access(v); +} + +int vector_as_param_nonempty() { + std::vector v(1); + return vector_param_access(v); +} diff --git a/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java b/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java index d907701a3..d45f9e08a 100644 --- a/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java +++ b/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java @@ -55,6 +55,7 @@ public class VectorEmptyAccessTest { "assign_empty", "empty_check_access_empty", "size_check0_empty", + "vector_as_param_empty", }; InferResults inferResults = InferRunner.runInferCPP(inferCmd); assertThat(