pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[cost] Simplify & optimize NodesBasicCost

Browse Source 
Summary:
`AnalyzerNodesBasicCost` is just mapping instructions to abstract costs, it doesn't need to use AI.
Also it was keeping a map (node -> cost) for each node, this is completely removed.

Depends on D14028171

Reviewed By: ddino

Differential Revision: D14028249

fbshipit-source-id: 63f39261a
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 17fc4ca5cf
commit 7c688583e0
3 changed files with 162 additions and 193 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/absint/AbstractDomain.mli
Unescape View File

@ -127,11 +127,16 @@ module type MapS = sig
include WithBottom with type t := t include WithBottom with type t := t
end end
(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. include
sig
[@@@warning "-60"]
(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
Every element implicitly maps to bottom unless it is explicitly bound to something else. Every element implicitly maps to bottom unless it is explicitly bound to something else.
Uses PPMap as the underlying map *) Uses PPMap as the underlying map *)
module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) : module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) :
MapS with type key = PPMap.key and type value = ValueDomain.t MapS with type key = PPMap.key and type value = ValueDomain.t
end
(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map. (** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
Every element implicitly maps to bottom unless it is explicitly bound to something else *) Every element implicitly maps to bottom unless it is explicitly bound to something else *)

238
infer/src/checkers/cost.ml
Unescape View File

