From a49b094e0cb1ab5739358de20b91efc512b0c9c9 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 18 Jun 2020 08:52:48 -0700 Subject: [PATCH] [inferbo] Remove unused issue types Summary: This diff removes unused issue types, `BUFFER_OVERRUN_R2`, `BUFFER_OVERRUN_T1`, `INTEGER_OVERFLOW_R2`, and `INFERBO_ALLOC_MAY_BE_TAINTED`. Reviewed By: ezgicicek Differential Revision: D22114388 fbshipit-source-id: 88743ce88 --- Makefile | 4 - infer/documentation/issues/BUFFER_OVERRUN.md | 21 -- .../documentation/issues/INTEGER_OVERFLOW.md | 4 - infer/man/man1/infer-analyze.txt | 5 - infer/man/man1/infer-full.txt | 9 - infer/man/man1/infer-report.txt | 4 - infer/man/man1/infer.txt | 9 - infer/src/base/Config.ml | 8 - infer/src/base/Config.mli | 2 - infer/src/base/IssueType.ml | 22 --- infer/src/base/IssueType.mli | 9 - .../src/bufferoverrun/bufferOverrunDomain.ml | 180 ++---------------- .../src/bufferoverrun/bufferOverrunDomain.mli | 28 +-- .../src/bufferoverrun/bufferOverrunModels.ml | 24 +-- .../bufferOverrunProofObligations.ml | 169 +++++++--------- .../bufferOverrunProofObligations.mli | 2 - .../bufferoverrun/bufferOverrunSemantics.ml | 7 +- infer/src/bufferoverrun/bufferOverrunTrace.ml | 54 +----- .../src/bufferoverrun/bufferOverrunTrace.mli | 16 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 18 +- infer/src/bufferoverrun/symb.ml | 11 -- infer/src/bufferoverrun/symb.mli | 4 - infer/src/opensource/FbPatternMatch.ml | 8 - infer/src/opensource/FbPatternMatch.mli | 8 - .../codetoanalyze/c/bufferoverrun/issues.exp | 6 +- .../cpp/bufferoverrun/issues.exp | 8 +- .../tests/codetoanalyze/cpp/fb-taint/Makefile | 20 -- 27 files changed, 111 insertions(+), 549 deletions(-) delete mode 100644 infer/src/opensource/FbPatternMatch.ml delete mode 100644 infer/src/opensource/FbPatternMatch.mli delete mode 100644 infer/tests/codetoanalyze/cpp/fb-taint/Makefile diff --git a/Makefile b/Makefile index 4f1808f4e..ecdd6e672 100644 --- a/Makefile +++ b/Makefile @@ -74,10 +74,6 @@ DIRECT_TESTS += \ cpp_starvation \ cpp_uninit \ -ifeq ($(IS_FACEBOOK_TREE),yes) -DIRECT_TESTS += cpp_fb-taint -endif - ifneq ($(BUCK),no) BUILD_SYSTEMS_TESTS += \ buck_blacklist \ diff --git a/infer/documentation/issues/BUFFER_OVERRUN.md b/infer/documentation/issues/BUFFER_OVERRUN.md index 33fc86c70..865ac995f 100644 --- a/infer/documentation/issues/BUFFER_OVERRUN.md +++ b/infer/documentation/issues/BUFFER_OVERRUN.md @@ -16,29 +16,8 @@ report. The higher the number, the more likely it is to be a false positive. * `L3`: The reports that are not included in the above cases. -Other than them, there are some specific-purpose buffer overrun reports as follows. - -* `R2`: An array access is unsafe by *risky* array values from `strndup`. For example, suppose - there is a `strndup` call as follows. - - ```c - char* s1 = (char*)malloc(sizeof(char) * size); - for (int i = 0; i < size; i++) { - s1[i] = 'a'; - } - s1[5] = '\0'; - char* s2 = strndup(s1, size - 1); - s2[size - 1] = 'a'; - ``` - - Even if the second parameter of `strndup` is `size - 1`, the length of `s2` can be shorter than - `size` if there is the null character in the middle of `s1`. - * `S2`: An array access is unsafe by symbolic values. For example, array size: `[n,n]`, offset `[n,+oo]`. -* `T1`: An array access is unsafe by tainted external values. This is experimental and will be - removed sooner or later. - * `U5`: An array access is unsafe by unknown values, which are usually from unknown function calls. diff --git a/infer/documentation/issues/INTEGER_OVERFLOW.md b/infer/documentation/issues/INTEGER_OVERFLOW.md index 7c5a63f1a..7a6f8d785 100644 --- a/infer/documentation/issues/INTEGER_OVERFLOW.md +++ b/infer/documentation/issues/INTEGER_OVERFLOW.md @@ -10,9 +10,5 @@ report. The higher the number, the more likely it is to be a false positive. * `L5`: The reports that are not included in the above cases. -Other than them, there as some specific-purpose buffer overrun reports as follows. - -* `R2`: A binary integer operation is unsafe by *risky* return values from `strndup`. - * `U5`: A binary integer operation is unsafe by unknown values, which are usually from unknown function calls. diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index b1b133aab..163ee5a7d 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -376,11 +376,6 @@ BUFFER OVERRUN OPTIONS --bo-field-depth-limit int Limit of field depth of abstract location in buffer-overrun checker - - --bo-service-handler-request - Activates: [EXPERIMENTAL] Use taint flow of service handler - requests in buffer overflow checking. (Conversely: - --no-bo-service-handler-request) CLANG OPTIONS --annotation-reachability-cxx json Specify annotation reachability analyses to be performed on diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 0d85fe1e1..51608b311 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -127,11 +127,6 @@ OPTIONS Limit of field depth of abstract location in buffer-overrun checker See also infer-analyze(1). - --bo-service-handler-request - Activates: [EXPERIMENTAL] Use taint flow of service handler - requests in buffer overflow checking. (Conversely: - --no-bo-service-handler-request) See also infer-analyze(1). - --bootclasspath string Specify the Java bootclasspath See also infer-capture(1). @@ -376,9 +371,7 @@ OPTIONS BUFFER_OVERRUN_L3 (enabled by default), BUFFER_OVERRUN_L4 (disabled by default), BUFFER_OVERRUN_L5 (disabled by default), - BUFFER_OVERRUN_R2 (enabled by default), BUFFER_OVERRUN_S2 (enabled by default), - BUFFER_OVERRUN_T1 (enabled by default), BUFFER_OVERRUN_U5 (disabled by default), Bad_footprint (enabled by default), CAPTURED_STRONG_SELF (enabled by default), @@ -452,14 +445,12 @@ OPTIONS INFERBO_ALLOC_IS_ZERO (enabled by default), INFERBO_ALLOC_MAY_BE_BIG (enabled by default), INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default), - INFERBO_ALLOC_MAY_BE_TAINTED (enabled by default), INFINITE_EXECUTION_TIME (disabled by default), INHERENTLY_DANGEROUS_FUNCTION (enabled by default), INSECURE_INTENT_HANDLING (enabled by default), INTEGER_OVERFLOW_L1 (enabled by default), INTEGER_OVERFLOW_L2 (enabled by default), INTEGER_OVERFLOW_L5 (disabled by default), - INTEGER_OVERFLOW_R2 (enabled by default), INTEGER_OVERFLOW_U5 (disabled by default), INTERFACE_NOT_THREAD_SAFE (enabled by default), INVARIANT_CALL (disabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 6e88fe21f..03c66c375 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -96,9 +96,7 @@ OPTIONS BUFFER_OVERRUN_L3 (enabled by default), BUFFER_OVERRUN_L4 (disabled by default), BUFFER_OVERRUN_L5 (disabled by default), - BUFFER_OVERRUN_R2 (enabled by default), BUFFER_OVERRUN_S2 (enabled by default), - BUFFER_OVERRUN_T1 (enabled by default), BUFFER_OVERRUN_U5 (disabled by default), Bad_footprint (enabled by default), CAPTURED_STRONG_SELF (enabled by default), @@ -172,14 +170,12 @@ OPTIONS INFERBO_ALLOC_IS_ZERO (enabled by default), INFERBO_ALLOC_MAY_BE_BIG (enabled by default), INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default), - INFERBO_ALLOC_MAY_BE_TAINTED (enabled by default), INFINITE_EXECUTION_TIME (disabled by default), INHERENTLY_DANGEROUS_FUNCTION (enabled by default), INSECURE_INTENT_HANDLING (enabled by default), INTEGER_OVERFLOW_L1 (enabled by default), INTEGER_OVERFLOW_L2 (enabled by default), INTEGER_OVERFLOW_L5 (disabled by default), - INTEGER_OVERFLOW_R2 (enabled by default), INTEGER_OVERFLOW_U5 (disabled by default), INTERFACE_NOT_THREAD_SAFE (enabled by default), INVARIANT_CALL (disabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 79a09c63c..518b279c9 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -127,11 +127,6 @@ OPTIONS Limit of field depth of abstract location in buffer-overrun checker See also infer-analyze(1). - --bo-service-handler-request - Activates: [EXPERIMENTAL] Use taint flow of service handler - requests in buffer overflow checking. (Conversely: - --no-bo-service-handler-request) See also infer-analyze(1). - --bootclasspath string Specify the Java bootclasspath See also infer-capture(1). @@ -376,9 +371,7 @@ OPTIONS BUFFER_OVERRUN_L3 (enabled by default), BUFFER_OVERRUN_L4 (disabled by default), BUFFER_OVERRUN_L5 (disabled by default), - BUFFER_OVERRUN_R2 (enabled by default), BUFFER_OVERRUN_S2 (enabled by default), - BUFFER_OVERRUN_T1 (enabled by default), BUFFER_OVERRUN_U5 (disabled by default), Bad_footprint (enabled by default), CAPTURED_STRONG_SELF (enabled by default), @@ -452,14 +445,12 @@ OPTIONS INFERBO_ALLOC_IS_ZERO (enabled by default), INFERBO_ALLOC_MAY_BE_BIG (enabled by default), INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default), - INFERBO_ALLOC_MAY_BE_TAINTED (enabled by default), INFINITE_EXECUTION_TIME (disabled by default), INHERENTLY_DANGEROUS_FUNCTION (enabled by default), INSECURE_INTENT_HANDLING (enabled by default), INTEGER_OVERFLOW_L1 (enabled by default), INTEGER_OVERFLOW_L2 (enabled by default), INTEGER_OVERFLOW_L5 (disabled by default), - INTEGER_OVERFLOW_R2 (enabled by default), INTEGER_OVERFLOW_U5 (disabled by default), INTERFACE_NOT_THREAD_SAFE (enabled by default), INVARIANT_CALL (disabled by default), diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index ca11cc52c..8bc422278 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -657,12 +657,6 @@ and bo_field_depth_limit = "Limit of field depth of abstract location in buffer-overrun checker" -and bo_service_handler_request = - CLOpt.mk_bool ~long:"bo-service-handler-request" - ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)] - "[EXPERIMENTAL] Use taint flow of service handler requests in buffer overflow checking." - - and bootclasspath = CLOpt.mk_string_opt ~long:"bootclasspath" ~in_help:InferCommand.[(Capture, manual_java)] @@ -2627,8 +2621,6 @@ and bo_debug = !bo_debug and bo_field_depth_limit = !bo_field_depth_limit -and bo_service_handler_request = !bo_service_handler_request - and buck = !buck and buck_blacklist = !buck_blacklist diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index a10869fac..22320c2c4 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -172,8 +172,6 @@ val bo_debug : int val bo_field_depth_limit : int option -val bo_service_handler_request : bool - val bootclasspath : string option val buck : bool diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index ca67c43ff..3c3b0906c 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -284,21 +284,11 @@ let buffer_overrun_l5 = ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" -let buffer_overrun_r2 = - register_from_string ~id:"BUFFER_OVERRUN_R2" Error BufferOverrunChecker - ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" - - let buffer_overrun_s2 = register_from_string ~id:"BUFFER_OVERRUN_S2" Error BufferOverrunChecker ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" -let buffer_overrun_t1 = - register_from_string ~id:"BUFFER_OVERRUN_T1" Error BufferOverrunChecker - ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" - - let buffer_overrun_u5 = register_from_string ~enabled:false ~id:"BUFFER_OVERRUN_U5" Error BufferOverrunChecker ~user_documentation:"See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)" @@ -648,13 +638,6 @@ let inferbo_alloc_may_be_negative = ~user_documentation:"`malloc` *may* be called with a negative value." -let inferbo_alloc_may_be_tainted = - register_from_string ~id:"INFERBO_ALLOC_MAY_BE_TAINTED" Error BufferOverrunChecker - ~user_documentation: - "`malloc` *may* be called with a tainted value from external sources. This is experimental \ - and will be removed sooner or later." - - let infinite_cost_call ~kind = register_from_cost_string ~enabled:false "INFINITE_%s" ~kind let inherently_dangerous_function = @@ -681,11 +664,6 @@ let integer_overflow_l5 = ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" -let integer_overflow_r2 = - register_from_string ~id:"INTEGER_OVERFLOW_R2" Error BufferOverrunChecker - ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" - - let integer_overflow_u5 = register_from_string ~enabled:false ~id:"INTEGER_OVERFLOW_U5" Error BufferOverrunChecker ~user_documentation:"See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index e1c8e87f3..58ca34c75 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -95,13 +95,8 @@ val buffer_overrun_l4 : t val buffer_overrun_l5 : t -val buffer_overrun_r2 : t - val buffer_overrun_s2 : t -val buffer_overrun_t1 : t -(** Tainted values is used in array accesses, causing buffer over/underruns *) - val buffer_overrun_u5 : t val cannot_star : t @@ -227,8 +222,6 @@ val inferbo_alloc_may_be_big : t val inferbo_alloc_may_be_negative : t -val inferbo_alloc_may_be_tainted : t - val infinite_cost_call : kind:CostKind.t -> t val inherently_dangerous_function : t @@ -241,8 +234,6 @@ val integer_overflow_l2 : t val integer_overflow_l5 : t -val integer_overflow_r2 : t - val integer_overflow_u5 : t val interface_not_thread_safe : t diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1cf1838e4..e1a657425 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -15,7 +15,6 @@ module F = Format module L = Logging module OndemandEnv = BufferOverrunOndemandEnv module SPath = Symb.SymbolPath -module SPathSet = Symb.SymbolPathSet module Trace = BufferOverrunTrace module TraceSet = Trace.Set module LoopHeadLoc = Location @@ -83,128 +82,10 @@ module ModeledRange = struct let of_big_int ~trace z = NonBottom (Bounds.NonNegativeBound.of_big_int ~trace z) end -module type TaintS = sig - include AbstractDomain.WithBottom - - val compare : t -> t -> int - - val pp : F.formatter -> t -> unit - - val is_tainted : t -> bool - - val param_of_path : SPath.partial -> t - - val tainted_of_path : SPath.partial -> t - - type eval_taint = SPath.partial -> t - - val subst : t -> eval_taint -> t -end - -module Taint = struct - module Unit = struct - include AbstractDomain.Empty - - let compare _ _ = 0 - - let bottom = () - - let is_bottom _ = true - - let pp _ _ = () - - let is_tainted _ = false - - let param_of_path _ = () - - let tainted_of_path _ = () - - type eval_taint = SPath.partial -> t - - let subst _ _ = () - end - - module ServiceHandlerRequest = struct - type t = - | Param of SPathSet.t - | Tainted of SPathSet.t (* The path set of [Tainted] should be non-empty. *) - [@@deriving compare] - - let pp f = function - | Param params -> - if SPathSet.is_empty params then F.pp_print_string f "not tainted" - else F.fprintf f "unknown taint from %a" SPathSet.pp params - | Tainted params -> - assert (not (SPathSet.is_empty params)) ; - F.fprintf f "tainted by %a" SPathSet.pp params - - - let leq ~lhs ~rhs = - match (lhs, rhs) with - | Param _, Tainted _ -> - true - | Tainted _, Param _ -> - false - | Param params1, Param params2 | Tainted params1, Tainted params2 -> - SPathSet.subset params1 params2 - - - let join x y = - match (x, y) with - | Param _, Tainted _ -> - y - | Tainted _, Param _ -> - x - | Param params1, Param params2 -> - Param (SPathSet.union params1 params2) - | Tainted params1, Tainted params2 -> - Tainted (SPathSet.union params1 params2) - - - let widen ~prev ~next ~num_iters:_ = join prev next - - let bottom = Param SPathSet.empty - - let is_bottom = function - | Param paths -> - SPathSet.is_empty paths - | Tainted paths -> - assert (not (SPathSet.is_empty paths)) ; - false - - - let is_tainted = function - | Tainted paths -> - assert (not (SPathSet.is_empty paths)) ; - true - | _ -> - false - - - let param_of_path path = Param (SPathSet.singleton path) - - let tainted_of_path path = Tainted (SPathSet.singleton path) - - type eval_taint = SPath.partial -> t - - let subst x eval_taint = - match x with - | Tainted _ -> - x - | Param params -> - let accum_subst path acc = join acc (eval_taint path) in - SPathSet.fold accum_subst params bottom - end - - include ( val if Config.bo_service_handler_request then (module ServiceHandlerRequest) - else (module Unit) : TaintS ) -end - type eval_sym_trace = { eval_sym: Bounds.Bound.eval_sym ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t - ; eval_locpath: PowLoc.eval_locpath - ; eval_taint: Taint.eval_taint } + ; eval_locpath: PowLoc.eval_locpath } module Val = struct type t = @@ -212,7 +93,6 @@ module Val = struct ; itv_thresholds: ItvThresholds.t ; itv_updated_by: ItvUpdatedBy.t ; modeled_range: ModeledRange.t - ; taint: Taint.t ; powloc: PowLoc.t ; arrayblk: ArrayBlk.t ; traces: TraceSet.t } @@ -222,7 +102,6 @@ module Val = struct ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.bottom ; modeled_range= ModeledRange.bottom - ; taint= Taint.bottom ; powloc= PowLoc.bot ; arrayblk= ArrayBlk.bot ; traces= TraceSet.bottom } @@ -240,16 +119,12 @@ module Val = struct if not (ModeledRange.is_bottom range) then F.fprintf fmt " (modeled_range:%a)" ModeledRange.pp range in - let taint_pp fmt taint = - if Config.bo_service_handler_request && Config.bo_debug >= 3 then - F.fprintf fmt "(%a)" Taint.pp taint - in let trace_pp fmt traces = if Config.bo_debug >= 3 then F.fprintf fmt ", %a" TraceSet.pp traces in - F.fprintf fmt "(%a%a%a%a%a, %a, %a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds - itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range taint_pp x.taint PowLoc.pp - x.powloc ArrayBlk.pp x.arrayblk trace_pp x.traces + F.fprintf fmt "(%a%a%a%a, %a, %a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds + itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range PowLoc.pp x.powloc + ArrayBlk.pp x.arrayblk trace_pp x.traces let unknown_from : Typ.t -> callee_pname:_ -> location:_ -> t = @@ -260,7 +135,6 @@ module Val = struct ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.Top ; modeled_range= ModeledRange.bottom - ; taint= Taint.bottom ; powloc= (if is_int then PowLoc.bot else PowLoc.unknown) ; arrayblk= (if is_int then ArrayBlk.bottom else ArrayBlk.unknown) ; traces } @@ -273,7 +147,6 @@ module Val = struct && ItvThresholds.leq ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds && ItvUpdatedBy.leq ~lhs:lhs.itv_updated_by ~rhs:rhs.itv_updated_by && ModeledRange.leq ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range - && Taint.leq ~lhs:lhs.taint ~rhs:rhs.taint && PowLoc.leq ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.leq ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk @@ -291,7 +164,6 @@ module Val = struct ItvUpdatedBy.widen ~prev:prev.itv_updated_by ~next:next.itv_updated_by ~num_iters ; modeled_range= ModeledRange.widen ~prev:prev.modeled_range ~next:next.modeled_range ~num_iters - ; taint= Taint.widen ~prev:prev.taint ~next:next.taint ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters ; traces= TraceSet.join prev.traces next.traces } @@ -305,7 +177,6 @@ module Val = struct ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds ; itv_updated_by= ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by ; modeled_range= ModeledRange.join x.modeled_range y.modeled_range - ; taint= Taint.join x.taint y.taint ; powloc= PowLoc.join x.powloc y.powloc ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk ; traces= TraceSet.join x.traces y.traces } @@ -325,11 +196,9 @@ module Val = struct let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x) - let get_taint : t -> Taint.t = fun x -> x.taint - let get_traces : t -> TraceSet.t = fun x -> x.traces - let of_itv ?(traces = TraceSet.bottom) ?(taint = Taint.bottom) itv = {bot with itv; taint; traces} + let of_itv ?(traces = TraceSet.bottom) itv = {bot with itv; traces} let of_int n = of_itv (Itv.of_int n) @@ -391,7 +260,6 @@ module Val = struct let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in let itv_updated_by = ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by in let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in - let taint = Taint.join x.taint y.taint in let traces = match f_trace with | Some f_trace -> @@ -405,7 +273,7 @@ module Val = struct | true, true | false, false -> TraceSet.join x.traces y.traces ) in - {bot with itv; itv_thresholds; itv_updated_by; modeled_range; taint; traces} + {bot with itv; itv_thresholds; itv_updated_by; modeled_range; traces} let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = @@ -579,7 +447,7 @@ module Val = struct let subst : t -> eval_sym_trace -> Location.t -> t = - fun x {eval_sym; trace_of_sym; eval_locpath; eval_taint} location -> + fun x {eval_sym; trace_of_sym; eval_locpath} location -> let symbols = get_symbols x in let traces_caller = Itv.SymbolSet.fold @@ -591,7 +459,6 @@ module Val = struct let powloc_from_arrayblk, arrayblk = ArrayBlk.subst x.arrayblk eval_sym eval_locpath in { x with itv= Itv.subst x.itv eval_sym - ; taint= Taint.subst x.taint eval_taint ; powloc= PowLoc.join powloc powloc_from_arrayblk ; arrayblk ; traces } @@ -619,14 +486,14 @@ module Val = struct fun location ~f v -> { v with arrayblk= ArrayBlk.transform_length ~f v.arrayblk - ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces } + ; traces= Trace.(Set.add_elem location Through) v.traces } let set_array_offset : Location.t -> Itv.t -> t -> t = fun location offset v -> { v with arrayblk= ArrayBlk.set_offset offset v.arrayblk - ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces } + ; traces= Trace.(Set.add_elem location Through) v.traces } let set_array_stride : Z.t -> t -> t = @@ -646,16 +513,16 @@ module Val = struct let cast typ v = {v with powloc= PowLoc.cast typ v.powloc} - let of_path tenv ~may_last_field ~is_service_handler integer_type_widths location typ path = + let of_path tenv ~may_last_field integer_type_widths location typ path = let traces_of_loc l = let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in TraceSet.singleton location trace in - let itv_val ~non_int ~taint = + let itv_val ~non_int = let l = Loc.of_path path in let traces = traces_of_loc l in let unsigned = Typ.is_unsigned_int typ in - of_itv ~traces ~taint (Itv.of_normal_path ~unsigned ~non_int path) + of_itv ~traces (Itv.of_normal_path ~unsigned ~non_int path) in let ptr_to_c_array_alloc deref_path size = let allocsite = Allocsite.make_symbol deref_path in @@ -667,20 +534,14 @@ module Val = struct L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ (if may_last_field then ", may_last_field" else "") (if is_java then ", is_java" else "") ; - let taint = - if (not Config.bo_service_handler_request) || is_java then Taint.bottom - else if Lazy.force_val is_service_handler && SPath.is_request path then - Taint.tainted_of_path path - else Taint.param_of_path path - in match typ.Typ.desc with | Tint (IBool | IChar | ISChar | IUChar | IUShort) -> - let v = itv_val ~non_int:is_java ~taint in + let v = itv_val ~non_int:is_java in if is_java then set_itv_updated_by_unknown v else set_itv_updated_by_addition v | Tfloat _ | Tfun | TVar _ -> - itv_val ~non_int:true ~taint |> set_itv_updated_by_unknown + itv_val ~non_int:true |> set_itv_updated_by_unknown | Tint _ | Tvoid -> - itv_val ~non_int:false ~taint |> set_itv_updated_by_addition + itv_val ~non_int:false |> set_itv_updated_by_addition | Tptr (elt, _) -> if is_java || SPath.is_this path then let deref_kind = @@ -730,7 +591,7 @@ module Val = struct let length = Itv.of_length_path ~is_void:false path in of_java_array_alloc allocsite ~length ~traces | Some JavaInteger -> - itv_val ~non_int:false ~taint:Taint.bottom + itv_val ~non_int:false | None -> let l = Loc.of_path path in let traces = traces_of_loc l in @@ -759,14 +620,11 @@ module Val = struct let on_demand : default:t -> ?typ:Typ.t -> OndemandEnv.t -> Loc.t -> t = - fun ~default ?typ - {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths; class_name} l -> + fun ~default ?typ {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} + l -> let do_on_demand path typ = let may_last_field = may_last_field path in - let is_service_handler = - lazy (Option.exists class_name ~f:(FbPatternMatch.is_subtype_of_fb_service_handler tenv)) - in - of_path tenv ~may_last_field ~is_service_handler integer_type_widths entry_location typ path + of_path tenv ~may_last_field integer_type_widths entry_location typ path in match Loc.get_literal_string l with | Some s -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 0de65705d..7ec271387 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -33,32 +33,11 @@ module ModeledRange : sig val of_modeled_function : Procname.t -> Location.t -> Bounds.Bound.t -> t end -module type TaintS = sig - include AbstractDomain.WithBottom - - val compare : t -> t -> int - - val pp : Format.formatter -> t -> unit - - val is_tainted : t -> bool - - val param_of_path : Symb.SymbolPath.partial -> t - - val tainted_of_path : Symb.SymbolPath.partial -> t - - type eval_taint = Symb.SymbolPath.partial -> t - - val subst : t -> eval_taint -> t -end - -module Taint : TaintS - (** type for on-demand symbol evaluation in Inferbo *) type eval_sym_trace = { eval_sym: Bounds.Bound.eval_sym (** evaluating symbol *) ; trace_of_sym: Symb.Symbol.t -> BufferOverrunTrace.Set.t (** getting traces of symbol *) - ; eval_locpath: AbsLoc.PowLoc.eval_locpath (** evaluating path *) - ; eval_taint: Taint.eval_taint (** evaluating taint of path *) } + ; eval_locpath: AbsLoc.PowLoc.eval_locpath (** evaluating path *) } module Val : sig type t = @@ -66,7 +45,6 @@ module Val : sig ; itv_thresholds: ItvThresholds.t ; itv_updated_by: ItvUpdatedBy.t ; modeled_range: ModeledRange.t - ; taint: Taint.t ; powloc: AbsLoc.PowLoc.t (** Simple pointers *) ; arrayblk: ArrayBlk.t (** Array blocks *) ; traces: BufferOverrunTrace.Set.t } @@ -95,7 +73,7 @@ module Val : sig val of_int_lit : IntLit.t -> t - val of_itv : ?traces:BufferOverrunTrace.Set.t -> ?taint:Taint.t -> Itv.t -> t + val of_itv : ?traces:BufferOverrunTrace.Set.t -> Itv.t -> t val of_literal_string : Typ.IntegerWidths.t -> string -> t @@ -135,8 +113,6 @@ module Val : sig val get_pow_loc : t -> AbsLoc.PowLoc.t - val get_taint : t -> Taint.t - val get_traces : t -> BufferOverrunTrace.Set.t val set_array_length : Location.t -> length:t -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5d5772a64..bf4aacb0f 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -83,11 +83,9 @@ let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem c | Bottom -> cond_set | NonBottom length -> - let taint = Dom.Val.get_taint v_length in let traces = Dom.Val.get_traces v_length in let latest_prune = Dom.Mem.get_latest_prune mem in - PO.ConditionSet.add_alloc_size location ~can_be_zero ~length ~taint traces latest_prune - cond_set + PO.ConditionSet.add_alloc_size location ~can_be_zero ~length traces latest_prune cond_set let fgets str_exp num_exp = @@ -319,7 +317,7 @@ let strndup src_exp length_exp = in let traces = Trace.Set.join (Dom.Val.get_traces src_strlen) (Dom.Val.get_traces length) - |> Trace.Set.add_elem location (Trace.through ~risky_fun:(Some Trace.strndup)) + |> Trace.Set.add_elem location Trace.Through |> Trace.Set.add_elem location ArrayDeclaration in Dom.Val.of_c_array_alloc allocsite @@ -363,16 +361,6 @@ let by_value = fun value -> {exec= exec ~value; check= no_check} -let by_risky_value_from lib_fun = - let exec ~value {location} ~ret:(ret_id, _) mem = - let traces = - Trace.(Set.add_elem location (through ~risky_fun:(Some lib_fun))) (Dom.Val.get_traces value) - in - model_by_value {value with traces} ret_id mem - in - fun value -> {exec= exec ~value; check= no_check} - - let bottom = let exec _model_env ~ret:_ _mem = Dom.Mem.unreachable in {exec; check= no_check} @@ -428,10 +416,6 @@ let set_array_length {exp; typ} length_exp = {exec; check} -let snprintf = by_risky_value_from Trace.snprintf Dom.Val.Itv.nat - -let vsnprintf = by_risky_value_from Trace.vsnprintf Dom.Val.Itv.nat - let copy array_v ret_id mem = let dest_loc = Loc.of_id ret_id |> PowLoc.singleton in Dom.Mem.update_mem dest_loc array_v mem @@ -1426,13 +1410,13 @@ module Call = struct ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc - ; -"snprintf" <>--> snprintf + ; -"snprintf" <>--> by_value Dom.Val.Itv.nat ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy ; -"strlen" <>$ capt_exp $!--> strlen ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"strndup" <>$ capt_exp $+ capt_exp $+...$--> strndup - ; -"vsnprintf" <>--> vsnprintf + ; -"vsnprintf" <>--> by_value Dom.Val.Itv.nat ; (* ObjC models *) -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array ; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> create_copy_array diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 58513b84d..d63326344 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -71,54 +71,36 @@ module ConditionTrace = struct let has_unknown ct = ValTrace.Issue.has_unknown ct.val_traces - let has_risky ct = ValTrace.Issue.has_risky ct.val_traces - let exists_str ~f ct = ValTrace.Issue.exists_str ~f ct.val_traces - let check ~issue_type_u5 ~issue_type_r2 : _ t0 -> IssueType.t option = - fun ct -> - if has_risky ct then Some issue_type_r2 else if has_unknown ct then Some issue_type_u5 else None - + let check ~issue_type_u5 : _ t0 -> IssueType.t option = + fun ct -> if has_unknown ct then Some issue_type_u5 else None - let check_buffer_overrun ct = - let issue_type_u5 = IssueType.buffer_overrun_u5 in - let issue_type_r2 = IssueType.buffer_overrun_r2 in - check ~issue_type_u5 ~issue_type_r2 ct + let check_buffer_overrun ct = check ~issue_type_u5:IssueType.buffer_overrun_u5 ct - let check_integer_overflow ct = - let issue_type_u5 = IssueType.integer_overflow_u5 in - let issue_type_r2 = IssueType.integer_overflow_r2 in - check ~issue_type_u5 ~issue_type_r2 ct - + let check_integer_overflow ct = check ~issue_type_u5:IssueType.integer_overflow_u5 ct let for_summary : _ t0 -> summary_t = fun ct -> {ct with cond_trace= ()} end -type report_issue_type = - | NotIssue - | Issue of IssueType.t - | SymbolicIssue - | TaintedIssue of IssueType.t +type report_issue_type = NotIssue | Issue of IssueType.t | SymbolicIssue type checked_condition = {report_issue_type: report_issue_type; propagate: bool} module AllocSizeCondition = struct - type t = {length: ItvPure.t; can_be_zero: bool; taint: Dom.Taint.t} [@@deriving compare] + type t = {length: ItvPure.t; can_be_zero: bool} [@@deriving compare] let get_symbols {length} = ItvPure.get_symbols length - let pp fmt {length; taint} = - F.fprintf fmt "alloc(%a)" ItvPure.pp length ; - if Config.bo_debug >= 3 then F.fprintf fmt "(%a)" Dom.Taint.pp taint - + let pp fmt {length} = F.fprintf fmt "alloc(%a)" ItvPure.pp length let pp_description ~markup fmt {length} = F.fprintf fmt "Length: %a" (ItvPure.pp_mark ~markup) length - let make ~can_be_zero ~length ~taint = - if ItvPure.is_invalid length then None else Some {length; can_be_zero; taint} + let make ~can_be_zero ~length = + if ItvPure.is_invalid length then None else Some {length; can_be_zero} let have_similar_bounds x y = @@ -158,60 +140,50 @@ module AllocSizeCondition = struct let itv_big = ItvPure.of_int 1_000_000 - let check {length; can_be_zero; taint} = - if Config.bo_service_handler_request && Dom.Taint.is_tainted taint then - {report_issue_type= TaintedIssue IssueType.inferbo_alloc_may_be_tainted; propagate= false} - else - match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with - | `Equal | `RightSubsumesLeft -> - if can_be_zero then {report_issue_type= NotIssue; propagate= false} - else {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false} - | `LeftSmallerThanRight -> - {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false} - | _ -> ( - let is_symbolic = ItvPure.is_symbolic length in - match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with - | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> - {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false} - | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) -> - { report_issue_type= Issue IssueType.inferbo_alloc_may_be_negative - ; propagate= is_symbolic } - | cmp_mone -> ( - match ItvPure.xcompare ~lhs:length ~rhs:itv_big with - | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> - {report_issue_type= Issue IssueType.inferbo_alloc_is_big; propagate= false} - | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) -> - {report_issue_type= Issue IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic} - | cmp_big -> - let propagate = - match (cmp_mone, cmp_big) with - | (`NotComparable | `LeftSubsumesRight), _ - | _, (`NotComparable | `LeftSubsumesRight) -> - is_symbolic - | _ -> - false - in - if propagate then {report_issue_type= SymbolicIssue; propagate} - else {report_issue_type= NotIssue; propagate} ) ) - - - let subst eval_sym eval_taint {length; can_be_zero; taint} = + let check {length; can_be_zero} = + match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with + | `Equal | `RightSubsumesLeft -> + if can_be_zero then {report_issue_type= NotIssue; propagate= false} + else {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false} + | `LeftSmallerThanRight -> + {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false} + | _ -> ( + let is_symbolic = ItvPure.is_symbolic length in + match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with + | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> + {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false} + | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) -> + { report_issue_type= Issue IssueType.inferbo_alloc_may_be_negative + ; propagate= is_symbolic } + | cmp_mone -> ( + match ItvPure.xcompare ~lhs:length ~rhs:itv_big with + | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> + {report_issue_type= Issue IssueType.inferbo_alloc_is_big; propagate= false} + | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) -> + {report_issue_type= Issue IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic} + | cmp_big -> + let propagate = + match (cmp_mone, cmp_big) with + | (`NotComparable | `LeftSubsumesRight), _ | _, (`NotComparable | `LeftSubsumesRight) + -> + is_symbolic + | _ -> + false + in + if propagate then {report_issue_type= SymbolicIssue; propagate} + else {report_issue_type= NotIssue; propagate} ) ) + + + let subst eval_sym {length; can_be_zero} = match ItvPure.subst length eval_sym with | NonBottom length -> - let taint = Dom.Taint.subst taint eval_taint in - Some {length; can_be_zero; taint} + Some {length; can_be_zero} | Bottom -> None end module ArrayAccessCondition = struct - type t = - { offset: ItvPure.t - ; idx: ItvPure.t - ; size: ItvPure.t - ; last_included: bool - ; void_ptr: bool - ; taint: Dom.Taint.t } + type t = {offset: ItvPure.t; idx: ItvPure.t; size: ItvPure.t; last_included: bool; void_ptr: bool} [@@deriving compare] let get_symbols c = @@ -226,8 +198,7 @@ module ArrayAccessCondition = struct in let cmp = if c.last_included then "<=" else "<" in F.fprintf fmt "%t%a %s %a" pp_offset ItvPure.pp c.idx cmp ItvPure.pp - (ItvPure.make_positive c.size) ; - if Config.bo_debug >= 3 then F.fprintf fmt "(%a)" Dom.Taint.pp c.taint + (ItvPure.make_positive c.size) let pp_description : markup:bool -> F.formatter -> t -> unit = @@ -245,18 +216,12 @@ module ArrayAccessCondition = struct pp_offset (ItvPure.pp_mark ~markup) (ItvPure.make_positive c.size) - let make : - offset:ItvPure.t - -> idx:ItvPure.t - -> size:ItvPure.t - -> last_included:bool - -> taint:Dom.Taint.t - -> t option = - fun ~offset ~idx ~size ~last_included ~taint -> + let make : offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t -> last_included:bool -> t option = + fun ~offset ~idx ~size ~last_included -> if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None else let void_ptr = ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb size in - Some {offset; idx; size; last_included; void_ptr; taint} + Some {offset; idx; size; last_included; void_ptr} let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; last_included= lcol} @@ -374,9 +339,6 @@ module ArrayAccessCondition = struct (* il >= 0 and iu < sl, definitely not an error *) if Boolean.is_true not_overrun && Boolean.is_true not_underrun then {report_issue_type= NotIssue; propagate= false} (* iu < 0 or il >= su, definitely an error *) - else if Config.bo_service_handler_request && Dom.Taint.is_tainted c.taint then - {report_issue_type= Issue IssueType.buffer_overrun_t1; propagate= false} - (* tainted values are used in array accesses *) else if Boolean.is_false not_overrun || Boolean.is_false not_underrun then {report_issue_type= Issue IssueType.buffer_overrun_l1; propagate= false} (* su <= iu < +oo, most probably an error *) @@ -401,8 +363,8 @@ module ArrayAccessCondition = struct {report_issue_type; propagate= is_symbolic} - let subst : Bound.eval_sym -> Dom.Taint.eval_taint -> t -> t option = - fun eval_sym eval_taint c -> + let subst : Bound.eval_sym -> t -> t option = + fun eval_sym c -> match (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) with @@ -411,8 +373,7 @@ module ArrayAccessCondition = struct c.void_ptr || ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb idx || ItvPure.has_void_ptr_symb size in - let taint = Dom.Taint.subst c.taint eval_taint in - Some {c with offset; idx; size; void_ptr; taint} + Some {c with offset; idx; size; void_ptr} | _ -> None end @@ -625,11 +586,11 @@ module Condition = struct BinaryOperationCondition.get_symbols c - let subst eval_sym eval_taint = function + let subst eval_sym = function | AllocSize c -> - AllocSizeCondition.subst eval_sym eval_taint c |> make_alloc_size + AllocSizeCondition.subst eval_sym c |> make_alloc_size | ArrayAccess c -> - ArrayAccessCondition.subst eval_sym eval_taint c |> make_array_access + ArrayAccessCondition.subst eval_sym c |> make_array_access | BinaryOperation c -> BinaryOperationCondition.subst eval_sym c |> make_binary_operation @@ -755,8 +716,8 @@ module ConditionWithTrace = struct call_site with | `Reachable reachability -> ( - let {Dom.eval_sym; eval_taint; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in - match Condition.subst eval_sym eval_taint cwt.cond with + let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in + match Condition.subst eval_sym cwt.cond with | None -> None | Some cond -> @@ -795,7 +756,7 @@ module ConditionWithTrace = struct let check cwt = let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond cwt.trace in match report_issue_type with - | NotIssue | SymbolicIssue | TaintedIssue _ -> + | NotIssue | SymbolicIssue -> checked | Issue issue_type -> let issue_type = set_u5 cwt issue_type in @@ -816,7 +777,7 @@ module ConditionWithTrace = struct match checked.report_issue_type with | NotIssue | SymbolicIssue -> () - | TaintedIssue issue_type | Issue issue_type -> + | Issue issue_type -> report cwt.cond cwt.trace issue_type @@ -828,7 +789,7 @@ module ConditionWithTrace = struct match report_issue_type with | NotIssue -> assert false - | SymbolicIssue | TaintedIssue _ -> + | SymbolicIssue -> reported | Issue issue_type -> Some (Reported.make issue_type) @@ -911,17 +872,17 @@ module ConditionSet = struct join_one condset (check_one cwt) - let add_array_access location ~offset ~idx ~size ~last_included ~taint ~idx_traces ~arr_traces + let add_array_access location ~offset ~idx ~size ~last_included ~idx_traces ~arr_traces ~latest_prune condset = - ArrayAccessCondition.make ~offset ~idx ~size ~last_included ~taint + ArrayAccessCondition.make ~offset ~idx ~size ~last_included |> Condition.make_array_access |> add_opt location (ValTrace.Issue.(binary location ArrayAccess) idx_traces arr_traces) latest_prune condset - let add_alloc_size location ~can_be_zero ~length ~taint val_traces latest_prune condset = - AllocSizeCondition.make ~can_be_zero ~length ~taint + let add_alloc_size location ~can_be_zero ~length val_traces latest_prune condset = + AllocSizeCondition.make ~can_be_zero ~length |> Condition.make_alloc_size |> add_opt location (ValTrace.Issue.alloc location val_traces) latest_prune condset diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 0a46ca802..26dcdcbb2 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -38,7 +38,6 @@ module ConditionSet : sig -> idx:ItvPure.t -> size:ItvPure.t -> last_included:bool - -> taint:BufferOverrunDomain.Taint.t -> idx_traces:BufferOverrunTrace.Set.t -> arr_traces:BufferOverrunTrace.Set.t -> latest_prune:BufferOverrunDomain.LatestPrune.t @@ -49,7 +48,6 @@ module ConditionSet : sig Location.t -> can_be_zero:bool -> length:ItvPure.t - -> taint:BufferOverrunDomain.Taint.t -> BufferOverrunTrace.Set.t -> BufferOverrunDomain.LatestPrune.t -> checked_t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index d028d281e..bc48a315b 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -483,12 +483,7 @@ let mk_eval_sym_trace ?(is_params_ref = false) integer_type_widths if Itv.eq itv Itv.bot then TraceSet.bottom else traces in let eval_locpath ~mode partial = eval_locpath ~mode params partial caller_mem in - let eval_taint ~mode path = eval_sympath_partial ~mode params path caller_mem |> Val.get_taint in - fun ~mode -> - { eval_sym= eval_sym ~mode - ; trace_of_sym - ; eval_locpath= eval_locpath ~mode - ; eval_taint= eval_taint ~mode } + fun ~mode -> {eval_sym= eval_sym ~mode; trace_of_sym; eval_locpath= eval_locpath ~mode} let mk_eval_sym_mode ~mode integer_type_widths callee_formals actual_exps caller_mem = diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index deed2ca70..78156a5c2 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -10,8 +10,6 @@ open AbsLoc module F = Format module BoTrace = struct - type lib_fun = Snprintf | Strndup | Vsnprintf [@@deriving compare] - type final = UnknownFrom of Procname.t option [@@deriving compare] type elem = @@ -21,7 +19,7 @@ module BoTrace = struct | JavaIntDecleration | Parameter of Loc.t | SetArraySize - | Through of {risky_fun: lib_fun option} + | Through [@@deriving compare] type t = @@ -31,12 +29,6 @@ module BoTrace = struct | Call of {location: Location.t; length: int; caller: t; callee: t} [@@deriving compare] - let snprintf = Snprintf - - let strndup = Strndup - - let vsnprintf = Vsnprintf - let length = function Empty -> 0 | Final _ -> 1 | Elem {length} | Call {length} -> length let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2) @@ -47,8 +39,6 @@ module BoTrace = struct let singleton location kind = add_elem location kind Empty - let through ~risky_fun = Through {risky_fun} - let call location ~caller ~callee = Call {location; length= 1 + length caller + length callee; caller; callee} @@ -62,15 +52,6 @@ module BoTrace = struct let pp_location = Location.pp_file_pos - let pp_lib_fun f = function - | Snprintf -> - F.fprintf f "snprintf" - | Strndup -> - F.fprintf f "strndup" - | Vsnprintf -> - F.fprintf f "vsnprintf" - - let pp_final f = function | UnknownFrom pname_opt -> F.fprintf f "UnknownFrom `%a`" pp_pname_opt pname_opt @@ -89,9 +70,8 @@ module BoTrace = struct F.fprintf f "Parameter `%a`" Loc.pp loc | SetArraySize -> F.pp_print_string f "SetArraySize" - | Through {risky_fun} -> - F.pp_print_string f "Through" ; - if Option.is_some risky_fun then F.pp_print_string f " RiskyLibCall" + | Through -> + F.pp_print_string f "Through" let rec pp f = function @@ -120,22 +100,6 @@ module BoTrace = struct let has_unknown = final_exists ~f:(function UnknownFrom _ -> true) - let elem_has_risky = function - | JavaIntDecleration | ArrayDeclaration | Assign _ | Global _ | Parameter _ | SetArraySize -> - false - | Through {risky_fun} -> - Option.is_some risky_fun - - - let rec has_risky = function - | Empty | Final _ -> - false - | Elem {kind; from} -> - elem_has_risky kind || has_risky from - | Call {caller; callee} -> - has_risky caller || has_risky callee - - let exists_str ~f = let rec helper = function | Empty | Final _ -> @@ -173,12 +137,8 @@ module BoTrace = struct if Loc.is_pretty loc then F.asprintf "Parameter `%a`" Loc.pp loc else "" | SetArraySize -> "Set array size" - | Through {risky_fun} -> ( - match risky_fun with - | None -> - "Through" - | Some f -> - F.asprintf "Risky value from: %a" pp_lib_fun f ) + | Through -> + "Through" let rec make_err_trace depth t tail = @@ -232,8 +192,6 @@ module Set = struct let has_unknown t = exists BoTrace.has_unknown t - let has_risky t = exists BoTrace.has_risky t - let exists_str ~f t = exists (BoTrace.exists_str ~f) t let make_err_trace depth set tail = @@ -283,8 +241,6 @@ module Issue = struct let has_unknown = has_common ~f:Set.has_unknown - let has_risky = has_common ~f:Set.has_risky - let exists_str ~f = has_common ~f:(Set.exists_str ~f) let binary_labels = function ArrayAccess -> ("Offset", "Length") | Binop -> ("LHS", "RHS") diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.mli b/infer/src/bufferoverrun/bufferOverrunTrace.mli index a9fa06007..23c8253d9 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.mli +++ b/infer/src/bufferoverrun/bufferOverrunTrace.mli @@ -7,15 +7,6 @@ open! IStd -(** Library function names that may be risky *) -type lib_fun = Snprintf | Strndup | Vsnprintf - -val snprintf : lib_fun - -val strndup : lib_fun - -val vsnprintf : lib_fun - (** Final unknown function in trace *) type final = UnknownFrom of Procname.t option @@ -27,9 +18,7 @@ type elem = | JavaIntDecleration | Parameter of AbsLoc.Loc.t | SetArraySize - | Through of {risky_fun: lib_fun option} - -val through : risky_fun:lib_fun option -> elem + | Through module Set : sig include AbstractDomain.WithBottom @@ -60,9 +49,6 @@ module Issue : sig val call : Location.t -> Set.t -> t -> t (** Merge caller's trace set and callee's issue, i.e., [call location caller callee] *) - val has_risky : t -> bool - (** Check if the issue trace includes risky function calls by [Through] *) - val has_unknown : t -> bool (** Check if the issue trace includes unknown function calls *) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 11ec65d6b..d8a96eef6 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -239,11 +239,11 @@ module Exec = struct end module Check = struct - let check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~taint ~latest_prune - location cond_set = + let check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location + cond_set = match (size, idx) with | NonBottom length, NonBottom idx -> - PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~last_included ~taint + PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~last_included ~idx_traces ~arr_traces ~latest_prune cond_set | _ -> cond_set @@ -264,10 +264,7 @@ module Check = struct offset - let get_taint arr idx = Dom.Taint.join (Dom.Val.get_taint arr) (Dom.Val.get_taint idx) - let array_access ~arr ~idx ~is_plus ~last_included ~latest_prune location cond_set = - let taint = get_taint arr idx in let idx_traces = Dom.Val.get_traces idx in let idx = let idx_itv = Dom.Val.get_itv idx in @@ -278,8 +275,8 @@ module Check = struct let size = ArrayBlk.ArrInfo.get_size arr_info in let offset = offsetof arr_info in log_array_access allocsite size offset idx ; - check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~taint ~latest_prune - location acc + check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location + acc in ArrayBlk.fold array_access1 (Dom.Val.get_array_blk arr) cond_set @@ -297,7 +294,6 @@ module Check = struct let array_access_byte ~arr ~idx ~is_plus ~last_included ~latest_prune location cond_set = - let taint = get_taint arr idx in let idx_traces = Dom.Val.get_traces idx in let idx = let idx_itv = Dom.Val.get_itv idx in @@ -308,8 +304,8 @@ module Check = struct let size = ArrayBlk.ArrInfo.byte_size arr_info in let offset = offsetof arr_info in log_array_access allocsite size offset idx ; - check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~taint ~latest_prune - location acc + check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location + acc in ArrayBlk.fold array_access_byte1 (Dom.Val.get_array_blk arr) cond_set diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index dc1b23326..e82d4edfe 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -91,11 +91,6 @@ module SymbolPath = struct None - let is_request x = - Option.exists (get_pvar x) ~f:(fun pvar -> - String.equal (Pvar.get_simplified_name pvar) "request" ) - - let rec pp_partial_paren ~paren fmt = function | BoField.Prim (Pvar pvar) -> if Config.bo_debug >= 3 then Pvar.pp_value fmt pvar else Pvar.pp_value_non_verbose fmt pvar @@ -395,9 +390,3 @@ module SymbolMap = struct | exception Exit -> false end - -module SymbolPathSet = PrettyPrintable.MakePPSet (struct - type t = SymbolPath.partial [@@deriving compare] - - let pp = SymbolPath.pp_partial -end) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index ea0908fd3..826e2f6c5 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -63,8 +63,6 @@ module SymbolPath : sig val is_this : partial -> bool - val is_request : partial -> bool - val get_pvar : partial -> Pvar.t option val represents_multiple_values : partial -> bool @@ -134,5 +132,3 @@ module SymbolMap : sig val for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool end - -module SymbolPathSet : PrettyPrintable.PPSet with type elt = SymbolPath.partial diff --git a/infer/src/opensource/FbPatternMatch.ml b/infer/src/opensource/FbPatternMatch.ml deleted file mode 100644 index fa707a079..000000000 --- a/infer/src/opensource/FbPatternMatch.ml +++ /dev/null @@ -1,8 +0,0 @@ -(* - * 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. - *) - -let is_subtype_of_fb_service_handler _tenv _name = false diff --git a/infer/src/opensource/FbPatternMatch.mli b/infer/src/opensource/FbPatternMatch.mli deleted file mode 100644 index 60d99bece..000000000 --- a/infer/src/opensource/FbPatternMatch.mli +++ /dev/null @@ -1,8 +0,0 @@ -(* - * 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. - *) - -val is_subtype_of_fb_service_handler : 'tenv_t -> 'typ_Name_t -> bool diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b5df0c09b..3749518c2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -220,10 +220,10 @@ codetoanalyze/c/bufferoverrun/models.c, strncpy_contents_Bad, 5, BUFFER_OVERRUN_ codetoanalyze/c/bufferoverrun/models.c, strncpy_good5_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 10 Size: 5] codetoanalyze/c/bufferoverrun/models.c, strncpy_no_null_2_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 5 Size: 5] codetoanalyze/c/bufferoverrun/models.c, strncpy_no_null_4_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 14 Size: 10] -codetoanalyze/c/bufferoverrun/models.c, strndup_1_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, 99] Size: 13] -codetoanalyze/c/bufferoverrun/models.c, strndup_2_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, 11] Size: 6] +codetoanalyze/c/bufferoverrun/models.c, strndup_1_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Through,Array declaration,Assignment,Array access: Offset: [0, 99] Size: 13] +codetoanalyze/c/bufferoverrun/models.c, strndup_2_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Through,Array declaration,Assignment,Array access: Offset: [0, 11] Size: 6] codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 7, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Assignment,,Assignment,Risky value from: strndup,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: 6] +codetoanalyze/c/bufferoverrun/models.c, strndup_3_Bad, 7, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Assignment,,Assignment,Through,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: 6] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop3_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 3f8d5c01a..e8e2a0443 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -103,15 +103,15 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Good, 2, CONDITION_ALWAYS_ 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: [-1, +oo] Size: 1024] -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: [-1, +oo] Size: 1024] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [-1, +oo] Size: 1024] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [-1, +oo] Size: 1024] codetoanalyze/cpp/bufferoverrun/std_string.cpp, length2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 11 Size: 10] codetoanalyze/cpp/bufferoverrun/std_string.cpp, length3_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 11 Size: 10] codetoanalyze/cpp/bufferoverrun/std_string.cpp, length_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 11 Size: 10] codetoanalyze/cpp/bufferoverrun/std_string.cpp, size_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 11 Size: 10] -codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Risky value from: snprintf,Assignment,,Array declaration,Array access: Offset added: [0, +oo] Size: 1024] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset added: [0, +oo] Size: 1024] codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Risky value from: vsnprintf,Assignment,,Array declaration,Array access: Offset added: [0, +oo] Size: 1024] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset added: [0, +oo] Size: 1024] codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc::symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/this.cpp, CThis::access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this->n`,,Parameter `this->n`,Array declaration,Array access: Offset: this->n + 1 Size: this->n + 1] diff --git a/infer/tests/codetoanalyze/cpp/fb-taint/Makefile b/infer/tests/codetoanalyze/cpp/fb-taint/Makefile deleted file mode 100644 index 8ac72b08c..000000000 --- a/infer/tests/codetoanalyze/cpp/fb-taint/Makefile +++ /dev/null @@ -1,20 +0,0 @@ -# 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 = --bufferoverrun-only --bo-service-handler-request --ml-buckets cpp --no-filtering \ - --debug-exceptions --project-root $(TESTS_DIR) --report-force-relative-path -INFERPRINT_OPTIONS = --issues-tests - -SOURCES = $(wildcard *.cpp) - -HEADERS = - -include $(TESTS_DIR)/clang.make - -infer-out/report.json: $(MAKEFILE_LIST)