From c1aac1e089cbfadf5042273a04a86ca231a5a93f Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 3 May 2018 05:07:38 -0700 Subject: [PATCH] Cost: Non-negative Bound abstract domain 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 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 9 +- infer/src/bufferoverrun/itv.ml | 151 ++++++++++++------ infer/src/bufferoverrun/itv.mli | 43 +++-- infer/src/checkers/cost.ml | 87 +++++----- infer/src/checkers/costDomain.ml | 7 +- 5 files changed, 183 insertions(+), 114 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e62faa3a0..c4e69dd09 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -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 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 45e9754f9..bf8e0539a 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -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. *) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 51c00a18f..d3c2167f9 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -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 diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 0f2f7762d..fb5355c45 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -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 -> diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 3d142fbcb..59afb9ebd 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -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