[inferbo] Revise split model semantics

Reviewed By: ezgicicek

Differential Revision: D19942999

fbshipit-source-id: c1d945160

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -674,20 +674,22 @@ module StdVector = struct
 end
 
 module Split = struct
-  let std_vector ~adds_at_least_one {exp= vector_exp; typ= vector_typ} location mem =
+  let std_vector model_env ~adds_at_least_one ({typ= vector_typ} as vec_arg) mem =
-    let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in
+    match vector_typ with
-    let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in
+    | Typ.{desc= Tptr ({desc= Tstruct (CppClass (_, Template {args= TType elt_typ :: _}))}, _)} ->
-    let size_field = Fieldname.make vector_type_name "infer_size" in
+        let arr_locs = StdVector.deref_of model_env elt_typ vec_arg mem in
-    let vector_size_locs = Sem.eval_locs vector_exp mem |> PowLoc.append_field ~fn:size_field in
+        let size = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in
-    let f_trace _ traces = Trace.(Set.add_elem location (through ~risky_fun:None)) traces in
+        StdVector.set_size model_env arr_locs size mem
-    Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem
+    | _ ->
+        Logging.d_printfln_escaped "Could not find element type of vector" ;
+        mem
 end
 
 module Boost = struct
   module Split = struct
     let std_vector vector_arg =
-      let exec {location} ~ret:_ mem =
+      let exec model_env ~ret:_ mem =
-        Split.std_vector ~adds_at_least_one:true vector_arg location mem
+        Split.std_vector model_env ~adds_at_least_one:true vector_arg mem
       in
       {exec; check= no_check}
   end
@@ -696,7 +698,7 @@ end
 module Folly = struct
   module Split = struct
     let std_vector vector_arg ignore_empty_opt =
-      let exec {location; integer_type_widths} ~ret:_ mem =
+      let exec ({integer_type_widths} as model_env) ~ret:_ mem =
         let adds_at_least_one =
           match ignore_empty_opt with
           | Some ignore_empty_exp ->
@@ -705,7 +707,7 @@ module Folly = struct
               (* default: ignore_empty is false *)
               true
         in
-        Split.std_vector ~adds_at_least_one vector_arg location mem
+        Split.std_vector model_env ~adds_at_least_one vector_arg mem
       in
       {exec; check= no_check}
   end

infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp

@@ -42,13 +42,13 @@ void splitTo(const Delim& delimiter,
 } // namespace folly
 
 namespace folly_split {
-std::string FP_do_not_ignore_empty_Good(const std::string& s) {
+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 FP_do_not_ignore_empty2_Good(const std::string& s) {
+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];

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

@@ -46,9 +46,7 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_throw_exc
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, throw_exception, 3, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::FP_do_not_ignore_empty2_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
+codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::FP_do_not_ignore_empty_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `length`,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]