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

[cost] Make it more Kind-generic

Browse Source 
Reviewed By: ezgicicek

Differential Revision: D14030111

fbshipit-source-id: 27bc58731
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent cab28a9461
commit 023d608530
3 changed files with 175 additions and 140 deletions
Show Stats Download Patch File Download Diff File

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

@ -127,16 +127,11 @@ module type MapS = sig
include WithBottom with type t := t
end
include
sig
[@@@warning "-60"]
(** 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.
Uses PPMap as the underlying map *)
module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) :
MapS with type key = PPMap.key and type value = ValueDomain.t
end
module MapOfPPMap (PPMap : PrettyPrintable.PPMap) (ValueDomain : S) :
MapS with type key = PPMap.key and type value = ValueDomain.t and type t = ValueDomain.t PPMap.t
(** 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 *)

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

@ -18,9 +18,24 @@ module Payload = SummaryPayload.Make (struct
let of_payloads (payloads : Payloads.t) = payloads.cost
end)
(* We use this treshold to give error if the cost is above it.
(* We use this threshold to give error if the cost is above it.
Currently it's set randomly to 200. *)
let expensive_threshold = BasicCost.of_int_exn 200
module ReportConfig = struct
type t = {name: string; threshold: int option; top_and_bottom: bool}
let as_list =
[ ( CostDomain.OperationCost
, { name= "The execution time"
; threshold= Option.some_if Config.use_cost_threshold 200
; top_and_bottom= true } )
; (CostDomain.AllocationCost, {name= "The allocations"; threshold= None; top_and_bottom= false})
; (CostDomain.IOCost, {name= "The IOs"; threshold= None; top_and_bottom= false}) ]
let as_map =
List.fold as_list ~init:CostDomain.CostKindMap.empty ~f:(fun acc (k, v) ->
CostDomain.CostKindMap.add k v acc )
end
(* CFG modules used in several other modules *)
module InstrCFG = ProcCfg.NormalOneInstrPerNode
@ -514,7 +529,7 @@ module ConstraintSolver = struct
Option.value_exn set |> ControlFlowCost.Set.cost
end
type extras_WCET =
type extras_WorstCaseCost =
{ inferbo_invariant_map: BufferOverrunAnalysis.invariant_map
; integer_type_widths: Typ.IntegerWidths.t
; get_node_nb_exec: Node.id -> BasicCost.t }
@ -533,19 +548,6 @@ module InstrBasicCost = struct
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
callee_formals params loc =
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
~callee_formals ~params ~callee_cost ~loc
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_callee_summary caller_pdesc callee_pname =
Ondemand.analyze_proc_name ~caller_pdesc callee_pname
|> Option.bind ~f:(fun summary ->
@ -557,7 +559,6 @@ module InstrBasicCost = struct
let get_instr_cost_record pdata instr_node instr =
match instr with
| Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> (
let loc = InstrCFG.Node.loc instr_node in
let ProcData.({pdesc; extras= {inferbo_invariant_map; integer_type_widths}}) = pdata in
match
BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map
@ -565,22 +566,20 @@ module InstrBasicCost = struct
| None ->
CostDomain.unit_cost_atomic_operation
| Some inferbo_mem -> (
match CostModels.Call.dispatch () callee_pname params with
| Some model ->
CostDomain.set_operation_cost (model loc inferbo_mem) CostDomain.zero_record
| None -> (
match get_callee_summary pdesc callee_pname with
| Some ({CostDomain.post= callee_cost_record}, callee_formals) ->
let callee_operation_cost =
callee_OperationCost callee_cost_record integer_type_widths inferbo_mem
callee_pname callee_formals params loc
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 ) ) )
let loc = InstrCFG.Node.loc instr_node in
match CostModels.Call.dispatch () callee_pname params with
| Some model ->
CostDomain.of_operation_cost (model loc inferbo_mem)
| None -> (
match get_callee_summary pdesc callee_pname with
| Some ({CostDomain.post= callee_cost_record}, callee_formals) ->
CostDomain.map callee_cost_record ~f:(fun callee_cost ->
if BasicCost.is_symbolic callee_cost then
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
~callee_pname ~callee_formals ~params ~callee_cost ~loc
else callee_cost )
| None ->
CostDomain.unit_cost_atomic_operation ) ) )
| Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ ->
CostDomain.unit_cost_atomic_operation
| Sil.ExitScope _ -> (
@ -612,68 +611,61 @@ let compute_errlog_extras cost =
; cost_degree= BasicCost.degree cost |> Option.map ~f:Polynomials.Degree.encode_to_int }
(*
Calculate the final Worst Case Execution Time predicted for each WTO component.
It is the dot product of basic_cost_map and get_node_nb_exec.
*)
module WCET = struct
type report = DontCheck | PleaseCheck | ReportOn of {location: Location.t; cost: BasicCost.t}
module ThresholdReports = struct
type threshold_or_report =
| Threshold of BasicCost.t
| ReportOn of {location: Location.t; cost: BasicCost.t}
type astate = {current_cost: BasicCost.t; report_on_threshold: report}
type t = threshold_or_report CostDomain.CostKindMap.t
let do_report summary loc cost =
let degree_str =
match BasicCost.degree cost with
| Some degree ->
Format.asprintf ", degree = %a" Polynomials.Degree.pp degree
| None ->
""
in
let message =
F.asprintf
"The execution time from the beginning of the function up to this program point is likely \
above the acceptable threshold of %a (estimated cost %a%s)"
BasicCost.pp expensive_threshold BasicCost.pp cost degree_str
in
let cost_trace =
let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp cost degree_str in
Errlog.make_trace_element 0 loc cost_desc []
in
let full_trace =
BasicCost.get_symbols cost
|> List.map ~f:Bounds.NonNegativeBound.make_err_trace
|> Errlog.concat_traces
in
Reporting.log_error summary ~loc ~ltr:(cost_trace :: full_trace)
~extras:(compute_errlog_extras cost) IssueType.expensive_execution_time_call message
let none = CostDomain.CostKindMap.empty
let config =
List.fold ReportConfig.as_list ~init:none ~f:(fun acc -> function
| k, ReportConfig.({threshold= Some threshold}) ->
CostDomain.CostKindMap.add k (Threshold (BasicCost.of_int_exn threshold)) acc
| _ ->
acc )
end
(*
Calculate the final Worst Case Cost predicted for each cost field and each WTO component.
It is the dot product of basic_cost_map and get_node_nb_exec.
*)
module WorstCaseCost = struct
type astate = {costs: CostDomain.t; reports: ThresholdReports.t}
(*
We don't report when the cost is Top as it corresponds to subsequent 'don't know's.
Instead, we report Top cost only at the top level per function when `report_infinity` is set to true
*)
let should_report_cost cost =
(not (BasicCost.is_top cost)) && not (BasicCost.( <= ) ~lhs:cost ~rhs:expensive_threshold)
let should_report_cost cost ~threshold =
(not (BasicCost.is_top cost)) && not (BasicCost.( <= ) ~lhs:cost ~rhs:threshold)
let exec_node {current_cost; report_on_threshold} pdata instr_node =
let exec_node {costs; reports} pdata instr_node =
let {ProcData.extras= {get_node_nb_exec}} = pdata in
let node_cost =
let instr_cost_record = InstrBasicCost.get_instr_node_cost_record pdata instr_node 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 nb_exec = get_node_nb_exec node_id in
BasicCost.mult instr_cost nb_exec
CostDomain.mult_by_scalar instr_cost_record nb_exec
in
let current_cost = BasicCost.plus current_cost node_cost in
let report_on_threshold =
match report_on_threshold with
| PleaseCheck when should_report_cost current_cost ->
ReportOn {location= InstrCFG.Node.loc instr_node; cost= current_cost}
| _ ->
report_on_threshold
let costs = CostDomain.plus costs node_cost in
let reports =
CostDomain.CostKindMap.merge
(fun _kind threshold_or_report_opt cost_opt ->
match (threshold_or_report_opt, cost_opt) with
| None, _ ->
None
| Some (ThresholdReports.Threshold threshold), Some cost
when should_report_cost cost ~threshold ->
Some (ThresholdReports.ReportOn {location= InstrCFG.Node.loc instr_node; cost})
| _ ->
threshold_or_report_opt )
reports costs
in
{current_cost; report_on_threshold}
{costs; reports}
let rec exec_partition astate pdata
@ -685,39 +677,73 @@ module WCET = struct
let astate = exec_node astate pdata node in
exec_partition astate pdata next
| Component {head; rest; next} ->
let {current_cost; report_on_threshold} = astate in
let {current_cost} =
exec_partition {current_cost; report_on_threshold= DontCheck} pdata rest
in
let {costs; reports} = astate in
let {costs} = exec_partition {costs; reports= ThresholdReports.none} pdata rest in
(* Execute head after the loop body to always report at loop head *)
let astate = exec_node {current_cost; report_on_threshold} pdata head in
let astate = exec_node {costs; reports} pdata head in
exec_partition astate pdata next
let compute pdata =
let cfg = InstrCFG.from_pdesc pdata.ProcData.pdesc in
let report_on_threshold = if Config.use_cost_threshold then PleaseCheck else DontCheck in
let initial = {current_cost= BasicCost.zero; report_on_threshold} in
let {current_cost; report_on_threshold} = exec_partition initial pdata (InstrCFG.wto cfg) in
( CostDomain.mk_cost_record ~operation_cost:current_cost ~allocation_cost:BasicCost.zero
~io_cost:BasicCost.zero
, report_on_threshold )
let initial = {costs= CostDomain.zero_record; reports= ThresholdReports.config} in
exec_partition initial pdata (InstrCFG.wto cfg)
end
let check_and_report_top_and_bottom cost_record proc_desc summary =
let cost = CostDomain.get_operation_cost cost_record in
let report issue suffix =
module Check = struct
let report_threshold summary ~name ~location ~cost ~threshold =
let degree_str =
match BasicCost.degree cost with
| Some degree ->
Format.asprintf ", degree = %a" Polynomials.Degree.pp degree
| None ->
""
in
let message =
F.asprintf "The execution time of the function %a %s" Typ.Procname.pp
(Procdesc.get_proc_name proc_desc)
suffix
F.asprintf
"%s from the beginning of the function up to this program point is likely above the \
acceptable threshold of %d (estimated cost %a%s)"
name threshold BasicCost.pp cost degree_str
in
let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in
Reporting.log_error ~loc ~extras:(compute_errlog_extras cost) summary issue message
in
if BasicCost.is_top cost then report IssueType.infinite_execution_time_call "cannot be computed"
else if BasicCost.is_zero cost then report IssueType.zero_execution_time_call "is zero"
let cost_trace =
let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp cost degree_str in
Errlog.make_trace_element 0 location cost_desc []
in
let full_trace =
BasicCost.get_symbols cost
|> List.map ~f:Bounds.NonNegativeBound.make_err_trace
|> Errlog.concat_traces
in
Reporting.log_error summary ~loc:location ~ltr:(cost_trace :: full_trace)
~extras:(compute_errlog_extras cost) IssueType.expensive_execution_time_call message
let report_top_and_bottom proc_desc summary ~name ~cost =
let report issue suffix =
let message =
F.asprintf "%s of the function %a %s" name Typ.Procname.pp
(Procdesc.get_proc_name proc_desc)
suffix
in
let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in
Reporting.log_error ~loc ~extras:(compute_errlog_extras cost) summary issue message
in
if BasicCost.is_top cost then
report IssueType.infinite_execution_time_call "cannot be computed"
else if BasicCost.is_zero cost then report IssueType.zero_execution_time_call "is zero"
let check_and_report WorstCaseCost.({costs; reports}) proc_desc summary =
CostDomain.CostKindMap.iter2 ReportConfig.as_map reports
~f:(fun _kind ReportConfig.({name; threshold}) -> function
| ThresholdReports.Threshold _ ->
()
| ThresholdReports.ReportOn {location; cost} ->
report_threshold summary ~name ~location ~cost ~threshold:(Option.value_exn threshold) ) ;
CostDomain.CostKindMap.iter2 ReportConfig.as_map costs
~f:(fun _kind ReportConfig.({name; top_and_bottom}) cost ->
if top_and_bottom then report_top_and_bottom proc_desc summary ~name ~cost )
end
let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.t =
let inferbo_invariant_map =
@ -764,17 +790,17 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
if Config.write_html then NodePrinter.finish_session start_node ;
ConstraintSolver.get_node_nb_exec equalities
in
let exit_cost_record, report =
let astate =
let pdata =
ProcData.make proc_desc tenv {inferbo_invariant_map; integer_type_widths; get_node_nb_exec}
in
WCET.compute pdata
WorstCaseCost.compute pdata
in
let exit_cost_record = astate.WorstCaseCost.costs in
L.(debug Analysis Verbose)
"@\n[COST ANALYSIS] PROCEDURE '%a' |CFG| = %i FINAL COST = %a @\n" Typ.Procname.pp
(Procdesc.get_proc_name proc_desc)
(Container.length ~fold:NodeCFG.fold_nodes node_cfg)
CostDomain.VariantCostMap.pp exit_cost_record ;
(match report with ReportOn {location; cost} -> WCET.do_report summary location cost | _ -> ()) ;
check_and_report_top_and_bottom exit_cost_record proc_desc summary ;
Check.check_and_report astate proc_desc summary ;
Payload.update_summary {post= exit_cost_record} summary

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

@ -27,56 +27,70 @@ module CostKind : PrettyPrintable.PrintableOrderedType with type t = cost_kind =
F.pp_print_string f k_str
end
(* Module to simulate a record
module CostKindMap = struct
include PrettyPrintable.MakePPMap (CostKind)
type no_value = |
let iter2 map1 map2 ~f =
let _ : no_value t =
merge
(fun k v1_opt v2_opt ->
(match (v1_opt, v2_opt) with Some v1, Some v2 -> f k v1 v2 | _ -> ()) ;
None )
map1 map2
in
()
end
(**
Module to simulate a record
{OperationCost:BasicCost.t; AllocationCost: BasicCost.t; IOCost:BasicCost.t} with a map
{OperationCost, AllocationCost, IOCost} -> BasicCost.t
*)
module VariantCostMap = struct
include AbstractDomain.Map (CostKind) (BasicCost)
let replace k v map = add k v map
include AbstractDomain.MapOfPPMap (CostKindMap) (BasicCost)
let[@warning "-32"] add _ = Logging.die InternalError "Don't call me"
let increase_by kind basic_cost record =
let existing = match find_opt kind record with Some c -> c | None -> BasicCost.zero in
replace kind (BasicCost.plus basic_cost existing) record
let get kind record = find_opt kind record |> Option.value ~default:BasicCost.zero
let increase_by kind cost_to_add record =
update kind
(function
| None -> Some cost_to_add | Some existing -> Some (BasicCost.plus cost_to_add existing))
record
let[@warning "-32"] increment kind record = increase_by kind BasicCost.one record
let increment kind record = increase_by kind BasicCost.one record
end
type summary = {post: VariantCostMap.t}
type t = VariantCostMap.t
let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" VariantCostMap.pp post
type summary = {post: t}
let get_cost_kind kind cost_record =
try VariantCostMap.find kind cost_record with _ ->
Logging.(die InternalError)
"Can't find %a for Cost Record %a" CostKind.pp kind VariantCostMap.pp cost_record
let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" VariantCostMap.pp post
let get_cost_kind kind cost_record = VariantCostMap.get kind cost_record
let get_operation_cost cost_record = get_cost_kind OperationCost cost_record
let get_allocation_cost cost_record = get_cost_kind AllocationCost cost_record
let get_IO_cost cost_record = get_cost_kind IOCost cost_record
let map ~f cost_record = VariantCostMap.map f cost_record
let mk_cost_record ~operation_cost:oc ~allocation_cost:ac ~io_cost:ioc =
let r1 = VariantCostMap.replace OperationCost oc VariantCostMap.empty in
let r2 = VariantCostMap.replace AllocationCost ac r1 in
VariantCostMap.replace IOCost ioc r2
(* Map representing cost record {OperationCost:0; AllocationCost:0; IOCost:0} *)
let zero_record = VariantCostMap.empty
let mult_by_scalar cost_record scalar = map cost_record ~f:(BasicCost.mult scalar)
(* Map representing cost record {OperationCost:0; AllocationCost:0; IOCost:0} *)
let zero_record =
mk_cost_record ~operation_cost:BasicCost.zero ~allocation_cost:BasicCost.zero
~io_cost:BasicCost.zero
let plus cost_record1 cost_record2 =
VariantCostMap.union
(fun _kind cost1 cost2 -> Some (BasicCost.plus cost1 cost2))
cost_record1 cost_record2
(* Map representing cost record {OperationCost:1; AllocationCost:0; IOCost:0} *)
let unit_cost_atomic_operation = VariantCostMap.replace OperationCost BasicCost.one zero_record
let unit_cost_atomic_operation = VariantCostMap.increment OperationCost zero_record
(* Map representing cost record {OperationCost:operation_cost; AllocationCost:0; IOCost:0} *)
let set_operation_cost operation_cost map = VariantCostMap.replace OperationCost operation_cost map
let of_operation_cost operation_cost =
VariantCostMap.increase_by OperationCost operation_cost zero_record

Write Preview
Loading…
Cancel
Save