[inferbo] Add model of String::operator==

Reviewed By: jvillard

Differential Revision: D13552213

fbshipit-source-id: a74460e87

infer/man/man1/infer-analyze.txt

@@ -281,6 +281,10 @@ OPTIONS
            Deactivates: Run the reporting phase once the analysis has
            completed (Conversely: --report)
 
+       --report-force-relative-path
+           Activates: Force converting an absolute path to a relative path to
+           the root directory (Conversely: --no-report-force-relative-path)
+
        --report-hook script
            Specify a script to be executed after the analysis results are
            written. This script will be passed, --issues-json, --issues-txt,

infer/man/man1/infer-full.txt

@@ -747,6 +747,11 @@ OPTIONS
        --report-current path
            report of the latest revision           See also infer-reportdiff(1).
 
+       --report-force-relative-path
+           Activates: Force converting an absolute path to a relative path to
+           the root directory (Conversely: --no-report-force-relative-path)       
+    See also infer-analyze(1) and infer-run(1).
+
        --report-formatter { none | phabricator }
            Which formatter to use when emitting the report (default:
            phabricator)           See also infer-report(1).

infer/man/man1/infer-run.txt

@@ -125,6 +125,10 @@ OPTIONS
            specified OCaml-style regex (to whitelist:
            --<analyzer>-whitelist-path-regex)
 
+       --report-force-relative-path
+           Activates: Force converting an absolute path to a relative path to
+           the root directory (Conversely: --no-report-force-relative-path)
+
        --report-hook script
            Specify a script to be executed after the analysis results are
            written. This script will be passed, --issues-json, --issues-txt,

infer/man/man1/infer.txt

@@ -747,6 +747,11 @@ OPTIONS
        --report-current path
            report of the latest revision           See also infer-reportdiff(1).
 
+       --report-force-relative-path
+           Activates: Force converting an absolute path to a relative path to
+           the root directory (Conversely: --no-report-force-relative-path)       
+    See also infer-analyze(1) and infer-run(1).
+
        --report-formatter { none | phabricator }
            Which formatter to use when emitting the report (default:
            phabricator)           See also infer-report(1).

infer/src/IR/ProcnameDispatcher.ml

@@ -134,7 +134,7 @@ let name_cons :
   let {on_templated_name; get_markers} = m in
   let match_fuzzy_name =
     let fuzzy_name_regexp =
-      name |> Str.quote |> Printf.sprintf "^%s\\(<[a-z0-9_]+>\\)?$" |> Str.regexp
+      name |> Str.quote |> Printf.sprintf "^%s\\(<[a-z0-9_:<>]+>\\)?$" |> Str.regexp
     in
     fun s -> Str.string_match fuzzy_name_regexp s 0
   in
@@ -863,13 +863,23 @@ module Call = struct
     {one_arg_matcher= match_any_arg; capture= capture_arg_var_exn}
 
 
+  let any_arg_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= no_capture}
+
   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 capt_exp_of_prim_typ typ =
+  let one_arg_matcher_of_prim_typ typ =
     let on_typ typ' = Typ.equal_ignore_quals typ typ' in
-    {one_arg_matcher= match_prim_typ on_typ; capture= capture_arg_exp}
+    match_prim_typ on_typ
+
+
+  let any_arg_of_prim_typ typ =
+    {one_arg_matcher= one_arg_matcher_of_prim_typ typ; capture= no_capture}
+
+
+  let capt_exp_of_prim_typ typ =
+    {one_arg_matcher= one_arg_matcher_of_prim_typ typ; capture= capture_arg_exp}
 
 
   let typ1 : 'marker -> ('context, unit, _, 'f, 'f, _, _) one_arg =

infer/src/IR/ProcnameDispatcher.mli

@@ -235,6 +235,10 @@ module Call : sig
   val capt_exp : ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
   (** Captures one arg expression *)
 
