pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cost: Non-negative Bound abstract domain

Browse Source 
Summary:
The Cost analysis uses `Bound` for non-negative values only, let's make it a separate module (and abstract type).
This also separates the abstract domain part of `Bound` which we wanted anyway.

Depends on D7844267
Depends on D7843351
Depends on D7782184

Reviewed By: ddino

Differential Revision: D7844572

fbshipit-source-id: 0e6b620
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 5fe28785bc
commit c1aac1e089
5 changed files with 183 additions and 114 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -319,12 +319,13 @@ module Heap = struct
if is_empty mem then Val.bot else snd (choose mem)
let range : filter_loc:(Loc.t -> bool) -> astate -> Itv.Bound.t =
let range : filter_loc:(Loc.t -> bool) -> astate -> Itv.NonNegativeBound.t =
fun ~filter_loc mem ->
fold
(fun loc v acc ->
if filter_loc loc then v |> Val.get_itv |> Itv.range |> Itv.Bound.mult acc else acc )
mem Itv.Bound.one
if filter_loc loc then v |> Val.get_itv |> Itv.range |> Itv.NonNegativeBound.mult acc
else acc )
mem Itv.NonNegativeBound.one
end
module AliasTarget = struct
@ -768,7 +769,7 @@ module MemReach = struct
fun locs m -> add_from_locs m.heap locs PowLoc.empty
let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.Bound.t =
let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativeBound.t =
fun ~filter_loc {heap} -> Heap.range ~filter_loc heap
end

