diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 4e9d8b331..f22848289 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -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) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index a01398a5c..b5b531ac1 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -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 diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index e258ef8b5..8ca4743ef 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -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 diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index 28149bbd1..e4249c1c0 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -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