[rec] new issue type INFINITE_RECURSION when the values in the call a…

…re the same as the current formals

Summary:
This is a likely infinite recursion, let's report it with more
confidence.

Reviewed By: geralt-encore

Differential Revision: D66876112

fbshipit-source-id: 75b9838323bf14ed9a303be24c3cf9dc3e69f71d

infer/man/man1/infer-full.txt

@@ -653,6 +653,7 @@ OPTIONS
              INFERBO_ALLOC_MAY_BE_BIG (enabled by default),
              INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default),
              INFINITE_EXECUTION_TIME (disabled by default),
+             INFINITE_RECURSION (disabled by default),
              INHERENTLY_DANGEROUS_FUNCTION (enabled by default),
              INTEGER_OVERFLOW_L1 (enabled by default),
              INTEGER_OVERFLOW_L2 (enabled by default),

infer/man/man1/infer-report.txt

@@ -168,6 +168,7 @@ OPTIONS
              INFERBO_ALLOC_MAY_BE_BIG (enabled by default),
              INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default),
              INFINITE_EXECUTION_TIME (disabled by default),
+             INFINITE_RECURSION (disabled by default),
              INHERENTLY_DANGEROUS_FUNCTION (enabled by default),
              INTEGER_OVERFLOW_L1 (enabled by default),
              INTEGER_OVERFLOW_L2 (enabled by default),

infer/man/man1/infer.txt

@@ -653,6 +653,7 @@ OPTIONS
              INFERBO_ALLOC_MAY_BE_BIG (enabled by default),
              INFERBO_ALLOC_MAY_BE_NEGATIVE (enabled by default),
              INFINITE_EXECUTION_TIME (disabled by default),
+             INFINITE_RECURSION (disabled by default),
              INHERENTLY_DANGEROUS_FUNCTION (enabled by default),
              INTEGER_OVERFLOW_L1 (enabled by default),
              INTEGER_OVERFLOW_L2 (enabled by default),

infer/src/base/IssueType.ml

@@ -655,6 +655,14 @@ let inferbo_alloc_may_be_negative =
 
 let infinite_cost_call ~kind = register_cost ~enabled:false "INFINITE_%s" ~kind
 
+let infinite_recursion =
+  register ~enabled:false ~category:RuntimeException ~id:"INFINITE_RECURSION" Warning Pulse
+    ~user_documentation:
+      "A special case of [MUTUAL_RECURSION_CYCLE](#mutual_recursion_cycle) where we detected that \
+       the recursive call is made with the exact same values, which guarantees an infinite \
+       recursion."
+
+
 let inherently_dangerous_function =
   register_hidden ~id:"INHERENTLY_DANGEROUS_FUNCTION" Warning Biabduction
 

infer/src/base/IssueType.mli

@@ -215,6 +215,8 @@ val inferbo_alloc_may_be_negative : t
 
 val infinite_cost_call : kind:CostKind.t -> t
 
+val infinite_recursion : t
+
 val inherently_dangerous_function : t
 
 val integer_overflow_l1 : t

infer/src/pulse/PulseAbductiveDomain.ml

@@ -672,6 +672,14 @@ module Internal = struct
   module SafeMemory = struct
     module Access = BaseMemory.Access
 
+    let select pre_or_post astate =
+      match pre_or_post with
+      | `Pre ->
+          (astate.pre :> base_domain).heap
+      | `Post ->
+          (astate.post :> base_domain).heap
+
+
     (** [astate] with [astate.post.heap = f astate.post.heap] *)
     let map_post_heap ~f astate =
       let new_post = PostDomain.update astate.post ~heap:(f (astate.post :> base_domain).heap) in
@@ -686,15 +694,15 @@ module Internal = struct
                 (WrittenTo (timestamp, Trace.Immediate {location; history})) )
 
 
-    let find_edge_opt address access astate =
+    let find_edge_opt pre_or_post address access astate =
       let get_var_repr v = Formula.get_var_repr astate.path_condition v in
-      BaseMemory.find_edge_opt ~get_var_repr address access (astate.post :> base_domain).heap
+      BaseMemory.find_edge_opt ~get_var_repr address access (select pre_or_post astate)
       |> CanonValue.canon_opt_fst astate
 
 
     let eval_edge (addr_src, hist_src) access astate =
       let astate, addr_hist_dst =
