[ondemand] record specialisation in active procedures (but don't use …

…it yet)

Summary:
This will allow analysing some trickier examples that might otherwise appear
to be recursive, where each recursive call uses a different
specialisation.

Do most of the changes but ignore the specialisation component for now as it seems to cause issues.

Reviewed By: ngorogiannis

Differential Revision: D62582811

fbshipit-source-id: ed1041f03e9336ee5e7fe866ffea61f88289069d

infer/src/backend/ondemand.ml

@@ -20,34 +20,46 @@ let () = AnalysisGlobalState.register_ref nesting ~init:(fun () -> -1)
 
 let max_nesting_to_print = 8
 
+(* can be switched to a [HashQueue] if we ever need to keep track of the order as well *)
+module AnalysisTargetsHashSet = HashSet.Make (struct
+  (* temporary: record [SpecializedProcname.t] but only compare by their proc names, ignoring specialization *)
+  type t = SpecializedProcname.t = {proc_name: Procname.t; specialization: Specialization.t option}
+
+  let equal {proc_name= proc_name1} {proc_name= proc_name2} = Procname.equal proc_name1 proc_name2
+
+  let hash {proc_name} = Procname.hash proc_name
+end)
+
 (* keep track of the "call stack" of procedures we are currently analyzing; used to break mutual
    recursion cycles in a naive way: if we are already analyzing a procedure and another one (whose
    summary we transitively need to analyze the original procedure) asks for its summary, return no
    summary instead of triggering a recursive analysis of the original procedure. *)
 let is_active, add_active, remove_active, clear_actives =
-  let open Procname.HashSet in
+  let open AnalysisTargetsHashSet in
   let currently_analyzed = create 0 in
-  let is_active proc_name = mem currently_analyzed proc_name in
-  let add_active proc_name = add proc_name currently_analyzed in
-  let remove_active proc_name = remove proc_name currently_analyzed in
+  let is_active analysis_target = mem currently_analyzed analysis_target in
+  let add_active analysis_target = add analysis_target currently_analyzed in
+  let remove_active analysis_target = remove analysis_target currently_analyzed in
   let clear_actives () = clear currently_analyzed in
   (is_active, add_active, remove_active, clear_actives)
 
 
 (** an alternative mean of "cutting" recursion cycles used when replaying a previous analysis: times
     where [is_active] caused ondemand to return an empty summary to avoid a recursive analysis in
-    the previous analysis scheduling are recorded in this variable *)
+    the previous analysis scheduling are recorded in this variable
+
+    TODO: [edges_to_ignore] should take specialization into account, like [is_active] *)
 let edges_to_ignore = ref None
 
 (** use either [is_active] or [edges_to_ignore] to determine if we should return an empty summary to
     avoid mutual recursion cycles *)
-let in_mutual_recursion_cycle ~caller_summary ~callee =
+let in_mutual_recursion_cycle ~caller_summary ~callee specialization =
   match (!edges_to_ignore, caller_summary) with
   | Some edges_to_ignore, Some {Summary.proc_name} ->
       Procname.Map.find_opt proc_name edges_to_ignore
       |> Option.exists ~f:(fun recursive_callees -> Procname.Set.mem callee recursive_callees)
   | None, _ | _, None ->
-      is_active callee
+      is_active {proc_name= callee; specialization}
 
 
 let procedure_is_defined proc_name =
@@ -122,7 +134,7 @@ let set_complete_result analysis_req summary =
       ()
 
 
-let analyze exe_env analysis_req ~specialization callee_summary callee_pdesc =
+let analyze exe_env analysis_req specialization callee_summary callee_pdesc =
   let summary =
     Callbacks.iterate_procedure_callbacks exe_env analysis_req ?specialization callee_summary
       callee_pdesc
@@ -132,7 +144,8 @@ let analyze exe_env analysis_req ~specialization callee_summary callee_pdesc =
   summary
 
 
-let run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname callee_pdesc =
+let run_proc_analysis exe_env tenv analysis_req specialization_context ?caller_pname callee_pdesc =
+  let specialization = Option.map ~f:snd specialization_context in
   let callee_pname = Procdesc.get_proc_name callee_pdesc in
   let callee_attributes = Procdesc.get_attributes callee_pdesc in
   let log_elapsed_time =
@@ -155,15 +168,15 @@ let run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname ca
     update_taskbar (Some callee_pname) (Some source_file) ;
     Preanal.do_preanalysis tenv callee_pdesc ;
     let initial_callee_summary =
-      match specialization with
+      match specialization_context with
       | None ->
           if Config.debug_mode then
             DotCfg.emit_proc_desc callee_attributes.translation_unit callee_pdesc |> ignore ;
           Summary.OnDisk.reset callee_pname analysis_req
       | Some (current_summary, _) ->
           current_summary
     in