151
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -242,7 +242,7 @@ module SymLinear = struct
M.merge f se1 se2
let mult_const : t -> NonZeroInt.t -> t = fun x n -> M.map (NonZeroInt.( * ) n) x
let mult_const : NonZeroInt.t -> t -> t = fun n x -> M.map (NonZeroInt.( * ) n) x
let exact_div_const_exn : t -> NonZeroInt.t -> t =
fun x n -> M.map (fun c -> NonZeroInt.exact_div_exn c n) x
@ -323,8 +323,6 @@ module Bound = struct
| PInf
[@@deriving compare]
type astate = t
let pp : F.formatter -> t -> unit =
fun fmt -> function
| MInf ->
@ -679,8 +677,8 @@ module Bound = struct
b1 b1 b2
let ub : ?default:t -> t -> t -> t =
fun ?(default= PInf) x y ->
let ub : default:t -> t -> t -> t =
fun ~default x y ->
if le x y then y
else if le y x then x
else
@ -697,7 +695,7 @@ module Bound = struct
default
let join : t -> t -> t = ub ~default:PInf
let max_u : t -> t -> t = ub ~default:PInf
let widen_l : t -> t -> t =
fun x y ->
@ -717,8 +715,6 @@ module Bound = struct
if le y x then x else PInf
let widen ~prev ~next ~num_iters:_ = widen_u prev next
let ( <= ) ~lhs ~rhs = le lhs rhs
let zero : t = Linear (0, SymLinear.zero)
@ -727,8 +723,6 @@ module Bound = struct
let mone : t = Linear (-1, SymLinear.zero)
let pinf : t = PInf
let is_some_const : int -> t -> bool =
fun c x -> match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false
@ -802,18 +796,22 @@ module Bound = struct
PInf )
let mult_const : t -> NonZeroInt.t -> t option =
fun x n ->
let mult_const : default:t -> NonZeroInt.t -> t -> t =
fun ~default n x ->
match x with
| MInf ->
Some (if NonZeroInt.is_positive n then MInf else PInf)
if NonZeroInt.is_positive n then MInf else PInf
| PInf ->
Some (if NonZeroInt.is_positive n then PInf else MInf)
if NonZeroInt.is_positive n then PInf else MInf
| Linear (c, x') ->
Some (Linear (c * (n :> int), SymLinear.mult_const x' n))
Linear (c * (n :> int), SymLinear.mult_const n x')
| _ ->
None
default
let mult_const_l = mult_const ~default:MInf
let mult_const_u = mult_const ~default:PInf
let neg : t -> t = function
| MInf ->
@ -826,22 +824,6 @@ module Bound = struct
mk_MinMax (-c, Sign.neg sign, min_max, d, x)
let mult : t -> t -> t =
fun x y ->
let default = PInf in
match (x, is_const x, y, is_const y) with
| x, _, _, Some n | _, Some n, x, _ -> (
match NonZeroInt.of_int n with
| Some n ->
if NonZeroInt.is_one n then x
else if NonZeroInt.is_minus_one n then neg x
else mult_const x n |> Option.value ~default
| None ->
zero )
| _ ->
default
let div_const : t -> NonZeroInt.t -> t option =
fun x n ->
match x with
@ -883,6 +865,85 @@ module Bound = struct
let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true
end
module NonNegativeBound = struct
type t = Bound.t [@@deriving compare]
type astate = t
let pp = Bound.pp
let zero = Bound.zero
let one = Bound.one
let top = Bound.PInf
let of_bound b = if Bound.le b Bound.zero then Bound.zero else b
let of_int_exn i =
assert (i >= 0) ;
Bound.of_int i
let is_not_infty = function
| Bound.PInf ->
false
| Bound.(Linear _ | MinMax _) ->
true
| Bound.MInf ->
assert false
let is_symbolic = Bound.is_symbolic
let ( <= ) = Bound.( <= )
(* For now let's check and fail when these operations don't give a non-negative result *)
let checked1 name f b =
let res = f b in
let () =
if Bound.lt res zero then
L.internal_error "NonNegativeBound.%s %a = %a < 0@\n" name pp b pp res
in
res
let checked2 name f b1 b2 =
let res = f b1 b2 in
let () =
if Bound.lt res zero then
L.internal_error "NonNegativeBound.%s %a %a = %a < 0@\n" name pp b1 pp b2 pp res
in
res
let join b1 b2 = checked2 "join" Bound.max_u b1 b2
let min b1 b2 = checked2 "min" Bound.min_u b1 b2
let mult : t -> t -> t =
fun x y ->
match (x, Bound.is_const x, y, Bound.is_const y) with
| x, _, _, Some n | _, Some n, x, _ -> (
match NonZeroInt.of_int n with
| Some n ->
if NonZeroInt.is_one n then x
else if NonZeroInt.is_minus_one n then assert false
else checked1 "neg(mult_const)" (Bound.mult_const_u n) x
| None ->
zero )
| _ ->
top
let plus b1 b2 = checked2 "plus" Bound.plus_u b1 b2
let widen ~prev ~next ~num_iters:_ = checked2 "widen" Bound.widen_u prev next
let subst b map = match Bound.subst_ub b map with Bottom -> zero | NonBottom b -> of_bound b
end
module ItvPure = struct
(** (l, u) represents the closed interval [l; u] (of course infinite bounds are open) *)
type astate = Bound.t * Bound.t [@@deriving compare]
@ -947,7 +1008,7 @@ module ItvPure = struct
`RightSubsumesLeft
let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb ~default:MInf l1 l2, Bound.ub u1 u2)
let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.max_u u1 u2)
let widen : prev:t -> next:t -> num_iters:int -> t =
fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2)
@ -1013,7 +1074,9 @@ module ItvPure = struct
let is_le_zero : t -> bool = fun (_, ub) -> Bound.le ub Bound.zero
let range : t -> Bound.t = fun (l, u) -> Bound.plus_u (Bound.plus_u u Bound.one) (Bound.neg l)
let range : t -> NonNegativeBound.t =
fun (l, u) -> Bound.plus_u (Bound.plus_u u Bound.one) (Bound.neg l) |> NonNegativeBound.of_bound
let neg : t -> t =
fun (l, u) ->
@ -1030,22 +1093,16 @@ module ItvPure = struct
let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
let mult_const : t -> int -> t =
fun ((l, u) as itv) n ->
let mult_const : int -> t -> t =
fun n ((l, u) as itv) ->
match NonZeroInt.of_int n with
| None ->
zero
| Some n ->
if NonZeroInt.is_one n then itv
else if NonZeroInt.is_minus_one n then neg itv
else if NonZeroInt.is_positive n then
let l' = Option.value ~default:Bound.MInf (Bound.mult_const l n) in
let u' = Option.value ~default:Bound.PInf (Bound.mult_const u n) in
(l', u')
else
let l' = Option.value ~default:Bound.MInf (Bound.mult_const u n) in
let u' = Option.value ~default:Bound.PInf (Bound.mult_const l n) in
(l', u')
else if NonZeroInt.is_positive n then (Bound.mult_const_l n l, Bound.mult_const_u n u)
else (Bound.mult_const_l n u, Bound.mult_const_u n l)
(* Returns a precise value only when all coefficients are divided by
@ -1072,9 +1129,9 @@ module ItvPure = struct
fun x y ->
match (is_const x, is_const y) with
| _, Some n ->
mult_const x n
mult_const n x
| Some n, _ ->
mult_const y n
mult_const n y
| None, None ->
top
@ -1101,7 +1158,7 @@ module ItvPure = struct
(* x << [-1,-1] does nothing. *)
let shiftlt : t -> t -> t =
fun x y -> match is_const y with Some n -> mult_const x (1 lsl n) | None -> top
fun x y -> match is_const y with Some n -> mult_const (1 lsl n) x | None -> top
(* x >> [-1,-1] does nothing. *)

43
infer/src/bufferoverrun/itv.mli
Unescape View File

@ -40,18 +40,8 @@ module SymbolMap : PrettyPrintable.PPMap with type key = Symbol.t
module Bound : sig
type t [@@deriving compare]
type astate = t
val pp : F.formatter -> t -> unit
val zero : t
val one : t
val pinf : t
val of_int : int -> t
val is_const : t -> int option
val is_not_infty : t -> bool
@ -65,20 +55,41 @@ module Bound : sig
val le : t -> t -> bool
val lt : t -> t -> bool
end
(** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *)
module NonNegativeBound : sig
type t
val plus_u : t -> t -> t
type astate = t
val pp : F.formatter -> t -> unit
val zero : t
val one : t
val top : t
val of_int_exn : int -> t
val is_not_infty : t -> bool
val is_symbolic : t -> bool
val ( <= ) : lhs:t -> rhs:t -> bool
val join : t -> t -> t
val min_u : t -> t -> t
val min : t -> t -> t
val mult : t -> t -> t
val widen : prev:t -> next:t -> num_iters:'a -> t
val plus : t -> t -> t
val ( <= ) : lhs:t -> rhs:t -> bool
val widen : prev:t -> next:t -> num_iters:'a -> t
val subst_ub : t -> t bottom_lifted SymbolMap.t -> t bottom_lifted
val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t
end
module ItvPure : sig
@ -193,7 +204,7 @@ val le : lhs:t -> rhs:t -> bool
val lnot : t -> Boolean.t
val range : t -> Bound.t
val range : t -> NonNegativeBound.t
val div : t -> t -> t

87
infer/src/checkers/cost.ml
Unescape View File

@ -23,7 +23,7 @@ end)
(* We use this treshold to give error if the cost is above it.
Currently it's set randomly to 200. *)
let expensive_threshold = Itv.Bound.of_int 200
let expensive_threshold = Itv.NonNegativeBound.of_int_exn 200
(* CFG modules used in several other modules *)
module InstrCFG = ProcCfg.NormalOneInstrPerNode
@ -49,20 +49,20 @@ module TransferFunctionsNodesBasicCost = struct
type extras = BufferOverrunChecker.invariant_map
let cost_atomic_instruction = Itv.Bound.one
let cost_atomic_instruction = Itv.NonNegativeBound.one
let instantiate_cost ~tenv ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
match Ondemand.get_proc_desc callee_pname with
| None ->
L.(die InternalError)
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" Itv.Bound.pp
callee_cost Typ.Procname.pp callee_pname
"Can't instantiate symbolic cost %a from call to %a (can't get procdesc)"
Itv.NonNegativeBound.pp callee_cost Typ.Procname.pp callee_pname
| Some callee_pdesc ->
match BufferOverrunChecker.Summary.read_summary caller_pdesc callee_pname with
| None ->
L.(die InternalError)
"Can't instantiate symbolic cost %a from call to %a (can't get summary)" Itv.Bound.pp
callee_cost Typ.Procname.pp callee_pname
"Can't instantiate symbolic cost %a from call to %a (can't get summary)"
Itv.NonNegativeBound.pp callee_cost Typ.Procname.pp callee_pname
| Some inferbo_summary ->
let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in
@ -72,13 +72,7 @@ module TransferFunctionsNodesBasicCost = struct
BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem
callee_entry_mem ~callee_ret_alias
in
match Itv.Bound.subst_ub callee_cost subst_map with
| Bottom ->
L.(die InternalError)
"Instantiation of cost %a from call to %a returned Bottom" Itv.Bound.pp callee_cost
Typ.Procname.pp callee_pname
| NonBottom callee_cost ->
callee_cost
Itv.NonNegativeBound.subst callee_cost subst_map
let exec_instr_cost inferbo_mem (astate: CostDomain.NodeInstructionToCostMap.astate)
@ -90,7 +84,7 @@ module TransferFunctionsNodesBasicCost = struct
let callee_cost =
match Summary.read_summary pdesc callee_pname with
| Some {post= callee_cost} ->
if Itv.Bound.is_symbolic callee_cost then
if Itv.NonNegativeBound.is_symbolic callee_cost then
instantiate_cost ~tenv ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem
~callee_pname ~params ~callee_cost
else callee_cost
@ -134,14 +128,14 @@ module AnalyzerNodesBasicCost =
*)
module BoundMap = struct
type t = Itv.Bound.t Node.IdMap.t
type t = Itv.NonNegativeBound.t Node.IdMap.t
let print_upper_bound_map bound_map =
L.(debug Analysis Medium) "@\n\n******* Bound Map ITV **** @\n" ;
Node.IdMap.iter
(fun nid b ->
L.(debug Analysis Medium) "@\n node: %a --> bound = %a @\n" Node.pp_id nid Itv.Bound.pp b
)
L.(debug Analysis Medium)
"@\n node: %a --> bound = %a @\n" Node.pp_id nid Itv.NonNegativeBound.pp b )
bound_map ;
L.(debug Analysis Medium) "@\n******* END Bound Map ITV **** @\n\n"
@ -167,7 +161,7 @@ module BoundMap = struct
let node_id = NodeCFG.id node in
match Procdesc.Node.get_kind node with
| Procdesc.Node.Exit_node _ ->
Node.IdMap.add node_id Itv.Bound.one bound_map
Node.IdMap.add node_id Itv.NonNegativeBound.one bound_map
| _ ->
let entry_state_opt =
let instr_node_id = InstrCFG.of_underlying_node node |> InstrCFG.id in
@ -190,18 +184,18 @@ module BoundMap = struct
"@\n\
[COST ANALYSIS INTERNAL WARNING:] No 'env' found. This location is \
unreachable returning cost 0 \n" ;
Itv.Bound.zero
Itv.NonNegativeBound.zero
| NonBottom mem ->
BufferOverrunDomain.MemReach.heap_range
~filter_loc:(filter_loc formal_pvars all_deps)
mem
in
L.(debug Analysis Medium)
"@\n>>>Setting bound for node = %a to %a@\n\n" Node.pp_id node_id Itv.Bound.pp
bound ;
"@\n>>>Setting bound for node = %a to %a@\n\n" Node.pp_id node_id
Itv.NonNegativeBound.pp bound ;
Node.IdMap.add node_id bound bound_map
| _ ->
Node.IdMap.add node_id Itv.Bound.zero bound_map
Node.IdMap.add node_id Itv.NonNegativeBound.zero bound_map
in
let bound_map =
List.fold (NodeCFG.nodes node_cfg) ~f:compute_node_upper_bound ~init:Node.IdMap.empty
@ -216,7 +210,7 @@ module BoundMap = struct
| None ->
L.(debug Analysis Medium)
"@\n\n[WARNING] Bound not found for node %a, returning Top @\n" Node.pp_id nid ;
Itv.Bound.pinf
Itv.NonNegativeBound.top
end
(* Structural Constraints are expressions of the kind:
@ -295,7 +289,10 @@ end
*)
module MinTree = struct
type mt_node = Leaf of (Node.id * Itv.Bound.t) | Min of mt_node list | Plus of mt_node list
type mt_node =
| Leaf of (Node.id * Itv.NonNegativeBound.t)
| Min of mt_node list
| Plus of mt_node list
let add_leaf node nid leaf =
let leaf' = Leaf (nid, leaf) in
@ -307,7 +304,7 @@ module MinTree = struct
let rec pp fmt node =
match node with
| Leaf (nid, c) ->
F.fprintf fmt "%a:%a" Node.pp_id nid Itv.Bound.pp c
F.fprintf fmt "%a:%a" Node.pp_id nid Itv.NonNegativeBound.pp c
| Min l ->
F.fprintf fmt "Min(%a)" (Pp.comma_seq pp) l
| Plus l ->
@ -338,9 +335,9 @@ return the addends of the sum x_j1+x_j2+..+x_j_n*)
| Leaf (_, c) ->
c
| Min l ->
evaluate_operator Itv.Bound.min_u l
evaluate_operator Itv.NonNegativeBound.min l
| Plus l ->
evaluate_operator Itv.Bound.plus_u l
evaluate_operator Itv.NonNegativeBound.plus l
and evaluate_operator op l =
@ -450,7 +447,7 @@ module ReportedOnNodes = AbstractDomain.FiniteSetOfPPSet (Node.IdSet)
type extras_TransferFunctionsWCET =
{ basic_cost_map: AnalyzerNodesBasicCost.invariant_map
; min_trees_map: Itv.Bound.t Node.IdMap.t
; min_trees_map: Itv.NonNegativeBound.t Node.IdMap.t
; summary: Specs.summary }
(* Calculate the final Worst Case Execution Time predicted for each node.
@ -459,7 +456,7 @@ type extras_TransferFunctionsWCET =
*)
module TransferFunctionsWCET = struct
module CFG = InstrCFG
module Domain = AbstractDomain.Pair (Itv.Bound) (ReportedOnNodes)
module Domain = AbstractDomain.Pair (Itv.NonNegativeBound) (ReportedOnNodes)
type extras = extras_TransferFunctionsWCET
@ -473,12 +470,13 @@ module TransferFunctionsWCET = struct
(* We don't report when the cost is Top as it corresponds to subsequent 'don't know's.
Instead, we report Top cost only at the top level per function when `report_infinity` is set to true *)
let should_report_cost cost =
Itv.Bound.is_not_infty cost && not (Itv.Bound.le cost expensive_threshold)
Itv.NonNegativeBound.is_not_infty cost
&& not (Itv.NonNegativeBound.( <= ) ~lhs:cost ~rhs:expensive_threshold)
let do_report summary loc cost =
let ltr =
let cost_desc = F.asprintf "with estimated cost %a" Itv.Bound.pp cost in
let cost_desc = F.asprintf "with estimated cost %a" Itv.NonNegativeBound.pp cost in
[Errlog.make_trace_element 0 loc cost_desc []]
in
let exn =
@ -486,7 +484,7 @@ module TransferFunctionsWCET = struct
F.asprintf
"The execution time from the beginning of the function up to this program point is \
likely above the acceptable threshold of %a (estimated cost %a)"
Itv.Bound.pp expensive_threshold Itv.Bound.pp cost
Itv.NonNegativeBound.pp expensive_threshold Itv.NonNegativeBound.pp cost
in
Exceptions.Checkers (IssueType.expensive_execution_time_call, Localise.verbatim_desc message)
in
@ -503,20 +501,20 @@ module TransferFunctionsWCET = struct
preds
let map_cost trees m : Itv.Bound.t =
let map_cost trees m : Itv.NonNegativeBound.t =
CostDomain.NodeInstructionToCostMap.fold
(fun ((node_id, _) as instr_node_id) c acc ->
let t = Node.IdMap.find node_id trees in
let c_node = Itv.Bound.mult c t in
let c_node' = Itv.Bound.plus_u acc c_node in
let c_node = Itv.NonNegativeBound.mult c t in
let c_node' = Itv.NonNegativeBound.plus acc c_node in
L.(debug Analysis Medium)
"@\n [AnalyzerWCET] Adding cost: (%a) --> c =%a t = %a @\n" InstrCFG.pp_id
instr_node_id Itv.Bound.pp c Itv.Bound.pp t ;
instr_node_id Itv.NonNegativeBound.pp c Itv.NonNegativeBound.pp t ;
L.(debug Analysis Medium)
"@\n [AnalyzerWCET] Adding cost: (%a) --> c_node=%a cost = %a @\n" InstrCFG.pp_id
instr_node_id Itv.Bound.pp c_node Itv.Bound.pp c_node' ;
instr_node_id Itv.NonNegativeBound.pp c_node Itv.NonNegativeBound.pp c_node' ;
c_node' )
m Itv.Bound.zero
m Itv.NonNegativeBound.zero
let exec_instr ((_, reported_so_far): Domain.astate) {ProcData.extras} (node: CFG.node) instr
@ -533,8 +531,8 @@ module TransferFunctionsWCET = struct
assert false
in
L.(debug Analysis Medium)
"@\n>>>AnalyzerWCET] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr Itv.Bound.pp
cost_node ;
"@\n>>>AnalyzerWCET] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr
Itv.NonNegativeBound.pp cost_node ;
let astate' =
let und_node = CFG.underlying_node node in
let preds = Procdesc.Node.get_preds und_node in
@ -559,7 +557,7 @@ end
module AnalyzerWCET = AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsWCET)
let check_and_report_infinity cost proc_desc summary =
if not (Itv.Bound.is_not_infty cost) then
if not (Itv.NonNegativeBound.is_not_infty cost) then
let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in
let message =
F.asprintf "The execution time of the function %a cannot be computed" Typ.Procname.pp
@ -609,11 +607,12 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Specs.summary =
List.fold
~f:(fun acc (nid, t) ->
let res = MinTree.evaluate_tree t in
L.(debug Analysis Medium) "@\n Tree %a eval to %a @\n" Node.pp_id nid Itv.Bound.pp res ;
L.(debug Analysis Medium)
"@\n Tree %a eval to %a @\n" Node.pp_id nid Itv.NonNegativeBound.pp res ;
Node.IdMap.add nid res acc )
~init:Node.IdMap.empty min_trees
in
let initWCET = (Itv.Bound.zero, ReportedOnNodes.empty) in
let initWCET = (Itv.NonNegativeBound.zero, ReportedOnNodes.empty) in
match
AnalyzerWCET.compute_post
(ProcData.make proc_desc tenv
@ -621,7 +620,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Specs.summary =
~debug:true ~initial:initWCET
with
| Some (exit_cost, _) ->
L.internal_error " PROCEDURE COST = %a @\n" Itv.Bound.pp exit_cost ;
L.internal_error " PROCEDURE COST = %a @\n" Itv.NonNegativeBound.pp exit_cost ;
check_and_report_infinity exit_cost proc_desc summary ;
Summary.update_summary {post= exit_cost} summary
| None ->

7
infer/src/checkers/costDomain.ml
Unescape View File

@ -11,8 +11,9 @@ open! IStd
module F = Format
(** Map (node,instr) -> basic cost *)
module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (Itv.Bound)
module NodeInstructionToCostMap =
AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (Itv.NonNegativeBound)
type summary = {post: Itv.Bound.t}
type summary = {post: Itv.NonNegativeBound.t}
let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" Itv.Bound.pp post
let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" Itv.NonNegativeBound.pp post

Write Preview
Loading…
Cancel
Save