-        match find_edge_opt addr_src access astate with
+        match find_edge_opt `Post addr_src access astate with
         | Some addr_hist_dst ->
             (astate, addr_hist_dst)
         | None ->
@@ -751,13 +759,7 @@ module Internal = struct
 
 
     let fold_edges pre_or_post address astate ~init ~f =
-      let heap =
-        match pre_or_post with
-        | `Pre ->
-            (astate.pre :> base_domain).heap
-        | `Post ->
-            (astate.post :> base_domain).heap
-      in
+      let heap = select pre_or_post astate in
       SafeBaseMemory.fold_edges astate address heap ~init ~f
 
 
@@ -1666,6 +1668,20 @@ let mk_initial tenv (proc_attrs : ProcAttributes.t) =
   update_pre_for_kotlin_proc astate proc_attrs formals
 
 
+let are_same_values_as_pre_formals proc_desc values astate =
+  List.for_all2 (Procdesc.get_formals proc_desc) values ~f:(fun (mangled_name, _, _) v ->
+      let formal = Pvar.mk mangled_name (Procdesc.get_proc_name proc_desc) in
+      let formal_addr =
+        SafeStack.find_opt `Pre (Var.of_pvar formal) astate |> Option.value_exn |> ValueOrigin.value
+      in
+      let formal_v =
+        SafeMemory.find_edge_opt `Pre formal_addr Dereference astate
+        |> Option.value_exn |> fst |> downcast
+      in
+      AbstractValue.equal formal_v v )
+  |> function List.Or_unequal_lengths.Ok b -> b | List.Or_unequal_lengths.Unequal_lengths -> false
+
+
 let leq ~lhs ~rhs =
   phys_equal lhs rhs
   || SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
@@ -2280,7 +2296,9 @@ let is_allocated_this_pointer proc_attrs astate address =
      let* this_pointer_address =
        SafeStack.find_opt `Post (Var.of_pvar this) astate >>| ValueOrigin.value
      in
-     let+ this_pointer, _ = SafeMemory.find_edge_opt this_pointer_address Dereference astate in
+     let+ this_pointer, _ =
+       SafeMemory.find_edge_opt `Post this_pointer_address Dereference astate
+     in
      CanonValue.equal this_pointer address )
 
 
@@ -2411,7 +2429,7 @@ module Memory = struct
 
 
   let find_edge_opt address access astate =
-    SafeMemory.find_edge_opt
+    SafeMemory.find_edge_opt `Post
       (CanonValue.canon' astate address)
       (CanonValue.canon_access astate access)
       astate

infer/src/pulse/PulseAbductiveDomain.mli

@@ -79,6 +79,8 @@ val pp : Format.formatter -> t -> unit
 
 val mk_initial : Tenv.t -> ProcAttributes.t -> t
 
+val are_same_values_as_pre_formals : Procdesc.t -> AbstractValue.t list -> t -> bool
+
 val mk_join_state :
      pre:PulseBaseStack.t * PulseBaseMemory.t * PulseBaseAddressAttributes.t
   -> post:PulseBaseStack.t * PulseBaseMemory.t * PulseBaseAddressAttributes.t

infer/src/pulse/PulseCallOperations.ml

@@ -685,10 +685,14 @@ let on_recursive_call ({InterproceduralAnalysis.proc_desc} as analysis_data) cal
              suppressing report"
             Procname.pp callee_pname
         else
+          let is_call_with_same_values =
+            AbductiveDomain.are_same_values_as_pre_formals proc_desc actuals_values astate
+          in
           PulseReport.report analysis_data ~is_suppressed:false ~latent:false
             (MutualRecursionCycle
                { cycle= PulseMutualRecursion.mk call_loc callee_pname actuals_values
-               ; location= call_loc } ) ) ;
+               ; location= call_loc
+               ; is_call_with_same_values } ) ) ;
     astate )
   else if
     AbductiveDomain.has_reachable_in_inner_pre_heap

infer/src/pulse/PulseDiagnostic.ml

@@ -198,7 +198,8 @@ type t =
   | DynamicTypeMismatch of {location: Location.t}
   | ErlangError of ErlangError.t
   | HackCannotInstantiateAbstractClass of {type_name: Typ.Name.t; trace: Trace.t}
