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]