[inferbo] Consider `this` to never be a pointer inside an array

Reviewed By: skcho

Differential Revision: D13128691

fbshipit-source-id: e74a168ba

infer/src/bufferoverrun/absLoc.ml

@@ -122,8 +122,15 @@ module Loc = struct
         else F.pp_print_string fmt s
     | Allocsite a ->
         Allocsite.pp_paren ~paren fmt a
-    | Field (Allocsite (Allocsite.Symbol (SP.Deref (SP.Deref_CPointer, p))), f)
+    | Field
-    | Field (Allocsite (Allocsite.Known {path= Some (SP.Deref (SP.Deref_CPointer, p))}), f) ->
+        ( Allocsite
+            (Allocsite.Symbol (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p)))
+        , f )
+    | Field
+        ( Allocsite
+            (Allocsite.Known
+              {path= Some (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p))})
+        , f ) ->
         BufferOverrunField.pp ~pp_lhs:(SP.pp_partial_paren ~paren:true)
           ~pp_lhs_alone:(SP.pp_pointer ~paren) ~sep:"->" fmt p f
     | Field (l, f) ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -397,8 +397,10 @@ module Val = struct
         let unsigned = Typ.is_unsigned_int typ in
         of_itv ~traces (Itv.of_normal_path ~unsigned path)
     | Tptr (elt, _) ->
-        if is_java then
+        if is_java || SPath.is_this path then
-          let deref_kind = SPath.Deref_JavaPointer in
+          let deref_kind =
+            if is_java then SPath.Deref_JavaPointer else SPath.Deref_COneValuePointer
+          in
           let deref_path = SPath.deref ~deref_kind path in
           let l = Loc.of_path deref_path in
           let traces = TraceSet.singleton location (Trace.Parameter l) in

infer/src/bufferoverrun/symb.ml

@@ -18,7 +18,11 @@ module BoundEnd = struct
 end
 
 module SymbolPath = struct
-  type deref_kind = Deref_ArrayIndex | Deref_CPointer | Deref_JavaPointer
+  type deref_kind =
+    | Deref_ArrayIndex
+    | Deref_COneValuePointer
+    | Deref_CPointer
+    | Deref_JavaPointer
 
   let compare_deref_kind _ _ = 0
 
@@ -49,6 +53,8 @@ module SymbolPath = struct
 
   let length p = Length p
 
+  let is_this = function Pvar pvar -> Pvar.is_this pvar || Pvar.is_self pvar | _ -> false
+
   let rec get_pvar = function
     | Pvar pvar ->
         Some pvar
@@ -65,9 +71,9 @@ module SymbolPath = struct
         pp_partial_paren ~paren fmt p
     | Deref (Deref_ArrayIndex, p) ->
         F.fprintf fmt "%a[*]" (pp_partial_paren ~paren:true) p
-    | Deref ((Deref_CPointer | Deref_JavaPointer), p) ->
+    | Deref ((Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer), p) ->
         pp_pointer ~paren fmt p
-    | Field (fn, Deref (Deref_CPointer, p)) ->
+    | Field (fn, Deref ((Deref_COneValuePointer | Deref_CPointer), p)) ->
         BufferOverrunField.pp ~pp_lhs:(pp_partial_paren ~paren:true)
           ~pp_lhs_alone:(pp_pointer ~paren) ~sep:"->" fmt p fn
     | Field (fn, p) ->
@@ -104,7 +110,7 @@ module SymbolPath = struct
         true
     | Deref (Deref_CPointer, p)
     (* Deref_CPointer is unsound here but avoids many FPs for non-array pointers *)
-    | Deref (Deref_JavaPointer, p)
+    | Deref ((Deref_COneValuePointer | Deref_JavaPointer), p)
     | Field (_, p) ->
         represents_multiple_values p
 
@@ -116,7 +122,7 @@ module SymbolPath = struct
         false
     | Deref ((Deref_ArrayIndex | Deref_CPointer), _) ->
         true
-    | Deref (Deref_JavaPointer, p) | Field (_, p) ->
+    | Deref ((Deref_COneValuePointer | Deref_JavaPointer), p) | Field (_, p) ->
         represents_multiple_values_sound p
 
 

infer/src/bufferoverrun/symb.mli

@@ -15,7 +15,12 @@ module BoundEnd : sig
 end
 
 module SymbolPath : sig
-  type deref_kind = Deref_ArrayIndex | Deref_CPointer | Deref_JavaPointer [@@deriving compare]
+  type deref_kind =
+    | Deref_ArrayIndex
+    | Deref_COneValuePointer
+    | Deref_CPointer
+    | Deref_JavaPointer
+  [@@deriving compare]
 
   type partial = private
     | Pvar of Pvar.t
@@ -40,8 +45,6 @@ module SymbolPath : sig
 
   val of_callsite : ret_typ:Typ.t -> CallSite.t -> partial
 
-  val get_pvar : partial -> Pvar.t option
-
   val deref : deref_kind:deref_kind -> partial -> partial
 
   val field : partial -> Typ.Fieldname.t -> partial
@@ -52,6 +55,10 @@ module SymbolPath : sig
 
   val length : partial -> t
 
+  val is_this : partial -> bool
+
+  val get_pvar : partial -> Pvar.t option
+
   val represents_multiple_values : partial -> bool
 
   val represents_multiple_values_sound : partial -> bool

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

@@ -99,6 +99,7 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Good, 3, CONDITION_AL
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [0, +oo] Size: 1024]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/this.cpp, CThis_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this->n`,<Length trace>,Parameter `this->n`,Array declaration,Array access: Offset: this->n + 1 Size: this->n + 1]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]

infer/tests/codetoanalyze/cpp/bufferoverrun/this.cpp

@@ -0,0 +1,18 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+class CThis {
+  unsigned int n;
+  void access_Good() {
+    char a[this->n + 1];
+    a[this->n] = 0;
+  }
+  void access_Bad() {
+    char a[this->n + 1];
+    a[this->n + 1] = 0;
+  }
+};