-  | MutualRecursionCycle of {cycle: PulseMutualRecursion.t; location: Location.t}
+  | MutualRecursionCycle of
+      {cycle: PulseMutualRecursion.t; location: Location.t; is_call_with_same_values: bool}
   | ReadonlySharedPtrParameter of
       {param: Var.t; typ: Typ.t; location: Location.t; used_locations: Location.t list}
   | ReadUninitialized of ReadUninitialized.t
@@ -254,9 +255,10 @@ let pp fmt diagnostic =
   | HackCannotInstantiateAbstractClass {type_name; trace} ->
       F.fprintf fmt "HackCannotInstantiateAbstractClass {@[type_name:%a;@;trace:%a@]" Typ.Name.pp
         type_name (Trace.pp ~pp_immediate) trace
-  | MutualRecursionCycle {cycle; location} ->
-      F.fprintf fmt "MutualRecursionCycle {@[cycle=%a;@;location=%a@]}" PulseMutualRecursion.pp
-        cycle Location.pp location
+  | MutualRecursionCycle {cycle; location; is_call_with_same_values} ->
+      F.fprintf fmt
+        "MutualRecursionCycle {@[cycle=%a;@;location=%a;@;is_call_with_same_values=%b@]}"
+        PulseMutualRecursion.pp cycle Location.pp location is_call_with_same_values
   | ReadonlySharedPtrParameter {param; typ; location; used_locations} ->
       F.fprintf fmt
         "ReadonlySharedPtrParameter {@[param=%a;@;typ=%a;@;location=%a;@;used_locations=%a@]}"
@@ -688,8 +690,8 @@ let get_message_and_suggestion diagnostic =
       F.asprintf "Abstract class `%s` is being instantiated %a" (Typ.Name.name type_name) pp_trace
         trace
       |> no_suggestion
-  | MutualRecursionCycle {cycle} ->
-      PulseMutualRecursion.get_error_message cycle |> no_suggestion
+  | MutualRecursionCycle {cycle; is_call_with_same_values} ->
+      PulseMutualRecursion.get_error_message cycle ~is_call_with_same_values |> no_suggestion
   | ReadonlySharedPtrParameter {param; location; used_locations} ->
       let pp_used_locations f =
         match used_locations with
@@ -1147,8 +1149,8 @@ let get_trace = function
         ~pp_immediate:(fun fmt ->
           F.fprintf fmt "abstract class %s is instantiated here" (Typ.Name.name type_name) )
         trace []
-  | MutualRecursionCycle {cycle} ->
-      PulseMutualRecursion.to_errlog cycle
+  | MutualRecursionCycle {cycle; is_call_with_same_values} ->
+      PulseMutualRecursion.to_errlog cycle ~is_call_with_same_values
   | ReadonlySharedPtrParameter {param; typ; location; used_locations} ->
       let nesting = 0 in
       Errlog.make_trace_element nesting location (get_param_typ param typ) []
@@ -1269,8 +1271,9 @@ let get_issue_type ~latent issue_type =
       IssueType.no_true_branch_in_if ~latent
   | ErlangError (Try_clause _), _ ->
       IssueType.no_matching_branch_in_try ~latent
-  | MutualRecursionCycle _, _ ->
-      IssueType.mutual_recursion_cycle
+  | MutualRecursionCycle {is_call_with_same_values}, _ ->
+      if is_call_with_same_values then IssueType.infinite_recursion
+      else IssueType.mutual_recursion_cycle
   | ReadonlySharedPtrParameter _, false ->
       IssueType.readonly_shared_ptr_param
   | ReadUninitialized {typ= Value}, _ ->

infer/src/pulse/PulseDiagnostic.mli

@@ -89,7 +89,8 @@ type t =
   | DynamicTypeMismatch of {location: Location.t}
   | ErlangError of ErlangError.t
   | HackCannotInstantiateAbstractClass of {type_name: Typ.Name.t; trace: Trace.t}
-  | MutualRecursionCycle of {cycle: PulseMutualRecursion.t; location: Location.t}
+  | MutualRecursionCycle of
+      {cycle: PulseMutualRecursion.t; location: Location.t; is_call_with_same_values: bool}
   | ReadonlySharedPtrParameter of
       {param: Var.t; typ: Typ.t; location: Location.t; used_locations: Location.t list}
   | ReadUninitialized of ReadUninitialized.t

infer/src/pulse/PulseInterproc.ml

