[inferbo] Downgrade issues of void pointer

Summary:
It downgrades issues of void pointer to L5, because of its impreciseness.  This is not
ideal but Inferbo cannot analyze arrays pointed by void pointers precisely at the moment.

Reviewed By: jvillard

Differential Revision: D16379911

fbshipit-source-id: f2c016aba

infer/src/bufferoverrun/bounds.ml

@@ -293,12 +293,36 @@ module Bound = struct
 
   let of_normal_path = of_path Symb.SymbolPath.normal
 
-  let of_offset_path = of_path Symb.SymbolPath.offset ~unsigned:false
+  let of_offset_path ~is_void = of_path (Symb.SymbolPath.offset ~is_void) ~unsigned:false
 
-  let of_length_path = of_path Symb.SymbolPath.length ~unsigned:true
+  let of_length_path ~is_void = of_path (Symb.SymbolPath.length ~is_void) ~unsigned:true
 
   let of_modeled_path = of_path Symb.SymbolPath.modeled ~unsigned:true
 
+  let is_path_of ~f = function
+    | Linear (n, se) when Z.(equal n zero) ->
+        Option.value_map (SymLinear.get_one_symbol_opt se) ~default:false ~f:(fun s ->
+            f (Symb.Symbol.path s) )
+    | _ ->
+        false
+
+
+  let is_offset_path_of path =
+    is_path_of ~f:(function
+      | Symb.SymbolPath.Offset {p} ->
+          Symb.SymbolPath.equal_partial p path
+      | _ ->
+          false )
+
+
+  let is_length_path_of path =
+    is_path_of ~f:(function
+      | Symb.SymbolPath.Length {p} ->
+          Symb.SymbolPath.equal_partial p path
+      | _ ->
+          false )
+
+
   let is_symbolic : t -> bool = function
     | MInf | PInf ->
         false
@@ -866,6 +890,12 @@ module Bound = struct
         Symb.SymbolSet.singleton s
 
 
+  let has_void_ptr_symb x =
+    Symb.SymbolSet.exists
+      (fun s -> Symb.SymbolPath.is_void_ptr_path (Symb.Symbol.path s))
+      (get_symbols x)
+
+
   let are_similar b1 b2 = Symb.SymbolSet.equal (get_symbols b1) (get_symbols b2)
 
   (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *)

infer/src/bufferoverrun/bounds.mli

@@ -42,14 +42,24 @@ module Bound : sig
     -> t
 
   val of_offset_path :
-    (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
+       is_void:bool
+    -> (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t)
+    -> Symb.SymbolPath.partial
+    -> t
 
   val of_length_path :
-    (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
+       is_void:bool
+    -> (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t)
+    -> Symb.SymbolPath.partial
+    -> t
 
   val of_modeled_path :
     (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
 
+  val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool
+
+  val is_length_path_of : Symb.SymbolPath.partial -> t -> bool
+
   val is_zero : t -> bool
 
   val is_not_infty : t -> bool
@@ -104,6 +114,8 @@ module Bound : sig
 
   val get_symbols : t -> Symb.SymbolSet.t
 
+  val has_void_ptr_symb : t -> bool
+
   val are_similar : t -> t -> bool
 
   val subst_lb : t -> eval_sym -> t AbstractDomain.Types.bottom_lifted

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -482,8 +482,8 @@ module Val = struct
               | _ ->
                   Itv.nat
             in
-            let offset = Itv.of_offset_path path in
-            let size = Itv.of_length_path path in
+            let offset = Itv.of_offset_path ~is_void:(Typ.is_pointer_to_void typ) path in
+            let size = Itv.of_length_path ~is_void:(Typ.is_pointer_to_void typ) path in
             ArrayBlk.make_c allocsite ~stride ~offset ~size
           in
           {bot with arrayblk; traces}
@@ -502,7 +502,7 @@ module Val = struct
           let l = Loc.of_path deref_path in
           let traces = traces_of_loc l in
           let allocsite = Allocsite.make_symbol deref_path in
-          let length = Itv.of_length_path path in
+          let length = Itv.of_length_path ~is_void:false path in
           of_java_array_alloc allocsite ~length ~traces
       | None ->
           let l = Loc.of_path path in
@@ -516,11 +516,11 @@ module Val = struct
         let size =
           match length with
           | None (* IncompleteArrayType, no-size flexible array *) ->
-              Itv.of_length_path path
+              Itv.of_length_path ~is_void:false path
           | Some length
             when may_last_field && (IntLit.iszero length || IntLit.isone length)
                  (* 0/1-sized flexible array *) ->
-              Itv.of_length_path path
+              Itv.of_length_path ~is_void:false path
           | Some length ->
               Itv.of_big_int (IntLit.to_big_int length)
         in

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -205,7 +205,8 @@ module ArrayAccessCondition = struct
     ; last_included: bool
     ; idx_sym_exp: Relation.SymExp.t option
     ; size_sym_exp: Relation.SymExp.t option
-    ; relation: Relation.t }
+    ; relation: Relation.t
+    ; void_ptr: bool }
   [@@deriving compare]
 
   let get_symbols c =
@@ -252,7 +253,9 @@ module ArrayAccessCondition = struct
       -> t option =
    fun ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp ~relation ->
     if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None
-    else Some {offset; idx; size; last_included; idx_sym_exp; size_sym_exp; relation}
+    else
+      let void_ptr = ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb size in
+      Some {offset; idx; size; last_included; idx_sym_exp; size_sym_exp; relation; void_ptr}
 
 
   let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; last_included= lcol}
