From caf61461ac40d3c772e238dd6c7803fa904c2772 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sat, 2 Feb 2019 23:29:08 -0800 Subject: [PATCH] [inferbo] Update reachability conditions at function call Summary: This diff updates the reachability conditions of proof obligations at every function calls. Depends on D13781124 Reviewed By: mbouaziz Differential Revision: D13781147 fbshipit-source-id: 3c8768bd9 --- infer/src/bufferoverrun/bufferOverrunChecker.ml | 2 ++ infer/src/bufferoverrun/bufferOverrunDomain.ml | 11 +++++++++-- .../bufferoverrun/bufferOverrunProofObligations.ml | 8 +++++++- .../bufferoverrun/bufferOverrunProofObligations.mli | 1 + .../bufferoverrun/conditional_proof_obligation.cpp | 2 +- .../tests/codetoanalyze/cpp/bufferoverrun/issues.exp | 1 - 6 files changed, 20 insertions(+), 5 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index f605f1ed8..418360823 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -260,7 +260,9 @@ let instantiate_cond : let eval_sym_trace = Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem in + let latest_prune = Dom.Mem.get_latest_prune caller_mem in PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel callee_pname location + latest_prune let check_instr : diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 344432e3c..f88491bc4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -741,7 +741,10 @@ module CoreVal = struct let pp fmt x = F.fprintf fmt "(%a, %a)" Itv.pp (Val.get_itv x) ArrayBlk.pp (Val.get_array_blk x) - let is_symbolic v = Itv.is_symbolic (Val.get_itv v) || ArrayBlk.is_symbolic (Val.get_array_blk v) + let is_symbolic v = + let itv = Val.get_itv v in + 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) && ArrayBlk.is_empty (Val.get_array_blk v) end @@ -999,7 +1002,7 @@ module Reachability = struct reachability. *) let add v x = if PrunedVal.is_symbolic v then M.add v x else x - let make latest_prune = + let of_latest_prune latest_prune = let of_prune_pairs p = PrunePairs.fold (fun _ v acc -> add v acc) p M.empty in match latest_prune with | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) -> @@ -1010,6 +1013,10 @@ module Reachability = struct M.empty + let make latest_prune = of_latest_prune latest_prune + + let add_latest_prune latest_prune x = M.union x (of_latest_prune latest_prune) + let subst x eval_sym_trace location = let exception Unreachable in let subst1 x acc = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index d6e72cb88..9c5965f8e 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -762,6 +762,10 @@ module ConditionWithTrace = struct None + let update_reachability latest_prune ({reachability} as cwt) = + {cwt with reachability= Dom.Reachability.add_latest_prune latest_prune reachability} + + let set_u5 {cond; trace} issue_type = if ( IssueType.equal issue_type IssueType.buffer_overrun_l3 @@ -918,7 +922,8 @@ module ConditionSet = struct latest_prune condset - let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site = + let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site + latest_prune = let subst_add_cwt condset cwt = match ConditionWithTrace.subst eval_sym_trace rel_subst_map caller_relation callee_pname @@ -927,6 +932,7 @@ module ConditionSet = struct | None -> condset | Some cwt -> + let cwt = ConditionWithTrace.update_reachability latest_prune cwt in join_one condset (check_one cwt) in List.fold condset ~f:subst_add_cwt ~init:[] diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 347a01b2a..97c022d27 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -77,6 +77,7 @@ module ConditionSet : sig -> Relation.t -> Typ.Procname.t -> Location.t + -> BufferOverrunDomain.LatestPrune.t -> checked_t val report_errors : diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index 7054f19e9..66efcbc51 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -191,7 +191,7 @@ void conditional_inequality_depth1(int i) { } } -void call_conditional_inequality_depth1_1_Good_FP() { +void call_conditional_inequality_depth1_1_Good() { conditional_inequality_depth1(5); } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 05286e15c..b55f25ef7 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -36,7 +36,6 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, 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,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality` ] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,,Parameter `i`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_depth1` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_3_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,,Parameter `i`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_depth1` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join1` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_join1` ]