diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index acf7d8f54..7c7c4e0ea 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -127,6 +127,17 @@ module ArrInfo = struct F.pp_print_string f SpecialChars.down_tack + let is_symbolic : t -> bool = + fun arr -> + match arr with + | C {offset; size; stride} -> + Itv.is_symbolic offset || Itv.is_symbolic size || Itv.is_symbolic stride + | Java {length} -> + Itv.is_symbolic length + | Top -> + false + + let get_symbols : t -> Itv.SymbolSet.t = fun arr -> match arr with @@ -235,6 +246,8 @@ end include AbstractDomain.Map (Allocsite) (ArrInfo) +let compare = compare ArrInfo.compare + let bot : t = empty let unknown : t = add Allocsite.unknown ArrInfo.top bot @@ -296,6 +309,8 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t = fold subst1 a empty +let is_symbolic : t -> bool = fun a -> exists (fun _ ai -> ArrInfo.is_symbolic ai) a + let get_symbols : t -> Itv.SymbolSet.t = fun a -> fold (fun _ ai acc -> Itv.SymbolSet.union acc (ArrInfo.get_symbols ai)) a Itv.SymbolSet.empty diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 702c784ac..548d4d0c6 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -706,21 +706,6 @@ end module PrunePairs = struct include AbstractDomain.InvertedMap (Loc) (Val) - (* [subst] returns [None] if a pruned value is bottom, i.g., unreachable. *) - let subst x eval_sym_trace location = - let exception Unreachable in - let is_empty_val v = - Itv.is_empty (Val.get_itv v) - && PowLoc.is_empty (Val.get_pow_loc v) - && ArrayBlk.is_empty (Val.get_array_blk v) - in - let subst1 x = - let v = Val.subst x eval_sym_trace location in - if is_empty_val v then raise Unreachable else v - in - match map subst1 x with x -> Some x | exception Unreachable -> None - - let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x end @@ -820,22 +805,6 @@ module LatestPrune = struct let top = Top - let subst x eval_sym_trace location = - match x with - | Latest p -> - Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> Latest p) - | TrueBranch (x, p) -> - Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> TrueBranch (x, p)) - | FalseBranch (x, p) -> - Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> FalseBranch (x, p)) - | V (x, ptrue, pfalse) -> - Option.map2 (PrunePairs.subst ptrue eval_sym_trace location) - (PrunePairs.subst pfalse eval_sym_trace location) ~f:(fun ptrue pfalse -> - V (x, ptrue, pfalse) ) - | Top -> - Some x - - let forget locs = let is_mem_locs x = PowLoc.mem (Loc.of_pvar x) locs in function @@ -852,6 +821,52 @@ module LatestPrune = struct Top end +module Reachability = struct + module PrunedVal = struct + type t = Val.t + + let compare x y = + let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in + if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y) + + + let pp = Val.pp + + let is_symbolic : t -> bool = fun x -> Itv.is_symbolic x.itv || ArrayBlk.is_symbolic x.arrayblk + + let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v) + end + + module M = PrettyPrintable.MakePPSet (PrunedVal) + + type t = M.t + + let equal = M.equal + + (* It keeps only symbolic pruned values, because non-symbolic ones are useless to see the + reachability. *) + let add v x = if PrunedVal.is_symbolic v then M.add v x else x + + let make = + let of_prune_pairs p = PrunePairs.fold (fun _ v acc -> add v acc) p M.empty in + function + | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) -> + of_prune_pairs p + | LatestPrune.V (_, ptrue, pfalse) -> + M.inter (of_prune_pairs ptrue) (of_prune_pairs pfalse) + | LatestPrune.Top -> + M.empty + + + let subst x eval_sym_trace location = + let exception Unreachable in + let subst1 x acc = + let v = Val.subst x eval_sym_trace location in + if PrunedVal.is_empty v then raise Unreachable else add v acc + in + match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable +end + module MemReach = struct type t = { stack_locs: StackLocs.t diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 4af9cd88a..60e1f0882 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -702,9 +702,11 @@ module ConditionWithTrace = struct { cond: Condition.t ; trace: 'cond_trace ConditionTrace.t0 ; reported: Reported.t option - ; latest_prune: Dom.LatestPrune.t } + ; reachability: Dom.Reachability.t } + + let make cond trace latest_prune = + {cond; trace; reported= None; reachability= Dom.Reachability.make latest_prune} - let make cond trace latest_prune = {cond; trace; reported= None; latest_prune} let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace @@ -717,12 +719,14 @@ module ConditionWithTrace = struct let have_similar_bounds {cond= cond1} {cond= cond2} = Condition.have_similar_bounds cond1 cond2 let xcompare ~lhs ~rhs = - match Condition.xcompare ~lhs:lhs.cond ~rhs:rhs.cond with - | `Equal -> - if ConditionTrace.compare lhs.trace rhs.trace <= 0 then `LeftSubsumesRight - else `RightSubsumesLeft - | (`LeftSubsumesRight | `RightSubsumesLeft | `NotComparable) as cmp -> - cmp + if Dom.Reachability.equal lhs.reachability rhs.reachability then + match Condition.xcompare ~lhs:lhs.cond ~rhs:rhs.cond with + | `Equal -> + if ConditionTrace.compare lhs.trace rhs.trace <= 0 then `LeftSubsumesRight + else `RightSubsumesLeft + | (`LeftSubsumesRight | `RightSubsumesLeft | `NotComparable) as cmp -> + cmp + else `NotComparable let subst eval_sym_trace rel_map caller_relation callee_pname call_site cwt = @@ -732,9 +736,8 @@ module ConditionWithTrace = struct "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \ the first place?" pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ; - Option.find_map - (Dom.LatestPrune.subst cwt.latest_prune (eval_sym_trace ~strict:true) call_site) - ~f:(fun latest_prune -> + match Dom.Reachability.subst cwt.reachability (eval_sym_trace ~strict:true) call_site with + | `Reachable reachability -> ( let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~strict:false in match Condition.subst eval_sym rel_map caller_relation cwt.cond with | None -> @@ -748,7 +751,9 @@ module ConditionWithTrace = struct let trace = ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace in - Some {cond; trace; reported= cwt.reported; latest_prune} ) + Some {cond; trace; reported= cwt.reported; reachability} ) + | `Unreachable -> + None let set_u5 {cond; trace} issue_type = diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 4248354e8..98a868b0c 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -612,6 +612,8 @@ let subst : t -> Bound.eval_sym -> t = fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x +let is_symbolic = bind1bool ItvPure.is_symbolic + let get_symbols : t -> SymbolSet.t = function | Bottom -> SymbolSet.empty diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 6ce51a1b9..c15e50c8e 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -156,6 +156,8 @@ val neg : t -> t val normalize : t -> t +val is_symbolic : t -> bool + val get_symbols : t -> SymbolSet.t val eq : t -> t -> bool diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index 9519e9cc5..1230b8307 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -289,7 +289,7 @@ void call_two_safety_conditions_l1_and_l2_Bad() { two_safety_conditions(10); } /* issue1 and issue2 are deduplicated since the offset of issue2 ([10,+oo]) subsumes that of issue1 ([10,10]). */ -void deduplicate_issues_Bad() { +void deduplicate_issues_1_Bad() { int a[10]; int x = 10; a[x] = 0; // issue1: [10,10] < [10,10] @@ -298,3 +298,15 @@ void deduplicate_issues_Bad() { a[x] = 0; // issue2: [10,+oo] < [10,10] } } + +/* issue1 and issue2 are not deduplicated since they have different + conditions to reach. */ +void deduplicate_issues_2_Bad(int y) { + int a[10]; + int x = 10; + a[x] = 0; // issue1: [10,10] < [10,10] + x = unknown_function(); + if (x >= 10 && y >= 0) { + a[x] = 0; // issue2: [10,+oo] < [10,10] + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 4ce2b01ac..4c57ed0af 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -131,7 +131,9 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Ba codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Parameter `n`,,Call,Assignment,Assignment,Binary operation: (100000000 + [0, +oo]):signed32 by call to `alloc_may_be_big2_Silenced` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `two_safety_conditions` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ] -codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,,Array declaration,Array access: Offset: [10, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_1_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,,Array declaration,Array access: Offset: [10, +oo] Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_2_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,,Array declaration,Array access: Offset: [10, +oo] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `*n`,Assignment,,Parameter `*n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,,Parameter `*n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10]