@ -9,7 +9,6 @@ open! IStd
module F = Format module F = Format
module L = Logging module L = Logging
module BasicCost = CostDomain.BasicCost module BasicCost = CostDomain.BasicCost
module NodesBasicCostDomain = CostDomain.NodeInstructionToCostMap
module Payload = SummaryPayload.Make (struct module Payload = SummaryPayload.Make (struct
type t = CostDomain.summary type t = CostDomain.summary
@ -28,106 +27,6 @@ module InstrCFG = ProcCfg.NormalOneInstrPerNode
module NodeCFG = ProcCfg.Normal module NodeCFG = ProcCfg.Normal
module Node = ProcCfg.DefaultNode module Node = ProcCfg.DefaultNode
(* Compute a map (node,instruction) -> basic_cost, where basic_cost is the
cost known for a certain operation. For example for basic operation we
set it to 1 and for function call we take it from the spec of the function.
The nodes in the domain of the map are those in the path reaching the current node.
*)
let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
match Ondemand.get_proc_desc callee_pname with
| None ->
L.(die InternalError)
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp
callee_cost Typ.Procname.pp callee_pname
| Some callee_pdesc ->
let callee_formals = Procdesc.get_pvar_formals callee_pdesc in
let eval_sym =
BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_formals params
inferbo_caller_mem
in
BasicCost.subst callee_cost eval_sym
module TransferFunctionsNodesBasicCost = struct
module CFG = InstrCFG
module Domain = NodesBasicCostDomain
type extras =
{ inferbo_invariant_map: BufferOverrunAnalysis.invariant_map
; integer_type_widths: Typ.IntegerWidths.t }
let callee_OperationCost callee_cost_record integer_type_widths inferbo_mem callee_pname params =
let callee_cost = CostDomain.get_operation_cost callee_cost_record in
if BasicCost.is_symbolic callee_cost then
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params
~callee_cost
else callee_cost
let callee_AllocationCost cost_record = CostDomain.get_allocation_cost cost_record
let callee_IOCost cost_record = CostDomain.get_IO_cost cost_record
let exec_instr_cost integer_type_widths inferbo_mem
(astate : CostDomain.NodeInstructionToCostMap.t) {ProcData.pdesc} (node : CFG.Node.t) instr :
CostDomain.NodeInstructionToCostMap.t =
let key = CFG.Node.id node in
let astate' =
match instr with
| Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) ->
let callee_cost =
match CostModels.Call.dispatch () callee_pname params with
| Some model ->
CostDomain.set_operation_cost (model inferbo_mem) CostDomain.zero_record
| None -> (
match Payload.read pdesc callee_pname with
| Some {post= callee_cost_record} ->
let callee_operation_cost =
callee_OperationCost callee_cost_record integer_type_widths inferbo_mem
callee_pname params
in
let callee_allocation_cost = callee_AllocationCost callee_cost_record in
let callee_IO_cost = callee_IOCost callee_cost_record in
CostDomain.mk_cost_record ~operation_cost:callee_operation_cost
~allocation_cost:callee_allocation_cost ~io_cost:callee_IO_cost
| None ->
CostDomain.unit_cost_atomic_operation )
in
CostDomain.NodeInstructionToCostMap.add key callee_cost astate
| Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ ->
CostDomain.NodeInstructionToCostMap.add key CostDomain.unit_cost_atomic_operation astate
| Sil.ExitScope _ -> (
match CFG.Node.kind node with
| Procdesc.Node.Start_node ->
CostDomain.NodeInstructionToCostMap.add key CostDomain.unit_cost_atomic_operation
astate
| _ ->
astate )
| _ ->
astate
in
L.(debug Analysis Medium)
"@\n>>>Instr: %a Cost: %a@\n"
(Sil.pp_instr ~print_types:false Pp.text)
instr CostDomain.NodeInstructionToCostMap.pp astate' ;
astate'
let exec_instr costmap ({ProcData.extras= {inferbo_invariant_map; integer_type_widths}} as pdata)
node instr =
let inferbo_mem =
Option.value_exn (BufferOverrunAnalysis.extract_pre (CFG.Node.id node) inferbo_invariant_map)
in
let costmap = exec_instr_cost integer_type_widths inferbo_mem costmap pdata node instr in
costmap
let pp_session_name node fmt = F.fprintf fmt "cost(basic) %a" CFG.Node.pp_id (CFG.Node.id node)
end
module AnalyzerNodesBasicCost = AbstractInterpreter.MakeRPO (TransferFunctionsNodesBasicCost)
(* Map associating to each node a bound on the number of times it can be executed. (* Map associating to each node a bound on the number of times it can be executed.
This bound is computed using environments (map: val -> values), using the following This bound is computed using environments (map: val -> values), using the following
observation: the number of environments associated with a program point is an upperbound observation: the number of environments associated with a program point is an upperbound
@ -615,10 +514,96 @@ module ConstraintSolver = struct
end end
type extras_WCET = type extras_WCET =
{ basic_cost_map: NodesBasicCostDomain.t { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map
; integer_type_widths: Typ.IntegerWidths.t
; get_node_nb_exec: Node.id -> BasicCost.t ; get_node_nb_exec: Node.id -> BasicCost.t
; summary: Summary.t } ; summary: Summary.t }
let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
match Ondemand.get_proc_desc callee_pname with
| None ->
L.(die InternalError)
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp
callee_cost Typ.Procname.pp callee_pname
| Some callee_pdesc ->
let callee_formals = Procdesc.get_pvar_formals callee_pdesc in
let eval_sym =
BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_formals params
inferbo_caller_mem
in
BasicCost.subst callee_cost eval_sym
module InstrBasicCost = struct
(*
Compute the cost for an instruction.
For example for basic operation we set it to 1 and for function call we take it from the spec of the function.
*)
let callee_OperationCost callee_cost_record integer_type_widths inferbo_mem callee_pname params =
let callee_cost = CostDomain.get_operation_cost callee_cost_record in
if BasicCost.is_symbolic callee_cost then
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params
~callee_cost
else callee_cost
let callee_AllocationCost cost_record = CostDomain.get_allocation_cost cost_record
let callee_IOCost cost_record = CostDomain.get_IO_cost cost_record
let get_instr_cost_record pdata instr_node instr =
match instr with
| Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> (
let ProcData.({pdesc; extras= {inferbo_invariant_map; integer_type_widths}}) = pdata in
match
BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map
with
| None ->
CostDomain.unit_cost_atomic_operation
| Some inferbo_mem -> (
match CostModels.Call.dispatch () callee_pname params with
| Some model ->
CostDomain.set_operation_cost (model inferbo_mem) CostDomain.zero_record
| None -> (
match Payload.read pdesc callee_pname with
| Some {post= callee_cost_record} ->
let callee_operation_cost =
callee_OperationCost callee_cost_record integer_type_widths inferbo_mem
callee_pname params
in
let callee_allocation_cost = callee_AllocationCost callee_cost_record in
let callee_IO_cost = callee_IOCost callee_cost_record in
CostDomain.mk_cost_record ~operation_cost:callee_operation_cost
~allocation_cost:callee_allocation_cost ~io_cost:callee_IO_cost
| None ->
CostDomain.unit_cost_atomic_operation ) ) )
| Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ ->
CostDomain.unit_cost_atomic_operation
| Sil.ExitScope _ -> (
match InstrCFG.Node.kind instr_node with
| Procdesc.Node.Start_node ->
CostDomain.unit_cost_atomic_operation
| _ ->
CostDomain.zero_record )
| _ ->
CostDomain.zero_record
let get_instr_node_cost_record pdata instr_node =
let instrs = InstrCFG.instrs instr_node in
let instr =
match IContainer.singleton_or_more instrs ~fold:Instrs.fold with
| Empty ->
Sil.skip_instr
| Singleton instr ->
instr
| More ->
assert false
in
get_instr_cost_record pdata instr_node instr
end
let compute_errlog_extras cost = let compute_errlog_extras cost =
{ Jsonbug_t.cost_polynomial= Some (Format.asprintf "%a" BasicCost.pp cost) { Jsonbug_t.cost_polynomial= Some (Format.asprintf "%a" BasicCost.pp cost)
; cost_degree= BasicCost.degree cost |> Option.map ~f:Polynomials.Degree.encode_to_int } ; cost_degree= BasicCost.degree cost |> Option.map ~f:Polynomials.Degree.encode_to_int }
@ -661,13 +646,10 @@ module WCET = struct
(not (BasicCost.is_top cost)) && not (BasicCost.( <= ) ~lhs:cost ~rhs:expensive_threshold) (not (BasicCost.is_top cost)) && not (BasicCost.( <= ) ~lhs:cost ~rhs:expensive_threshold)
let exec_node {current_cost; report_on_threshold} {basic_cost_map; get_node_nb_exec; summary} let exec_node {current_cost; report_on_threshold} pdata instr_node =
instr_node = let {ProcData.extras= {get_node_nb_exec; summary}} = pdata in
let node_cost = let node_cost =
match NodesBasicCostDomain.find_opt (InstrCFG.Node.id instr_node) basic_cost_map with let instr_cost_record = InstrBasicCost.get_instr_node_cost_record pdata instr_node in
| None ->
BasicCost.zero
| Some instr_cost_record ->
let instr_cost = CostDomain.get_operation_cost instr_cost_record in let instr_cost = CostDomain.get_operation_cost instr_cost_record in
let node_id = InstrCFG.Node.underlying_node instr_node |> Node.id in let node_id = InstrCFG.Node.underlying_node instr_node |> Node.id in
let nb_exec = get_node_nb_exec node_id in let nb_exec = get_node_nb_exec node_id in
@ -683,29 +665,28 @@ module WCET = struct
{current_cost; report_on_threshold} {current_cost; report_on_threshold}
let rec exec_partition astate extras let rec exec_partition astate pdata
(partition : InstrCFG.Node.t WeakTopologicalOrder.Partition.t) = (partition : InstrCFG.Node.t WeakTopologicalOrder.Partition.t) =
match partition with match partition with
| Empty -> | Empty ->
astate astate
| Node {node; next} -> | Node {node; next} ->
let astate = exec_node astate extras node in let astate = exec_node astate pdata node in
exec_partition astate extras next exec_partition astate pdata next
| Component {head; rest; next} -> | Component {head; rest; next} ->
let {current_cost; report_on_threshold} = astate in let {current_cost; report_on_threshold} = astate in
let {current_cost} = let {current_cost} =
exec_partition {current_cost; report_on_threshold= false} extras rest exec_partition {current_cost; report_on_threshold= false} pdata rest
in in
(* Execute head after the loop body to always report at loop head *) (* Execute head after the loop body to always report at loop head *)
let astate = exec_node {current_cost; report_on_threshold} extras head in let astate = exec_node {current_cost; report_on_threshold} pdata head in
exec_partition astate extras next exec_partition astate pdata next
let compute pdata = let compute pdata =
let ProcData.({pdesc; extras}) = pdata in let cfg = InstrCFG.from_pdesc pdata.ProcData.pdesc in
let cfg = InstrCFG.from_pdesc pdesc in
let initial = {current_cost= BasicCost.zero; report_on_threshold= Config.use_cost_threshold} in let initial = {current_cost= BasicCost.zero; report_on_threshold= Config.use_cost_threshold} in
let {current_cost} = exec_partition initial extras (InstrCFG.wto cfg) in let {current_cost} = exec_partition initial pdata (InstrCFG.wto cfg) in
CostDomain.mk_cost_record ~operation_cost:current_cost ~allocation_cost:BasicCost.zero CostDomain.mk_cost_record ~operation_cost:current_cost ~allocation_cost:BasicCost.zero
~io_cost:BasicCost.zero ~io_cost:BasicCost.zero
end end
@ -729,16 +710,6 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
let inferbo_invariant_map = let inferbo_invariant_map =
BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths
in in
let basic_cost_map_opt =
let proc_data =
ProcData.make proc_desc tenv
TransferFunctionsNodesBasicCost.{inferbo_invariant_map; integer_type_widths}
in
(*compute_WCET cfg invariant_map min_trees in *)
AnalyzerNodesBasicCost.compute_post proc_data ~initial:NodesBasicCostDomain.empty
in
match basic_cost_map_opt with
| Some basic_cost_map ->
let node_cfg = NodeCFG.from_pdesc proc_desc in let node_cfg = NodeCFG.from_pdesc proc_desc in
(* computes reaching defs: node -> (var -> node set) *) (* computes reaching defs: node -> (var -> node set) *)
let reaching_defs_invariant_map = let reaching_defs_invariant_map =
@ -781,8 +752,11 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
ConstraintSolver.get_node_nb_exec equalities ConstraintSolver.get_node_nb_exec equalities
in in
let exit_cost_record = let exit_cost_record =
let proc_data = ProcData.make proc_desc tenv {basic_cost_map; get_node_nb_exec; summary} in let pdata =
WCET.compute proc_data ProcData.make proc_desc tenv
{inferbo_invariant_map; integer_type_widths; get_node_nb_exec; summary}
in
WCET.compute pdata
in in
L.(debug Analysis Verbose) L.(debug Analysis Verbose)
"@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" Typ.Procname.pp "@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" Typ.Procname.pp
@ -791,9 +765,3 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
CostDomain.VariantCostMap.pp exit_cost_record ; CostDomain.VariantCostMap.pp exit_cost_record ;
check_and_report_top_and_bottom exit_cost_record proc_desc summary ; check_and_report_top_and_bottom exit_cost_record proc_desc summary ;
Payload.update_summary {post= exit_cost_record} summary Payload.update_summary {post= exit_cost_record} summary
| None ->
if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
L.internal_error "Failed to compute final cost for function %a" Typ.Procname.pp
(Procdesc.get_proc_name proc_desc) ;
summary )
else summary

4
infer/src/checkers/costDomain.ml
Unescape View File

@ -51,10 +51,6 @@ type summary = {post: VariantCostMap.t}
let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" VariantCostMap.pp post let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" VariantCostMap.pp post
(** Map (node,instr) -> basic cost *)
module NodeInstructionToCostMap =
AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (VariantCostMap)
let get_cost_kind kind cost_record = let get_cost_kind kind cost_record =
try VariantCostMap.find kind cost_record with _ -> try VariantCostMap.find kind cost_record with _ ->
Logging.(die InternalError) Logging.(die InternalError)

Write Preview
Loading…
Cancel
Save