Using record data structure for the cost domain

Reviewed By: mbouaziz

Differential Revision: D13897572

fbshipit-source-id: 4148b18b4
master
Dino Distefano 6 years ago committed by Facebook Github Bot
parent 7907fac13b
commit e6d2872a4e

@ -346,8 +346,10 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct
let hum =
if Config.developer_mode then
Some
{ Jsonbug_t.hum_polynomial= Format.asprintf "%a" CostDomain.BasicCost.pp post
; hum_degree= Format.asprintf "%a" CostDomain.BasicCost.pp_degree post }
{ Jsonbug_t.hum_polynomial=
Format.asprintf "%a" CostDomain.BasicCost.pp post.basic_operation_cost
; hum_degree=
Format.asprintf "%a" CostDomain.BasicCost.pp_degree post.basic_operation_cost }
else None
in
let cost_item =
@ -355,7 +357,7 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct
{ Jsonbug_t.hash= compute_hash ~severity:"" ~bug_type:"" ~proc_name ~file ~qualifier:""
; loc= {file; lnum= loc.Location.line; cnum= loc.Location.col; enum= -1}
; procedure_id= procedure_id_of_procname proc_name
; polynomial= CostDomain.BasicCost.encode post
; polynomial= CostDomain.BasicCost.encode post.basic_operation_cost
; hum }
in
Some (Jsonbug_j.string_of_cost_item cost_item)

@ -72,7 +72,7 @@ module TransferFunctionsNodesBasicCost = struct
model inferbo_mem
| None -> (
match Payload.read pdesc callee_pname with
| Some {post= callee_cost} ->
| Some {post= {CostDomain.basic_operation_cost= callee_cost}} ->
if BasicCost.is_symbolic callee_cost then
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
~callee_pname ~params ~callee_cost
@ -806,7 +806,7 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
(Container.length ~fold:NodeCFG.fold_nodes node_cfg)
BasicCost.pp exit_cost ;
check_and_report_top_and_bottom exit_cost proc_desc summary ;
Payload.update_summary {post= exit_cost} summary
Payload.update_summary {post= {CostDomain.basic_operation_cost= exit_cost}} 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

@ -12,6 +12,9 @@ module BasicCost = Polynomials.NonNegativePolynomial
(** Map (node,instr) -> basic cost *)
module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (BasicCost)
type summary = {post: BasicCost.t}
type cost_record = {basic_operation_cost: BasicCost.t}
let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" BasicCost.pp post
type summary = {post: cost_record}
let pp_summary fmt {post} =
F.fprintf fmt "@\n Post: {basic_operatio_cost: %a} @\n" BasicCost.pp post.basic_operation_cost

@ -90,7 +90,7 @@ let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths in
(* only report if function call has expensive/symbolic cost *)
match Ondemand.analyze_proc_name pname with
| Some {Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost}}}
when CostDomain.BasicCost.is_symbolic cost ->
when CostDomain.BasicCost.is_symbolic cost.basic_operation_cost ->
let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in
let inferbo_invariant_map = Lazy.force inferbo_invariant_map in
let inferbo_mem =
@ -98,7 +98,7 @@ let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths in
in
(* get the cost of the function call *)
Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
~callee_pname:pname ~params ~callee_cost:cost
~callee_pname:pname ~params ~callee_cost:cost.basic_operation_cost
|> CostDomain.BasicCost.is_symbolic
| _ ->
false

Loading…
Cancel
Save