|
|
@ -34,26 +34,18 @@ module Node = ProcCfg.DefaultNode
|
|
|
|
The nodes in the domain of the map are those in the path reaching the current node.
|
|
|
|
The nodes in the domain of the map are those in the path reaching the current node.
|
|
|
|
*)
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
|
|
let instantiate_cost integer_type_widths ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params
|
|
|
|
let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
|
|
|
|
~callee_cost =
|
|
|
|
|
|
|
|
match Ondemand.get_proc_desc callee_pname with
|
|
|
|
match Ondemand.get_proc_desc callee_pname with
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
L.(die InternalError)
|
|
|
|
L.(die InternalError)
|
|
|
|
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp
|
|
|
|
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp
|
|
|
|
callee_cost Typ.Procname.pp callee_pname
|
|
|
|
callee_cost Typ.Procname.pp callee_pname
|
|
|
|
| Some callee_pdesc -> (
|
|
|
|
| Some callee_pdesc ->
|
|
|
|
match BufferOverrunChecker.Payload.read caller_pdesc callee_pname with
|
|
|
|
|
|
|
|
| None ->
|
|
|
|
|
|
|
|
L.(die InternalError)
|
|
|
|
|
|
|
|
"Can't instantiate symbolic cost %a from call to %a (can't get summary)" BasicCost.pp
|
|
|
|
|
|
|
|
callee_cost Typ.Procname.pp callee_pname
|
|
|
|
|
|
|
|
| Some _ ->
|
|
|
|
|
|
|
|
let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
|
|
|
|
|
|
|
|
let eval_sym =
|
|
|
|
let eval_sym =
|
|
|
|
BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_pdesc params
|
|
|
|
BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_pdesc params
|
|
|
|
inferbo_caller_mem
|
|
|
|
inferbo_caller_mem
|
|
|
|
in
|
|
|
|
in
|
|
|
|
BasicCost.subst callee_cost eval_sym )
|
|
|
|
BasicCost.subst callee_cost eval_sym
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module TransferFunctionsNodesBasicCost = struct
|
|
|
|
module TransferFunctionsNodesBasicCost = struct
|
|
|
@ -77,8 +69,8 @@ module TransferFunctionsNodesBasicCost = struct
|
|
|
|
match Payload.read pdesc callee_pname with
|
|
|
|
match Payload.read pdesc callee_pname with
|
|
|
|
| Some {post= callee_cost} ->
|
|
|
|
| Some {post= callee_cost} ->
|
|
|
|
if BasicCost.is_symbolic callee_cost then
|
|
|
|
if BasicCost.is_symbolic callee_cost then
|
|
|
|
instantiate_cost integer_type_widths ~caller_pdesc:pdesc
|
|
|
|
instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
|
|
|
|
~inferbo_caller_mem:inferbo_mem ~callee_pname ~params ~callee_cost
|
|
|
|
~callee_pname ~params ~callee_cost
|
|
|
|
else callee_cost
|
|
|
|
else callee_cost
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
cost_atomic_instruction
|
|
|
|
cost_atomic_instruction
|
|
|
@ -104,7 +96,9 @@ module TransferFunctionsNodesBasicCost = struct
|
|
|
|
|
|
|
|
|
|
|
|
let exec_instr costmap ({ProcData.extras= {inferbo_invariant_map; integer_type_widths}} as pdata)
|
|
|
|
let exec_instr costmap ({ProcData.extras= {inferbo_invariant_map; integer_type_widths}} as pdata)
|
|
|
|
node instr =
|
|
|
|
node instr =
|
|
|
|
let inferbo_mem = BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map in
|
|
|
|
let inferbo_mem =
|
|
|
|
|
|
|
|
Option.value_exn (BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map)
|
|
|
|
|
|
|
|
in
|
|
|
|
let costmap = exec_instr_cost integer_type_widths inferbo_mem costmap pdata node instr in
|
|
|
|
let costmap = exec_instr_cost integer_type_widths inferbo_mem costmap pdata node instr in
|
|
|
|
costmap
|
|
|
|
costmap
|
|
|
|
|
|
|
|
|
|
|
|