[multicore][2/n] domain-local analysis state

Summary:
Use domain-local storage to make global state thread safe in
- Preanal
- Ondemand
- Language (plus improve its interface)

Reviewed By: skcho

Differential Revision:
D66812601

Privacy Context Container: L1208441

fbshipit-source-id: 1a6e4ef3029049bbe64cf9fd471e33eda221d057

infer/src/backend/callbacks.ml

@@ -57,7 +57,7 @@ let register_file_callback checker language (callback : file_callback_t) =
 let iterate_procedure_callbacks exe_env analysis_req ?specialization
     ({Summary.proc_name} as summary) proc_desc =
   let procedure_language = Procname.get_language proc_name in
-  Language.curr_language := procedure_language ;
+  Language.set_language procedure_language ;
   let is_specialized = Procdesc.is_specialized proc_desc in
   let is_requested =
     let is_dependency_of checker =
@@ -115,7 +115,7 @@ let iterate_file_callbacks_and_store_issues procedures exe_env source_file =
     in
     List.iter (List.rev !file_callbacks_rev) ~f:(fun {checker; language; callback} ->
         if language_matches language then (
-          Language.curr_language := language ;
+          Language.set_language language ;
           if not (IssueLog.is_stored ~checker ~file:source_file) then
             let issue_log = callback environment in
             IssueLog.store ~checker ~file:source_file issue_log ) )

infer/src/backend/ondemand.ml

@@ -113,24 +113,26 @@ let procedure_is_defined proc_name =
 
 (* Remember what the last status sent was so that we can update the status correctly when entering
    and exiting nested ondemand analyses. In particular we need to remember the original time.*)
-let current_taskbar_status : (Mtime.t * string) option ref = ref None
+let current_taskbar_status : (Mtime.t * string) option Domain.DLS.key =
+  Domain.DLS.new_key (fun () -> None)
+
 
 let () =
   let open IOption.Let_syntax in
   AnalysisGlobalState.register
     ~save:(fun () ->
-      let+ t0, status = !current_taskbar_status in
+      let+ t0, status = Domain.DLS.get current_taskbar_status in
       (* the time elapsed doing [status] so far *)
       (Mtime.span t0 (Mtime_clock.now ()), status) )
     ~restore:(fun proc_analysis_time ->
-      current_taskbar_status :=
-        let+ suspended_span, status = proc_analysis_time in
-        (* forget about the time spent doing a nested analysis and resend the status of the outer
-           analysis with the updated "original" start time *)
-        let new_t0 = Mtime.sub_span (Mtime_clock.now ()) suspended_span |> Option.value_exn in
-        !ProcessPoolState.update_status (Some new_t0) status ;
-        (new_t0, status) )
-    ~init:(fun _ -> current_taskbar_status := None)
+      Domain.DLS.set current_taskbar_status
+        (let+ suspended_span, status = proc_analysis_time in
+         (* forget about the time spent doing a nested analysis and resend the status of the outer
+            analysis with the updated "original" start time *)
+         let new_t0 = Mtime.sub_span (Mtime_clock.now ()) suspended_span |> Option.value_exn in
+         !ProcessPoolState.update_status (Some new_t0) status ;
+         (new_t0, status) ) )
+    ~init:(fun _ -> Domain.DLS.set current_taskbar_status None)
 
 
 let () =
@@ -147,7 +149,7 @@ let () =
 
 
 (** reference to log errors only at the innermost recursive call *)
-let logged_error = ref false
+let logged_error = Domain.DLS.new_key (fun () -> false)
 
 let update_taskbar proc_name_opt source_file_opt =
   let t0 = Mtime_clock.now () in
@@ -166,7 +168,7 @@ let update_taskbar proc_name_opt source_file_opt =
     | None, None ->
         "Unspecified task"
   in
-  current_taskbar_status := Some (t0, status) ;
+  Domain.DLS.set current_taskbar_status (Some (t0, status)) ;
   !ProcessPoolState.update_status (Some t0) status
 
 