@@ -938,7 +938,8 @@ let apply_post_from_callee_post path callee_proc_name call_location callee_summa
 
 
 let report_mutual_recursion_cycle
-    ({InterproceduralAnalysis.add_errlog; proc_desc; err_log} as analysis_data) cycle =
+    ({InterproceduralAnalysis.add_errlog; proc_desc; err_log} as analysis_data) cycle
+    ~is_call_with_same_values =
   let proc_name = Procdesc.get_proc_name proc_desc in
   PulseMutualRecursion.iter_rotations cycle ~f:(fun cycle ->
       let inner_call = PulseMutualRecursion.get_inner_call cycle in
@@ -959,7 +960,7 @@ let report_mutual_recursion_cycle
           L.d_printfln "reporting on procedure %a (foreign=%b) at %a" Procname.pp inner_call
             is_foreign_procedure Location.pp_file_pos location ;
           PulseReport.report report_analysis_data ~is_suppressed:false ~latent:false
-            (MutualRecursionCycle {cycle; location}) ;
+            (MutualRecursionCycle {cycle; location; is_call_with_same_values}) ;
           if is_foreign_procedure then add_errlog inner_call err_log )
 
 
@@ -999,7 +1000,11 @@ let record_recursive_calls ({InterproceduralAnalysis.proc_desc} as analysis_data
                   (PulseMutualRecursion.get_inner_call cycle)
                   (Procdesc.get_proc_name proc_desc)
               then (
-                report_mutual_recursion_cycle analysis_data cycle ;
+                let is_call_with_same_values =
+                  AbductiveDomain.are_same_values_as_pre_formals proc_desc actuals_values
+                    call_state.astate
+                in
+                report_mutual_recursion_cycle ~is_call_with_same_values analysis_data cycle ;
                 None )
               else Some cycle )
         (AbductiveDomain.Summary.get_recursive_calls callee_summary)

infer/src/pulse/PulseMutualRecursion.ml

@@ -52,7 +52,7 @@ let pp fmt cycle =
   pp_chain fmt cycle.chain
 
 
-let get_error_message cycle =
+let get_error_message cycle ~is_call_with_same_values =
   let pp_cycle fmt cycle =
     match cycle.chain with
     | [] ->
@@ -61,9 +61,11 @@ let get_error_message cycle =
         F.fprintf fmt "mutual recursion cycle: %a -> %a" CallEvent.pp
           (CallEvent.Call cycle.innermost.call.proc_name) pp cycle
   in
-  F.asprintf
-    "%a; make sure this is intentional and cannot lead to non-termination or stack overflow"
-    pp_cycle cycle
+  F.asprintf "%a; %s" pp_cycle cycle
+    ( if is_call_with_same_values then
+        "moreover, the same values are passed along the cycle so there is a high chance of an \
+         infinite recursion"
+      else "make sure this is intentional and cannot lead to non-termination or stack overflow" )
 
 
 let iter_rotations cycle ~f =
@@ -86,12 +88,13 @@ let iter_rotations cycle ~f =
   done
 
 
-let to_errlog cycle =
+let to_errlog cycle ~is_call_with_same_values =
   let rec chain_to_errlog prev_call = function
     | [] ->
         Errlog.make_trace_element 0 cycle.innermost.call.location
-          (F.asprintf "%a makes a recursive call to %a" CallEvent.pp (CallEvent.Call prev_call)
-             CallEvent.pp (CallEvent.Call cycle.innermost.call.proc_name) )
+          (F.asprintf "%a makes a recursive call to %a%s" CallEvent.pp (CallEvent.Call prev_call)
+             CallEvent.pp (CallEvent.Call cycle.innermost.call.proc_name)
+             (if is_call_with_same_values then " with the same argument values" else "") )
           []
         :: []
     | call :: chain ->

infer/src/pulse/PulseMutualRecursion.mli

@@ -36,8 +36,8 @@ val iter_rotations : t -> f:(t -> unit) -> unit
 
 val pp : F.formatter -> t -> unit
 
-val get_error_message : t -> string
+val get_error_message : t -> is_call_with_same_values:bool -> string
 
-val to_errlog : t -> Errlog.loc_trace
+val to_errlog : t -> is_call_with_same_values:bool -> Errlog.loc_trace
 
 module Set : PrettyPrintable.PPSet with type elt = t