+  val any_arg_of_typ :
+    ('context, unit, _, unit, unit, unit) name_matcher -> ('context, unit, _, 'f, 'f, _, _) one_arg
+  (** Eats one arg of the given type *)
+
   val capt_arg_of_typ :
        ('context, unit, _, unit, unit, unit) name_matcher
     -> ('context, FuncArg.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
@@ -245,6 +249,9 @@ module Call : sig
     -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
   (** Captures one arg expression of the given type *)
 
+  val any_arg_of_prim_typ : Typ.t -> ('context, unit, _, 'f, 'f, _, _) one_arg
+  (** Eats one arg of the given primitive 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 *)

infer/src/backend/InferPrint.ml

@@ -273,7 +273,9 @@ module JsonIssuePrinter = MakeJsonListPrinter (struct
     then
       let severity = Exceptions.severity_string err_key.severity in
       let bug_type = err_key.err_name.IssueType.unique_id in
-      let file = SourceFile.to_string source_file in
+      let file =
+        SourceFile.to_string ~force_relative:Config.report_force_relative_path source_file
+      in
       let json_ml_loc =
         match err_data.loc_in_ml_source with
         | Some (file, lnum, cnum, enum) when Config.reports_include_ml_loc ->

infer/src/base/Config.ml

@@ -1875,6 +1875,12 @@ and report_current =
 
 and report_custom_error = CLOpt.mk_bool ~long:"report-custom-error" ""
 
+and report_force_relative_path =
+  CLOpt.mk_bool ~long:"report-force-relative-path" ~default:false
+    ~in_help:InferCommand.[(Analyze, manual_generic); (Run, manual_generic)]
+    "Force converting an absolute path to a relative path to the root directory"
+
+
 and report_formatter =
   CLOpt.mk_symbol ~long:"report-formatter"
     ~in_help:InferCommand.[(Report, manual_generic)]
@@ -2883,6 +2889,8 @@ and report_current = !report_current
 
 and report_custom_error = !report_custom_error
 
+and report_force_relative_path = !report_force_relative_path
+
 and report_formatter = !report_formatter
 
 and report_hook = !report_hook

infer/src/base/Config.mli

@@ -165,6 +165,8 @@ val report_condition_always_true_in_clang : bool
 
 val report_custom_error : bool
 
+val report_force_relative_path : bool
+
 val report_json : string
 
 val report_nullable_inconsistency : bool

infer/src/base/SourceFile.ml

@@ -67,14 +67,20 @@ let from_abs_path ?(warn_on_error = true) fname =
         Absolute fname_real )
 
 
-let to_string fname =
+let to_string =
-  match fname with
+  let root = Utils.realpath Config.project_root in
-  | Invalid origin ->
+  fun ?(force_relative = false) fname ->
-      "DUMMY from " ^ origin
+    match fname with
-  | RelativeInferModel path ->
+    | Invalid origin ->
-      "INFER_MODEL/" ^ path
+        "DUMMY from " ^ origin
-  | RelativeProjectRoot path | Absolute path ->
+    | RelativeInferModel path ->
-      path
+        "INFER_MODEL/" ^ path
+    | RelativeProjectRoot path ->
+        path
+    | Absolute path ->
+        if force_relative then
+          Option.value_exn (Utils.filename_to_relative ~force_full_backtrack:true ~root path)
+        else path
 
 
 let pp fmt fname = Format.pp_print_string fmt (to_string fname)

infer/src/base/SourceFile.mli

@@ -67,7 +67,7 @@ val to_abs_path : t -> string
 val to_rel_path : t -> string
 (** get the relative path of a source file *)
 
-val to_string : t -> string
+val to_string : ?force_relative:bool -> t -> string
 (** convert a source file to a string
     WARNING: result may not be valid file path, do not use this function to perform operations
              on filenames *)

infer/src/base/Utils.ml

@@ -95,12 +95,12 @@ let filename_to_absolute ~root fname =
 
 
 (** Convert an absolute filename to one relative to the given directory. *)
-let filename_to_relative ?(backtrack = 0) ~root fname =
+let filename_to_relative ?(force_full_backtrack = false) ?(backtrack = 0) ~root fname =
   let rec relativize_if_under origin target =
     match (origin, target) with
     | x :: xs, y :: ys when String.equal x y ->
         relativize_if_under xs ys
-    | _ :: _, _ when backtrack >= List.length origin ->
+    | _ :: _, _ when force_full_backtrack || backtrack >= List.length origin ->
         let parent_dir = List.init (List.length origin) ~f:(fun _ -> Filename.parent_dir_name) in
         Some (Filename.of_parts (parent_dir @ target))
     | [], [] ->

infer/src/base/Utils.mli

@@ -23,7 +23,8 @@ val read_file : string -> (string list, string) Result.t
 val filename_to_absolute : root:string -> string -> string
 (** Convert a filename to an absolute one if it is relative, and normalize "." and ".." *)
 
-val filename_to_relative : ?backtrack:int -> root:string -> string -> string option
+val filename_to_relative :
+  ?force_full_backtrack:bool -> ?backtrack:int -> root:string -> string -> string option
 (** Convert an absolute filename to one relative to a root directory.  Returns [None] if filename is
     not under root. The backtrack level sets the maximum level of steps in the parent directories
     to search for a common prefix *)

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -493,6 +493,8 @@ module Val = struct
 
     let top = of_itv Itv.top
 
+    let unknown_bool = of_itv Itv.unknown_bool
+
     let zero = of_itv Itv.zero
   end
 end

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -530,6 +530,7 @@ module Call = struct
     let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in
     let std_array0 = mk_std_array () in
     let std_array2 = mk_std_array () in
+    let char_ptr = Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)) in
     make_dispatcher
       [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min
       ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size
@@ -569,16 +570,35 @@ module Call = struct
       ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
         $+ capt_exp_of_typ (-"std" &:: "basic_string")
         $--> StdBasicString.copy_constructor
-      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
+      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp $+ capt_exp_of_prim_typ char_ptr
-        $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)))
         $--> StdBasicString.constructor_from_char_ptr_without_len
