diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 5930e2efb..5f3d4e3bd 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -635,6 +635,8 @@ module Val = struct let unknown_locs = of_pow_loc PowLoc.unknown ~traces:TraceSet.bottom + let is_bot x = Itv.is_bottom x.itv && PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk + let is_mone x = Itv.is_mone (get_itv x) let is_incr_of l {itv} = @@ -1564,10 +1566,7 @@ module CoreVal = struct if Itv.is_bottom itv then ArrayBlk.is_symbolic (Val.get_array_blk v) else Itv.is_symbolic itv - let is_empty v = - Itv.is_bottom (Val.get_itv v) - && PowLoc.is_empty (Val.get_pow_loc v) - && ArrayBlk.is_empty (Val.get_array_blk v) + let is_bot = Val.is_bot end module PruningExp = struct @@ -1686,7 +1685,7 @@ module PrunedVal = struct let is_symbolic {v; pruning_exp} = CoreVal.is_symbolic v || PruningExp.is_symbolic pruning_exp - let is_empty {v; pruning_exp} = CoreVal.is_empty v || PruningExp.is_empty pruning_exp + let is_bot {v; pruning_exp} = CoreVal.is_bot v || PruningExp.is_empty pruning_exp end (* [PrunePairs] is a map from abstract locations to abstract values that represents pruned results @@ -1713,7 +1712,7 @@ module PrunePairs = struct fold subst1 x (Ok empty) - let is_reachable x = not (exists (fun _ v -> PrunedVal.is_empty v) x) + let is_reachable x = not (exists (fun _ v -> PrunedVal.is_bot v) x) end module LatestPrune = struct @@ -1923,7 +1922,7 @@ module Reachability = struct let exception Unreachable in let subst1 x acc = let v = PrunedVal.subst x eval_sym_trace location in - if PrunedVal.is_empty v then raise Unreachable else add v acc + if PrunedVal.is_bot v then raise Unreachable else add v acc in match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable end diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index c225eda5a..3f07c2a90 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -108,6 +108,9 @@ module Val : sig val unknown_from : Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t (** Unknown return value of [callee_pname] *) + val is_bot : t -> bool + (** Check if the value is bottom *) + val is_mone : t -> bool (** Check if the value is [\[-1,-1\]] *) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 6d0274e19..b1d27c8cf 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -655,9 +655,11 @@ module Prune = struct let v' = eval integer_type_widths e mem in if IntLit.iszero i then v' else Val.minus_a v' (Val.of_int_lit i) in - let v = val_prune_eq lhs rhs in - let pruning_exp = make_pruning_exp ~lhs ~rhs in - update_mem_in_prune lv v ~pruning_exp acc ) + if Val.is_bot rhs then acc + else + let v = val_prune_eq lhs rhs in + let pruning_exp = make_pruning_exp ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp acc ) in gen_prune_alias_functions ~prune_alias_core diff --git a/infer/tests/codetoanalyze/objc/performance/control.m b/infer/tests/codetoanalyze/objc/performance/control.m index e729cf17c..208e48b26 100644 --- a/infer/tests/codetoanalyze/objc/performance/control.m +++ b/infer/tests/codetoanalyze/objc/performance/control.m @@ -15,7 +15,7 @@ enum { }; // expected linear -bool wrong_cvar_FN(int x) { +bool wrong_cvar_FP(int x) { while (true) { switch (x) { diff --git a/infer/tests/codetoanalyze/objc/performance/issues.exp b/infer/tests/codetoanalyze/objc/performance/issues.exp index 51a1b4daa..c668c6c0a 100644 --- a/infer/tests/codetoanalyze/objc/performance/issues.exp +++ b/infer/tests/codetoanalyze/objc/performance/issues.exp @@ -2,7 +2,5 @@ codetoanalyze/objc/performance/cf.m, array_count_linear, 2, EXPENSIVE_EXECUTION_ codetoanalyze/objc/performance/cf.m, cf_array_create_copy_linear, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1009, O(1), degree = 0] codetoanalyze/objc/performance/cf.m, cf_array_create_linear, 13, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 3 ⋅ x + 2 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 41, column 3,{x},Loop at line 41, column 3] codetoanalyze/objc/performance/cf.m, dict_count_linear, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ dict.length + 2 ⋅ (dict.length + 1), O(dict.length), degree = 1,{dict.length + 1},Loop at line 24, column 3,{dict.length},Loop at line 24, column 3] -codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] -codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/objc/performance/control.m, wrong_cvar_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 20, column 3] +codetoanalyze/objc/performance/control.m, wrong_cvar_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]