[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

@@ -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
 
 

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]

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<char const*>
+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);
+}