-      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
+      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp $+ capt_exp_of_prim_typ char_ptr
-        $+ 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" &:: "empty" $ capt_exp $--> StdBasicString.empty
       ; -"std" &:: "basic_string" &:: "length" $ capt_exp $--> StdBasicString.length
       ; -"std" &:: "basic_string" &:: "size" $ capt_exp $--> StdBasicString.length
+      ; -"std" &:: "basic_string" &:: "compare" &--> by_value Dom.Val.Itv.top
+      ; -"std" &:: "operator=="
+        $ any_arg_of_typ (-"std" &:: "basic_string")
+        $+ any_arg_of_typ (-"std" &:: "basic_string")
+        $--> by_value Dom.Val.Itv.unknown_bool
+      ; -"std" &:: "operator=="
+        $ any_arg_of_typ (-"std" &:: "basic_string")
+        $+ any_arg_of_prim_typ char_ptr $--> by_value Dom.Val.Itv.unknown_bool
+      ; -"std" &:: "operator==" $ any_arg_of_prim_typ char_ptr
+        $+ any_arg_of_typ (-"std" &:: "basic_string")
+        $--> by_value Dom.Val.Itv.unknown_bool
+      ; -"std" &:: "operator!="
+        $ any_arg_of_typ (-"std" &:: "basic_string")
+        $+ any_arg_of_typ (-"std" &:: "basic_string")
+        $--> by_value Dom.Val.Itv.unknown_bool
+      ; -"std" &:: "operator!="
+        $ any_arg_of_typ (-"std" &:: "basic_string")
+        $+ any_arg_of_prim_typ char_ptr $--> by_value Dom.Val.Itv.unknown_bool
+      ; -"std" &:: "operator!=" $ any_arg_of_prim_typ char_ptr
+        $+ any_arg_of_typ (-"std" &:: "basic_string")
+        $--> by_value Dom.Val.Itv.unknown_bool
       ; -"std" &:: "basic_string" &::.*--> no_model
       ; +PatternMatch.implements_collection
         &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_or_set_at_index

infer/src/bufferoverrun/itv.mli

@@ -123,6 +123,9 @@ val top : t
 val zero : t
 (** 0 *)
 
+val unknown_bool : t
+(** [0, 1] *)
+
 val get_iterator_itv : t -> t
 
 val of_bool : Boolean.t -> t

infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile

@@ -8,7 +8,7 @@ TESTS_DIR = ../../..
 # see explanations in cpp/errors/Makefile for the custom isystem
 CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(MODELS_DIR)/cpp/include -isystem$(CLANG_INCLUDES)/c++/v1/ -c
 INFER_OPTIONS = --bufferoverrun-only --ml-buckets cpp --no-filtering --debug-exceptions \
-                --project-root $(TESTS_DIR)
+                --project-root $(TESTS_DIR) --report-force-relative-path
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.cpp)

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

@@ -1,3 +1,5 @@
+../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==<std::allocator<char>_>, 10, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==<std::allocator<char>_>, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<Int_no_copy,std::allocator<Int_no_copy>>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Binary operation: (this->infer_size - [-oo, +oo]):unsigned64]
 INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<int,std::allocator<int>>_insert<std::__list_iterator<int,_void_*>_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Unknown value from: std::distance<std::__list_iterator<int,_void_*>_>,Binary operation: (this->infer_size + [-oo, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow2_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@@ -76,8 +78,13 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal2_Good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
 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]

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

@@ -158,3 +158,43 @@ void size_Bad() {
   int a[10];
   a[s.size()] = 0;
 }
+
+void compare_Good_FP(std::string s) {
+  if (s.compare(0, s.size(), s) != 0) {
+    int a[10];
+    a[10] = 0;
+  }
+}
+
+void compare_Bad(std::string s) {
+  if (s.compare(0, s.size(), s) == 0) {
+    int a[10];
+    a[10] = 0;
+  }
+}
+
+void equal_Good_FP(std::string s) {
+  if (s != s) {
+    int a[10];
+    a[10] = 0;
+  }
+}
+
+void equal_Bad() {
+  std::string s1("hello");
+  std::string s2("hello");
+  if (s1 == s2) {
+    int a[10];
+    a[10] = 0;
+  }
+}
+
+constexpr char const_s[] = "const_s";
+
+void equal2_Good_FP() {
+  std::string s(const_s);
+  if (s != const_s) {
+    int a[10];
+    a[10] = 0;
+  }
+}