Skip to content

Commit

Permalink
[multicore][5/n] domain-local state
Browse files Browse the repository at this point in the history
Summary:
More global state moved to domain-local.
- AbsInt.AnalysisState
- More in Ondemand

Reviewed By: jvillard

Differential Revision:
D67013701

Privacy Context Container: L1208441

fbshipit-source-id: 2b01450d49cf995eadaa06a3d605902e1604adb7
  • Loading branch information
ngorogiannis authored and facebook-github-bot committed Dec 10, 2024
1 parent 1badf12 commit 2a1ff41
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 21 deletions.
33 changes: 19 additions & 14 deletions infer/src/absint/AnalysisState.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,40 +20,45 @@ type t =
let initial () = {last_instr= None; last_node= None; last_session= 0; remaining_disjuncts= None}

(** Global state *)
let gs = ref (initial ())
let gs = Domain.DLS.new_key initial

let () = AnalysisGlobalState.register_ref gs ~init:initial
let () = AnalysisGlobalState.register_dls gs ~init:initial

let get_instr () = !gs.last_instr
let get_instr () = (Domain.DLS.get gs).last_instr

let set_instr instr = !gs.last_instr <- Some instr
let set_instr instr = (Domain.DLS.get gs).last_instr <- Some instr

let get_node_exn () = Option.value_exn !gs.last_node
let get_node_exn () = Option.value_exn (Domain.DLS.get gs).last_node

let get_node () = !gs.last_node
let get_node () = (Domain.DLS.get gs).last_node

let set_node (node : Procdesc.Node.t) =
!gs.last_instr <- None ;
!gs.last_node <- Some node
let gs = Domain.DLS.get gs in
gs.last_instr <- None ;
gs.last_node <- Some node


let get_session () = !gs.last_session
let get_session () = (Domain.DLS.get gs).last_session

let set_session (session : int) = !gs.last_session <- session
let set_session (session : int) = (Domain.DLS.get gs).last_session <- session

let get_loc_exn () =
match !gs.last_instr with
match (Domain.DLS.get gs).last_instr with
| Some instr ->
Sil.location_of_instr instr
| None ->
get_node_exn () |> Procdesc.Node.get_loc


let get_loc () =
match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None
match (Domain.DLS.get gs).last_instr with
| Some instr ->
Some (Sil.location_of_instr instr)
| None ->
None


let get_remaining_disjuncts () = !gs.remaining_disjuncts
let get_remaining_disjuncts () = (Domain.DLS.get gs).remaining_disjuncts

let set_remaining_disjuncts remaining_disjuncts =
!gs.remaining_disjuncts <- Some remaining_disjuncts
(Domain.DLS.get gs).remaining_disjuncts <- Some remaining_disjuncts
17 changes: 10 additions & 7 deletions infer/src/backend/ondemand.ml
Original file line number Diff line number Diff line change
Expand Up @@ -45,31 +45,34 @@ end = struct

module AnalysisTargets = Hash_queue.Make (SpecializedProcname)

let currently_analyzed = AnalysisTargets.create ()
let currently_analyzed = Domain.DLS.new_key (fun () -> AnalysisTargets.create ())

let pp_actives fmt =
AnalysisTargets.iteri currently_analyzed ~f:(fun ~key:target ~data:_ ->
F.fprintf fmt "%a,@," SpecializedProcname.pp target )
Domain.DLS.get currently_analyzed
|> AnalysisTargets.iteri ~f:(fun ~key:target ~data:_ ->
F.fprintf fmt "%a,@," SpecializedProcname.pp target )


let mem analysis_target = AnalysisTargets.mem currently_analyzed analysis_target
let mem analysis_target = AnalysisTargets.mem (Domain.DLS.get currently_analyzed) analysis_target

let add analysis_target =
if Config.trace_ondemand then L.progress "add %a@." SpecializedProcname.pp analysis_target ;
AnalysisTargets.enqueue_back_exn currently_analyzed analysis_target ()
AnalysisTargets.enqueue_back_exn (Domain.DLS.get currently_analyzed) analysis_target ()


let remove analysis_target =
if Config.trace_ondemand then L.progress "remove %a@." SpecializedProcname.pp analysis_target ;
let popped_target, () = AnalysisTargets.dequeue_back_with_key_exn currently_analyzed in
let popped_target, () =
AnalysisTargets.dequeue_back_with_key_exn (Domain.DLS.get currently_analyzed)
in
if not (SpecializedProcname.equal popped_target analysis_target) then
L.die InternalError
"Queue structure for ondemand violated: expected to pop %a but got %a instead@\n\
Active procedures: %t@\n"
SpecializedProcname.pp analysis_target SpecializedProcname.pp popped_target pp_actives


let get_all () = AnalysisTargets.keys currently_analyzed
let get_all () = AnalysisTargets.keys @@ Domain.DLS.get currently_analyzed

let get_cycle_start recursive =
let all = get_all () in
Expand Down

0 comments on commit 2a1ff41

Please sign in to comment.