diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 5d9df444f..1668b7c14 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -618,8 +618,11 @@ module MemPure = struct let bot = empty let range : - filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t = - fun ~filter_loc mem -> + filter_loc:(Loc.t -> LoopHeadLoc.t option) + -> node_id:ProcCfg.Normal.Node.id + -> t + -> Polynomials.NonNegativePolynomial.t = + fun ~filter_loc ~node_id mem -> fold (fun loc (_, v) acc -> match filter_loc loc with @@ -627,8 +630,19 @@ module MemPure = struct let itv = Val.get_itv v in if Itv.has_only_non_int_symbols itv then acc else - Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial - |> Polynomials.NonNegativePolynomial.mult acc + let range1 = Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial in + if Polynomials.NonNegativePolynomial.is_top range1 then + L.d_printfln_escaped "Range of %a (loc:%a) became top at %a." Itv.pp itv Loc.pp loc + ProcCfg.Normal.Node.pp_id node_id ; + let range = Polynomials.NonNegativePolynomial.mult acc range1 in + if + (not (Polynomials.NonNegativePolynomial.is_top acc)) + && Polynomials.NonNegativePolynomial.is_top range + then + L.d_printfln_escaped "Multiplication of %a and %a (loc:%a) became top at %a." + Polynomials.NonNegativePolynomial.pp acc Polynomials.NonNegativePolynomial.pp + range1 Loc.pp loc ProcCfg.Normal.Node.pp_id node_id ; + range | None -> acc ) mem Polynomials.NonNegativePolynomial.one @@ -1609,8 +1623,11 @@ module MemReach = struct let range : - filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t = - fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure + filter_loc:(Loc.t -> LoopHeadLoc.t option) + -> node_id:ProcCfg.Normal.Node.id + -> t + -> Polynomials.NonNegativePolynomial.t = + fun ~filter_loc ~node_id {mem_pure} -> MemPure.range ~filter_loc ~node_id mem_pure let get_relation : t -> Relation.t = fun m -> m.relation diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 4d766a5cb..062c3aa66 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -121,6 +121,7 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) : | Symbolic symbol -> Bounds.Symbolic {degree_kind; symbol} | ValTop trace -> + Logging.d_printfln_escaped "subst(%a) became top." (S.pp ~hum:false) symbol ; Bounds.ValTop trace diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 02c52b12a..963d58f76 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -82,7 +82,8 @@ module BoundMap = struct unreachable returning cost 0 \n" ; BasicCost.zero | NonBottom mem -> - BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) mem + BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) + ~node_id mem in L.(debug Analysis Medium) "@\n>>>Setting bound for node = %a to %a@\n\n" Node.pp_id node_id BasicCost.pp @@ -604,7 +605,13 @@ module InstrBasicCost = struct | More -> assert false in - get_instr_cost_record tenv extras instr_node instr + let cost = get_instr_cost_record tenv extras instr_node instr in + if BasicCost.is_top (CostDomain.get_operation_cost cost) then + Logging.d_printfln_escaped "Statement cost became top at %a (%a)." InstrCFG.Node.pp_id + (InstrCFG.Node.id instr_node) + (Sil.pp_instr ~print_types:false Pp.text) + instr ; + cost end let compute_errlog_extras cost = @@ -653,6 +660,9 @@ module WorstCaseCost = struct let instr_cost_record = InstrBasicCost.get_instr_node_cost_record tenv extras instr_node in let node_id = InstrCFG.Node.underlying_node instr_node |> Node.id in let nb_exec = get_node_nb_exec node_id in + if BasicCost.is_top nb_exec then + Logging.d_printfln_escaped "Node %a is analyzed to visit infinite (top) times." Node.pp_id + node_id ; CostDomain.mult_by_scalar instr_cost_record nb_exec in let costs = CostDomain.plus costs node_cost in