[inferbo] Model for folly::split

Summary:
Model for `folly::split` that handles the representation in the cpp model.

Depends on D6544992

Reviewed By: jvillard

Differential Revision: D6545006

fbshipit-source-id: 2b7a139

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 <! () &+ template_arg
 
   let ( >:: ) 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}
 

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 *)
 

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

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
+

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
 

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
 

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

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

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 <vector>
+#include <string>
+
+namespace folly {
+
+template <class T>
+class fbvector;
+
+template <class T>
+struct Optional;
+
+class fbstring;
+class StringPiece;
+
+template <class Delim, class String, class OutputType>
+void split(const Delim& delimiter,
+           const String& input,
+           std::vector<OutputType>& out,
+           const bool ignoreEmpty = false);
+
+template <class Delim, class String, class OutputType>
+void split(const Delim& delimiter,
+           const String& input,
+           folly::fbvector<OutputType>& out,
+           const bool ignoreEmpty = false);
+
+template <class OutputValueType,
+          class Delim,
+          class String,
+          class OutputIterator>
+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<std::string> v;
+  folly::split("delimiter", s, v);
+  return v[0];
+}
+
+std::string do_not_ignore_empty2_Good(const std::string& s) {
+  std::vector<std::string> v;
+  folly::split("delimiter", s, v, false);
+  return v[0];
+}
+
+std::string do_not_ignore_empty_Bad(const std::string& s) {
+  std::vector<std::string> v;
+  folly::split("delimiter", s, v, true);
+  return v[0];
+}
+} // namespace folly_split

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