From 0f8444e235c63e8924105e9fb931ec6f69ed2ea5 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 2 Jan 2019 00:23:19 -0800 Subject: [PATCH] [inferbo] Substitute conditions of proof obligations strictly Summary: This diff substitutes the conditions of proof obligations strictly, so that the condition of "p!=Null" becomes bottom when callee's p is Null. In the non-strict substitution (which is used by default), if p's location is not found it returns the unknown location. On the other hand, in the strict substitution (which is used only in the substitution of condition of proof obligation), it returns bottom location. Depends on D13415366, D13414636 Reviewed By: mbouaziz, jvillard Differential Revision: D13415377 fbshipit-source-id: 5ae1e888e --- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- .../bufferOverrunProofObligations.ml | 7 ++-- .../bufferOverrunProofObligations.mli | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 39 +++++++++++-------- .../conditional_proof_obligation.cpp | 4 +- .../cpp/bufferoverrun/issues.exp | 2 - 6 files changed, 31 insertions(+), 25 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a007b4a68..5b5c52f82 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -144,7 +144,7 @@ module TransferFunctions = struct Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem in let eval_sym_trace = - Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem + Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem ~strict:false in let caller_mem = instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 1dbd93dc9..80411165a 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -711,16 +711,17 @@ module ConditionWithTrace = struct cmp - let subst ({Dom.eval_sym; trace_of_sym} as eval_sym_trace) rel_map caller_relation callee_pname - call_site cwt = + let subst eval_sym_trace rel_map caller_relation callee_pname call_site cwt = let symbols = Condition.get_symbols cwt.cond in if Symb.SymbolSet.is_empty symbols then L.(die InternalError) "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 call_site) + Option.find_map + (Dom.LatestPrune.subst cwt.latest_prune (eval_sym_trace ~strict:true) call_site) ~f:(fun latest_prune -> + 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 -> None diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index a24bc0b1c..6b8a7b7b0 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -74,7 +74,7 @@ module ConditionSet : sig val subst : summary_t - -> BufferOverrunDomain.eval_sym_trace + -> (strict:bool -> BufferOverrunDomain.eval_sym_trace) -> Relation.SubstMap.t -> Relation.t -> Typ.Procname.t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 3e0504033..850c51b5f 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -339,7 +339,7 @@ module ParamBindings = struct add_binding formals actuals empty end -let rec eval_sympath_partial params p mem = +let rec eval_sympath_partial ~strict params p mem = match p with | Symb.SymbolPath.Pvar x -> ( try ParamBindings.find x params with Caml.Not_found -> @@ -350,42 +350,47 @@ let rec eval_sympath_partial params p mem = (CallSite.pname cs) ; Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ -> - let locs = eval_locpath params p mem in + let locs = eval_locpath ~strict params p mem in Mem.find_set locs mem -and eval_locpath params p mem = +and eval_locpath ~strict params p mem = let res = match p with | Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ -> - let v = eval_sympath_partial params p mem in + let v = eval_sympath_partial ~strict params p mem in Val.get_all_locs v | Symb.SymbolPath.Deref (_, p) -> - let v = eval_sympath_partial params p mem in + let v = eval_sympath_partial ~strict params p mem in Val.get_all_locs v | Symb.SymbolPath.Field (fn, p) -> - let locs = eval_locpath params p mem in + let locs = eval_locpath ~strict params p mem in PowLoc.append_field ~fn locs in - if PowLoc.is_empty res then ( + if PowLoc.is_empty res && not strict then ( L.d_printfln_escaped "Location value for %a is not found." Symb.SymbolPath.pp_partial p ; PowLoc.unknown ) else res -let eval_sympath params sympath mem = +let eval_sympath ~strict params sympath mem = match sympath with | Symb.SymbolPath.Normal p -> - let v = eval_sympath_partial params p mem in + let v = eval_sympath_partial ~strict params p mem in (Val.get_itv v, Val.get_traces v) | Symb.SymbolPath.Offset p -> - let v = eval_sympath_partial params p mem in + let v = eval_sympath_partial ~strict params p mem in (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v) | Symb.SymbolPath.Length p -> - let v = eval_sympath_partial params p mem in + let v = eval_sympath_partial ~strict params p mem in (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v) +(* We have two modes (strict and non-strict) on evaluating location paths. When a location to + substitute is not found: + - non-strict mode (which is used by default): it returns the unknown location. + - strict mode (which is used only in the substitution of condition of proof obligation): it + returns the bottom location. *) let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem = let params = let formals = Procdesc.get_pvar_formals callee_pdesc in @@ -394,21 +399,23 @@ let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem = in let eval_sym s bound_end = let sympath = Symb.Symbol.path s in - let itv, _ = eval_sympath params sympath caller_mem in + let itv, _ = eval_sympath ~strict:false params sympath caller_mem in Symb.Symbol.assert_bound_end s bound_end ; Itv.get_bound itv bound_end in let trace_of_sym s = let sympath = Symb.Symbol.path s in - let itv, traces = eval_sympath params sympath caller_mem in + let itv, traces = eval_sympath ~strict:false params sympath caller_mem in if Itv.eq itv Itv.bot then TraceSet.empty else traces in - let eval_locpath partial = eval_locpath params partial caller_mem in - {eval_sym; trace_of_sym; eval_locpath} + let eval_locpath ~strict partial = eval_locpath ~strict params partial caller_mem in + fun ~strict -> {eval_sym; trace_of_sym; eval_locpath= eval_locpath ~strict} let mk_eval_sym integer_type_widths callee_pdesc actual_exps caller_mem = - let eval_sym_trace = mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem in + let eval_sym_trace = + mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem ~strict:false + in eval_sym_trace.eval_sym diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index 0b58a20d8..354dd5a2c 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -51,7 +51,7 @@ void conditional_minus(int* ptr, unsigned int size) { } } -void call_conditional_minus_1_Good_FP() { conditional_minus(NULL, 0); } +void call_conditional_minus_1_Good() { conditional_minus(NULL, 0); } void call_conditional_minus_2_Good() { int a[3]; @@ -69,7 +69,7 @@ unsigned int conditional_minus2(int* ptr, unsigned int size) { } } -void call_conditional_minus2_1_Good_FP() { conditional_minus2(NULL, 0); } +void call_conditional_minus2_1_Good() { conditional_minus2(NULL, 0); } void call_conditional_minus2_2_Good() { int a[3]; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 9f9652b6c..fa3453e0b 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -30,9 +30,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L 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_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_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` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]