From e5381a90d5d003c4a06d72732ef8bc4ff205eea8 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 1 Apr 2019 00:00:36 -0700 Subject: [PATCH] [inferbo] Propagate LatestPrune on function calls Summary: This diff propagates LatestPrune on function calls. Depends on D14321605 Reviewed By: mbouaziz Differential Revision: D14321618 fbshipit-source-id: cb2e1b547 --- .../bufferoverrun/bufferOverrunAnalysis.ml | 14 ++++ .../src/bufferoverrun/bufferOverrunDomain.ml | 81 ++++++++++++++++++- .../c/bufferoverrun/issue_kinds.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 4 +- .../c/bufferoverrun/prune_constant.c | 2 +- 5 files changed, 96 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index c8bf45e83..dd56931fa 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -59,6 +59,19 @@ module TransferFunctions = struct type nonrec extras = extras + let instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location mem = + match + Dom.Mem.get_latest_prune callee_exit_mem + |> Dom.LatestPrune.subst ~ret_id eval_sym_trace location + with + | Ok latest_prune' -> + Dom.Mem.set_latest_prune latest_prune' mem + | Error `SubstBottom -> + Dom.Mem.bottom + | Error `SubstFail -> + mem + + let instantiate_mem_reachable (ret_id, _) callee_formals callee_pname ~callee_exit_mem ({Dom.eval_locpath} as eval_sym_trace) mem location = let formal_locs = @@ -104,6 +117,7 @@ module TransferFunctions = struct Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem |> instantiate_ret_alias |> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val)) + |> instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location let forget_ret_relation ret callee_pname mem = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 59d0959b9..dba0543b0 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -980,6 +980,22 @@ module PrunePairs = struct let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x + let subst x ({eval_locpath} as eval_sym_trace) location = + let open Result.Monad_infix in + let subst1 l pruned_val acc = + acc + >>= fun acc -> + match PowLoc.is_singleton_or_more (PowLoc.subst_loc l eval_locpath) with + | Singleton loc -> + Ok (add loc (PrunedVal.subst pruned_val eval_sym_trace location) acc) + | Empty -> + Error `SubstBottom + | More -> + Error `SubstFail + in + fold subst1 x (Ok empty) + + let is_reachable x = not (exists (fun _ v -> PrunedVal.is_empty v) x) end @@ -999,12 +1015,16 @@ module LatestPrune = struct respectively. There is no other memory updates after the latest prunings. + VRet (x, ptrue, pfalse): Similar to V, but this is for return + values of functions. + Top: No information about the latest pruning. *) type t = | Latest of PrunePairs.t | TrueBranch of Pvar.t * PrunePairs.t | FalseBranch of Pvar.t * PrunePairs.t | V of Pvar.t * PrunePairs.t * PrunePairs.t + | VRet of Ident.t * PrunePairs.t * PrunePairs.t | Top let pvar_pp = Pvar.pp Pp.text @@ -1020,6 +1040,8 @@ module LatestPrune = struct F.fprintf fmt "LatestPrune: false(%a) %a" pvar_pp v PrunePairs.pp p | V (v, p1, p2) -> F.fprintf fmt "LatestPrune: v(%a) %a / %a" pvar_pp v PrunePairs.pp p1 PrunePairs.pp p2 + | VRet (v, p1, p2) -> + F.fprintf fmt "LatestPrune: ret(%a) %a / %a" Ident.pp v PrunePairs.pp p1 PrunePairs.pp p2 let ( <= ) ~lhs ~rhs = @@ -1041,6 +1063,10 @@ module LatestPrune = struct Pvar.equal x1 x2 && PrunePairs.( <= ) ~lhs:ptrue1 ~rhs:ptrue2 && PrunePairs.( <= ) ~lhs:pfalse1 ~rhs:pfalse2 + | VRet (x1, ptrue1, pfalse1), VRet (x2, ptrue2, pfalse2) -> + Ident.equal x1 x2 + && PrunePairs.( <= ) ~lhs:ptrue1 ~rhs:ptrue2 + && PrunePairs.( <= ) ~lhs:pfalse1 ~rhs:pfalse2 | _, _ -> false @@ -1071,6 +1097,8 @@ module LatestPrune = struct V (x1, ptrue, PrunePairs.join pfalse1 pfalse2) | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) when Pvar.equal x1 x2 -> V (x1, PrunePairs.join ptrue1 ptrue2, PrunePairs.join pfalse1 pfalse2) + | VRet (x1, ptrue1, pfalse1), VRet (x2, ptrue2, pfalse2) when Ident.equal x1 x2 -> + VRet (x1, PrunePairs.join ptrue1 ptrue2, PrunePairs.join pfalse1 pfalse2) | _, _ -> Top @@ -1091,6 +1119,8 @@ module LatestPrune = struct | V (x, ptrue, pfalse) -> if is_mem_locs x then Top else V (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse) + | VRet (x, ptrue, pfalse) -> + VRet (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse) | Top -> Top @@ -1105,6 +1135,41 @@ module LatestPrune = struct V (to_, ptrue, pfalse) | _ -> x + + + let subst ~ret_id ({eval_locpath} as eval_sym_trace) location = + let open Result.Monad_infix in + let subst_pvar x = + match PowLoc.is_singleton_or_more (PowLoc.subst_loc (Loc.of_pvar x) eval_locpath) with + | Empty -> + Error `SubstBottom + | Singleton (Loc.Var (Var.ProgramVar x')) -> + Ok x' + | Singleton _ | More -> + Error `SubstFail + in + function + | Latest p -> + PrunePairs.subst p eval_sym_trace location >>| fun p' -> Latest p' + | TrueBranch (x, p) -> + subst_pvar x + >>= fun x' -> PrunePairs.subst p eval_sym_trace location >>| fun p' -> TrueBranch (x', p') + | FalseBranch (x, p) -> + subst_pvar x + >>= fun x' -> PrunePairs.subst p eval_sym_trace location >>| fun p' -> FalseBranch (x', p') + | V (x, ptrue, pfalse) when Pvar.is_return x -> + PrunePairs.subst ptrue eval_sym_trace location + >>= fun ptrue' -> + PrunePairs.subst pfalse eval_sym_trace location + >>| fun pfalse' -> VRet (ret_id, ptrue', pfalse') + | V (x, ptrue, pfalse) -> + subst_pvar x + >>= fun x' -> + PrunePairs.subst ptrue eval_sym_trace location + >>= fun ptrue' -> + PrunePairs.subst pfalse eval_sym_trace location >>| fun pfalse' -> V (x', ptrue', pfalse') + | VRet _ | Top -> + Ok Top end module Reachability = struct @@ -1125,7 +1190,7 @@ module Reachability = struct match latest_prune with | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) -> of_prune_pairs p - | LatestPrune.V (_, ptrue, pfalse) -> + | LatestPrune.V (_, ptrue, pfalse) | LatestPrune.VRet (_, ptrue, pfalse) -> M.inter (of_prune_pairs ptrue) (of_prune_pairs pfalse) | LatestPrune.Top -> M.empty @@ -1366,6 +1431,10 @@ module MemReach = struct (PrunePairs.fold apply1 prunes m, prunes) | _ -> (m, PrunePairs.empty) ) + | LatestPrune.VRet (x, prunes, _), Exp.Var r + | LatestPrune.VRet (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> + if Ident.equal x r then (PrunePairs.fold apply1 prunes m, prunes) + else (m, PrunePairs.empty) | _ -> (m, PrunePairs.empty) @@ -1387,7 +1456,9 @@ module MemReach = struct {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune} - let get_latest_prune : t -> LatestPrune.t = fun {latest_prune} -> latest_prune + let get_latest_prune : _ t0 -> LatestPrune.t = fun {latest_prune} -> latest_prune + + let set_latest_prune : LatestPrune.t -> t -> t = fun latest_prune x -> {x with latest_prune} let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> _ t0 -> PowLoc.t = let add_reachable1 ~root loc v acc = @@ -1589,10 +1660,14 @@ module Mem = struct fun ~updated_locs e1 e2 -> map ~f:(MemReach.update_latest_prune ~updated_locs e1 e2) - let get_latest_prune : t -> LatestPrune.t = + let get_latest_prune : _ t0 -> LatestPrune.t = fun m -> f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune m + let set_latest_prune : LatestPrune.t -> t -> t = + fun latest_prune m -> map ~f:(MemReach.set_latest_prune latest_prune) m + + let get_relation : t -> Relation.t = fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index 1230b8307..c9b249028 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -59,7 +59,7 @@ void l1_symbolic_widened_Bad(int n) { } } -void l1_symbolic_widened_Good_FP(int n) { +void l1_symbolic_widened_Good(int n) { int a[n]; for (int i = n; less_than(i, n); i++) { a[i] = 0; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 2e5a57d4b..7834427fa 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -161,7 +161,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun2_Bad, 2, BUFFER codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `i`,,Array declaration,Array access: Offset: [max(10, i), i] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `i`,,Array declaration,Array access: Offset: [i, min(-1, i)] Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `n`,Assignment,,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `n`,Assignment,,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 10] Size: 10] @@ -270,7 +270,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 6, BUFFER_OVERRU codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good_FP, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,,Parameter `a`,Assignment,,Parameter `a`,Assignment,Array declaration,Array access: Offset: [-1, 9] Size: [0, 10] by call to `null_pruning_symbols` ] codetoanalyze/c/bufferoverrun/prune_constant.c, call_null_pruning_symbols_3_Good_FP, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Call,,Parameter `a`,Assignment,Binary operation: ([0, 10] - 1):unsigned32 by call to `null_pruning_symbols` ] codetoanalyze/c/bufferoverrun/prune_constant.c, call_prune_add2_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 Size: 10 by call to `prune_add2` ] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index 057b4a662..447ba3ec4 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -167,7 +167,7 @@ void null_pruning2_Bad(int* p) { int greater_than(unsigned int x, unsigned int y) { return (x > y); } -void call_greater_than_Good_FP() { +void call_greater_than_Good() { unsigned int idx = 0; if (greater_than(idx, 0)) { idx = idx - 1;