From 49fb5b7c85358ea2be473c178ddae31d82abfddf Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 12 Dec 2019 03:16:11 -0800 Subject: [PATCH] [pulse] do arithmetic on pointers too Summary: A plus is a plus, no need to give up when +/- is about pointers. This gets rid of some false positives involving pointer arithmetic. However, the problem remains if we make things a bit more inter-procedural. This is documented in an added test. Reviewed By: ezgicicek Differential Revision: D18932877 fbshipit-source-id: 4ad1cfe72 --- infer/src/bufferoverrun/itv.ml | 38 +++++++++---------- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../tests/codetoanalyze/cpp/pulse/values.cpp | 38 +++++++++++++++++++ 3 files changed, 57 insertions(+), 20 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5f4eab64b..24887542e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -419,43 +419,41 @@ module ItvPure = struct let arith_binop (bop : Binop.t) x y = match bop with - | Binop.PlusA _ -> + | PlusA _ | PlusPI -> plus x y - | Binop.MinusA _ -> + | MinusA _ | MinusPI | MinusPP -> minus x y - | Binop.Mult _ -> + | Mult _ -> mult x y - | Binop.PlusPI | Binop.MinusPI | Binop.MinusPP -> - top - | Binop.Div -> + | Div -> div x y - | Binop.Mod -> + | Mod -> mod_sem x y - | Binop.Shiftlt -> + | Shiftlt -> shiftlt x y - | Binop.Shiftrt -> + | Shiftrt -> shiftrt x y - | Binop.Lt -> + | Lt -> of_boolean (lt_sem x y) |> assert_no_bottom - | Binop.Gt -> + | Gt -> of_boolean (gt_sem x y) |> assert_no_bottom - | Binop.Le -> + | Le -> of_boolean (le_sem x y) |> assert_no_bottom - | Binop.Ge -> + | Ge -> of_boolean (ge_sem x y) |> assert_no_bottom - | Binop.Eq -> + | Eq -> of_boolean (eq_sem x y) |> assert_no_bottom - | Binop.Ne -> + | Ne -> of_boolean (ne_sem x y) |> assert_no_bottom - | Binop.BAnd -> + | BAnd -> band_sem x y - | Binop.BXor -> + | BXor -> top - | Binop.BOr -> + | BOr -> top - | Binop.LAnd -> + | LAnd -> of_boolean (land_sem x y) |> assert_no_bottom - | Binop.LOr -> + | LOr -> of_boolean (lor_sem x y) |> assert_no_bottom diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 5e756565d..5de67ac28 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -69,6 +69,7 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AF codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, function_empty_range_interproc_ok_FP, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,when calling `StringRange::StringRange` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,variable `x` declared here,passed as argument to `StringRange::StringRange`,assigned,return from call to `StringRange::StringRange`,when calling `find_first_non_space` here,parameter `x` of find_first_non_space,passed as argument to `StringRange::data`,return from call to `StringRange::data`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp index ef1fb1867..2494917f0 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/values.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp @@ -77,3 +77,41 @@ void function_call_infeasible_error_path_ok(int* x) { *x = 42; } } + +// somewhat like folly::Range +struct StringRange { + char const *b_, *e_; + StringRange() : b_(), e_(){}; + char const* data() const { return b_; } + std::size_t size() const { return std::size_t(e_ - b_); } +}; + +void function_empty_range_ok() { + StringRange x{}; + auto b = x.data(), past = x.data() + x.size(); + for (;; ++b) { + if (b >= past) { + return; + } + if (*b != ' ') { + break; + } + } +} + +void find_first_non_space(StringRange& x) { + auto b = x.data(), past = x.data() + x.size(); + for (;; ++b) { + if (b >= past) { + return; + } + if (*b != ' ') { + break; + } + } +} + +void function_empty_range_interproc_ok_FP() { + StringRange x{}; + find_first_non_space(x); +}