-    add_active callee_pname ;
+    add_active {proc_name= callee_pname; specialization} ;
     initial_callee_summary
   in
   let postprocess summary =
@@ -178,7 +191,7 @@ let run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname ca
                    Dependencies.record_pname_dep ~caller:callee_pname RecursionEdge callee )
                  recursive_callees ) ) ;
     let summary = Summary.OnDisk.store analysis_req summary in
-    remove_active callee_pname ;
+    remove_active {proc_name= callee_pname; specialization} ;
     Printer.write_proc_html callee_pdesc ;
     log_elapsed_time () ;
     summary
@@ -197,16 +210,15 @@ let run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname ca
     in
     let new_summary = {summary with stats; payloads} in
     let new_summary = Summary.OnDisk.store analysis_req new_summary in
-    remove_active callee_pname ;
+    remove_active {proc_name= callee_pname; specialization} ;
     log_elapsed_time () ;
     new_summary
   in
   let initial_callee_summary = preprocess () in
   try
     let callee_summary =
       if callee_attributes.ProcAttributes.is_defined then
-        let specialization = Option.map ~f:snd specialization in
-        analyze exe_env analysis_req ~specialization initial_callee_summary callee_pdesc
+        analyze exe_env analysis_req specialization initial_callee_summary callee_pdesc
       else initial_callee_summary
     in
     let final_callee_summary = postprocess callee_summary in
@@ -243,15 +255,15 @@ let run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname ca
 
 
 (* shadowed for tracing *)
-let run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname callee_pdesc =
+let run_proc_analysis exe_env tenv analysis_req specialization ?caller_pname callee_pdesc =
   PerfEvent.(
     log (fun logger ->
         let callee_pname = Procdesc.get_proc_name callee_pdesc in
         log_begin_event logger ~name:"ondemand" ~categories:["backend"]
           ~arguments:[("proc", `String (Procname.to_string callee_pname))]
           () ) ) ;
   let summary =
-    run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname callee_pdesc
+    run_proc_analysis exe_env tenv analysis_req specialization ?caller_pname callee_pdesc
   in
   PerfEvent.(log (fun logger -> log_end_event logger ())) ;
   summary
@@ -327,13 +339,15 @@ let is_in_block_list =
 
 let rec analyze_callee exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t) ~specialization
     ?caller_summary ?(from_file_analysis = false) callee_pname : _ AnalysisResult.t =
-  let cycle_detected = in_mutual_recursion_cycle ~caller_summary ~callee:callee_pname in
+  let cycle_detected =
+    in_mutual_recursion_cycle ~caller_summary ~callee:callee_pname specialization
+  in
   let analysis_result_of_option opt = Result.of_option opt ~error:AnalysisResult.AnalysisFailed in
   register_callee ~cycle_detected ?caller_summary callee_pname ;
   if cycle_detected then Error MutualRecursionCycle
   else if is_in_block_list callee_pname then Error InBlockList
   else
-    let analyze_callee_aux ~specialization =
+    let analyze_callee_aux specialization_context =
       error_if_ondemand_analysis_during_replay ~from_file_analysis caller_summary callee_pname ;
       Procdesc.load callee_pname
       >>= fun callee_pdesc ->
@@ -348,8 +362,8 @@ let rec analyze_callee exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t)
                 ~f:(fun () ->
                   let caller_pname = caller_summary >>| fun summ -> summ.Summary.proc_name in
                   Some
-                    (run_proc_analysis exe_env tenv analysis_req ~specialization ?caller_pname
-                       callee_pdesc ) )
+                    (run_proc_analysis exe_env tenv analysis_req specialization_context
+                       ?caller_pname callee_pdesc ) )
                 ~on_timeout:(fun span ->
                   L.debug Analysis Quiet
                     "TIMEOUT after %fs of CPU time analyzing %a:%a, outside of any checkers \
@@ -360,7 +374,7 @@ let rec analyze_callee exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t)
             ~finally:(fun () -> AnalysisGlobalState.restore previous_global_state) )
     in
     let analyze_specialization_none () =
-      let res = analyze_callee_aux ~specialization:None in
+      let res = analyze_callee_aux None in
       Option.iter res ~f:(set_complete_result analysis_req) ;
       analysis_result_of_option res
     in
@@ -387,8 +401,7 @@ let rec analyze_callee exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t)
           Ok summary
         else if procedure_is_defined callee_pname then
           (* the current summary is not suitable for this specialization request *)
-          analyze_callee_aux ~specialization:(Some (summary, specialization))
-          |> analysis_result_of_option
+          analyze_callee_aux (Some (summary, specialization)) |> analysis_result_of_option
         else (* can we even get there? *) Error UnknownProcedure
     | None, None ->
         if procedure_is_defined callee_pname then analyze_specialization_none ()

infer/src/pulse/PulseCallOperations.ml

@@ -631,8 +631,17 @@ let maybe_dynamic_type_specialization_is_needed already_specialized contradictio
       `UseCurrentSummary
 
 
-let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency} as analysis_data)
-    path call_loc callee_pname ~ret ~actuals ~formals_opt ~call_kind (astate : AbductiveDomain.t)
+let on_recursive_call ({InterproceduralAnalysis.proc_desc} as analysis_data) call_loc callee_pname
+    astate =
+  let astate, cycle = AbductiveDomain.add_recursive_call call_loc callee_pname astate in
+  if Procname.equal callee_pname (Procdesc.get_proc_name proc_desc) then
+    PulseReport.report analysis_data ~is_suppressed:false ~latent:false
+      (MutualRecursionCycle {cycle; location= call_loc}) ;
+  astate
+
+
+let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analysis_data) path
+    call_loc callee_pname ~ret ~actuals ~formals_opt ~call_kind (astate : AbductiveDomain.t)
     ?call_flags non_disj_caller =
   let has_continue_program results =
     let f one_result =
@@ -658,7 +667,8 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
       ([], non_disj) )
     else (results, non_disj)
   in
