|
|
@ -9,8 +9,10 @@
|
|
|
|
open! IStd
|
|
|
|
open! IStd
|
|
|
|
module L = Logging
|
|
|
|
module L = Logging
|
|
|
|
|
|
|
|
|
|
|
|
(** add instructions to perform abstraction *)
|
|
|
|
(** add Abstract instructions into the IR to give hints about when abstraction should be
|
|
|
|
let add_abstraction_instructions pdesc =
|
|
|
|
performed *)
|
|
|
|
|
|
|
|
module AddAbstractionInstructions = struct
|
|
|
|
|
|
|
|
let process pdesc =
|
|
|
|
let open Procdesc in
|
|
|
|
let open Procdesc in
|
|
|
|
(* true if there is a succ node s.t.: it is an exit node, or the succ of >1 nodes *)
|
|
|
|
(* true if there is a succ node s.t.: it is an exit node, or the succ of >1 nodes *)
|
|
|
|
let converging_node node =
|
|
|
|
let converging_node node =
|
|
|
@ -32,14 +34,17 @@ let add_abstraction_instructions pdesc =
|
|
|
|
if node_requires_abstraction node then Node.append_instrs node [Sil.Metadata (Abstract loc)]
|
|
|
|
if node_requires_abstraction node then Node.append_instrs node [Sil.Metadata (Abstract loc)]
|
|
|
|
in
|
|
|
|
in
|
|
|
|
Procdesc.iter_nodes do_node pdesc
|
|
|
|
Procdesc.iter_nodes do_node pdesc
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** perform liveness analysis and insert Nullify/Remove_temps instructions into the IR to make it
|
|
|
|
module BackwardCfg = ProcCfg.Backward (ProcCfg.Exceptional)
|
|
|
|
easy for analyses to do abstract garbage collection *)
|
|
|
|
module LivenessAnalysis =
|
|
|
|
module Liveness = struct
|
|
|
|
|
|
|
|
module BackwardCfg = ProcCfg.Backward (ProcCfg.Exceptional)
|
|
|
|
|
|
|
|
module LivenessAnalysis =
|
|
|
|
AbstractInterpreter.MakeRPO (Liveness.PreAnalysisTransferFunctions (BackwardCfg))
|
|
|
|
AbstractInterpreter.MakeRPO (Liveness.PreAnalysisTransferFunctions (BackwardCfg))
|
|
|
|
module VarDomain = Liveness.Domain
|
|
|
|
module VarDomain = Liveness.Domain
|
|
|
|
|
|
|
|
|
|
|
|
(** computes the non-nullified reaching definitions at the end of each node by building on the
|
|
|
|
(** computes the non-nullified reaching definitions at the end of each node by building on the
|
|
|
|
results of a liveness analysis to be precise, what we want to compute is:
|
|
|
|
results of a liveness analysis to be precise, what we want to compute is:
|
|
|
|
|
|
|
|
|
|
|
|
to_nullify := (live_before U non_nullifed_reaching_defs) - live_after
|
|
|
|
to_nullify := (live_before U non_nullifed_reaching_defs) - live_after
|
|
|
@ -50,7 +55,7 @@ module VarDomain = Liveness.Domain
|
|
|
|
after the fact, nor can it be done with liveness alone. We will insert nullify instructions for
|
|
|
|
after the fact, nor can it be done with liveness alone. We will insert nullify instructions for
|
|
|
|
each pvar in to_nullify afer we finish the analysis. Nullify instructions speed up the analysis
|
|
|
|
each pvar in to_nullify afer we finish the analysis. Nullify instructions speed up the analysis
|
|
|
|
by enabling it to GC state that will no longer be read. *)
|
|
|
|
by enabling it to GC state that will no longer be read. *)
|
|
|
|
module NullifyTransferFunctions = struct
|
|
|
|
module NullifyTransferFunctions = struct
|
|
|
|
module Domain = AbstractDomain.Pair (VarDomain) (VarDomain)
|
|
|
|
module Domain = AbstractDomain.Pair (VarDomain) (VarDomain)
|
|
|
|
(** (reaching non-nullified vars) * (vars to nullify) *)
|
|
|
|
(** (reaching non-nullified vars) * (vars to nullify) *)
|
|
|
|
|
|
|
|
|
|
|
@ -119,11 +124,11 @@ module NullifyTransferFunctions = struct
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp_session_name _node fmt = Format.pp_print_string fmt "nullify"
|
|
|
|
let pp_session_name _node fmt = Format.pp_print_string fmt "nullify"
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
module NullifyAnalysis = AbstractInterpreter.MakeRPO (NullifyTransferFunctions)
|
|
|
|
module NullifyAnalysis = AbstractInterpreter.MakeRPO (NullifyTransferFunctions)
|
|
|
|
|
|
|
|
|
|
|
|
let add_nullify_instrs summary tenv liveness_inv_map =
|
|
|
|
let add_nullify_instrs summary tenv liveness_inv_map =
|
|
|
|
let address_taken_vars =
|
|
|
|
let address_taken_vars =
|
|
|
|
if Typ.Procname.is_java (Summary.get_proc_name summary) then AddressTaken.Domain.empty
|
|
|
|
if Typ.Procname.is_java (Summary.get_proc_name summary) then AddressTaken.Domain.empty
|
|
|
|
(* can't take the address of a variable in Java *)
|
|
|
|
(* can't take the address of a variable in Java *)
|
|
|
@ -183,36 +188,34 @@ let add_nullify_instrs summary tenv liveness_inv_map =
|
|
|
|
if not (AddressTaken.Domain.is_empty address_taken_vars) then
|
|
|
|
if not (AddressTaken.Domain.is_empty address_taken_vars) then
|
|
|
|
let exit_node = ProcCfg.Exceptional.exit_node nullify_proc_cfg in
|
|
|
|
let exit_node = ProcCfg.Exceptional.exit_node nullify_proc_cfg in
|
|
|
|
let exit_loc = Procdesc.Node.get_last_loc exit_node in
|
|
|
|
let exit_loc = Procdesc.Node.get_last_loc exit_node in
|
|
|
|
prepend_node_nullify_instructions exit_loc (AddressTaken.Domain.elements address_taken_vars) []
|
|
|
|
prepend_node_nullify_instructions exit_loc
|
|
|
|
|
|
|
|
(AddressTaken.Domain.elements address_taken_vars)
|
|
|
|
|
|
|
|
[]
|
|
|
|
|> Procdesc.Node.append_instrs exit_node
|
|
|
|
|> Procdesc.Node.append_instrs exit_node
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** perform liveness analysis and insert Nullify/Remove_temps instructions into the IR to make it
|
|
|
|
let process summary tenv =
|
|
|
|
easy for analyses to do abstract garbage collection *)
|
|
|
|
|
|
|
|
let do_liveness summary tenv =
|
|
|
|
|
|
|
|
let liveness_proc_cfg = BackwardCfg.from_pdesc (Summary.get_proc_desc summary) in
|
|
|
|
let liveness_proc_cfg = BackwardCfg.from_pdesc (Summary.get_proc_desc summary) in
|
|
|
|
let initial = Liveness.Domain.empty in
|
|
|
|
let initial = Liveness.Domain.empty in
|
|
|
|
let liveness_inv_map =
|
|
|
|
let liveness_inv_map =
|
|
|
|
LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default summary tenv) ~initial
|
|
|
|
LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default summary tenv) ~initial
|
|
|
|
in
|
|
|
|
in
|
|
|
|
add_nullify_instrs summary tenv liveness_inv_map
|
|
|
|
add_nullify_instrs summary tenv liveness_inv_map
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module FunctionPointerSubstitution = struct
|
|
|
|
(** add Abstract instructions into the IR to give hints about when abstraction should be
|
|
|
|
let process summary tenv =
|
|
|
|
performed *)
|
|
|
|
|
|
|
|
let do_abstraction pdesc = add_abstraction_instructions pdesc
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let do_funptr_sub summary tenv =
|
|
|
|
|
|
|
|
let updated = FunctionPointers.substitute_function_pointers summary tenv in
|
|
|
|
let updated = FunctionPointers.substitute_function_pointers summary tenv in
|
|
|
|
let pdesc = Summary.get_proc_desc summary in
|
|
|
|
let pdesc = Summary.get_proc_desc summary in
|
|
|
|
if updated then Attributes.store ~proc_desc:(Some pdesc) (Procdesc.get_attributes pdesc)
|
|
|
|
if updated then Attributes.store ~proc_desc:(Some pdesc) (Procdesc.get_attributes pdesc)
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
let do_preanalysis pdesc tenv =
|
|
|
|
let do_preanalysis pdesc tenv =
|
|
|
|
let summary = Summary.OnDisk.reset pdesc in
|
|
|
|
let summary = Summary.OnDisk.reset pdesc in
|
|
|
|
if
|
|
|
|
if
|
|
|
|
Config.function_pointer_specialization
|
|
|
|
Config.function_pointer_specialization
|
|
|
|
&& not (Typ.Procname.is_java (Procdesc.get_proc_name pdesc))
|
|
|
|
&& not (Typ.Procname.is_java (Procdesc.get_proc_name pdesc))
|
|
|
|
then do_funptr_sub summary tenv ;
|
|
|
|
then FunctionPointerSubstitution.process summary tenv ;
|
|
|
|
do_liveness summary tenv ;
|
|
|
|
Liveness.process summary tenv ;
|
|
|
|
do_abstraction pdesc
|
|
|
|
AddAbstractionInstructions.process pdesc ;
|
|
|
|
|
|
|
|
()
|
|
|
|