From d2cc5e72f791d5576397e3f95806bb86d34456ae Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Fri, 9 Mar 2018 01:29:39 -0800 Subject: [PATCH] Extending analysis to parametric case Reviewed By: mbouaziz Differential Revision: D7179463 fbshipit-source-id: 1711a0e --- .../src/bufferoverrun/bufferOverrunChecker.ml | 9 + .../bufferoverrun/bufferOverrunChecker.mli | 6 + infer/src/checkers/cost.ml | 191 +++++++++++------- infer/src/checkers/costDomain.ml | 4 +- .../codetoanalyze/c/performance/Makefile | 20 ++ .../codetoanalyze/c/performance/cost_test.c | 56 +++-- .../codetoanalyze/c/performance/issues.exp | 7 + 7 files changed, 209 insertions(+), 84 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/performance/Makefile create mode 100644 infer/tests/codetoanalyze/c/performance/issues.exp diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index bbf64eaa1..aaaa35412 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -308,6 +308,8 @@ end module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) module CFG = Analyzer.TransferFunctions.CFG +type invariant_map = Analyzer.invariant_map + module Report = struct (* I'd like to avoid rebuilding this :( Everything depend on CFG only because of `get_allocsite` *) @@ -543,6 +545,13 @@ module Report = struct PO.ConditionSet.check_all ~report cond_set end +let compute_invariant_map : Callbacks.proc_callback_args -> Analyzer.invariant_map = + fun {proc_desc; tenv; get_proc_desc} -> + Preanal.do_preanalysis proc_desc tenv ; + let pdata = ProcData.make proc_desc tenv get_proc_desc in + Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata + + let extract_post inv_map node = let id = CFG.id node in Analyzer.extract_post id inv_map diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index 5b1dbca2a..4d6750e2c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/infer/src/bufferoverrun/bufferOverrunChecker.mli @@ -10,3 +10,9 @@ open! IStd val checker : Callbacks.proc_callback_t + +type invariant_map + +val compute_invariant_map : Callbacks.proc_callback_args -> invariant_map + +val extract_post : invariant_map -> Procdesc.Node.t -> BufferOverrunDomain.Mem.astate option diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 0c3c4dd21..81839d8bb 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -38,9 +38,7 @@ module TransferFunctionsSemantics (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = CostDomain.SemanticDomain - type extras = ProcData.no_extras - - let exec_instr ((env, alias) as astate: Domain.astate) {ProcData.tenv} _ instr = + let _exec_instr ((env, alias) as astate: Domain.astate) {ProcData.tenv} _ instr = let astate' = match instr with | Sil.Store (lhs, {Typ.desc= Tint _}, rhs, _) -> @@ -86,9 +84,6 @@ module TransferFunctionsSemantics (CFG : ProcCfg.S) = struct astate' end -(* TODO: use inferbo for the parametric version *) -module AnalyzerSemantics = AbstractInterpreter.Make (CFG) (TransferFunctionsSemantics) - (* Map associating to each node a bound on the number of times it can be executed. This bound is computed using environments (map: val -> values), using the following observation: the number of environments associated with a program point is an upperbound @@ -111,34 +106,71 @@ module BoundMap = struct L.(debug Analysis Medium) "@\n******* END Bound Map **** @\n\n" + let convert (mem: BufferOverrunDomain.Mem.astate) : CostDomain.EnvDomainBO.astate = + let open AbstractDomain.Types in + match mem with + | Bottom -> + assert false + | NonBottom {BufferOverrunDomain.MemReach.heap} -> + let env = + BufferOverrunDomain.Heap.fold + (fun loc data acc -> + match loc with + | AbsLoc.Loc.Var Var.LogicalVar id -> + let key = Exp.Var id in + CostDomain.EnvDomain.add key (BufferOverrunDomain.Val.get_itv data) acc + | AbsLoc.Loc.Var Var.ProgramVar v -> + let key = Exp.Lvar v in + CostDomain.EnvDomain.add key (BufferOverrunDomain.Val.get_itv data) acc + | _ -> + acc ) + heap CostDomain.EnvDomainBO.empty + in + 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_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 | _ -> - match AnalyzerSemantics.extract_post node_id invariant_map with - | Some (env, _) -> + match entry_mem_opt with + | Some entry_mem -> + let env = convert entry_mem in (* bound = env(v1) *... * env(vn) *) let bound = - CostDomain.EnvDomain.fold + CostDomain.EnvDomainBO.fold (fun exp itv acc -> let itv' = match exp with | Exp.Lvar _ -> itv | Exp.Var _ -> - CostDomain.ItvPureCost.of_int 1 + Itv.one (* For temp var we give [1,1] so it doesn't count*) | _ -> assert false in - let itv_range = CostDomain.ItvPureCost.range itv' in + let itv_range = range itv' in L.(debug Analysis Medium) - "@\n>>>LB =%a and UB =%a UB-LB =%a for node = %i @\n\n" CostDomain.Cost.pp - (fst itv') CostDomain.Cost.pp (snd itv') CostDomain.Cost.pp itv_range - (node_id :> int) ; + "@\n>>>For node = %i : 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 in @@ -430,6 +462,7 @@ module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct end module AnalyzerNodesBasicCost = AbstractInterpreter.Make (CFG) (TransferFunctionsNodesBasicCost) +module RepSet = AbstractDomain.FiniteSet (Int) (* Calculate the final Worst Case Execution Time predicted for each node. It uses the basic cost of the nodes (computed previously by AnalyzerNodesBasicCost) @@ -437,93 +470,114 @@ module AnalyzerNodesBasicCost = AbstractInterpreter.Make (CFG) (TransferFunction *) module TransferFunctionsWCET (CFG : ProcCfg.S) = struct module CFG = CFG - module Domain = CostDomain.CostSingleIteration + module CSI = CostDomain.CostSingleIteration + module Domain = AbstractDomain.Pair (CSI) (RepSet) type extras = (* extras: (map with basic costs, min trees map, summary ) *) AnalyzerNodesBasicCost.invariant_map * CostDomain.Cost.astate Int.Map.t * Specs.summary - let report_cost summary instr cost = - match instr with - | Sil.Call (_, _, _, loc, _) when not (Domain.( <= ) ~lhs:cost ~rhs: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 " Domain.pp cost - in - let exn = - Exceptions.Checkers - (IssueType.expensive_execution_time_call, Localise.verbatim_desc message) - in - Reporting.log_error summary ~loc ~ltr exn - | Sil.Load (_, _, _, loc) - | Sil.Store (_, _, _, loc) - | Sil.Call (_, _, _, loc, _) - | Sil.Prune (_, loc, _, _) - when not (Domain.( <= ) ~lhs:cost ~rhs: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)" Domain.pp cost - in - let exn = - Exceptions.Checkers - (IssueType.expensive_execution_time_call, Localise.verbatim_desc message) - in - Reporting.log_error summary ~loc ~ltr exn + let report_cost summary instr cost nid reported_so_far = + 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 + 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) + in + Reporting.log_error summary ~loc ~ltr exn ; + (cost, RepSet.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) + in + Reporting.log_error summary ~loc ~ltr exn ; + (cost, RepSet.add nid reported_so_far) + | _ -> + (cost, reported_so_far) + + (* 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. *) + 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) ) + preds - let exec_instr (_: Domain.astate) {ProcData.extras} (node: CFG.node) instr : Domain.astate = + + let exec_instr (astate: Domain.astate) {ProcData.extras} (node: CFG.node) instr : Domain.astate = let invariant_map_cost, trees, summary = extras in - let map_cost m : Domain.astate = + 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 = CostDomain.NodeInstructionToCostMap.fold (fun (nid, idx) c acc -> match Int.Map.find trees nid with | Some t -> - let c_node = Domain.mult c t in + let c_node = CSI.mult c t in L.(debug Analysis Medium) - "@\n [AnalizerWCTE] Adding cost: (%i,%i) --> c =%a t = %a @\n" nid idx Domain.pp - c Domain.pp t ; - let c_node' = Domain.plus acc c_node in + "@\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 L.(debug Analysis Medium) "@\n [AnalizerWCTE] Adding cost: (%i,%i) --> c_node=%a cost = %a @\n" nid idx - Domain.pp c_node Domain.pp c_node' ; - report_cost summary instr c_node' ; + CSI.pp c_node CSI.pp c_node' ; c_node' | _ -> assert false ) - m Domain.zero + m CSI.zero in - let astate' = - let node_id = Procdesc.Node.get_id (CFG.underlying_node node) in + let cost_node = match AnalyzerNodesBasicCost.extract_post node_id invariant_map_cost with | Some node_map -> L.(debug Analysis Medium) "@\n AnalizerWCTE] Final map for node: %a @\n" Procdesc.Node.pp_id node_id ; - let map_cost = map_cost node_map in - map_cost + map_cost node_map | _ -> assert false in L.(debug Analysis Medium) - "@\n>>>AnalizerWCTE] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr Domain.pp astate' ; + "@\n>>>AnalizerWCTE] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr CSI.pp cost_node ; + let reported_so_far = snd astate in + let astate' = + if should_report (und_node :: preds) reported_so_far then + report_cost summary instr cost_node (node_id :> int) reported_so_far + else (cost_node, reported_so_far) + in astate' end module AnalyzerWCET = AbstractInterpreter.Make (CFG) (TransferFunctionsWCET) -let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = +let checker ({Callbacks.tenv; summary; proc_desc} as proc_callback_args) : Specs.summary = let cfg = CFG.from_pdesc proc_desc in (* computes the semantics: node -> (environment, alias map) *) - let semantics_invariant_map = - AnalyzerSemantics.exec_cfg cfg - (ProcData.make_default proc_desc tenv) - ~initial:(CostDomain.EnvDomain.empty, []) ~debug:true - in + let semantics_invariant_map = BufferOverrunChecker.compute_invariant_map proc_callback_args in (* given the semantics computes the upper bound on the number of times a node could be executed *) BoundMap.compute_upperbound_map cfg semantics_invariant_map ; let constraints = StructuralConstraints.compute_structural_constraints cfg in @@ -542,14 +596,15 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = (ProcData.make_default proc_desc tenv) ~initial:CostDomain.NodeInstructionToCostMap.empty ~debug:true in + let initWCET = (CostDomain.CostSingleIteration.zero, RepSet.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)) - ~initial:CostDomain.CostSingleIteration.zero ~debug:true + ~initial:initWCET ~debug:true in match AnalyzerWCET.extract_post (CFG.id (CFG.exit_node cfg)) invariant_map_WCETFinal with - | Some exit_cost -> + | Some (exit_cost, _) -> Summary.update_summary {post= exit_cost} summary | None -> if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then ( diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml index 3dcb309d0..6341d1f96 100644 --- a/infer/src/checkers/costDomain.ml +++ b/infer/src/checkers/costDomain.ml @@ -187,6 +187,7 @@ module ItvPureCost = struct end module EnvDomain = AbstractDomain.Map (Exp) (ItvPureCost) +module EnvDomainBO = AbstractDomain.Map (Exp) (Itv) module SemanticDomain = struct include AbstractDomain.Pair (EnvDomain) (Alias) @@ -346,9 +347,6 @@ module SemanticDomain = struct | _ -> L.die InternalError " @\n Incomplete Sem function. Dies with e= %a @\n" Exp.pp e - - let pp fmt (env, alias) = - F.fprintf fmt "@\n env: %a @\n alias: [ %a ] @\n" EnvDomain.pp env Alias.pp alias end type summary = {post: Cost.astate} diff --git a/infer/tests/codetoanalyze/c/performance/Makefile b/infer/tests/codetoanalyze/c/performance/Makefile new file mode 100644 index 000000000..bedd10ad1 --- /dev/null +++ b/infer/tests/codetoanalyze/c/performance/Makefile @@ -0,0 +1,20 @@ +# Copyright (c) 2018 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +# see explanations in cpp/errors/Makefile for the custom isystem +CLANG_OPTIONS = -c +INFER_OPTIONS = --cost-only --debug-exceptions --project-root $(TESTS_DIR) +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.c) + +include $(TESTS_DIR)/clang.make + +infer-out/report.json: $(MAKEFILE_LIST) diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index eccc67a1b..9d3630f4c 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -6,7 +6,8 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ -int foo() { +// Cost: 5 +int foo_OK() { int i, j; i = 17; j = 31; @@ -14,31 +15,34 @@ int foo() { return i + j + 3 + 7; } -int bar() { +// Cost: 17 +int bar_OK() { int j = 0; j++; j++; j++; - j = foo(); + j = foo_OK(); j++; return j; } -int cond(int i) { +// Cost: 25 +int cond_OK(int i) { int x; if (i < 0) { - x = bar(); + x = bar_OK(); } else { x = 1; } return x; } -void alias() { +// Cost: 5 +void alias_OK() { int i, j; @@ -46,7 +50,8 @@ void alias() { i = ++i; } -void alias2() { +// Cost: 6 +void alias2_OK() { int i, j, z; @@ -57,20 +62,45 @@ void alias2() { i = z; } -int loop0() { +// Cost: 1004 +int loop0_bad() { for (int i = 0; i < 100; i++) { - alias2(); + alias2_OK(); } return 0; } -int main() { +// Cost: 1006 +int loop1_bad() { + + int k = 100; + for (int i = 0; i < k; i++) { + alias2_OK(); + } + return 0; +} + +// This is currently evaluated to Top as the analysis is not powerful enough +int FN_loop2(int k) { - int k; + for (int i = 0; i < k; i++) { + alias2_OK(); + } + return 0; +} + +// Cost: 218 +// Shows that calling many times non expensive function can +// result in an expensive computation +int main() { - cond(2); - k = bar() + foo() * 2; + int k1, k2, k3, k4; + cond_OK(2); + k1 = bar_OK() + foo_OK() + cond_OK(15) * 2; + k2 = bar_OK() + foo_OK() + cond_OK(17) * 3; + k3 = bar_OK() + foo_OK() + cond_OK(11) * 3; + k4 = bar_OK() + foo_OK() + cond_OK(19) * 3; return 0; } diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp new file mode 100644 index 000000000..22bfa3731 --- /dev/null +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -0,0 +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, []