diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index c968ab9ae..a72df3f0f 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -343,20 +343,19 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct let to_string {loc; proc_name; cost_opt} = match cost_opt with | Some {post} -> + let basic_operation_cost = CostDomain.get_operation_cost post in let hum = { 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 - ; big_o= - Format.asprintf "%a" CostDomain.BasicCost.pp_degree_hum post.basic_operation_cost } + Format.asprintf "%a" CostDomain.BasicCost.pp basic_operation_cost + ; hum_degree= Format.asprintf "%a" CostDomain.BasicCost.pp_degree basic_operation_cost + ; big_o= Format.asprintf "%a" CostDomain.BasicCost.pp_degree_hum basic_operation_cost } in let cost_item = let file = SourceFile.to_rel_path loc.Location.file in { 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.basic_operation_cost + ; polynomial= CostDomain.BasicCost.encode 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 b5b531ac1..6dcfc3835 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -57,7 +57,17 @@ module TransferFunctionsNodesBasicCost = struct { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map ; integer_type_widths: Typ.IntegerWidths.t } - let cost_atomic_instruction = BasicCost.one + 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 : @@ -69,24 +79,29 @@ module TransferFunctionsNodesBasicCost = struct let callee_cost = match CostModels.Call.dispatch () callee_pname params with | Some model -> - model inferbo_mem + CostDomain.set_operation_cost (model inferbo_mem) CostDomain.zero_record | None -> ( match Payload.read pdesc callee_pname with - | 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 - else callee_cost + | 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 -> - cost_atomic_instruction ) + 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 cost_atomic_instruction astate + 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 cost_atomic_instruction astate + CostDomain.NodeInstructionToCostMap.add key CostDomain.unit_cost_atomic_operation + astate | _ -> astate ) | _ -> @@ -611,13 +626,10 @@ 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 node. - It uses the basic cost of the nodes (computed previously by AnalyzerNodesBasicCost) - and MinTrees which give an upperbound on the number of times a node can be executed -*) +(* Calculate the final Worst Case Execution Time predicted for each node. *) module TransferFunctionsWCET = struct module CFG = InstrCFG - module Domain = AbstractDomain.Pair (BasicCost) (ReportedOnNodes) + module Domain = AbstractDomain.Pair (CostDomain.VariantCostMap) (ReportedOnNodes) type extras = extras_TransferFunctionsWCET @@ -668,9 +680,10 @@ module TransferFunctionsWCET = struct preds - let map_cost get_node_nb_exec m : BasicCost.t = + let map_operation_cost get_node_nb_exec m : BasicCost.t = CostDomain.NodeInstructionToCostMap.fold - (fun ((node_id, _) as instr_node_id) c acc -> + (fun ((node_id, _) as instr_node_id) c_record acc -> + let c = CostDomain.get_operation_cost c_record in let t = get_node_nb_exec node_id in let c_node = BasicCost.mult c t in let c_node' = BasicCost.plus acc c_node in @@ -693,7 +706,7 @@ module TransferFunctionsWCET = struct | Some node_map -> L.(debug Analysis Medium) "@\n [AnalyzerWCET] Final map for node: %a @\n" CFG.Node.pp_id instr_node_id ; - map_cost get_node_nb_exec node_map + map_operation_cost get_node_nb_exec node_map | _ -> assert false in @@ -715,7 +728,11 @@ module TransferFunctionsWCET = struct ReportedOnNodes.add nid reported_so_far ) else reported_so_far in - (cost_node, reported_so_far) + let cost_map = + CostDomain.mk_cost_record ~operation_cost:cost_node ~allocation_cost:BasicCost.zero + ~io_cost:BasicCost.zero + in + (cost_map, reported_so_far) in astate' @@ -725,7 +742,8 @@ end module AnalyzerWCET = AbstractInterpreter.MakeRPO (TransferFunctionsWCET) -let check_and_report_top_and_bottom cost proc_desc summary = +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 = let message = F.asprintf "The execution time of the function %a %s" Typ.Procname.pp @@ -793,20 +811,20 @@ 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 initWCET = (BasicCost.zero, ReportedOnNodes.empty) in + let initWCET = (CostDomain.zero_record, ReportedOnNodes.empty) in match AnalyzerWCET.compute_post ~initial:initWCET (ProcData.make proc_desc tenv {basic_cost_map= invariant_map_NodesBasicCost; get_node_nb_exec; summary}) with - | Some (exit_cost, _) -> + | Some (exit_cost_record, _) -> 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) - BasicCost.pp exit_cost ; - check_and_report_top_and_bottom exit_cost proc_desc summary ; - Payload.update_summary {post= {CostDomain.basic_operation_cost= exit_cost}} summary + CostDomain.VariantCostMap.pp exit_cost_record ; + check_and_report_top_and_bottom exit_cost_record proc_desc 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 diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 8ca4743ef..852e6c5c1 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -9,12 +9,78 @@ open! IStd module F = Format module BasicCost = Polynomials.NonNegativePolynomial +type cost_kind = OperationCost | AllocationCost | IOCost [@@deriving compare] + +module CostKind : PrettyPrintable.PrintableOrderedType with type t = cost_kind = struct + type t = cost_kind [@@deriving compare] + + let pp f k = + let k_str = + match k with + | OperationCost -> + "OperationCost" + | AllocationCost -> + "AllocationCost" + | IOCost -> + "IOCost" + in + F.pp_print_string f k_str +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 + + 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[@warning "-32"] increment kind record = increase_by kind BasicCost.one record +end + +type summary = {post: VariantCostMap.t} + +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) (BasicCost) +module NodeInstructionToCostMap = + AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (VariantCostMap) + +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 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 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 = + mk_cost_record ~operation_cost:BasicCost.zero ~allocation_cost:BasicCost.zero + ~io_cost:BasicCost.zero -type cost_record = {basic_operation_cost: BasicCost.t} -type summary = {post: cost_record} +(* Map representing cost record {OperationCost:1; AllocationCost:0; IOCost:0} *) +let unit_cost_atomic_operation = VariantCostMap.replace OperationCost BasicCost.one zero_record -let pp_summary fmt {post} = - F.fprintf fmt "@\n Post: {basic_operatio_cost: %a} @\n" BasicCost.pp post.basic_operation_cost +(* Map representing cost record {OperationCost:operation_cost; AllocationCost:0; IOCost:0} *) +let set_operation_cost operation_cost map = VariantCostMap.replace OperationCost operation_cost map diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index f8311ddce..b1d6ff8ae 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -91,8 +91,8 @@ 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.basic_operation_cost -> + | Some {Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost_record}}} + when CostDomain.BasicCost.is_symbolic (CostDomain.get_operation_cost cost_record) -> 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 = @@ -100,7 +100,8 @@ 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.basic_operation_cost + ~callee_pname:pname ~params + ~callee_cost:(CostDomain.get_operation_cost cost_record) |> CostDomain.BasicCost.is_symbolic | _ -> false