[inferbo] Add model of basic_string

Reviewed By: mbouaziz, jvillard

Differential Revision: D13527054

fbshipit-source-id: 97915e462

infer/src/IR/ProcnameDispatcher.ml

@@ -107,6 +107,8 @@ type ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, 'empt
   ; path_extra: ('context, 'f_in, 'f_out, 'captured_types, 'emptyness) path_extra
   ; get_markers: 'markers_in -> 'markers_out }
 
+type typ_matcher = typ -> bool
+
 (* Combinators *)
 
 let empty : ('context, 'f, 'f, unit, 'markers, 'markers, empty) path_matcher =
@@ -772,6 +774,13 @@ module Call = struct
     {match_arg; marker_static_checker= no_marker_checker}
 
 
+  (** Matches the type matched by the given typ_matcher *)
+  let match_prim_typ : typ_matcher -> _ one_arg_matcher =
+   fun on_typ ->
+    let match_arg _context _capt arg = on_typ (FuncArg.typ arg) in
+    {match_arg; marker_static_checker= no_marker_checker}
+
+
   (* Function argument capture *)
 
   (** Do not capture this argument *)
@@ -855,6 +864,11 @@ module Call = struct
 
   let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp}
 
+  let capt_exp_of_prim_typ typ =
+    let on_typ typ' = Typ.equal typ typ' in
+    {one_arg_matcher= match_prim_typ on_typ; capture= capture_arg_exp}
+
+
   let typ1 : 'marker -> ('context, unit, _, 'f, 'f, _, _) one_arg =
    fun m -> {one_arg_matcher= match_typ1 m; capture= no_capture}
 

infer/src/IR/ProcnameDispatcher.mli

@@ -245,6 +245,10 @@ module Call : sig
     -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
   (** Captures one arg expression of the given type *)
 
+  val capt_exp_of_prim_typ :
+    Typ.t -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
+  (** Captures one arg expression of the given primitive type *)
+
   val capt_var_exn : ('context, Ident.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
   (** Captures one arg Var. Fails with an internal error if the expression is not a Var *)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -37,6 +37,14 @@ let no_exec _model_env ~ret:_ mem = mem
 
 let no_check _model_env _mem cond_set = cond_set
 
+let no_model =
+  let exec {pname} ~ret:_ mem =
+    L.d_printfln_escaped "No model for %a" Typ.Procname.pp pname ;
+    mem
+  in
+  {exec; check= no_check}
+
+
 (* It returns a tuple of:
      - type of array element
      - stride of the type
@@ -312,12 +320,36 @@ module StdArray = struct
         location cond_set
     in
     {exec; check}
+end
+
+module StdBasicString = struct
+  (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
+  let constructor_from_char_ptr tgt src len =
+    let {exec= malloc_exec; check= malloc_check} = malloc len in
+    let exec model_env ~ret:((ret_id, _) as ret) mem =
+      let mem = malloc_exec model_env ~ret mem in
+      let v = Dom.Mem.find (Loc.of_id ret_id) mem in
+      let mem = Dom.Mem.update_mem (Sem.eval_locs tgt mem) v mem in
+      let contents =
+        let src_locs = Sem.eval_locs src mem in
+        Dom.Mem.find_set src_locs mem
+      in
+      Dom.Mem.update_mem (Dom.Val.get_all_locs v) contents mem
+    in
+    let check ({location; integer_type_widths} as model_env) mem cond_set =
+      let cond_set = malloc_check model_env mem cond_set in
+      BoUtils.Check.lindex integer_type_widths ~array_exp:src ~index_exp:len ~last_included:true
+        mem location cond_set
+    in
+    {exec; check}
 
 
-  let no_model =
-    let exec {pname} ~ret:_ mem =
-      L.d_printfln_escaped "No model for %a" Typ.Procname.pp pname ;
-      mem
+  (* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
+  let copy_constructor tgt src =
+    let exec _ ~ret:_ mem =
+      let tgt_locs = Sem.eval_locs tgt mem in
+      let v = Dom.Mem.find_set (Sem.eval_locs src mem) mem in
+      Dom.Mem.update_mem tgt_locs v mem
     in
     {exec; check= no_check}
 end
@@ -492,7 +524,15 @@ module Call = struct
       ; std_array0 >:: "array" &--> StdArray.constructor
       ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at
       ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at
-      ; -"std" &:: "array" &::.*--> StdArray.no_model
+      ; -"std" &:: "array" &::.*--> no_model
+      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
+        $+ capt_exp_of_typ (-"std" &:: "basic_string")
+        $--> StdBasicString.copy_constructor
+      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
+        $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)))
+        $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t))
+        $--> StdBasicString.constructor_from_char_ptr
+      ; -"std" &:: "basic_string" &::.*--> no_model
       ; +PatternMatch.implements_collection
         &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_or_set_at_index
       ; +PatternMatch.implements_collection

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

@@ -79,6 +79,8 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRU
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: snprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: vsnprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024]
+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: [-oo, +oo] Size: 1024]
 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/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]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp

@@ -31,7 +31,7 @@ char last_char2_Bad(const char* fmt, ...) {
   return buf[n - 1];
 }
 
-std::string to_string1_Bad_FN(char* s, int i) {
+std::string to_string1_Bad(char* s, int i) {
   char buf[1024];
   int n = snprintf(buf, sizeof(buf), "%s%d", s, i);
   return std::string(buf, n);
@@ -48,7 +48,7 @@ std::string to_string1_Good(char* s, int i) {
   return std::string(buf, n);
 }
 
-std::string to_string2_Bad_FN(const char* fmt, ...) {
+std::string to_string2_Bad(const char* fmt, ...) {
   char buf[1024];
   va_list args;
   va_start(args, fmt);