From 14445fad0550f37d2ccc69b658de39b2554974d6 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Fri, 9 Feb 2018 03:06:02 -0800 Subject: [PATCH] [bi-abduction] Do not abduce reference parameters constraints for recursive calls Summary: Added a check for recursive calls not to add abduced reference parameters constraints. Abduced reference parameters constraints were causing assertion failure when renaming variables in specs, in particular, when transforming variables into callee variables. A similar check is already in place for abduced retvals constraints. Reviewed By: jeremydubreil Differential Revision: D6856919 fbshipit-source-id: acfe840 --- infer/src/backend/symExec.ml | 17 +++--- .../tests/codetoanalyze/cpp/errors/issues.exp | 1 + .../cpp/errors/npe/recursive_call.cpp | 52 +++++++++++++++++++ 3 files changed, 62 insertions(+), 8 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/errors/npe/recursive_call.cpp 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