Skip to content

Commit

Permalink
[multicore][3/n] domain-local analysis state
Browse files Browse the repository at this point in the history
Summary:
Use domain-local storage to make global state thread safe in
- Pulse / Topl
- Lineage
- SilValidation

Reviewed By: skcho

Differential Revision:
D66825242

Privacy Context Container: L1208441

fbshipit-source-id: a9a58ed30a9a93c56c507172aac0f3d95e4d844a
  • Loading branch information
ngorogiannis authored and facebook-github-bot committed Dec 9, 2024
1 parent 2f1713f commit a09bcd8
Show file tree
Hide file tree
Showing 8 changed files with 51 additions and 43 deletions.
10 changes: 5 additions & 5 deletions infer/src/checkers/Lineage.ml
Original file line number Diff line number Diff line change
Expand Up @@ -939,23 +939,23 @@ module Out = struct
[@@deriving compare, equal, hash, sexp]
end

let channel_ref = ref None
let channel_key = Domain.DLS.new_key (fun () -> None)

let get_pid_channel () =
(* We keep the old simple-lineage output dir for historical reasons and should change it to
lineage once no external infra code depends on it anymore *)
let output_dir = Filename.concat Config.results_dir "simple-lineage" in
Unix.mkdir_p output_dir ;
match !channel_ref with
match Domain.DLS.get channel_key with
| None ->
let filename = Format.asprintf "lineage-%a.json" Pid.pp (Unix.getpid ()) in
let channel = Filename.concat output_dir filename |> Out_channel.create in
let close_channel () =
Option.iter !channel_ref ~f:Out_channel.close_no_err ;
channel_ref := None
Domain.DLS.get channel_key |> Option.iter ~f:Out_channel.close_no_err ;
Domain.DLS.set channel_key None
in
Epilogues.register ~f:close_channel ~description:"close output channel for lineage" ;
channel_ref := Some channel ;
Domain.DLS.set channel_key (Some channel) ;
channel
| Some channel ->
channel
Expand Down
6 changes: 3 additions & 3 deletions infer/src/checkers/SilValidation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ end = struct
let callbacks = {instr_conforms; call_exp_conforms; arg_exp_conforms= is_pure}
end

let error_counter = ref 0
let error_counter = Domain.DLS.new_key (fun () -> 0)

let error_limit = 10000