@@ -409,7 +412,11 @@ module ArrayAccessCondition = struct
         let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in
         let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in
         let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in
-        Some {c with offset; idx; size; idx_sym_exp; size_sym_exp; relation}
+        let void_ptr =
+          c.void_ptr || ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb idx
+          || ItvPure.has_void_ptr_symb size
+        in
+        Some {c with offset; idx; size; idx_sym_exp; size_sym_exp; relation; void_ptr}
     | _ ->
         None
 
@@ -699,6 +706,9 @@ module Condition = struct
         ArrayAccess (ArrayAccessCondition.relation_forget_locs locs c)
     | AllocSize _ | BinaryOperation _ ->
         x
+
+
+  let is_array_access_of_void_ptr = function ArrayAccess {void_ptr} -> void_ptr | _ -> false
 end
 
 module Reported = struct
@@ -783,7 +793,10 @@ module ConditionWithTrace = struct
 
 
   let set_u5 {cond; trace} issue_type =
-    if
+    (* It suppresses issues of array accesses by void pointers.  This is not ideal but Inferbo
+       cannot analyze them precisely at the moment. *)
+    if Condition.is_array_access_of_void_ptr cond then IssueType.buffer_overrun_l5
+    else if
       ( IssueType.equal issue_type IssueType.buffer_overrun_l3
       || IssueType.equal issue_type IssueType.buffer_overrun_l4
       || IssueType.equal issue_type IssueType.buffer_overrun_l5 )

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -439,10 +439,10 @@ let eval_sympath ~mode params sympath mem =
   | Symb.SymbolPath.Normal p ->
       let v = eval_sympath_partial ~mode params p mem in
       (Val.get_itv v, Val.get_traces v)
-  | Symb.SymbolPath.Offset p ->
+  | Symb.SymbolPath.Offset {p} ->
       let v = eval_sympath_partial ~mode params p mem in
       (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v)
-  | Symb.SymbolPath.Length p ->
+  | Symb.SymbolPath.Length {p} ->
       let v = eval_sympath_partial ~mode params p mem in
       (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v)
 

infer/src/bufferoverrun/itv.ml

@@ -433,11 +433,21 @@ module ItvPure = struct
 
   let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned)
 
-  let of_offset_path = of_path Bound.of_offset_path
+  let of_offset_path ~is_void = of_path (Bound.of_offset_path ~is_void)
 
-  let of_length_path = of_path Bound.of_length_path
+  let of_length_path ~is_void = of_path (Bound.of_length_path ~is_void)
 
   let of_modeled_path = of_path Bound.of_modeled_path
+
+  let is_offset_path_of path x =
+    Bound.is_offset_path_of path (lb x) && Bound.is_offset_path_of path (ub x)
+
+
+  let is_length_path_of path x =
+    Bound.is_length_path_of path (lb x) && Bound.is_length_path_of path (ub x)
+
+
+  let has_void_ptr_symb x = Bound.has_void_ptr_symb (lb x) || Bound.has_void_ptr_symb (ub x)
 end
 
 include AbstractDomain.BottomLifted (ItvPure)
@@ -656,12 +666,12 @@ let max_of_ikind integer_type_widths ikind =
 
 let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned path)
 
-let of_offset_path path = NonBottom (ItvPure.of_offset_path path)
+let of_offset_path ~is_void path = NonBottom (ItvPure.of_offset_path ~is_void path)
 
-let of_length_path path = NonBottom (ItvPure.of_length_path path)
+let of_length_path ~is_void path = NonBottom (ItvPure.of_length_path ~is_void path)
 
 let of_modeled_path path = NonBottom (ItvPure.of_modeled_path path)
 
-let is_offset_path_of path x = eq (of_offset_path path) x
+let is_offset_path_of path = bind1_gen ~bot:false (ItvPure.is_offset_path_of path)
 
-let is_length_path_of path x = eq (of_length_path path) x
+let is_length_path_of path = bind1_gen ~bot:false (ItvPure.is_length_path_of path)

