[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

@@ -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)]

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]

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