From 05ceaebb7d5974eb7e26b900a7dae4dfe58a7973 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sun, 6 Jan 2019 21:01:27 -0800 Subject: [PATCH] [inferbo] Add model of String::operator== Reviewed By: jvillard Differential Revision: D13552213 fbshipit-source-id: a74460e87 --- infer/man/man1/infer-analyze.txt | 4 ++ infer/man/man1/infer-full.txt | 5 +++ infer/man/man1/infer-run.txt | 4 ++ infer/man/man1/infer.txt | 5 +++ infer/src/IR/ProcnameDispatcher.ml | 16 ++++++-- infer/src/IR/ProcnameDispatcher.mli | 7 ++++ infer/src/backend/InferPrint.ml | 4 +- infer/src/base/Config.ml | 8 ++++ infer/src/base/Config.mli | 2 + infer/src/base/SourceFile.ml | 22 ++++++---- infer/src/base/SourceFile.mli | 2 +- infer/src/base/Utils.ml | 4 +- infer/src/base/Utils.mli | 3 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 + .../src/bufferoverrun/bufferOverrunModels.ml | 28 +++++++++++-- infer/src/bufferoverrun/itv.mli | 3 ++ .../codetoanalyze/cpp/bufferoverrun/Makefile | 2 +- .../cpp/bufferoverrun/issues.exp | 7 ++++ .../cpp/bufferoverrun/std_string.cpp | 40 +++++++++++++++++++ 19 files changed, 147 insertions(+), 21 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 53104923c..a2b57db4c 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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, diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index ab1fcc774..abcbad7f4 100644 --- a/infer/man/man1/infer-full.txt +++ b/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). diff --git a/infer/man/man1/infer-run.txt b/infer/man/man1/infer-run.txt index aff1029c1..f698386f8 100644 --- a/infer/man/man1/infer-run.txt +++ b/infer/man/man1/infer-run.txt @@ -125,6 +125,10 @@ OPTIONS specified OCaml-style regex (to whitelist: ---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, diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 857134e6f..e5804bdac 100644 --- a/infer/man/man1/infer.txt +++ b/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). diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index dab11b58c..389cae900 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/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 = diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 1251ec8c3..d2cdb4d80 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/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 *) diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 19064bb38..a522975d4 100644 --- a/infer/src/backend/InferPrint.ml +++ b/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 -> diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 2ce393a21..a9ac0b849 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 5e6f43d6b..376ea3822 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/base/SourceFile.ml b/infer/src/base/SourceFile.ml index 243a606c6..860d3fa11 100644 --- a/infer/src/base/SourceFile.ml +++ b/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 = - match fname with - | Invalid origin -> - "DUMMY from " ^ origin - | RelativeInferModel path -> - "INFER_MODEL/" ^ path - | RelativeProjectRoot path | Absolute path -> - path +let to_string = + let root = Utils.realpath Config.project_root in + fun ?(force_relative = false) fname -> + match fname with + | Invalid origin -> + "DUMMY from " ^ origin + | RelativeInferModel 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) diff --git a/infer/src/base/SourceFile.mli b/infer/src/base/SourceFile.mli index e5955fac8..c825fbb30 100644 --- a/infer/src/base/SourceFile.mli +++ b/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 *) diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index 96184aad9..6f54f1152 100644 --- a/infer/src/base/Utils.ml +++ b/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)) | [], [] -> diff --git a/infer/src/base/Utils.mli b/infer/src/base/Utils.mli index ca246b057..002b30bc9 100644 --- a/infer/src/base/Utils.mli +++ b/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 *) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 8b67a04fd..005744555 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 899d2858c..1264eb3c9 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 - $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer))) + ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp $+ capt_exp_of_prim_typ char_ptr $--> StdBasicString.constructor_from_char_ptr_without_len - ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp - $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer))) + ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp $+ capt_exp_of_prim_typ char_ptr $+ 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 diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 1547d0ae2..a8f3a0928 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile index 18af120f8..f7c584692 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile +++ b/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) diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index d8a4b17c5..0e90e825a 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,3 +1,5 @@ +../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==_>, 10, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==_>, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this->infer_size`,,Unknown value from: std::distance_>,Binary operation: (this->infer_size - [-oo, +oo]):unsigned64] INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this->infer_size`,,Unknown value from: std::distance_>,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, [,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, [,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,,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, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,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, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, equal_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Risky value from: snprintf,Assignment,,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, [,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, [,Risky value from: vsnprintf,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp index e5133e169..645ffb262 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp +++ b/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; + } +}