From 1f68f1e8727a8c9dcbe00f20c383e79103fd9b89 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@meta.com>
Date: Thu, 14 Nov 2024 06:27:14 -0800
Subject: [PATCH] [pulse] suppress mutual recursion errors when actuals are the
 wrong length

Summary:
Another workaround for the issue with Hack traits and optional values
that is more generally applicable: do not report likely-FPs when the
number of arguments don't match in the recursive call anyway as it's
likely that we have the wrong procedure.

Reviewed By: dulmarod

Differential Revision:
D65665048

Privacy Context Container: L1208441

fbshipit-source-id: 45a0e16f0542d97d8231f10fb8de333c0eedcaa2
---
 infer/src/pulse/PulseCallOperations.ml | 43 +++++++++++++++++++++-----
 1 file changed, 35 insertions(+), 8 deletions(-)

diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml
index 38af931689..df3b152d06 100644
--- a/infer/src/pulse/PulseCallOperations.ml
+++ b/infer/src/pulse/PulseCallOperations.ml
@@ -80,6 +80,28 @@ module GlobalForStats = struct
   let one_call_is_stuck () = global := {!global with one_call_is_stuck= true}
 end
 
+let print_arity_mismatch_message ?(extra_call_prefix = "") callee_pname_opt ~formals ~actuals =
+  let formals_n = List.length formals in
+  let actuals_n = List.length actuals in
+  let pp_args pp_val fmt args =
+    Pp.seq ~sep:"," (Pp.pair ~fst:pp_val ~snd:(Typ.pp_full Pp.text)) fmt args
+  in
+  let message =
+    F.asprintf
+      "Arities mismatch in%s call to %a, something bogus is going on.@\n\
+      \  %d formals: %a@\n\
+      \  %d actuals: %a@\n"
+      extra_call_prefix (Pp.option Procname.pp_verbose) callee_pname_opt formals_n
+      (pp_args (Pvar.pp Pp.text))
+      formals actuals_n
+      (pp_args (fun fmt (v, _hist) -> AbstractValue.pp fmt v))
+      actuals
+  in
+  L.debug Analysis Medium "%s" message ;
+  L.d_printfln "%s" message ;
+  ()
+
+
 let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallEvent.t)
     ?(force_pure = false) callee_pname_opt ~ret ~actuals ~formals_opt astate0 =
   let hist =
@@ -238,8 +260,7 @@ let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallE
             havoc_actual_if_ptr actual_typ (Some formal) astate )
       with
       | Unequal_lengths ->
-          L.d_printfln "ERROR: formals have length %d but actuals have length %d"
-            (List.length formals) (List.length actuals) ;
+          print_arity_mismatch_message callee_pname_opt ~formals ~actuals ;
           havoc_actuals_without_typ_info astate
       | Ok result ->
           result ) )
@@ -640,11 +661,16 @@ let maybe_dynamic_type_specialization_is_needed already_specialized contradictio
 
 
 let on_recursive_call ({InterproceduralAnalysis.proc_desc} as analysis_data) call_loc callee_pname
-    astate =
+    ~actuals ~formals_opt astate =
   if Procname.equal callee_pname (Procdesc.get_proc_name proc_desc) then (
-    PulseReport.report analysis_data ~is_suppressed:false ~latent:false
-      (MutualRecursionCycle
-         {cycle= PulseMutualRecursion.mk call_loc callee_pname; location= call_loc} ) ;
+    ( match formals_opt with
+    | Some formals when List.length formals <> List.length actuals ->
+        print_arity_mismatch_message ~extra_call_prefix:" recursive" (Some callee_pname) ~formals
+          ~actuals
+    | _ ->
+        PulseReport.report analysis_data ~is_suppressed:false ~latent:false
+          (MutualRecursionCycle
+             {cycle= PulseMutualRecursion.mk call_loc callee_pname; location= call_loc} ) ) ;
     astate )
   else AbductiveDomain.add_recursive_call call_loc callee_pname astate
 
@@ -841,7 +867,8 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
                        match exec_state with
                        | ContinueProgram astate ->
                            ContinueProgram
-                             (on_recursive_call analysis_data call_loc callee_pname astate)
+                             (on_recursive_call analysis_data call_loc callee_pname ~actuals
+                                ~formals_opt astate )
                        | exec_state ->
                            exec_state ) )
                 in
@@ -894,7 +921,7 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
       let astate =
         match no_summary with
         | MutualRecursionCycle ->
-            on_recursive_call analysis_data call_loc callee_pname astate
+            on_recursive_call analysis_data call_loc callee_pname ~actuals ~formals_opt astate
         | AnalysisFailed | InBlockList | UnknownProcedure ->
             astate
       in