diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index 431cc2941..5e25710e7 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -181,9 +181,12 @@ let name_cons -> ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher = fun m name -> let {on_templated_name; get_markers} = m in + let fuzzy_name_regexp = + name |> Str.quote |> Printf.sprintf "^%s\\(<[a-z0-9]+>\\)?$" |> Str.regexp + in let on_qual_name f qual_name = match QualifiedCppName.extract_last qual_name with - | Some (last, rest) when String.equal name last -> + | Some (last, rest) when Str.string_match fuzzy_name_regexp last 0 -> on_templated_name f (rest, []) | _ -> None @@ -497,6 +500,10 @@ module Common = struct let ( &+ ) templ_matcher template_arg = templ_cons templ_matcher template_arg + let ( &+...>! ) templ_matcher () = templ_matcher &+ any_template_args >! () + + let ( <...>! ) name_matcher () = name_matcher ! () + let ( < ) name_matcher template_arg = name_matcher :: ) templ_matcher name = templ_matcher >! () &::! name @@ -530,11 +537,13 @@ module Procname = struct (* Function args *) + + let no_marker_checker _markers = true + (** Matches any arg *) let match_any_arg : (_, _) one_arg_matcher = let match_arg _capt _arg = true in - let marker_static_checker _markers = true in - {match_arg; marker_static_checker} + {match_arg; marker_static_checker= no_marker_checker} let mk_match_typ_nth @@ -565,6 +574,23 @@ module Procname = struct fun marker -> mk_match_typ_nth pos3 pos3 marker + (** Matches the type matched by the given path_matcher *) + let match_typ : (_, _, unit, unit, unit, non_empty) path_matcher -> (_, _) one_arg_matcher = + fun m -> + let {on_templated_name} = m in + let rec match_typ typ = + match typ with + | {Typ.desc= Tstruct name} -> + name |> templated_name_of_class_name |> on_templated_name () |> Option.is_some + | {Typ.desc= Tptr (typ, _ptr_kind)} -> + match_typ typ + | _ -> + false + in + let match_arg _capt arg = match_typ (FuncArg.typ arg) in + {match_arg; marker_static_checker= no_marker_checker} + + (* Function argument capture *) (** Do not capture this argument *) let no_capture : (_, _, 'f, 'f) arg_capture = @@ -631,6 +657,10 @@ module Procname = struct {one_arg_matcher= match_any_arg; capture= capture_arg_exp} + let capt_arg_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg} + + let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp} + let typ1 : 'marker -> (unit, _, 'f, 'f, _, _) one_arg = fun m -> {one_arg_matcher= match_typ1 m; capture= no_capture} diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index e669e5101..d3358130d 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -184,6 +184,16 @@ module Procname : sig val capt_exp : (Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg (** Captures one arg expression *) + val capt_arg_of_typ : + (unit, _, unit, unit, unit) name_matcher + -> (FuncArg.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg + (** Captures one arg of the given type *) + + val capt_exp_of_typ : + (unit, _, unit, unit, unit) name_matcher + -> (Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg + (** Captures one arg expression of the given type *) + val typ1 : 'marker -> (unit, _, 'f, 'f, 'marker mtyp * _, 'marker * _) one_arg (** Matches first captured type *) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 274895c1f..4856a1886 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -59,7 +59,7 @@ module Loc = struct let of_id id = Var (Var.of_id id) - let append_field l f = Field (l, f) + let append_field l ~fn = Field (l, fn) let is_return = function | Var Var.ProgramVar x -> @@ -82,9 +82,9 @@ module PowLoc = struct let of_id id = singleton (Loc.of_id id) - let append_field ploc fn = + let append_field ploc ~fn = if is_bot ploc then singleton Loc.unknown - else fold (fun l -> add (Loc.append_field l fn)) ploc empty + else fold (fun l -> add (Loc.append_field l ~fn)) ploc empty let is_singleton x = Int.equal (cardinal x) 1 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index fd13607c4..43dffd698 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -77,7 +77,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ~new_sym_num ~new_alloc_num mem | None -> let decl_fld mem (fn, typ, _) = - let loc_fld = Loc.append_field loc fn in + let loc_fld = Loc.append_field loc ~fn in decl_sym_val pname tenv node location ~depth loc_fld typ mem in let decl_flds str = List.fold ~f:decl_fld ~init:mem str.Typ.Struct.fields in @@ -137,9 +137,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in let instantiate_fld mem (fn, _, _) = - let formal_fields = PowLoc.append_field formal_locs fn in + let formal_fields = PowLoc.append_field formal_locs ~fn in let v = Dom.Mem.find_heap_set formal_fields callee_exit_mem in - let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) fn in + let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update_heap actual_fields) mem in @@ -553,3 +553,4 @@ let checker : Callbacks.proc_callback_args -> Specs.summary = Summary.update_summary post summary | None -> summary + diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b43bcd103..ddcc0cb5d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -83,12 +83,10 @@ module Val = struct let set_traces : TraceSet.t -> t -> t = fun traces x -> {x with traces} - let of_itv itv = {bot with itv} + let of_itv ?(traces= TraceSet.empty) itv = {bot with itv; traces} let of_int n = of_itv (Itv.of_int n) - let of_itv : Itv.t -> t = fun itv -> {bot with itv} - let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} let of_array_blk : ArrayBlk.astate -> t = fun a -> {bot with arrayblk= a} @@ -329,6 +327,10 @@ module Heap = struct PowLoc.fold find_join locs Val.bot + let transform : f:(Val.t -> Val.t) -> PowLoc.t -> astate -> astate = + fun ~f locs mem -> PowLoc.fold (fun loc -> find loc mem |> f |> add loc) locs mem + + let strong_update : PowLoc.t -> Val.t -> astate -> astate = fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem @@ -630,6 +632,10 @@ module MemReach = struct fun p v m -> {m with heap= Heap.strong_update p v m.heap} + let transform_heap : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = + fun ~f p m -> {m with heap= Heap.transform ~f p m.heap} + + let weak_update_stack : PowLoc.t -> Val.t -> t -> t = fun p v m -> {m with stack= Stack.weak_update p v m.stack} @@ -659,6 +665,10 @@ module MemReach = struct weak_update_heap ploc v s + let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = + fun ~f ploc s -> transform_heap ~f ploc s + + let remove_temps : Ident.t list -> t -> t = fun temps m -> {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias} @@ -759,6 +769,10 @@ module Mem = struct let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> f_lift (MemReach.update_mem ploc v) + let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = + fun ~f ploc -> f_lift (MemReach.transform_mem ~f ploc) + + let remove_temps : Ident.t list -> t -> t = fun temps -> f_lift (MemReach.remove_temps temps) end diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d7d389715..69b140b6c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -165,6 +165,50 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct {exec; check} + module Split = struct + let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = + let traces = BufferOverrunTrace.(Call location |> singleton |> Set.singleton) in + let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat in + let increment = Dom.Val.of_itv ~traces increment_itv in + let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in + let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in + let vector_size_locs = + Sem.eval vector_exp mem |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field + in + Dom.Mem.transform_mem ~f:(Dom.Val.plus increment) vector_size_locs mem + + end + + module Boost = struct + module Split = struct + let std_vector vector_arg = + let exec _pname _ret _node location mem = + Split.std_vector ~adds_at_least_one:true vector_arg location mem + in + {exec; check= no_check} + + end + end + + module Folly = struct + module Split = struct + let std_vector vector_arg ignore_empty_opt = + let exec _pname _ret _node location mem = + let adds_at_least_one = + match ignore_empty_opt with + | Some ignore_empty_exp -> + Sem.eval ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false + | None -> + (* default: ignore_empty is false *) + true + in + Split.std_vector ~adds_at_least_one vector_arg location mem + in + {exec; check= no_check} + + end + end + module Procname = struct let dispatch : model ProcnameDispatcher.dispatcher = let open ProcnameDispatcher.Procname in @@ -179,7 +223,11 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct ; -"__new_array" <>$ capt_exp $+...$--> malloc ; -"realloc" <>$ any_arg $+ capt_exp $+...$--> realloc ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length - ; -"strlen" <>--> by_value Dom.Val.Itv.nat ] + ; -"strlen" <>--> by_value Dom.Val.Itv.nat + ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg + $+? any_arg $--> Boost.Split.std_vector + ; -"folly" &:: "split" $ any_arg $+ any_arg $+ capt_arg_of_typ (-"std" &:: "vector") + $+? capt_exp $--> Folly.Split.std_vector ] end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index e32438a83..6fd7df976 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -206,7 +206,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.Cast (_, e) -> eval e mem | Exp.Lfield (e, fn, _) -> - eval e mem |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc + eval e mem |> Val.get_array_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc | Exp.Lindex (e1, e2) -> eval_lindex e1 e2 mem | Exp.Sizeof {nbytes= Some size} -> @@ -299,7 +299,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.Cast (_, e) -> eval_locs e mem | Exp.Lfield (e, fn, _) -> - eval e mem |> Val.get_all_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc + eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc | Exp.Lindex (e1, e2) -> let arr = eval e1 mem in let idx = eval e2 mem in @@ -458,7 +458,7 @@ module Make (CFG : ProcCfg.S) = struct let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in let get_field_name (fn, _, _) = fn in - let append_field v fn = PowLoc.append_field (Val.get_all_locs v) fn in + let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in let deref_ptr v mem = let array_locs = Val.get_array_locs v in diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 174827d71..5aa9fd33c 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -1186,6 +1186,8 @@ let is_bot : t -> bool = fun x -> equal x Bottom let is_finite : t -> bool = function NonBottom x -> ItvPure.is_finite x | Bottom -> false +let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false + let false_sem = NonBottom ItvPure.false_sem let m1_255 = NonBottom ItvPure.m1_255 diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp new file mode 100644 index 000000000..a959defb8 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp @@ -0,0 +1,64 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +#include +#include + +namespace folly { + +template +class fbvector; + +template +struct Optional; + +class fbstring; +class StringPiece; + +template +void split(const Delim& delimiter, + const String& input, + std::vector& out, + const bool ignoreEmpty = false); + +template +void split(const Delim& delimiter, + const String& input, + folly::fbvector& out, + const bool ignoreEmpty = false); + +template +void splitTo(const Delim& delimiter, + const String& input, + OutputIterator out, + const bool ignoreEmpty = false); + +} // namespace folly + +namespace folly_split { +std::string do_not_ignore_empty_Good(const std::string& s) { + std::vector v; + folly::split("delimiter", s, v); + return v[0]; +} + +std::string do_not_ignore_empty2_Good(const std::string& s) { + std::vector v; + folly::split("delimiter", s, v, false); + return v[0]; +} + +std::string do_not_ignore_empty_Bad(const std::string& s) { + std::vector v; + folly::split("delimiter", s, v, true); + return v[0]; +} +} // namespace folly_split diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index e375315a7..599ff3b43 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -2,6 +2,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERR codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]