-  let call_aux specialization {PulseSummary.pre_post_list= exec_states; non_disj= non_disj_callee} =
+  let call_specialized specialization
+      {PulseSummary.pre_post_list= exec_states; non_disj= non_disj_callee} astate =
     let results, (non_disj, contradiction) =
       call_aux disjunct_limit analysis_data path call_loc callee_pname ret actuals call_kind
         (IRAttributes.load_exn callee_pname)
@@ -670,8 +680,8 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
     (results, non_disj, contradiction)
   in
   let rec iter_call ~max_iteration ~nth_iteration ~is_pulse_specialization_limit_not_reached
-      ?(specialization = Specialization.Pulse.bottom) already_given summary =
-    let res, non_disj, contradiction = call_aux specialization summary in
+      ?(specialization = Specialization.Pulse.bottom) already_given summary astate =
+    let res, non_disj, contradiction = call_specialized specialization summary astate in
     let needs_aliasing_specialization =
       match (res, contradiction) with
       | [], Some (Aliasing _) ->
@@ -682,13 +692,9 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
           `NoAliasSpecializationRequired
     in
     let request_specialization specialization =
-      let specialized_summary : PulseSummary.t =
-        match analyze_dependency ~specialization:(Pulse specialization) callee_pname with
-        | Ok summary ->
-            summary
-        | Error no_summary ->
-            L.die InternalError "No summary found by specialization: %a"
-              AnalysisResult.pp_no_summary no_summary
+      let open IResult.Let_syntax in
+      let+ (specialized_summary : PulseSummary.t) =
+        analyze_dependency ~specialization:(Pulse specialization) callee_pname
       in
       let is_limit_not_reached =
         Specialization.Pulse.is_pulse_specialization_limit_not_reached
@@ -702,8 +708,8 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
       | Some pre_posts ->
           (pre_posts, is_limit_not_reached)
     in
-    let case_if_specialization_is_impossible ~f =
-      ( f res
+    let case_if_specialization_is_impossible res =
+      ( res
       , summary
       , non_disj
       , contradiction
@@ -713,8 +719,7 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
         | `NoAliasSpecializationRequired ->
             `KnownCall )
     in
-    if not is_pulse_specialization_limit_not_reached then
-      case_if_specialization_is_impossible ~f:Fun.id
+    if not is_pulse_specialization_limit_not_reached then case_if_specialization_is_impossible res
     else
       let more_specialization, ask_caller_of_caller_first, needs_from_caller =
         match needs_aliasing_specialization with
@@ -773,17 +778,32 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
             || Specialization.Pulse.is_bottom specialization
           then
             case_if_specialization_is_impossible
-              ~f:(add_need_dynamic_type_specialization needs_from_caller)
+              (add_need_dynamic_type_specialization needs_from_caller res)
           else (
             L.d_printfln "requesting specialized analysis using %sspecialization %a"
               (if not (AbstractValue.Set.is_empty needs_from_caller) then "partial " else "")
               Specialization.Pulse.pp specialization ;
-            let summary, is_pulse_specialization_limit_not_reached =
-              request_specialization specialization
-            in
-            let already_given = Specialization.Pulse.Set.add specialization already_given in
-            iter_call ~max_iteration ~nth_iteration:(nth_iteration + 1)
-              ~is_pulse_specialization_limit_not_reached ~specialization already_given summary )
+            match request_specialization specialization with
+            | Error MutualRecursionCycle ->
+                let res =
+                  List.map res ~f:(function result ->
+                      (let+ exec_state = result in
+                       match exec_state with
+                       | ContinueProgram astate ->
+                           ContinueProgram
+                             (on_recursive_call analysis_data call_loc callee_pname astate)
+                       | exec_state ->
+                           exec_state ) )
+                in
+                case_if_specialization_is_impossible res
+            | Error ((AnalysisFailed | InBlockList | UnknownProcedure) as no_summary) ->
+                L.die InternalError "No summary found by specialization: %a"
+                  AnalysisResult.pp_no_summary no_summary
+            | Ok (summary, is_pulse_specialization_limit_not_reached) ->
+                let already_given = Specialization.Pulse.Set.add specialization already_given in
+                iter_call ~max_iteration ~nth_iteration:(nth_iteration + 1)
+                  ~is_pulse_specialization_limit_not_reached ~specialization already_given summary
+                  astate )
   in
   match analyze_dependency callee_pname with
   | Ok summary ->
@@ -795,7 +815,7 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
       let already_given = Specialization.Pulse.Set.empty in
       let res, summary_used, non_disj, contradiction, resolution_status =
         iter_call ~max_iteration ~nth_iteration:0 ~is_pulse_specialization_limit_not_reached
-          already_given summary.PulseSummary.main
+          already_given summary.PulseSummary.main astate
       in
       let has_continue_program = has_continue_program res in
       if has_continue_program then GlobalForStats.node_is_not_stuck () ;
@@ -824,11 +844,7 @@ let call ?disjunct_limit ({InterproceduralAnalysis.proc_desc; analyze_dependency
       let astate =
         match no_summary with
         | MutualRecursionCycle ->
-            let astate, cycle = AbductiveDomain.add_recursive_call call_loc callee_pname astate in
-            if Procname.equal callee_pname (Procdesc.get_proc_name proc_desc) then
-              PulseReport.report analysis_data ~is_suppressed:false ~latent:false
-                (MutualRecursionCycle {cycle; location= call_loc}) ;
-            astate
+            on_recursive_call analysis_data call_loc callee_pname astate
         | AnalysisFailed | InBlockList | UnknownProcedure ->
             astate
       in

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -175,6 +175,12 @@ codetoanalyze/c/pulse/resource_leak.c, socketNotClosed_bad, 4, PULSE_RESOURCE_LE
 codetoanalyze/c/pulse/setlocale.c, FP_setlocale_null_impossible_ok, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/shift.c, return_null_deref1_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `return_depends_on_lshift`,is assigned to the null pointer,returned,return from call to `return_depends_on_lshift`,invalid access occurs here]
 codetoanalyze/c/pulse/shift.c, return_null_deref2_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `return_depends_on_rshift`,is assigned to the null pointer,returned,return from call to `return_depends_on_rshift`,invalid access occurs here]
+codetoanalyze/c/pulse/specialization.c, invoke, 0, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`invoke` calls `add_more_bad`,`add_more_bad` makes a recursive call to `invoke`]
+codetoanalyze/c/pulse/specialization.c, add_more_bad, 2, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`add_more_bad` calls `invoke`,`invoke` makes a recursive call to `add_more_bad`]
+codetoanalyze/c/pulse/specialization.c, test_invoke_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/specialization.c, test_recursive_invoke_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/specialization.c, two_pointers_recursion_bad, 2, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`two_pointers_recursion_bad` makes a recursive call to `two_pointers_recursion_bad`]
+codetoanalyze/c/pulse/specialization.c, invoke_itself_bad, 3, MUTUAL_RECURSION_CYCLE, no_bucket, WARNING, [`invoke_itself_bad` makes a recursive call to `invoke_itself_bad`]
 codetoanalyze/c/pulse/taint_var_arg.c, printf_source_bad1, 0, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `int_source` with kind `Simple`,flows to this sink: value passed as argument `#2` to `printf` with kind `Simple`], source: int_source, sink: printf, tainted expression: int_source()
 codetoanalyze/c/pulse/taint_var_arg.c, printf_source_bad2, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `int_source` with kind `Simple`,flows to this sink: value passed as argument `#2` to `printf` with kind `Simple`], source: int_source, sink: printf, tainted expression: int_source()
 codetoanalyze/c/pulse/taint_var_arg.c, printf_source_bad3, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `float_source` with kind `Simple`,flows to this sink: value passed as argument `#3` to `printf` with kind `Simple`], source: float_source, sink: printf, tainted expression: float_source()