From e54df20eb77cdc379a22a60f53c0d6cafc509289 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Fri, 23 Mar 2018 09:48:47 -0700 Subject: [PATCH] Migrate to Itv.Bound Reviewed By: mbouaziz Differential Revision: D7351195 fbshipit-source-id: 7f4f57b --- infer/src/bufferoverrun/itv.ml | 28 +++- infer/src/bufferoverrun/itv.mli | 22 ++- infer/src/checkers/cost.ml | 151 ++++++++---------- infer/src/checkers/costDomain.ml | 11 +- .../codetoanalyze/c/performance/cost_test.c | 11 +- .../codetoanalyze/c/performance/issues.exp | 14 +- 6 files changed, 141 insertions(+), 96 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 4c6619396..88c63c193 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -294,6 +294,8 @@ module Bound = struct | PInf [@@deriving compare] + type astate = t + let equal = [%compare.equal : t] let pp : F.formatter -> t -> unit = @@ -659,6 +661,10 @@ module Bound = struct default + let join : t -> t -> t = ub ~default:PInf + + let min : t -> t -> t = lb ~default:MInf + let widen_l : t -> t -> t = fun x y -> if equal x PInf || equal y PInf then L.(die InternalError) "Lower bound cannot be +oo." @@ -673,12 +679,18 @@ module Bound = struct 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) let one : t = Linear (1, SymLinear.zero) 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 @@ -767,6 +779,20 @@ module Bound = struct None + let mult : t -> t -> t = + fun x y -> + let res_opt = + match (is_const x, is_const y) with + | _, Some n -> ( + match NonZeroInt.of_int n with Some n' -> mult_const x n' | _ -> Some zero ) + | Some n, _ -> ( + match NonZeroInt.of_int n with Some n' -> mult_const y n' | _ -> Some zero ) + | _, _ -> + None + in + Option.value res_opt ~default:PInf + + let div_const : t -> NonZeroInt.t -> t option = fun x n -> match x with @@ -1283,7 +1309,7 @@ let le : lhs:t -> rhs:t -> bool = ( <= ) let eq : t -> t -> bool = fun x y -> ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x -let _range : t -> Bound.t = function Bottom -> Bound.zero | NonBottom itv -> ItvPure.range itv +let range : t -> Bound.t = function Bottom -> Bound.zero | NonBottom itv -> ItvPure.range itv let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t = fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 7c5e6fe07..97abd72e1 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -20,10 +20,18 @@ module SubstMap : Caml.Map.S 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 @@ -37,6 +45,18 @@ module Bound : sig val le : t -> t -> bool val lt : t -> t -> bool + + val plus_u : t -> t -> t + + val join : t -> t -> t + + val min : t -> t -> t + + val mult : t -> t -> t + + val widen : prev:t -> next:t -> num_iters:'a -> t + + val ( <= ) : lhs:t -> rhs:t -> bool end module ItvPure : sig @@ -165,7 +185,7 @@ val eq : t -> t -> bool val le : lhs:t -> rhs:t -> bool -val _range : t -> Bound.t +val range : t -> Bound.t val div : t -> t -> t diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 81839d8bb..d362f437e 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -10,7 +10,6 @@ open! IStd module F = Format module L = Logging -open AbstractDomain.Types module Summary = Summary.Make (struct type payload = CostDomain.summary @@ -24,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 = CostDomain.Cost.nth 200 +let expensive_threshold = Itv.Bound.of_int 200 (* CFG module used in several other modules *) module CFG = ProcCfg.Normal @@ -97,13 +96,13 @@ end *) module BoundMap = struct - let bound_map : CostDomain.Cost.astate Int.Map.t ref = ref Int.Map.empty + let bound_map : Itv.Bound.t Int.Map.t ref = ref Int.Map.empty let print_upper_bound_map () = - L.(debug Analysis Medium) "@\n\n******* Bound Map **** @\n" ; + L.(debug Analysis Medium) "@\n\n******* Bound Map ITV **** @\n" ; Int.Map.iteri !bound_map ~f:(fun ~key:nid ~data:b -> - L.(debug Analysis Medium) "@\n node: %i --> bound = %a @\n" nid CostDomain.Cost.pp b ) ; - L.(debug Analysis Medium) "@\n******* END Bound Map **** @\n\n" + L.(debug Analysis Medium) "@\n node: %i --> bound = %a @\n" nid Itv.Bound.pp b ) ; + L.(debug Analysis Medium) "@\n******* END Bound Map ITV **** @\n\n" let convert (mem: BufferOverrunDomain.Mem.astate) : CostDomain.EnvDomainBO.astate = @@ -129,25 +128,16 @@ module BoundMap = struct env - let compute_upperbound_map cfg invariant_map = - let range itv = - let rng = Itv._range itv in - match Itv.Bound.is_const rng with - | Some r -> - CostDomain.Cost.nth r - | _ -> - (* TODO: write code for the non constant case *) - L.(debug Analysis Medium) - "@\n [Range computation]: Can't determine a range for itv = %a. Returning Top@\n" - Itv.Bound.pp rng ; - Top - in + let compute_upperbound_map pdesc invariant_map = + let fparam = Procdesc.get_formals pdesc in + let pname = Procdesc.get_proc_name pdesc in + let fparam' = List.map ~f:(fun (m, _) -> Exp.Lvar (Pvar.mk m pname)) fparam in let compute_node_upper_bound node = let node_id = Procdesc.Node.get_id node in let entry_mem_opt = BufferOverrunChecker.extract_post invariant_map node in match Procdesc.Node.get_kind node with | Procdesc.Node.Exit_node _ -> - bound_map := Int.Map.set !bound_map ~key:(node_id :> int) ~data:CostDomain.Cost.one + bound_map := Int.Map.set !bound_map ~key:(node_id :> int) ~data:Itv.Bound.one | _ -> match entry_mem_opt with | Some entry_mem -> @@ -158,31 +148,34 @@ module BoundMap = struct (fun exp itv acc -> let itv' = match exp with - | Exp.Lvar _ -> - itv | Exp.Var _ -> Itv.one (* For temp var we give [1,1] so it doesn't count*) + | Exp.Lvar _ + when List.mem fparam' exp ~equal:Exp.equal -> + Itv.one + | Exp.Lvar _ -> + itv | _ -> assert false in - let itv_range = range itv' in + let range = Itv.range itv' in L.(debug Analysis Medium) - "@\n>>>For node = %i : itv=%a range=%a @\n\n" + "@\n>>>For node = %i : exp=%a itv=%a range =%a @\n\n" (node_id :> int) - Itv.pp itv' CostDomain.Cost.pp itv_range ; - CostDomain.Cost.mult acc itv_range ) - env CostDomain.Cost.one + Exp.pp exp Itv.pp itv' Itv.Bound.pp range ; + Itv.Bound.mult acc range ) + env Itv.Bound.one in L.(debug Analysis Medium) "@\n>>>Setting bound for node = %i to %a@\n\n" (node_id :> int) - CostDomain.Cost.pp bound ; + Itv.Bound.pp bound ; bound_map := Int.Map.set !bound_map ~key:(node_id :> int) ~data:bound | _ -> - bound_map := Int.Map.set !bound_map ~key:(node_id :> int) ~data:CostDomain.Cost.zero + bound_map := Int.Map.set !bound_map ~key:(node_id :> int) ~data:Itv.Bound.zero in - List.iter (CFG.nodes cfg) ~f:compute_node_upper_bound ; + List.iter (CFG.nodes pdesc) ~f:compute_node_upper_bound ; print_upper_bound_map () @@ -193,7 +186,7 @@ module BoundMap = struct | None -> L.(debug Analysis Medium) "@\n\n[WARNING] Bound not found for node %i, returning Top @\n" nid ; - Top + Itv.Bound.pinf end (* Structural Constraints are expressions of the kind: @@ -254,10 +247,7 @@ end *) module MinTree = struct - type mt_node = - | Leaf of (int * CostDomain.Cost.astate) - | Min of mt_node list - | Plus of mt_node list + type mt_node = Leaf of (int * Itv.Bound.t) | Min of mt_node list | Plus of mt_node list let add_leaf node nid leaf = let leaf' = Leaf (nid, leaf) in @@ -269,7 +259,7 @@ module MinTree = struct let rec pp fmt node = match node with | Leaf (nid, c) -> - F.fprintf fmt "%i:%a" nid CostDomain.Cost.pp c + F.fprintf fmt "%i:%a" nid Itv.Bound.pp c | Min l -> F.fprintf fmt "Min(%a)" (Pp.comma_seq pp) l | Plus l -> @@ -326,9 +316,9 @@ return the addends of the sum x_j1+x_j2+..+x_j_n*) | Leaf (_, c) -> c | Min l -> - evaluate_operator CostDomain.Cost.min l + evaluate_operator Itv.Bound.min l | Plus l -> - evaluate_operator CostDomain.Cost.plus l + evaluate_operator Itv.Bound.plus_u l and evaluate_operator op l = @@ -427,7 +417,7 @@ module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct type extras = ProcData.no_extras - let cost_atomic_instruction = CostDomain.Cost.one + let cost_atomic_instruction = Itv.Bound.one let instr_idx (node: CFG.node) instr = match CFG.instrs node with @@ -462,7 +452,12 @@ module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct end module AnalyzerNodesBasicCost = AbstractInterpreter.Make (CFG) (TransferFunctionsNodesBasicCost) -module RepSet = AbstractDomain.FiniteSet (Int) +module ReportedOnNodes = AbstractDomain.FiniteSet (Int) + +type extras_TransferFunctionsWCET = + { basic_cost_map: AnalyzerNodesBasicCost.invariant_map + ; min_trees_map: Itv.Bound.t Int.Map.t + ; summary: Specs.summary } (* Calculate the final Worst Case Execution Time predicted for each node. It uses the basic cost of the nodes (computed previously by AnalyzerNodesBasicCost) @@ -470,87 +465,81 @@ module RepSet = AbstractDomain.FiniteSet (Int) *) module TransferFunctionsWCET (CFG : ProcCfg.S) = struct module CFG = CFG - module CSI = CostDomain.CostSingleIteration - module Domain = AbstractDomain.Pair (CSI) (RepSet) + module Domain = AbstractDomain.Pair (Itv.Bound) (ReportedOnNodes) - type extras = - (* extras: (map with basic costs, min trees map, summary ) *) - AnalyzerNodesBasicCost.invariant_map * CostDomain.Cost.astate Int.Map.t * Specs.summary + type extras = extras_TransferFunctionsWCET - let report_cost summary instr cost nid reported_so_far = + let report_cost summary instr (cost: Itv.Bound.t) nid reported_so_far = + let mk_message () = + F.asprintf + "The excetution 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 + in match cost with - | Top -> - (cost, reported_so_far) - (* We don't report when the cost Top as it corresponds to 'don't know'*) - | _ -> - let above_expensive_threshold = not (CSI.( <= ) ~lhs:cost ~rhs:expensive_threshold) in + | b when Itv.Bound.is_not_infty b + -> ( + let above_expensive_threshold = not (Itv.Bound.le cost expensive_threshold) in match instr with | Sil.Call (_, _, _, loc, _) when above_expensive_threshold -> let ltr = [Errlog.make_trace_element 0 loc "" []] in - let message = - F.asprintf - "This instruction is expensive (estimated cost %a). Its execution time is likely \ - above the acceptable treshold " CSI.pp cost - in let exn = Exceptions.Checkers - (IssueType.expensive_execution_time_call, Localise.verbatim_desc message) + (IssueType.expensive_execution_time_call, Localise.verbatim_desc (mk_message ())) in Reporting.log_error summary ~loc ~ltr exn ; - (cost, RepSet.add nid reported_so_far) + (cost, ReportedOnNodes.add nid reported_so_far) | Sil.Load (_, _, _, loc) | Sil.Store (_, _, _, loc) | Sil.Call (_, _, _, loc, _) | Sil.Prune (_, loc, _, _) when above_expensive_threshold -> let ltr = [Errlog.make_trace_element 0 loc "" []] in - let message = - F.asprintf - "The execution time from the beginning of the function is above the acceptable \ - treshold (estimated cost %a up to here)" CSI.pp cost - in let exn = Exceptions.Checkers - (IssueType.expensive_execution_time_call, Localise.verbatim_desc message) + (IssueType.expensive_execution_time_call, Localise.verbatim_desc (mk_message ())) in Reporting.log_error summary ~loc ~ltr exn ; - (cost, RepSet.add nid reported_so_far) + (cost, ReportedOnNodes.add nid reported_so_far) | _ -> - (cost, reported_so_far) + (cost, reported_so_far) ) + | _ -> + (cost, reported_so_far) + (* We don't report when the cost is Top as it corresponds to 'don't know'*) (* get a list of nodes and check if we have already reported for at - least one of them. In that case no need to report again. *) + least one of them. In that case no need to report again. *) let should_report preds reported_so_far = List.for_all ~f:(fun n -> let n_id = (Procdesc.Node.get_id n :> int) in - not (RepSet.mem n_id reported_so_far) ) + not (ReportedOnNodes.mem n_id reported_so_far) ) preds let exec_instr (astate: Domain.astate) {ProcData.extras} (node: CFG.node) instr : Domain.astate = - let invariant_map_cost, trees, summary = extras in + let {basic_cost_map= invariant_map_cost; min_trees_map= trees; summary} = extras in let und_node = CFG.underlying_node node in let node_id = Procdesc.Node.get_id und_node in let preds = Procdesc.Node.get_preds und_node in - let map_cost m : CSI.astate = + let map_cost m : Itv.Bound.t = CostDomain.NodeInstructionToCostMap.fold (fun (nid, idx) c acc -> match Int.Map.find trees nid with | Some t -> - let c_node = CSI.mult c t in + let c_node = Itv.Bound.mult c t in L.(debug Analysis Medium) - "@\n [AnalizerWCTE] Adding cost: (%i,%i) --> c =%a t = %a @\n" nid idx CSI.pp c - CSI.pp t ; - let c_node' = CSI.plus acc c_node in + "@\n [AnalizerWCTE] Adding cost: (%i,%i) --> c =%a t = %a @\n" nid idx + Itv.Bound.pp c Itv.Bound.pp t ; + let c_node' = Itv.Bound.plus_u acc c_node in L.(debug Analysis Medium) "@\n [AnalizerWCTE] Adding cost: (%i,%i) --> c_node=%a cost = %a @\n" nid idx - CSI.pp c_node CSI.pp c_node' ; + Itv.Bound.pp c_node Itv.Bound.pp c_node' ; c_node' | _ -> assert false ) - m CSI.zero + m Itv.Bound.zero in let cost_node = match AnalyzerNodesBasicCost.extract_post node_id invariant_map_cost with @@ -562,7 +551,8 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct assert false in L.(debug Analysis Medium) - "@\n>>>AnalizerWCTE] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr CSI.pp cost_node ; + "@\n>>>AnalizerWCTE] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr Itv.Bound.pp + cost_node ; let reported_so_far = snd astate in let astate' = if should_report (und_node :: preds) reported_so_far then @@ -586,7 +576,7 @@ let checker ({Callbacks.tenv; summary; proc_desc} as proc_callback_args) : Specs List.fold ~f:(fun acc (n, t) -> let res = MinTree.evaluate_tree t in - L.(debug Analysis Medium) "@\n Tree %i eval to %a @\n" n CostDomain.Cost.pp res ; + L.(debug Analysis Medium) "@\n Tree %i eval to %a @\n" n Itv.Bound.pp res ; Int.Map.set acc ~key:n ~data:res ) ~init:Int.Map.empty min_trees in @@ -596,11 +586,12 @@ let checker ({Callbacks.tenv; summary; proc_desc} as proc_callback_args) : Specs (ProcData.make_default proc_desc tenv) ~initial:CostDomain.NodeInstructionToCostMap.empty ~debug:true in - let initWCET = (CostDomain.CostSingleIteration.zero, RepSet.empty) in + let initWCET = (Itv.Bound.zero, ReportedOnNodes.empty) in let invariant_map_WCETFinal = (* Final map with nodes cost *) AnalyzerWCET.exec_cfg cfg - (ProcData.make proc_desc tenv (invariant_map_NodesBasicCost, trees_valuation, summary)) + (ProcData.make proc_desc tenv + {basic_cost_map= invariant_map_NodesBasicCost; min_trees_map= trees_valuation; summary}) ~initial:initWCET ~debug:true in match AnalyzerWCET.extract_post (CFG.id (CFG.exit_node cfg)) invariant_map_WCETFinal with diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 6341d1f96..5cc36810e 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -83,7 +83,7 @@ module Cost = struct NonTop (c1' - c2') - let mult c1 c2 = + let _mult c1 c2 = match (c1, c2) with Top, _ | _, Top -> Top | NonTop c1', NonTop c2' -> NonTop (c1' * c2') @@ -105,7 +105,7 @@ module Cost = struct NonTop (Int.max c1' c2') - let one = NonTop 1 + let _one = NonTop 1 let zero = NonTop 0 @@ -133,7 +133,7 @@ module IntPair = struct end (* Map (node,instr) -> basic cost *) -module NodeInstructionToCostMap = AbstractDomain.Map (IntPair) (Cost) +module NodeInstructionToCostMap = AbstractDomain.Map (IntPair) (Itv.Bound) module ItvPureCost = struct (** (l, u) represents the closed interval [-l; u] (of course infinite bounds are open) *) @@ -346,9 +346,8 @@ module SemanticDomain = struct sem_unop op res1 | _ -> L.die InternalError " @\n Incomplete Sem function. Dies with e= %a @\n" Exp.pp e - end -type summary = {post: Cost.astate} +type summary = {post: Itv.Bound.t} -let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" Cost.pp post +let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" Itv.Bound.pp post diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index 9d3630f4c..b5d006b26 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -90,10 +90,19 @@ int FN_loop2(int k) { return 0; } +// This is currently evaluated to Top as the analysis is not powerful enough +int FN_loop3(int k) { + + for (int i = k; i < k + 15; i++) { + alias2_OK(); + } + return 0; +} + // Cost: 218 // Shows that calling many times non expensive function can // result in an expensive computation -int main() { +int main_bad() { int k1, k2, k3, k4; diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 22bfa3731..908039d2f 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -1,7 +1,7 @@ -codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, [] -codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, [] -codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, [] -codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, [] -codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, [] -codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, [] -codetoanalyze/c/performance/cost_test.c, main, 8, EXPENSIVE_EXECUTION_TIME_CALL, [] +codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, []