infer/src/bufferoverrun/itv.mli

@@ -63,6 +63,8 @@ module ItvPure : sig
 
   val has_infty : t -> bool
 
+  val has_void_ptr_symb : t -> bool
+
   val make_positive : t -> t
 
   val join : t -> t -> t
@@ -231,9 +233,9 @@ val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t
 
 val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t
 
-val of_offset_path : Symb.SymbolPath.partial -> t
+val of_offset_path : is_void:bool -> Symb.SymbolPath.partial -> t
 
-val of_length_path : Symb.SymbolPath.partial -> t
+val of_length_path : is_void:bool -> Symb.SymbolPath.partial -> t
 
 val of_modeled_path : Symb.SymbolPath.partial -> t
 

infer/src/bufferoverrun/symb.ml

@@ -92,7 +92,11 @@ module SymbolPath = struct
         val star_field : partial -> Typ.Fieldname.t -> partial
       end )
 
-  type t = Normal of partial | Offset of partial | Length of partial | Modeled of partial
+  type t =
+    | Normal of partial
+    | Offset of {p: partial; is_void: bool}
+    | Length of {p: partial; is_void: bool}
+    | Modeled of partial
   [@@deriving compare]
 
   let equal = [%compare.equal: t]
@@ -101,9 +105,9 @@ module SymbolPath = struct
 
   let normal p = Normal p
 
-  let offset p = Offset p
+  let offset p ~is_void = Offset {p; is_void}
 
-  let length p = Length p
+  let length p ~is_void = Length {p; is_void}
 
   let modeled p = Modeled p
 
@@ -150,15 +154,17 @@ module SymbolPath = struct
 
   let pp_partial = pp_partial_paren ~paren:false
 
+  let pp_is_void fmt is_void = if is_void then F.fprintf fmt "(v)"
+
   let pp fmt = function
     | Modeled p ->
         F.fprintf fmt "%a.modeled" pp_partial p
     | Normal p ->
         pp_partial fmt p
-    | Offset p ->
-        F.fprintf fmt "%a.offset" pp_partial p
-    | Length p ->
-        F.fprintf fmt "%a.length" pp_partial p
+    | Offset {p; is_void} ->
+        F.fprintf fmt "%a.offset%a" pp_partial p pp_is_void is_void
+    | Length {p; is_void} ->
+        F.fprintf fmt "%a.length%a" pp_partial p pp_is_void is_void
 
 
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
@@ -217,8 +223,15 @@ module SymbolPath = struct
 
 
   let exists_str ~f = function
-    | Modeled p | Normal p | Offset p | Length p ->
+    | Modeled p | Normal p | Offset {p} | Length {p} ->
         exists_str_partial ~f p
+
+
+  let is_void_ptr_path = function
+    | Offset {is_void} | Length {is_void} ->
+        is_void
+    | Normal _ | Modeled _ ->
+        false
 end
 
 module Symbol = struct

infer/src/bufferoverrun/symb.mli

@@ -38,7 +38,11 @@ module SymbolPath : sig
         *)
   [@@deriving compare]
 
-  type t = private Normal of partial | Offset of partial | Length of partial | Modeled of partial
+  type t = private
+    | Normal of partial
+    | Offset of {p: partial; is_void: bool}
+    | Length of {p: partial; is_void: bool}
+    | Modeled of partial
 
   val equal_partial : partial -> partial -> bool
 
@@ -62,9 +66,9 @@ module SymbolPath : sig
 
   val normal : partial -> t
 
-  val offset : partial -> t
+  val offset : partial -> is_void:bool -> t
 
-  val length : partial -> t
+  val length : partial -> is_void:bool -> t
 
   val modeled : partial -> t
 
@@ -81,6 +85,8 @@ module SymbolPath : sig
   val exists_pvar_partial : f:(Pvar.t -> bool) -> partial -> bool
 
   val exists_str_partial : f:(string -> bool) -> partial -> bool
+
+  val is_void_ptr_path : t -> bool
 end
 
 module Symbol : sig

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

@@ -59,8 +59,7 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVER
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Assignment,Array declaration,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 12]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `y`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params2` ]
@@ -132,3 +131,4 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1,
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/cpp/bufferoverrun/void_ptr.cpp, FP_call_casting_void_ptr_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ]

infer/tests/codetoanalyze/cpp/bufferoverrun/void_ptr.cpp

@@ -0,0 +1,17 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <cstdint>
+
+void casting_void_ptr(void* p) {
+  uint8_t* q = (uint8_t*)p;
+  q[14] = 0;
+}
+
+void FP_call_casting_void_ptr_Ok() {
+  uint64_t p[2];
+  casting_void_ptr(p);
+}