diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 86ee10f14..afd48dd0d 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -226,7 +226,7 @@ module TransferFunctions = struct mem else mem in - let mem = Dom.Mem.update_latest_prune exp1 exp2 mem in + let mem = Dom.Mem.update_latest_prune ~updated_locs:locs exp1 exp2 mem in mem | Prune (exp, _, _, _) -> Sem.Prune.prune integer_type_widths exp mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 8c0d46de3..774955a1d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -663,6 +663,9 @@ module PrunePairs = struct 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 module LatestPrune = struct @@ -775,6 +778,22 @@ module LatestPrune = struct V (x, ptrue, pfalse) ) | Top -> Some x + + + let forget locs = + let is_mem_locs x = PowLoc.mem (Loc.of_pvar x) locs in + function + | Latest p -> + Latest (PrunePairs.forget locs p) + | TrueBranch (x, p) -> + if is_mem_locs x then Top else TrueBranch (x, PrunePairs.forget locs p) + | FalseBranch (x, p) -> + if is_mem_locs x then Top else FalseBranch (x, PrunePairs.forget locs p) + | V (x, ptrue, pfalse) -> + if is_mem_locs x then Top + else V (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse) + | Top -> + Top end module MemReach = struct @@ -988,15 +1007,15 @@ module MemReach = struct m - let update_latest_prune : Exp.t -> Exp.t -> t -> t = - fun e1 e2 m -> + let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = + fun ~updated_locs e1 e2 m -> match (e1, e2, m.latest_prune) with | Lvar x, Const (Const.Cint i), LatestPrune.Latest p -> if IntLit.isone i then {m with latest_prune= LatestPrune.TrueBranch (x, p)} else if IntLit.iszero i then {m with latest_prune= LatestPrune.FalseBranch (x, p)} - else {m with latest_prune= LatestPrune.Top} + else {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune} | _, _, _ -> - {m with latest_prune= LatestPrune.Top} + {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune} let get_latest_prune : t -> LatestPrune.t = fun {latest_prune} -> latest_prune @@ -1161,8 +1180,8 @@ module Mem = struct let apply_latest_prune : Exp.t -> t -> t = fun e -> map ~f:(MemReach.apply_latest_prune e) - let update_latest_prune : Exp.t -> Exp.t -> t -> t = - fun e1 e2 -> map ~f:(MemReach.update_latest_prune e1 e2) + let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = + fun ~updated_locs e1 e2 -> map ~f:(MemReach.update_latest_prune ~updated_locs e1 e2) let get_latest_prune : t -> LatestPrune.t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 173653a78..1299ab114 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -197,8 +197,10 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVER codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_alias.c, call_forget_locs_latest_prune_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 10 Size: 5 by call to `forget_locs_latest_prune` ] codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `n`,,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ] +codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `length`,,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index ea33697ac..2aee13274 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -264,3 +264,19 @@ void call_latest_prune_join_3_Bad() { int a[2]; latest_prune_join(a, 3); } + +void forget_locs_latest_prune(unsigned int n) { + int x; + int* a[5]; + if (n < 5) { + x = 1; + } else { + x = 0; + x = 2; + } + if (x) { + a[n] = 0; + } +} + +void call_forget_locs_latest_prune_Bad() { forget_locs_latest_prune(10); } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index 2c4674f11..0b58a20d8 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -26,7 +26,7 @@ void conditional_buffer_access(int* ptr, unsigned int size) { } } -void call_conditional_buffer_access_Good_FP() { +void call_conditional_buffer_access_Good() { int a[1]; conditional_buffer_access(a, 1); } @@ -41,13 +41,9 @@ void conditional_buffer_access2(unsigned int n) { conditional_buffer_access(a, n); } -void call_conditional_buffer_access2_1_Good_FP() { - conditional_buffer_access2(1); -} +void call_conditional_buffer_access2_1_Good() { conditional_buffer_access2(1); } -void call_conditional_buffer_access2_2_Good_FP() { - conditional_buffer_access2(3); -} +void call_conditional_buffer_access2_2_Good() { conditional_buffer_access2(3); } void conditional_minus(int* ptr, unsigned int size) { int i = 0; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index b4244aea8..06c5485dc 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -28,11 +28,8 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFE codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 32 Size: 30] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access2` ] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_2_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 3 by call to `conditional_buffer_access2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `size`,,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]