@@ -269,7 +271,7 @@ let run_proc_analysis exe_env tenv analysis_req specialization_context ?caller_p
     in
     let final_callee_summary = postprocess callee_summary in
     (* don't forget to reset this so we output messages for future errors too *)
-    logged_error := false ;
+    Domain.DLS.set logged_error false ;
     final_callee_summary
   with exn -> (
     let backtrace = Printexc.get_backtrace () in
@@ -282,13 +284,13 @@ let run_proc_analysis exe_env tenv analysis_req specialization_context ?caller_p
             ActiveProcedures.remove {proc_name= callee_pname; specialization} ;
             true
         | exn ->
-            if not !logged_error then (
+            if not (Domain.DLS.get logged_error) then (
               let source_file = callee_attributes.ProcAttributes.translation_unit in
               let location = callee_attributes.ProcAttributes.loc in
               L.internal_error "While analysing function %a:%a at %a, raised %s@\n" SourceFile.pp
                 source_file Procname.pp callee_pname Location.pp_file_pos location
                 (Exn.to_string exn) ;
-              logged_error := true ) ;
+              Domain.DLS.set logged_error true ) ;
             not Config.keep_going ) ;
     L.internal_error "@\nERROR RUNNING BACKEND: %a %s@\n@\nBACK TRACE@\n%s@?" Procname.pp
       callee_pname (Exn.to_string exn) backtrace ;
@@ -428,7 +430,7 @@ let analysis_result_of_option opt = Result.of_option opt ~error:AnalysisResult.A
 
 (** track how many times we restarted the analysis of the current dependency chain to make the
     analysis of mutual recursion cycles deterministic *)
-let number_of_recursion_restarts = ref 0
+let number_of_recursion_restarts = Domain.DLS.new_key (fun () -> 0)
 
 let rec analyze_callee_can_raise_recursion exe_env ~lazy_payloads (analysis_req : AnalysisRequest.t)
     ~specialization ?caller_summary ?(from_file_analysis = false) callee_pname : _ AnalysisResult.t
@@ -438,14 +440,14 @@ let rec analyze_callee_can_raise_recursion exe_env ~lazy_payloads (analysis_req
       let target = {SpecializedProcname.proc_name= callee_pname; specialization} in
       let cycle_start, cycle_length, first_active = ActiveProcedures.get_cycle_start target in
       if
-        !number_of_recursion_restarts >= Config.ondemand_recursion_restart_limit
+        Domain.DLS.get number_of_recursion_restarts >= Config.ondemand_recursion_restart_limit
         || SpecializedProcname.equal cycle_start target
       then (
         register_callee ~cycle_detected:true ?caller_summary callee_pname ;
         if Config.trace_ondemand then
           L.progress "Closed the cycle finishing in recursive call to %a@." Procname.pp callee_pname ;
         if
-          !number_of_recursion_restarts >= Config.ondemand_recursion_restart_limit
+          Domain.DLS.get number_of_recursion_restarts >= Config.ondemand_recursion_restart_limit
           && not (SpecializedProcname.equal cycle_start target)
         then Stats.incr_ondemand_recursion_cycle_restart_limit_hit () ;
         Error MutualRecursionCycle )
@@ -457,7 +459,7 @@ let rec analyze_callee_can_raise_recursion exe_env ~lazy_payloads (analysis_req
             (Pp.seq ~sep:"," SpecializedProcname.pp)
             (ActiveProcedures.get_all ()) ;
         (* we want the exception to pop back up to the beginning of the cycle, so we set [ttl= cycle_length] *)
-        incr number_of_recursion_restarts ;
+        Utils.with_dls number_of_recursion_restarts ~f:(( + ) 1) ;
         raise (RecursiveCycleException.RecursiveCycle {recursive= cycle_start; ttl= cycle_length}) )
   | `ReplayCycleCut ->
       register_callee ~cycle_detected:true ?caller_summary callee_pname ;
@@ -555,7 +557,7 @@ let analyze_callee exe_env ~lazy_payloads analysis_req ~specialization ?caller_s
   (* If [caller_summary] is set then we are analyzing a dependency of another procedure, so we
      should keep counting restarts within that dependency chain (or cycle). If it's not set then
      this is a "toplevel" analysis of [callee_pname] so we start fresh. *)
-  if Option.is_none caller_summary then number_of_recursion_restarts := 0 ;
+  if Option.is_none caller_summary then Domain.DLS.set number_of_recursion_restarts 0 ;
   analyze_callee exe_env ~lazy_payloads analysis_req ~specialization ?caller_summary
     ?from_file_analysis callee_pname
 
@@ -575,7 +577,7 @@ let analyze_proc_name_for_file_analysis exe_env analysis_req callee_pname =
 
 
 let analyze_file_procedures exe_env analysis_req procs_to_analyze source_file_opt =
-  let saved_language = !Language.curr_language in
+  let saved_language = Language.get_language () in
   let analyze_proc_name_call pname =
     ignore
       (analyze_proc_name_for_file_analysis exe_env analysis_req pname : Summary.t AnalysisResult.t)
@@ -584,7 +586,7 @@ let analyze_file_procedures exe_env analysis_req procs_to_analyze source_file_op
   Option.iter source_file_opt ~f:(fun source_file ->
       if Config.dump_duplicate_symbols then dump_duplicate_procs source_file procs_to_analyze ;
       Callbacks.iterate_file_callbacks_and_store_issues procs_to_analyze exe_env source_file ) ;
-  Language.curr_language := saved_language
+  Language.set_language saved_language
 
 
 (** Invoke all procedure-level and file-level callbacks on a given environment. *)

infer/src/backend/preanal.ml

@@ -318,20 +318,21 @@ module Liveness = struct
           astate
 
 
-    let cache_node = ref (Procdesc.Node.dummy (Procname.from_string_c_fun ""))
-
-    let cache_instr = ref Sil.skip_instr
-
-    let last_instr_in_node node =
-      let get_last_instr () =
-        CFG.instrs node |> Instrs.last |> Option.value ~default:Sil.skip_instr
+    let last_instr_in_node =
+      let cache_node =
+        Stdlib.Domain.DLS.new_key (fun () -> Procdesc.Node.dummy (Procname.from_string_c_fun ""))
       in
-      if phys_equal node !cache_node then !cache_instr
-      else
-        let last_instr = get_last_instr () in
-        cache_node := node ;
-        cache_instr := last_instr ;
-        last_instr
+      let cache_instr = Stdlib.Domain.DLS.new_key (fun () -> Sil.skip_instr) in
+      fun node ->
+        let get_last_instr () =
+          CFG.instrs node |> Instrs.last |> Option.value ~default:Sil.skip_instr
+        in
+        if phys_equal node (Stdlib.Domain.DLS.get cache_node) then Stdlib.Domain.DLS.get cache_instr
+        else
+          let last_instr = get_last_instr () in
+          Stdlib.Domain.DLS.set cache_node node ;
+          Stdlib.Domain.DLS.set cache_instr last_instr ;
+          last_instr
 
 
     let is_last_instr_in_node instr node = phys_equal (last_instr_in_node node) instr

infer/src/base/Language.ml

@@ -19,6 +19,10 @@ let language_to_string =
 
 let to_string lang = List.Assoc.find_exn language_to_string ~equal lang
 
-let curr_language = ref Clang
+let curr_language = Domain.DLS.new_key (fun () -> Clang)
 
-let curr_language_is lang = equal !curr_language lang
+let get_language () = Domain.DLS.get curr_language
+
+let curr_language_is lang = equal (get_language ()) lang
+
+let set_language lang = Domain.DLS.set curr_language lang

infer/src/base/Language.mli

@@ -13,6 +13,8 @@ val equal : t -> t -> bool
 
 val to_string : t -> string
 
-val curr_language : t ref
-
 val curr_language_is : t -> bool
+
+val get_language : unit -> t
+
+val set_language : t -> unit

infer/src/biabduction/PropUtil.ml

@@ -140,7 +140,7 @@ let remove_abduced_retvars tenv p =
 let remove_locals tenv (curr_f : Procdesc.t) p =
   let names_of_locals = List.map ~f:(get_name_of_local curr_f) (Procdesc.get_locals curr_f) in
   let names_of_locals' =
-    match !Language.curr_language with
+    match Language.get_language () with
     | Language.Clang ->
         (* in ObjC to deal with block we need to remove static locals *)
         let names_of_static_locals = get_name_of_objc_static_locals curr_f p in

infer/src/biabduction/Prover.ml

@@ -2234,7 +2234,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
     let root = Exp.Const (Const.Cstr s) in
     let sexp =
       let index = Exp.int (IntLit.of_int (String.length s)) in
-      match !Language.curr_language with
+      match Language.get_language () with
       | Clang ->
           Predicates.Earray
             ( Exp.int len
@@ -2270,7 +2270,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
           L.die InternalError "Python not supported"
     in
     let const_string_texp =
-      match !Language.curr_language with
+      match Language.get_language () with
       | Clang ->
           Exp.Sizeof
             { typ= Typ.mk_array (Typ.mk (Tint Typ.IChar)) ~length:len ~stride:(IntLit.of_int 1)

infer/src/biabduction/Rearrange.ml

@@ -476,7 +476,7 @@ let mk_ptsto_exp_footprint analysis_data pname tenv orig_prop (lexp, typ) max_st
       raise (Exceptions.Dangling_pointer_dereference (false, err_desc, __POS__)) ) ;
   let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
   let subtype =
-    match !Language.curr_language with
+    match Language.get_language () with
     | Clang ->
         Subtype.exact
     | Java ->

infer/src/biabduction/SymExec.ml

@@ -1628,7 +1628,7 @@ and proc_call callee_pname callee_summary
   let actuals = comb actual_pars formal_types in
   (* In case we call an objc instance method we add an extra spec
      where the receiver is null and the semantics of the call is nop *)
-  match (!Language.curr_language, callee_attributes.ProcAttributes.clang_method_kind) with
+  match (Language.get_language (), callee_attributes.ProcAttributes.clang_method_kind) with
   | Language.Clang, ClangMethodKind.OBJC_INSTANCE ->
       handle_objc_instance_method_call actual_pars pre tenv (fst ret_id_typ) caller_pdesc
         callee_pname path (fun () ->

infer/src/biabduction/interproc.ml

@@ -623,7 +623,7 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
   let sigma_new_formals =
     let do_formal (pv, typ) =
       let texp =
-        match !Language.curr_language with
+        match Language.get_language () with
         | Clang ->
             Exp.Sizeof
               {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact; nullable= true}
@@ -841,7 +841,7 @@ let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; err_log; tenv} a
 
 let set_current_language proc_desc =
   let language = Procname.get_language (Procdesc.get_proc_name proc_desc) in
-  Language.curr_language := language
+  Language.set_language language
 
 
 (** reset global values before analysing a procedure *)

infer/src/clang/Capture.ml

@@ -29,7 +29,7 @@ let validate_decl_from_channel chan =
 let init_global_state_for_capture_and_linters source_file =
   L.debug Capture Medium "Processing %s" (Filename.basename (SourceFile.to_abs_path source_file)) ;
   !ProcessPoolState.update_status None (SourceFile.to_string source_file) ;
-  Language.curr_language := Language.Clang ;
+  Language.set_language Clang ;
   if Config.capture then DB.Results_dir.init source_file ;
   CFrontend_config.reset_global_state ()
 

infer/src/concurrency/AbstractAddress.ml

@@ -52,7 +52,7 @@ let normalise_access_list (accesses : access_list) =
 
 let pp_with_base pp_base fmt (base, accesses) =
   let rec pp_rev_accesses fmt (accesses : access_list) =
-    match (accesses, !Language.curr_language) with
+    match (accesses, Language.get_language ()) with
     | _, Erlang ->
         L.internal_error "Erlang not supported@\n"
     | _, Hack ->
@@ -65,7 +65,7 @@ let pp_with_base pp_base fmt (base, accesses) =
         F.fprintf fmt "%a[]" pp_rev_accesses rest
     | FieldAccess field_name :: Dereference :: rest, _ ->
         let op =
-          match !Language.curr_language with
+          match Language.get_language () with
           | Clang ->
               "->"
           | Java ->

infer/src/concurrency/RacerDDomain.ml

@@ -28,7 +28,7 @@ let apply_to_first_actual actuals astate ~f =
 
 
 let pp_exp fmt exp =
-  match !Language.curr_language with
+  match Language.get_language () with
   | Clang ->
       AccessExpression.pp fmt exp
   | Java ->

infer/src/java/jMain.ml

@@ -11,7 +11,7 @@ open Javalib_pack
 module L = Logging
 
 let init_global_state source_file =
-  Language.curr_language := Language.Java ;
+  Language.set_language Java ;
   DB.Results_dir.init source_file ;
   Ident.NameGenerator.reset () ;
   JContext.reset_exn_node_table ()

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1963,7 +1963,7 @@ let filter_for_summary proc_name location astate0 =
 
 
 let should_havoc_if_unknown () =
-  match !Language.curr_language with
+  match Language.get_language () with
   | Java
     (* TODO(T138610370): temporary until we improve the way taint propagates for unknown calls *)
   | Hack

infer/src/pulse/PulseTopl.ml

@@ -536,16 +536,16 @@ let get env x =
 let set = List.Assoc.add ~equal:String.equal
 
 let make_field class_name field_name : Fieldname.t =
-  match !Language.curr_language with
+  match Language.get_language () with
   | Erlang -> (
     match ErlangTypeName.from_string class_name with
     | None ->
         L.die UserError "Unknown/unsupported Erlang type %s" class_name
     | Some typ ->
         Fieldname.make (ErlangType typ) field_name )
-  | _ ->
+  | lang ->
       L.die InternalError "Field access is not supported for current language (%s)"
-        (Language.to_string !Language.curr_language)
+        (Language.to_string lang)
 
 
 let deref_field_access pulse_state value class_name field_name : Formula.operand option =

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -231,7 +231,7 @@ let test_with_all_types_Nil phi =
       test_with_initial phi init_phi
 
 
-let () = Language.curr_language := Language.Erlang
+let () = Language.set_language Language.Erlang
 
 let simplify ~keep phi =
   let keep = AbstractValue.Set.of_list keep in