Simulate record domain in cost analysis

Reviewed By: mbouaziz

Differential Revision: D13971520

fbshipit-source-id: a43ff1329

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
+              Format.asprintf "%a" CostDomain.BasicCost.pp basic_operation_cost
-          ; hum_degree=
+          ; hum_degree= Format.asprintf "%a" CostDomain.BasicCost.pp_degree basic_operation_cost
-              Format.asprintf "%a" CostDomain.BasicCost.pp_degree post.basic_operation_cost
+          ; big_o= Format.asprintf "%a" CostDomain.BasicCost.pp_degree_hum basic_operation_cost }
-          ; big_o=
-              Format.asprintf "%a" CostDomain.BasicCost.pp_degree_hum post.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)

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}} ->
+              | Some {post= callee_cost_record} ->
-                  if BasicCost.is_symbolic callee_cost then
+                  let callee_operation_cost =
-                    instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
+                    callee_OperationCost callee_cost_record integer_type_widths inferbo_mem
-                      ~callee_pname ~params ~callee_cost
+                      callee_pname params
-                  else callee_cost
+                  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.
+(* 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
-*)
 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 ;
+        CostDomain.VariantCostMap.pp exit_cost_record ;
-      check_and_report_top_and_bottom exit_cost proc_desc summary ;
+      check_and_report_top_and_bottom exit_cost_record proc_desc summary ;
-      Payload.update_summary {post= {CostDomain.basic_operation_cost= exit_cost}} 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

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} =
+(* Map representing cost record {OperationCost:operation_cost; AllocationCost:0; IOCost:0} *)
-  F.fprintf fmt "@\n Post: {basic_operatio_cost: %a} @\n" BasicCost.pp post.basic_operation_cost
+let set_operation_cost operation_cost map = VariantCostMap.replace OperationCost operation_cost map

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}}}
+    | Some {Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost_record}}}
-      when CostDomain.BasicCost.is_symbolic cost.basic_operation_cost ->
+      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