|
|
@ -28,7 +28,10 @@ module ReportConfig = struct
|
|
|
|
, { name= "The execution time"
|
|
|
|
, { name= "The execution time"
|
|
|
|
; threshold= Option.some_if Config.use_cost_threshold 200
|
|
|
|
; threshold= Option.some_if Config.use_cost_threshold 200
|
|
|
|
; top_and_bottom= true } )
|
|
|
|
; top_and_bottom= true } )
|
|
|
|
; (CostDomain.AllocationCost, {name= "The allocations"; threshold= None; top_and_bottom= false})
|
|
|
|
; ( CostDomain.AllocationCost
|
|
|
|
|
|
|
|
, { name= "The allocations"
|
|
|
|
|
|
|
|
; threshold= Option.some_if Config.use_cost_threshold 3
|
|
|
|
|
|
|
|
; top_and_bottom= false } )
|
|
|
|
; (CostDomain.IOCost, {name= "The IOs"; threshold= None; top_and_bottom= false}) ]
|
|
|
|
; (CostDomain.IOCost, {name= "The IOs"; threshold= None; top_and_bottom= false}) ]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -551,30 +554,41 @@ 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.
|
|
|
|
For example for basic operation we set it to 1 and for function call we take it from the spec of the function.
|
|
|
|
*)
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let allocation_functions = [BuiltinDecl.__new]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let is_allocation_function callee_pname =
|
|
|
|
|
|
|
|
List.exists allocation_functions ~f:(fun f -> Typ.Procname.equal callee_pname f)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let get_instr_cost_record extras instr_node instr =
|
|
|
|
let get_instr_cost_record extras instr_node instr =
|
|
|
|
match instr with
|
|
|
|
match instr with
|
|
|
|
| Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> (
|
|
|
|
| Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) ->
|
|
|
|
let {inferbo_invariant_map; integer_type_widths; get_callee_summary_and_formals} =
|
|
|
|
let {inferbo_invariant_map; integer_type_widths; get_callee_summary_and_formals} =
|
|
|
|
extras
|
|
|
|
extras
|
|
|
|
in
|
|
|
|
in
|
|
|
|
match
|
|
|
|
let operation_cost =
|
|
|
|
BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map
|
|
|
|
match
|
|
|
|
with
|
|
|
|
BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map
|
|
|
|
| None ->
|
|
|
|
with
|
|
|
|
CostDomain.unit_cost_atomic_operation
|
|
|
|
| None ->
|
|
|
|
| Some inferbo_mem -> (
|
|
|
|
CostDomain.unit_cost_atomic_operation
|
|
|
|
let loc = InstrCFG.Node.loc instr_node in
|
|
|
|
| Some inferbo_mem -> (
|
|
|
|
match CostModels.Call.dispatch () callee_pname params with
|
|
|
|
let loc = InstrCFG.Node.loc instr_node in
|
|
|
|
| Some model ->
|
|
|
|
match CostModels.Call.dispatch () callee_pname params with
|
|
|
|
CostDomain.of_operation_cost (model loc inferbo_mem)
|
|
|
|
| Some model ->
|
|
|
|
| None -> (
|
|
|
|
CostDomain.of_operation_cost (model loc inferbo_mem)
|
|
|
|
match get_callee_summary_and_formals callee_pname with
|
|
|
|
| None -> (
|
|
|
|
| Some ({CostDomain.post= callee_cost_record}, callee_formals) ->
|
|
|
|
match get_callee_summary_and_formals callee_pname with
|
|
|
|
CostDomain.map callee_cost_record ~f:(fun callee_cost ->
|
|
|
|
| Some ({CostDomain.post= callee_cost_record}, callee_formals) ->
|
|
|
|
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
|
|
|
|
CostDomain.map callee_cost_record ~f:(fun callee_cost ->
|
|
|
|
~callee_pname ~callee_formals ~params ~callee_cost ~loc )
|
|
|
|
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
|
|
|
|
| None ->
|
|
|
|
~callee_pname ~callee_formals ~params ~callee_cost ~loc )
|
|
|
|
CostDomain.unit_cost_atomic_operation ) ) )
|
|
|
|
| None ->
|
|
|
|
|
|
|
|
CostDomain.unit_cost_atomic_operation ) )
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
if is_allocation_function callee_pname then
|
|
|
|
|
|
|
|
CostDomain.plus CostDomain.unit_cost_allocation operation_cost
|
|
|
|
|
|
|
|
else operation_cost
|
|
|
|
| Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ ->
|
|
|
|
| Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ ->
|
|
|
|
CostDomain.unit_cost_atomic_operation
|
|
|
|
CostDomain.unit_cost_atomic_operation
|
|
|
|
| Sil.ExitScope _ -> (
|
|
|
|
| Sil.ExitScope _ -> (
|
|
|
|