Expand Down Expand Up @@ -332,11 +332,11 @@ let checker (language : Language.t) ({proc_desc; err_log} : IntraproceduralAnaly
(* Clang is the most general, i.e., least restrictive validator. *)
Clang.callbacks
in
if !error_counter < error_limit then
if Domain.DLS.get error_counter < error_limit then
Procdesc.iter_instrs
(fun _ instr ->
if not (instr_conforms instr) then (
let msg = instr_error_msg ~call_exp_conforms ~arg_exp_conforms instr in
report_error proc_desc err_log instr msg ;
error_counter := !error_counter + 1 ) )
Utils.with_dls error_counter ~f:(( + ) 1) ) )
proc_desc
11 changes: 6 additions & 5 deletions infer/src/pulse/Pulse.ml
Original file line number Diff line number Diff line change
Expand Up @@ -192,13 +192,14 @@ let report_unnecessary_parameter_copies ({InterproceduralAnalysis.proc_desc; ten
let heap_size () = (Gc.quick_stat ()).heap_words

(* for printing the session name only, promise! *)
let current_specialization = ref None
let current_specialization = Domain.DLS.new_key (fun () -> None)

let () = AnalysisGlobalState.register_ref ~init:(fun () -> None) current_specialization
let () = AnalysisGlobalState.register_dls ~init:(fun () -> None) current_specialization

let pp_space_specialization fmt =
Option.iter !current_specialization ~f:(function _, Specialization.Pulse specialization ->
F.fprintf fmt " (specialized: %a)" Specialization.Pulse.pp specialization )
Domain.DLS.get current_specialization
|> Option.iter ~f:(function _, Specialization.Pulse specialization ->
F.fprintf fmt " (specialized: %a)" Specialization.Pulse.pp specialization )


module PulseTransferFunctions = struct
Expand Down Expand Up @@ -1856,7 +1857,7 @@ let analyze specialization ({InterproceduralAnalysis.tenv; proc_desc; exe_env} a
let checker ?specialization ({InterproceduralAnalysis.proc_desc} as analysis_data) =
let open IOption.Let_syntax in
if should_analyze proc_desc then (
current_specialization := specialization ;
Domain.DLS.set current_specialization specialization ;
try
match specialization with
| None ->
Expand Down
16 changes: 8 additions & 8 deletions infer/src/pulse/PulseAbstractValue.ml
Original file line number Diff line number Diff line change
Expand Up @@ -11,21 +11,21 @@ type t = int [@@deriving compare, equal, hash]

let initial_next_fresh = 1

let next_fresh = ref initial_next_fresh
let next_fresh = Domain.DLS.new_key (fun () -> initial_next_fresh)

let mk_fresh () =
let l = !next_fresh in
incr next_fresh ;
let l = Domain.DLS.get next_fresh in
Domain.DLS.set next_fresh (l + 1) ;
l


let initial_next_fresh_restricted = -1

let next_fresh_restricted = ref initial_next_fresh_restricted
let next_fresh_restricted = Domain.DLS.new_key (fun () -> initial_next_fresh_restricted)

let mk_fresh_restricted () =
let v = !next_fresh_restricted in
decr next_fresh_restricted ;
let v = Domain.DLS.get next_fresh_restricted in
Domain.DLS.set next_fresh_restricted (v - 1) ;
v


Expand Down Expand Up @@ -63,7 +63,7 @@ module Map = struct
end

let () =
AnalysisGlobalState.register_ref next_fresh ~init:(fun () -> initial_next_fresh) ;
AnalysisGlobalState.register_ref next_fresh_restricted ~init:(fun () ->
AnalysisGlobalState.register_dls next_fresh ~init:(fun () -> initial_next_fresh) ;
AnalysisGlobalState.register_dls next_fresh_restricted ~init:(fun () ->
initial_next_fresh_restricted ) ;
()
19 changes: 12 additions & 7 deletions infer/src/pulse/PulseCallOperations.ml
Original file line number Diff line number Diff line change
Expand Up @@ -65,19 +65,24 @@ module GlobalForStats = struct

let empty = {node_is_not_stuck= false; one_call_is_stuck= false}

let global = ref empty
let global = Domain.DLS.new_key (fun () -> empty)

let () = AnalysisGlobalState.register_ref ~init:(fun () -> empty) global
let () = AnalysisGlobalState.register_dls ~init:(fun () -> empty) global

let init_before_call () = global := {!global with node_is_not_stuck= false}
let init_before_call () =
Utils.with_dls global ~f:(fun global -> {global with node_is_not_stuck= false})

let is_node_not_stuck () = !global.node_is_not_stuck

let node_is_not_stuck () = global := {!global with node_is_not_stuck= true}
let is_node_not_stuck () = (Domain.DLS.get global).node_is_not_stuck

let is_one_call_stuck () = !global.one_call_is_stuck
let node_is_not_stuck () =
Utils.with_dls global ~f:(fun global -> {global with node_is_not_stuck= true})

let one_call_is_stuck () = global := {!global with one_call_is_stuck= true}

let is_one_call_stuck () = (Domain.DLS.get global).one_call_is_stuck

let one_call_is_stuck () =
Utils.with_dls global ~f:(fun global -> {global with one_call_is_stuck= true})
end

let print_arity_mismatch_message ?(extra_call_prefix = "") callee_pname_opt ~formals ~actuals =
Expand Down
14 changes: 7 additions & 7 deletions infer/src/pulse/PulseContext.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,23 +7,23 @@

open! IStd

let proc_desc_ref = ref None
let proc_desc_key = Domain.DLS.new_key (fun () -> None)

let tenv_ref = ref (None : Tenv.t Option.t)
let tenv_key = Domain.DLS.new_key (fun () : Tenv.t Option.t -> None)

let () =
AnalysisGlobalState.register_ref_with_proc_desc_and_tenv proc_desc_ref
AnalysisGlobalState.register_dls_with_proc_desc_and_tenv proc_desc_key
~init:(fun proc_desc _tenv -> Some proc_desc )


let () =
AnalysisGlobalState.register_ref_with_proc_desc_and_tenv tenv_ref ~init:(fun _proc_desc tenv ->
AnalysisGlobalState.register_dls_with_proc_desc_and_tenv tenv_key ~init:(fun _proc_desc tenv ->
Some tenv )


let proc_desc () = !proc_desc_ref
let proc_desc () = Domain.DLS.get proc_desc_key

let tenv () = !tenv_ref
let tenv () = Domain.DLS.get tenv_key

let tenv_exn () =
match tenv () with
Expand All @@ -33,4 +33,4 @@ let tenv_exn () =
tenv


let set_tenv_global_for_testing tenv = tenv_ref := Some tenv
let set_tenv_global_for_testing tenv = Domain.DLS.set tenv_key (Some tenv)
10 changes: 6 additions & 4 deletions infer/src/pulse/PulseTopl.ml
Original file line number Diff line number Diff line change
Expand Up @@ -716,7 +716,7 @@ let static_match_call tenv return arguments procname label : tcontext option =


module Debug = struct
let dropped_disjuncts_count = ref 0
let dropped_disjuncts_count = Domain.DLS.new_key (fun () -> 0)

let rec matched_transitions =
lazy
Expand All @@ -743,9 +743,11 @@ module Debug = struct
(F.pp_print_list pp) unseen


let () = AnalysisGlobalState.register_ref dropped_disjuncts_count ~init:(fun () -> 0)
let () = AnalysisGlobalState.register_dls dropped_disjuncts_count ~init:(fun () -> 0)

let get_dropped_disjuncts_count () = !dropped_disjuncts_count
let get_dropped_disjuncts_count () = Domain.DLS.get dropped_disjuncts_count

let set_dropped_disjuncts_count count = Domain.DLS.set dropped_disjuncts_count count
end

(** Returns a list of transitions whose pattern matches (e.g., event type matches). Each match
Expand Down Expand Up @@ -867,7 +869,7 @@ let apply_limits pulse_state state =
let old_len = List.length state in
let new_len = (Config.topl_max_disjuncts / 2) + 1 in
if Config.trace_topl then
Debug.dropped_disjuncts_count := !Debug.dropped_disjuncts_count + old_len - new_len ;
Debug.set_dropped_disjuncts_count (Debug.get_dropped_disjuncts_count () + old_len - new_len) ;
let add_score simple_state =
let score = Constraint.size simple_state.pruned in
if score > Config.topl_max_conjuncts then None else Some (score, simple_state)
Expand Down
8 changes: 4 additions & 4 deletions infer/src/pulse/PulseValueHistory.ml
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,13 @@ module CellId = struct

let pp = Int.pp

let next_id = ref 0
let next_id = Domain.DLS.new_key (fun () -> 0)

let () = AnalysisGlobalState.register_ref ~init:(fun () -> 0) next_id
let () = AnalysisGlobalState.register_dls ~init:(fun () -> 0) next_id

let next () =
let id = !next_id in
incr next_id ;
let id = Domain.DLS.get next_id in
Domain.DLS.set next_id (id + 1) ;
id


Expand Down

0 comments on commit a09bcd8

Please sign in to comment.