From 124ab9fed75549d8978844ca5c8b1bbf0c341c7c Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 22 Jul 2019 07:42:22 -0700 Subject: [PATCH] [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 | 34 +++++++++++++++++-- infer/src/bufferoverrun/bounds.mli | 16 +++++++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 10 +++--- .../bufferOverrunProofObligations.ml | 21 +++++++++--- .../bufferoverrun/bufferOverrunSemantics.ml | 4 +-- infer/src/bufferoverrun/itv.ml | 22 ++++++++---- infer/src/bufferoverrun/itv.mli | 6 ++-- infer/src/bufferoverrun/symb.ml | 29 +++++++++++----- infer/src/bufferoverrun/symb.mli | 12 +++++-- .../cpp/bufferoverrun/issues.exp | 4 +-- .../cpp/bufferoverrun/void_ptr.cpp | 17 ++++++++++ 11 files changed, 139 insertions(+), 36 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/void_ptr.cpp diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 8bb57b2b6..6bda8e3d8 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/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]. *) diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 31bbe6d7d..f00b77d50 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 397104b75..f43a4f52c 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index a21401732..de857c8ea 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 ) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index a8d633743..158480da1 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index b0a1414db..7402ed01a 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 0b2c824dd..2f91f0c7d 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index f08b3b3e6..fc2df5597 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/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 diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index b1866d2ab..83ca7bb2b 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index af06d0eb5..02e4616fc 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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, [,Assignment,,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,,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, [,Assignment,,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,,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,,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,,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, [,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,,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,,Parameter `y`,,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,,Parameter `index`,,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,,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/void_ptr.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/void_ptr.cpp new file mode 100644 index 000000000..1e4551e85 --- /dev/null +++ b/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 + +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); +}