diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 52f8a77d9..30ceaa8cb 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -899,14 +899,15 @@ let add_struct_value_to_footprint tenv abduced_pv typ prop = (prop', struct_strexp) +let is_rec_call callee_pname caller_pdesc = + (* TODO: (t7147096) extend this to detect mutual recursion *) + Typ.Procname.equal callee_pname (Procdesc.get_proc_name caller_pdesc) + + let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ callee_pname callee_loc = if Typ.Procname.is_infer_undefined callee_pname then prop else - let is_rec_call pname = - (* TODO: (t7147096) extend this to detect mutual recursion *) - Typ.Procname.equal pname (Procdesc.get_proc_name pdesc) - in let lookup_abduced_expression p abduced_ret_pv = List.find_map ~f:(fun hpred -> @@ -933,7 +934,7 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ cal match typ.Typ.desc with Typ.Tptr _ -> Prop.conjoin_neq tenv exp Exp.zero prop | _ -> prop else prop in - if not (is_rec_call callee_pname) then + if not (is_rec_call callee_pname pdesc) then (* introduce a fresh program variable to allow abduction on the return value *) let prop_with_abduced_var = let abduced_ret_pv = @@ -1421,7 +1422,7 @@ and instrs ?(mask_errors= false) tenv pdesc instrs ppl = List.fold ~f ~init:ppl instrs -and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname callee_loc = +and add_constraints_on_actuals_by_ref tenv caller_pdesc prop actuals_by_ref callee_pname callee_loc = let add_actual_by_ref_to_footprint prop (actual, actual_typ, actual_index) = let abduced = match actual with @@ -1441,7 +1442,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call p.Prop.sigma_fp in (* prevent introducing multiple abduced retvals for a single call site in a loop *) - if already_has_abduced_retval prop then prop + if already_has_abduced_retval prop || is_rec_call callee_pname caller_pdesc then prop else if !Config.footprint then let prop', abduced_strexp = match actual_typ.Typ.desc with @@ -1570,7 +1571,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots | _ -> pre_1 in - add_constraints_on_actuals_by_ref tenv pre_2 actuals_by_ref callee_pname loc + add_constraints_on_actuals_by_ref tenv pdesc pre_2 actuals_by_ref callee_pname loc in if is_scan (* if scan function, don't mark anything with undef attributes *) then [(Tabulation.remove_constant_string_class tenv pre_final, path)] diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index ec474563d..cb16fb112 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -66,6 +66,7 @@ codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe, 2 codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe_person, 2, NULL_DEREFERENCE, [start of procedure npe_added_to_b1::causes_npe_person(),start of procedure Person,return from a call to npe_added_to_b1::Person_Person,start of procedure npe_added_to_b1::deref_person()] codetoanalyze/cpp/errors/npe/null_returned_by_method.cpp, testNullDeref, 3, NULL_DEREFERENCE, [start of procedure testNullDeref(),Condition is true,start of procedure getNull,return from a call to XFactory_getNull] codetoanalyze/cpp/errors/npe/object_deref.cpp, object_deref::derefNullField, 2, NULL_DEREFERENCE, [start of procedure object_deref::derefNullField(),start of procedure object_deref::getNull(),return from a call to object_deref::getNull] +codetoanalyze/cpp/errors/npe/recursive_call.cpp, recursive_call::test_rec2_ok_FP, 2, PRECONDITION_NOT_MET, [start of procedure recursive_call::test_rec2_ok_FP(),start of procedure F,return from a call to recursive_call::F_F,start of procedure F,return from a call to recursive_call::F_F] codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, FP_const_skip2_then_split_case_ok, 5, MEMORY_LEAK, [start of procedure FP_const_skip2_then_split_case_ok(),Skipping skip_const2(): function or method not found,start of procedure test_pointer(),Condition is true,return from a call to test_pointer] codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, FP_const_skip_then_split_case_ok, 6, MEMORY_LEAK, [start of procedure FP_const_skip_then_split_case_ok(),Skipping skip_const(): function or method not found,start of procedure test_pointer(),Condition is true,return from a call to test_pointer] codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp, FP_typedef_skip_then_split_case_ok, 2, MEMORY_LEAK, [start of procedure FP_typedef_skip_then_split_case_ok(),Skipping skip_typedef(): function or method not found] diff --git a/infer/tests/codetoanalyze/cpp/errors/npe/recursive_call.cpp b/infer/tests/codetoanalyze/cpp/errors/npe/recursive_call.cpp new file mode 100644 index 000000000..6d99c3a72 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/npe/recursive_call.cpp @@ -0,0 +1,52 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +namespace recursive_call { + +struct A { + A() { f = 0; } + int f; + A* getptr(); + A* mk(); +}; + +struct F { + A* mk(); +}; + +int rec(A* a = nullptr) { + if (a == nullptr) { + A* a = new A(); + int r = rec(a); + delete a; + return r; + } + + return a->f; +}; + +int test_rec_ok() { + return rec(); // infer should not report here +} + +A* rec2(F f, A* a = nullptr) { + if (a == nullptr) { + auto tmp = f.mk(); + return rec2( + f, tmp); // assertion failure because of abducedRefParam0 in `getptr` + } + return a->getptr(); +} + +int test_rec2_ok_FP() { + F f; + return rec2(f)->f; // PRECONDITION_NOT_MET +} + +} // namespace recursive_call