[cost] Add model of `google::StrLen`

Reviewed By: ezgicicek

Differential Revision: D22357433

fbshipit-source-id: f3a8bf1b4

Makefile

@@ -66,6 +66,7 @@ DIRECT_TESTS += \
   cpp_linters \
   cpp_linters-for-test-only \
   cpp_liveness \
+  cpp_performance \
   cpp_pulse \
   cpp_quandary \
   cpp_racerd \

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -177,11 +177,9 @@ let memset arr_exp size_exp =
   {exec; check}
 
 
-let eval_string_len arr_exp mem = Dom.Mem.get_c_strlen (Sem.eval_locs arr_exp mem) mem
-
 let strlen arr_exp =
   let exec _ ~ret:(id, _) mem =
-    let v = eval_string_len arr_exp mem in
+    let v = Sem.eval_string_len arr_exp mem in
     Dom.Mem.add_stack (Loc.of_id id) v mem
   in
   {exec; check= no_check}
@@ -1536,6 +1534,7 @@ module Call = struct
       ; -"std" &:: "vector" < capt_typ &+ any_typ >:: "vector"
         $ capt_arg_of_typ (-"std" &:: "vector")
         $--> StdVector.constructor_empty
+      ; -"google" &:: "StrLen" <>$ capt_exp $--> strlen
       ; (* Java models *)
         -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone
       ; +PatternMatch.implements_arrays &:: "asList" <>$ capt_exp $!--> create_copy_array

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -518,6 +518,8 @@ let eval_array_locs_length arr_locs mem =
         conservative_array_length ~traces arr_locs mem
 
 
+let eval_string_len exp mem = Mem.get_c_strlen (eval_locs exp mem) mem
+
 module Prune = struct
   type t = {prune_pairs: PrunePairs.t; mem: Mem.t}
 

infer/src/bufferoverrun/bufferOverrunSemantics.mli

@@ -32,6 +32,9 @@ val eval_array_locs_length :
   AbsLoc.PowLoc.t -> _ BufferOverrunDomain.Mem.t0 -> BufferOverrunDomain.Val.t
 (** Evaluate length of array locations *)
 
+val eval_string_len : Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
+(** Evaluate length of C string *)
+
 val conservative_array_length :
      ?traces:BufferOverrunTrace.Set.t
   -> AbsLoc.PowLoc.t

infer/src/cost/costModels.ml

@@ -138,6 +138,7 @@ end
 
 module BoundsOfCollection = BoundsOf (CostUtils.Collection)
 module BoundsOfArray = BoundsOf (CostUtils.Array)
+module BoundsOfCString = BoundsOf (CostUtils.CString)
 
 module ImmutableSet = struct
   let construct = linear ~of_function:"ImmutableSet.construct"
@@ -151,7 +152,9 @@ module Call = struct
     let int_typ = Typ.mk (Typ.Tint Typ.IInt) in
     let dispatcher =
       make_dispatcher
-        [ +PatternMatch.implements_collections
+        [ -"google" &:: "StrLen" <>$ capt_exp
+          $--> BoundsOfCString.linear_length ~of_function:"google::StrLen"
+        ; +PatternMatch.implements_collections
           &:: "sort" $ capt_exp
           $+...$--> BoundsOfCollection.n_log_n_length ~of_function:"Collections.sort"
         ; +PatternMatch.implements_list &:: "sort" $ capt_exp

infer/src/cost/costUtils.ml

@@ -54,3 +54,7 @@ module Collection : S = struct
   let length coll_exp inferbo_mem =
     BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem
 end
+
+module CString : S = struct
+  let length exp inferbo_mem = BufferOverrunSemantics.eval_string_len exp inferbo_mem
+end

infer/tests/codetoanalyze/cpp/performance/Makefile

@@ -0,0 +1,22 @@
+# 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.
+
+TESTS_DIR = ../../..
+
+# see explanations in cpp/biabduction/Makefile for the custom isystem
+CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
+INFER_OPTIONS = --cost-only --ml-buckets cpp --no-filtering --debug-exceptions \
+                --project-root $(TESTS_DIR) --report-force-relative-path --debug
+INFERPRINT_OPTIONS = --issues-tests
+INFERPRINT_COST_OPTIONS = --cost-issues-tests
+
+SOURCES = $(wildcard *.cpp)
+
+HEADERS =
+
+include $(TESTS_DIR)/clang.make
+include $(TESTS_DIR)/cost.make
+
+infer-out/report.json: $(MAKEFILE_LIST)

infer/tests/codetoanalyze/cpp/performance/cost-issues.exp

@@ -0,0 +1,2 @@
+codetoanalyze/cpp/performance/string_test.cpp, call_google_strlen_linear, 3 + str->strlen.ub(u),  OnUIThread:false, [{str->strlen.ub(u)},Modeled call to google::StrLen]
+codetoanalyze/cpp/performance/string_test.cpp, call_google_strlen_with_loop_linear, 5 + 3 ⋅ str->strlen.ub(u) + str->strlen.ub(u) + 2 ⋅ (str->strlen.ub(u) + 1),  OnUIThread:false, [{str->strlen.ub(u) + 1},Loop at line 16, column 3,{str->strlen.ub(u)},Modeled call to google::StrLen,{str->strlen.ub(u)},Loop at line 16, column 3]

infer/tests/codetoanalyze/cpp/performance/string_test.cpp

@@ -0,0 +1,18 @@
+/*
+ * 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.
+ */
+
+namespace google {
+int StrLen(char*);
+}
+
+void call_google_strlen_linear(char* str) { int len = google::StrLen(str); }
+
+void call_google_strlen_with_loop_linear(char* str) {
+  int len = google::StrLen(str);
+  for (int i = 0; i < len; i++) {
+  }
+}