From 69bfc0535c70fc914c4f136e5e9e5ebfbaf25e51 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Wed, 28 Feb 2018 03:58:22 -0800 Subject: [PATCH] [Experimental] First very basic version of performance analysis tool Reviewed By: mbouaziz Differential Revision: D6910940 fbshipit-source-id: b2ea060 --- infer/src/backend/specs.ml | 13 +- infer/src/backend/specs.mli | 3 +- infer/src/base/Config.ml | 5 + infer/src/base/Config.mli | 2 + infer/src/base/IssueType.ml | 2 + infer/src/base/IssueType.mli | 2 + infer/src/base/Pp.ml | 2 +- infer/src/checkers/cost.ml | 559 ++++++++++++++++++ infer/src/checkers/costDomain.ml | 356 +++++++++++ infer/src/checkers/registerCheckers.ml | 6 +- .../codetoanalyze/c/performance/cost_test.c | 76 +++ 11 files changed, 1019 insertions(+), 7 deletions(-) create mode 100644 infer/src/checkers/cost.ml create mode 100644 infer/src/checkers/costDomain.ml create mode 100644 infer/tests/codetoanalyze/c/performance/cost_test.c diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 5a5f4a950..16fc4b7a7 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -269,7 +269,8 @@ type payload = ; resources: ResourceLeakDomain.summary option ; siof: SiofDomain.astate option ; typestate: unit TypeState.t option - ; uninit: UninitDomain.summary option } + ; uninit: UninitDomain.summary option + ; cost: CostDomain.summary option } type summary = { phase: phase (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) @@ -411,14 +412,15 @@ let pp_payload pe fmt ; litho ; buffer_overrun ; annot_map - ; uninit } = + ; uninit + ; cost } = let pp_opt prefix pp fmt = function | Some x -> F.fprintf fmt "%s: %a@\n" prefix pp x | None -> () in - F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a@\n" + F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a@\n" (pp_opt "PrePosts" (pp_specs pe)) (Option.map ~f:NormSpec.tospecs preposts) (pp_opt "TypeState" (TypeState.pp TypeState.unit_ext)) @@ -435,6 +437,8 @@ let pp_payload pe fmt annot_map (pp_opt "Uninitialised" UninitDomain.pp_summary) uninit + (pp_opt "Cost" CostDomain.pp_summary) + cost let pp_summary_text fmt summary = @@ -623,7 +627,8 @@ let empty_payload = ; racerd= None ; litho= None ; buffer_overrun= None - ; uninit= None } + ; uninit= None + ; cost= None } (** [init_summary (depend_list, nodes, diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 136ed90a1..a83ae8cf9 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -105,7 +105,8 @@ type payload = ; resources: ResourceLeakDomain.summary option ; siof: SiofDomain.astate option ; typestate: unit TypeState.t option - ; uninit: UninitDomain.summary option } + ; uninit: UninitDomain.summary option + ; cost: CostDomain.summary option } (** Procedure summary *) type summary = diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 96ae2aac0..459ffc3b8 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -673,6 +673,7 @@ and ( annotation_reachability , biabduction , bufferoverrun , check_nullable + , cost , crashcontext , eradicate , fragment_retains_view @@ -710,6 +711,7 @@ and ( annotation_reachability and check_nullable = mk_checker ~long:"check-nullable" "checks that values annotated with nullable are always checked for null before dereference" + and cost = mk_checker ~long:"cost" ~default:false "checker for performance cost analysis" and crashcontext = mk_checker ~long:"crashcontext" "the crashcontext checker for Java stack trace context reconstruction" @@ -783,6 +785,7 @@ and ( annotation_reachability , biabduction , bufferoverrun , check_nullable + , cost , crashcontext , eradicate , fragment_retains_view @@ -2361,6 +2364,8 @@ and compute_analytics = !compute_analytics and continue_capture = !continue +and cost = !cost + and current_to_previous_script = !current_to_previous_script and crashcontext = !crashcontext diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 3427efaaa..c811faf8e 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -300,6 +300,8 @@ val compute_analytics : bool val continue_capture : bool +val cost : bool + val crashcontext : bool val current_to_previous_script : string option diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 8d39fdb6e..4d22b28a5 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -222,6 +222,8 @@ let eradicate_value_not_present = from_string "ERADICATE_VALUE_NOT_PRESENT" ~hum:"Value Not Present" +let expensive_execution_time_call = from_string "EXPENSIVE_EXECUTION_TIME_CALL" + let failure_exe = from_string "Failure_exe" let field_should_be_nullable = from_string "FIELD_SHOULD_BE_NULLABLE" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 497caaaba..9db97408b 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -144,6 +144,8 @@ val eradicate_return_value_not_present : t val eradicate_value_not_present : t +val expensive_execution_time_call : t + val failure_exe : t val field_should_be_nullable : t diff --git a/infer/src/base/Pp.ml b/infer/src/base/Pp.ml index 79896341e..31f75bebd 100644 --- a/infer/src/base/Pp.ml +++ b/infer/src/base/Pp.ml @@ -116,7 +116,7 @@ let seq ?(print_env= text) ?sep:(sep_text = " ") ?(sep_html= sep_text) pp = let comma_seq ?print_env pp f l = seq ?print_env ~sep:"," pp f l -let semicolon_seq ?print_env pp f l = seq ?print_env ~sep:";" pp f l +let semicolon_seq ?print_env pp f l = seq ?print_env ~sep:"; " pp f l (** Print the current time and date in a format similar to the "date" command *) let current_time f () = diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml new file mode 100644 index 000000000..0c3c4dd21 --- /dev/null +++ b/infer/src/checkers/cost.ml @@ -0,0 +1,559 @@ +(* + * Copyright (c) 2017 - 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. + *) + +open! IStd +module F = Format +module L = Logging +open AbstractDomain.Types + +module Summary = Summary.Make (struct + type payload = CostDomain.summary + + let update_payload sum (summary: Specs.summary) = + {summary with payload= {summary.payload with cost= Some sum}} + + + let read_payload (summary: Specs.summary) = summary.payload.cost +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 + +(* CFG module used in several other modules *) +module CFG = ProcCfg.Normal + +(* Transfer function computing the semantics of the program. + Here semantics means: for each node a pair (env, alias) where + 1. env is an 'environment', i.e. a map from variables to values + 2 alias is an alias map. +*) +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 astate' = + match instr with + | Sil.Store (lhs, {Typ.desc= Tint _}, rhs, _) -> + let env' = CostDomain.SemanticDomain.update_env env lhs rhs in + let alias' = CostDomain.SemanticDomain.update_alias tenv alias lhs rhs in + (env', alias') + | Sil.Load (id, rhs, {Typ.desc= Tint _}, _) -> + let env' = CostDomain.SemanticDomain.update_env env (Exp.Var id) rhs in + let alias' = CostDomain.SemanticDomain.update_alias tenv alias (Exp.Var id) rhs in + (env', alias') + | Sil.Prune (e, _, _, _) -> ( + match CostDomain.SemanticDomain.sem env e with + | Some e', Some v -> + L.(debug Analysis Medium) "@\n e'= %a, v=%a @\n" Exp.pp e' CostDomain.ItvPureCost.pp v ; + let v' = + match CostDomain.EnvDomain.find_opt e' env with + | Some v_pre -> + L.(debug Analysis Medium) "@\n>>>Starting meet 2 \n" ; + let meet = CostDomain.ItvPureCost.meet v_pre v in + L.(debug Analysis Medium) + "@\n>>> Result Meet v_pre= %a e_val= %a --> %a\n" CostDomain.ItvPureCost.pp + v_pre CostDomain.ItvPureCost.pp v CostDomain.ItvPureCost.pp meet ; + if CostDomain.ItvPureCost.is_empty meet then v else meet + | None -> + v + in + let env' = CostDomain.EnvDomain.add e' v' env in + L.(debug Analysis Medium) + "@\n e'= %a, v'=%a @\n" Exp.pp e' CostDomain.ItvPureCost.pp v' ; + let env'' = CostDomain.SemanticDomain.update_alias_env env' alias e' in + (env'', alias) + | _ -> + (env, alias) ) + | Sil.Load _ + | Sil.Store _ + | Sil.Call _ + | Sil.Declare_locals _ + | Remove_temps _ + | Abstract _ + | Nullify _ -> + astate + in + 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 + of the number of times the program point can be executed in any execution. + The size of an environment env is computed as: + |env| = |env(v1)| * ... * |env(n_k)| + + where |env(v)| is the size of the interval associated to v by env. + + Reference: see Stefan Bygde PhD thesis, 2010 + +*) +module BoundMap = struct + let bound_map : CostDomain.Cost.astate Int.Map.t ref = ref Int.Map.empty + + let print_upper_bound_map () = + L.(debug Analysis Medium) "@\n\n******* Bound Map **** @\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" + + + let compute_upperbound_map cfg invariant_map = + let compute_node_upper_bound node = + let node_id = Procdesc.Node.get_id 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, _) -> + (* bound = env(v1) *... * env(vn) *) + let bound = + CostDomain.EnvDomain.fold + (fun exp itv acc -> + let itv' = + match exp with + | Exp.Lvar _ -> + itv + | Exp.Var _ -> + CostDomain.ItvPureCost.of_int 1 + (* For temp var we give [1,1] so it doesn't count*) + | _ -> + assert false + in + let itv_range = CostDomain.ItvPureCost.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) ; + CostDomain.Cost.mult acc itv_range ) + env CostDomain.Cost.one + in + L.(debug Analysis Medium) + "@\n>>>Setting bound for node = %i to %a@\n\n" + (node_id :> int) + CostDomain.Cost.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 + in + List.iter (CFG.nodes cfg) ~f:compute_node_upper_bound ; + print_upper_bound_map () + + + let upperbound nid = + match Int.Map.find !bound_map nid with + | Some bound -> + bound + | None -> + L.(debug Analysis Medium) + "@\n\n[WARNING] Bound not found for node %i, returning Top @\n" nid ; + Top +end + +(* Structural Constraints are expressions of the kind: + n <= n1 +...+ nk + + The informal meaning is: the number of times node n can be executed is less or + equal to the sum of the number of times nodes n1,..., nk can be executed. +*) +module StructuralConstraints = struct + let print_constraint_list constraints = + L.(debug Analysis Medium) "@\n\n******* Structural Constraints **** @\n" ; + List.iter ~f:(fun c -> L.(debug Analysis Medium) "@\n %a @\n" Exp.pp c) constraints ; + L.(debug Analysis Medium) "@\n******* END Structural Constraints **** @\n\n" + + + (* for each program point return a set of contraints of the kind + + i<=Sum_{j \in Predecessors(i) } j + i<=Sum_{j \in Successors(i)} j +*) + let compute_structural_constraints cfg = + let exp_nid n = + let nid = (Procdesc.Node.get_id n :> int) in + Exp.Const (Cint (IntLit.of_int nid)) + in + let rec exp_sum nodes = + match nodes with + | [] -> + assert false (* this cannot happen here *) + | [n] -> + exp_nid n + | n :: nodes' -> + let sum_nodes' = exp_sum nodes' in + Exp.BinOp (Binop.PlusA, exp_nid n, sum_nodes') + in + let compute_node_constraints acc node = + let constrants_preds_succs gets_preds_succs = + match gets_preds_succs node with + | [] -> + [] + | res_nodes -> + [Exp.BinOp (Binop.Le, exp_nid node, exp_sum res_nodes)] + in + let preds_con = constrants_preds_succs Procdesc.Node.get_preds in + let succs_con = constrants_preds_succs Procdesc.Node.get_succs in + preds_con @ succs_con @ acc + in + let constraints = List.fold (CFG.nodes cfg) ~f:compute_node_constraints ~init:[] in + print_constraint_list constraints ; constraints +end + +(* MinTree is used to compute: + + \max (\Sum_{n \in Nodes} c_n * x_n ) + + given a set of contraints on x_n. The constraints involve the contro flow + of the program. + +*) +module MinTree = struct + type mt_node = + | Leaf of (int * CostDomain.Cost.astate) + | Min of mt_node list + | Plus of mt_node list + + let add_leaf node nid leaf = + let leaf' = Leaf (nid, leaf) in + match node with Min l -> Min (leaf' :: l) | Plus l -> Plus (leaf' :: l) | _ -> assert false + + + let plus_seq pp f l = Pp.seq ~sep:" + " pp f l + + let rec pp fmt node = + match node with + | Leaf (nid, c) -> + F.fprintf fmt "%i:%a" nid CostDomain.Cost.pp c + | Min l -> + F.fprintf fmt "Min(%a)" (Pp.comma_seq pp) l + | Plus l -> + F.fprintf fmt "(%a)" (plus_seq pp) l + + + let add_child node child = + match child with + | Plus [] | Min [] -> + node (* if it's a dummy child, don't add it *) + | _ -> + match node with Plus l -> Plus (child :: l) | Min l -> Min (child :: l) | _ -> assert false + + + (* finds the subset of constraints of the form x_k <= x_j *) + let get_k_single_constraints constraints k = + List.filter_map + ~f:(fun c -> + match c with + (* constraint x_k <= x_j is represented by k<=j *) + | Exp.BinOp (Binop.Le, Exp.Const Cint k', Exp.Const Cint nid) + when Int.equal k (IntLit.to_int k') -> + Some (IntLit.to_int nid) + | _ -> + None ) + constraints + + + (* finds the subset of constraints of the form x_k <= x_j1 +...+ x_jn and +return the addends of the sum x_j1+x_j2+..+x_j_n*) + let get_k_sum_constraints constraints k = + let rec addends e = + match e with + | Exp.Const Cint nid -> + Int.Set.singleton (IntLit.to_int nid) + | Exp.BinOp (Binop.PlusA, e1, e2) -> + Int.Set.union (addends e1) (addends e2) + | _ -> + assert false + in + List.filter_map + ~f:(fun c -> + match c with + | Exp.BinOp (Binop.Le, Exp.Const Cint k', (Exp.BinOp (Binop.PlusA, _, _) as sum_exp)) + when Int.equal k (IntLit.to_int k') -> + Some (addends sum_exp) + | _ -> + None ) + constraints + + + let rec evaluate_tree t = + match t with + | Leaf (_, c) -> + c + | Min l -> + evaluate_operator CostDomain.Cost.min l + | Plus l -> + evaluate_operator CostDomain.Cost.plus l + + + and evaluate_operator op l = + match l with + | [] -> + assert false + | [c] -> + evaluate_tree c + | c :: l' -> + let res_c = evaluate_tree c in + let res_l' = evaluate_operator op l' in + op res_c res_l' + + + (* TO DO: replace equality on sets with something more efficient*) + let rec add_without_rep s list_of_sets = + match list_of_sets with + | [] -> + [s] + | s' :: tail -> + if Int.Set.equal s s' then list_of_sets else s' :: add_without_rep s tail + + + (* a plus node is well formed if has at least two addends *) + let is_well_formed_plus_node plus_node = + match plus_node with Plus (_ :: _ :: _) -> true | _ -> false + + + (* TO DO: rewrite in a functional way rather than imperative T26418766 *) + let rec minimum_propagation (q: int) (visited: Int.Set.t) (constraints: Exp.t list) = + let node = ref (Min []) in + let worklist : int Stack.t = Stack.create () in + Stack.push worklist q ; + let branch = ref [] in + let visited_acc = ref visited in + while not (Stack.is_empty worklist) do + let k = + match Stack.pop worklist with Some k' -> k' | None -> assert false + (* we cant be here *) + in + if Int.Set.mem !visited_acc k then () + else ( + visited_acc := Int.Set.add !visited_acc k ; + node := add_leaf !node k (BoundMap.upperbound k) ; + let k_constraints_upperbound = get_k_single_constraints constraints k in + List.iter + ~f:(fun ub_id -> if not (Int.Set.mem !visited_acc ub_id) then Stack.push worklist ub_id) + k_constraints_upperbound ; + let k_sum_constraints = get_k_sum_constraints constraints k in + List.iter + ~f:(fun set_addend -> + if Int.Set.is_empty (Int.Set.inter set_addend !visited_acc) then + branch := add_without_rep set_addend !branch ) + k_sum_constraints ) + done ; + List.iter + ~f:(fun addend -> + if Int.Set.length addend < 2 then assert false + else ( + L.(debug Analysis Medium) "@\n\n|Set addends| = %i {" (Int.Set.length addend) ; + Int.Set.iter ~f:(fun e -> L.(debug Analysis Medium) " %i, " e) addend ; + L.(debug Analysis Medium) " }@\n " ) ; + let plus_node = + Set.fold + ~f:(fun acc n -> + let child = minimum_propagation n !visited_acc constraints in + add_child acc child ) + ~init:(Plus []) addend + in + (* without this check it would add plus node with just one child, and give wrong results *) + if is_well_formed_plus_node plus_node then node := add_child !node plus_node ) + !branch ; + !node + + + let compute_trees_from_contraints cfg constraints = + let min_trees = + List.fold + ~f:(fun acc n -> + let nid = (Procdesc.Node.get_id n :> int) in + (nid, minimum_propagation nid Int.Set.empty constraints) :: acc ) + ~init:[] (CFG.nodes cfg) + in + List.iter ~f:(fun (n, t) -> L.(debug Analysis Medium) "@\n node %i = %a @\n" n pp t) min_trees ; + min_trees +end + +(* Compute a map (node,instruction) -> basic_cost, where basic_cost is the + cost known for a certain operation. For example for basic operation we + set it to 1 and for function call we take it from the spec of the function. + The nodes in the domain of the map are those in the path reaching the current node. +*) +module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = CostDomain.NodeInstructionToCostMap + + type extras = ProcData.no_extras + + let cost_atomic_instruction = CostDomain.Cost.one + + let instr_idx (node: CFG.node) instr = + match CFG.instrs node with + | [] -> + 0 + | instrs -> + List.find_mapi_exn + ~f:(fun idx i -> if Sil.equal_instr i instr then Some idx else None) + instrs + + + let exec_instr (astate: Domain.astate) {ProcData.pdesc} (node: CFG.node) instr : Domain.astate = + let nid_int = (Procdesc.Node.get_id (CFG.underlying_node node) :> int) in + let instr_idx = instr_idx node instr in + let key = (nid_int, instr_idx) in + let astate' = + match instr with + | Sil.Call (_, Exp.Const Const.Cfun callee_pname, _, _, _) -> ( + match Summary.read_summary pdesc callee_pname with + | Some {post= cost_callee} -> + Domain.add key cost_callee astate + | None -> + Domain.add key cost_atomic_instruction astate ) + | Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ -> + Domain.add key cost_atomic_instruction astate + | _ -> + astate + in + L.(debug Analysis Medium) + "@\n>>>Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr Domain.pp astate' ; + astate' +end + +module AnalyzerNodesBasicCost = AbstractInterpreter.Make (CFG) (TransferFunctionsNodesBasicCost) + +(* Calculate the final Worst Case Execution Time predicted for each node. + It uses the basic cost of the nodes (computed previously by AnalyzerNodesBasicCost) + and MinTrees which give an upperbound on the number of times a node can be executed +*) +module TransferFunctionsWCET (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = CostDomain.CostSingleIteration + + 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 exec_instr (_: Domain.astate) {ProcData.extras} (node: CFG.node) instr : Domain.astate = + let invariant_map_cost, trees, summary = extras in + let map_cost m : Domain.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 + 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 + 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' ; + c_node' + | _ -> + assert false ) + m Domain.zero + in + let astate' = + let node_id = Procdesc.Node.get_id (CFG.underlying_node node) in + 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 + | _ -> + assert false + in + L.(debug Analysis Medium) + "@\n>>>AnalizerWCTE] Instr: %a Cost: %a@\n" (Sil.pp_instr Pp.text) instr Domain.pp astate' ; + astate' +end + +module AnalyzerWCET = AbstractInterpreter.Make (CFG) (TransferFunctionsWCET) + +let checker {Callbacks.tenv; summary; proc_desc} : 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 + (* 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 + let min_trees = MinTree.compute_trees_from_contraints cfg constraints in + let trees_valuation = + 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 ; + Int.Map.set acc ~key:n ~data:res ) + ~init:Int.Map.empty min_trees + in + let invariant_map_NodesBasicCost = + (*compute_WCET cfg invariant_map min_trees in *) + AnalyzerNodesBasicCost.exec_cfg cfg + (ProcData.make_default proc_desc tenv) + ~initial:CostDomain.NodeInstructionToCostMap.empty ~debug:true + 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 + in + match AnalyzerWCET.extract_post (CFG.id (CFG.exit_node cfg)) invariant_map_WCETFinal with + | Some exit_cost -> + Summary.update_summary {post= exit_cost} summary + | None -> + if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then ( + L.internal_error "Failed to compute final cost for function %a" Typ.Procname.pp + (Procdesc.get_proc_name proc_desc) ; + summary ) + else summary diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml new file mode 100644 index 000000000..3dcb309d0 --- /dev/null +++ b/infer/src/checkers/costDomain.ml @@ -0,0 +1,356 @@ +(* + * Copyright (c) 2017 - 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. + *) + +open! IStd +module F = Format +module L = Logging +open AbstractDomain.Types + +module Alias = struct + type astate = Prop.pi + + let pp = Prop.pp_pi Pp.text + + let join pi1 pi2 = pi1 @ pi2 + + let widen ~prev ~next:_ ~num_iters:_ = prev + + (* DINO: ??? what should be this one?*) + + let ( <= ) ~lhs:_ ~rhs:_ = true + + (*DINO: ???? what should be this one?*) +end + +module IntCost = struct + type astate = int [@@deriving compare] + + let pp fmt i = F.fprintf fmt "%i" i + + let join = Int.max + + let widen ~prev:_ ~next:_ ~num_iters:_ = assert false + + let ( <= ) ~lhs ~rhs = Int.( <= ) lhs rhs +end + +module Cost = struct + include AbstractDomain.TopLifted (IntCost) + + let widen ~prev ~next ~num_iters:_ = + if phys_equal prev next then prev + else + match (prev, next) with + | NonTop prev, NonTop next when IntCost.( <= ) ~lhs:next ~rhs:prev -> + NonTop prev + | _, _ -> + Top + + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | Top, Top | NonTop _, Top -> + true + | Top, NonTop _ -> + false + | NonTop c1, NonTop c2 -> + Int.( <= ) c1 c2 + + + let plus c1 c2 = + match (c1, c2) with + | Top, _ -> + Top + | _, Top -> + Top + | NonTop c1', NonTop c2' -> + NonTop (c1' + c2') + + + let _minus c1 c2 = + match (c1, c2) with + | Top, _ -> + Top + | _, Top -> + assert false (* ????? *) + | NonTop c1', NonTop c2' -> + NonTop (c1' - c2') + + + let mult c1 c2 = + match (c1, c2) with Top, _ | _, Top -> Top | NonTop c1', NonTop c2' -> NonTop (c1' * c2') + + + let min c1 c2 = + match (c1, c2) with + | Top, _ -> + c2 + | _, Top -> + c1 + | NonTop c1', NonTop c2' -> + NonTop (Int.min c1' c2') + + + let max c1 c2 = + match (c1, c2) with + | Top, _ | _, Top -> + Top + | NonTop c1', NonTop c2' -> + NonTop (Int.max c1' c2') + + + let one = NonTop 1 + + let zero = NonTop 0 + + let nth n = NonTop n + + let dec n = match n with NonTop n' -> NonTop (n' - 1) | _ -> n + + let inc n = match n with NonTop n' -> NonTop (n' + 1) | _ -> n + + let pp_l fmt c = + let c'' = match c with Top -> Top | NonTop c' -> NonTop (-c') in + pp fmt c'' + + + let pp_u = pp +end + +module CostSingleIteration = Cost + +module IntPair = struct + (* Represents node id,instr index within node *) + include AbstractDomain.Pair (IntCost) (IntCost) + + type t = IntCost.astate * IntCost.astate [@@deriving compare] +end + +(* Map (node,instr) -> basic cost *) +module NodeInstructionToCostMap = AbstractDomain.Map (IntPair) (Cost) + +module ItvPureCost = struct + (** (l, u) represents the closed interval [-l; u] (of course infinite bounds are open) *) + type astate = Cost.astate * Cost.astate + + type t = astate + + let ( <= ) : lhs:t -> rhs:t -> bool = + fun ~lhs:(l1, u1) ~rhs:(l2, u2) -> Cost.( <= ) ~lhs:l1 ~rhs:l2 && Cost.( <= ) ~lhs:u1 ~rhs:u2 + + + let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Cost.join l1 l2, Cost.join u1 u2) + + let meet (l1, u1) (l2, u2) = + let l = match (l1, l2) with Top, _ -> l2 | _, Top -> l1 | _, _ -> Cost.max l1 l2 in + L.(debug Analysis Medium) + "@\n l1= %a, l2=%a l/max=%a @\n" Cost.pp_l l1 Cost.pp_l l2 Cost.pp_l l ; + (* l1 l2 are negative so we use min instead of max *) + let u = Cost.min u1 u2 in + L.(debug Analysis Medium) + "@\n u1= %a, u2=%a u/min=%a @\n" Cost.pp_u u1 Cost.pp_u u2 Cost.pp_u u ; + (l, u) + + + let widen : prev:t -> next:t -> num_iters:int -> t = + fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters -> + (Cost.widen ~prev:l1 ~next:l2 ~num_iters, Cost.widen ~prev:u1 ~next:u2 ~num_iters) + + + let pp : F.formatter -> t -> unit = + fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Cost.pp_l l Cost.pp_u u + + + let of_int n = (Cost.nth (-n), Cost.nth n) + + let of_int_lit i = of_int (IntLit.to_int i) + + (* range [-a,b] = (b+a+1) *) + let range (l, u) = Cost.inc (Cost.plus u l) + + let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Cost.plus l1 l2, Cost.plus u1 u2) + + (* a const interval is of type [-n,n] *) + let is_const (l, u) = + match (l, u) with NonTop l', NonTop u' -> Int.equal (-l') u' | _, _ -> false + + + let is_empty itv = Cost.( <= ) ~lhs:(range itv) ~rhs:Cost.zero + + let negation (u, l) = (l, u) +end + +module EnvDomain = AbstractDomain.Map (Exp) (ItvPureCost) + +module SemanticDomain = struct + include AbstractDomain.Pair (EnvDomain) (Alias) + + let get_val env e = + match e with + | Exp.Var _ | Exp.Lvar _ -> ( + match EnvDomain.find_opt e env with + | Some c -> + c + | None -> + L.(debug Analysis Medium) + " @\n[WARNING:] Expression %a not found on env. Returning zero@\n" Exp.pp e ; + ItvPureCost.of_int 0 ) + | Exp.Const Cint i -> + ItvPureCost.of_int (IntLit.to_int i) + | _ -> + L.(debug Analysis Medium) " @\n[WARNING:] Returning value zero for %a @\n" Exp.pp e ; + ItvPureCost.of_int 0 + + + let eval_bin_op op val1 val2 = + match op with Binop.PlusA -> ItvPureCost.plus val1 val2 | _ -> assert false + + + let update_env env lhs rhs = + let open Exp in + match rhs with + | Var _ | UnOp _ -> + env + | BinOp (op, e1, e2) -> + let val1 = get_val env e1 in + let val2 = get_val env e2 in + let res = eval_bin_op op val1 val2 in + L.(debug Analysis Medium) + " @\n #### Operation: %a val1= %a val2=%a res = %a@\n" Exp.pp rhs ItvPureCost.pp + val1 ItvPureCost.pp val2 ItvPureCost.pp res ; + L.(debug Analysis Medium) + " @\nAdding binding %a --> %a to env o@\n" Exp.pp lhs ItvPureCost.pp res ; + EnvDomain.add lhs res env + | Const Cint i -> + (*let lhs_var = Var.of_pvar lhs in*) + let itv = ItvPureCost.of_int_lit i in + EnvDomain.add lhs itv env + | Lvar _ -> + let val_rhs = get_val env rhs in + L.(debug Analysis Medium) + " @\nAdding binding %a --> %a to env o@\n" Exp.pp lhs ItvPureCost.pp val_rhs ; + EnvDomain.add lhs val_rhs env + | Exn _ | Closure _ | Const _ | Cast _ | Lfield _ | Lindex _ | Sizeof _ -> + env + + + let remove_from_alias_list alias e = + let remove_exp a = + match a with Sil.Aeq (e1, e2) when Exp.equal e1 e || Exp.equal e e2 -> false | _ -> true + in + List.filter ~f:remove_exp alias + + + let update_alias tenv alias e1 e2 = + match (e1, e2) with + | Exp.Var _, Exp.Var _ | Exp.Var _, Exp.Lvar _ | Exp.Lvar _, Exp.Var _ | Exp.Lvar _, Exp.Lvar _ -> + (*Sil.Aeq (e1,e2) :: alias*) + let alias' = remove_from_alias_list alias e1 in + let prop = Prop.normalize tenv (Prop.from_pi alias') in + let prop' = Prop.conjoin_eq tenv e1 e2 prop in + Prop.get_pure prop' + | Exp.Lvar _, _ -> + remove_from_alias_list alias e1 + | _ -> + alias + + + (* Try to improve value for e using alias variables to get the tightest interval *) + let update_alias_env env alias e = + let try_restrict_itv env_acc e' e_val = + let v' = + match EnvDomain.find_opt e' env_acc with + | Some v_pre -> + L.(debug Analysis Medium) "@\n>>>Starting meet \n" ; + let meet = ItvPureCost.meet v_pre e_val in + L.(debug Analysis Medium) + "@\n>>>Result Meet v_pre= %a e_val= %a --> %a\n" ItvPureCost.pp v_pre + ItvPureCost.pp e_val ItvPureCost.pp meet ; + if ItvPureCost.is_empty meet then e_val else meet + | None -> + e_val + in + EnvDomain.add e' v' env_acc + in + let do_atom env_acc e_val a = + match a with + | Sil.Aeq (e1, e2) -> + if Exp.equal e1 e then try_restrict_itv env_acc e2 e_val + else if Exp.equal e2 e then try_restrict_itv env_acc e1 e_val + else env_acc + | _ -> + env + in + match EnvDomain.find_opt e env with + | Some e_val -> + List.fold ~f:(fun acc a -> do_atom acc e_val a) ~init:env alias + | _ -> + env + + + let sem_binop op (e1_opt, v1_opt) (e2_opt, v2_opt) = + let open Binop in + match op with + | Lt -> ( + match ((e1_opt, v1_opt), (e2_opt, v2_opt)) with + | (Some e, _), (_, Some (v1, v2)) when ItvPureCost.is_const (v1, v2) -> + let ub = Cost.dec v2 in + (Some e, Some (Top, ub)) + | (Some e1, Some v1), (Some e2, Some v2) -> + L.die InternalError + " @\n Incomplete Lt binon. Dies with (e1,v1)= (%a,%a) (e2,v2)=(%a, %a) @\n" Exp.pp e1 + ItvPureCost.pp v1 Exp.pp e2 ItvPureCost.pp v2 + | (Some e1, None), (Some e2, None) -> + L.die InternalError + " @\n Incomplete Lt binon. Dies with (e1,v1)= (%a,None) (e2,v2)=(%a,None) @\n" Exp.pp + e1 Exp.pp e2 + | _ -> + assert false ) + | Gt | Le | Ge | Eq | _ -> + L.die InternalError " @\n Incomplete Sem_binop function. Dies with op= %s @\n" + (Binop.str Pp.text op) + + + let sem_unop op (e1_opt, v1_opt) = + match op with + | Unop.LNot -> ( + match (e1_opt, v1_opt) with + | Some e, Some v -> + (Some e, Some (ItvPureCost.negation v)) + | _ -> + assert false ) + | _ -> + L.die InternalError " @\n Incomplete Sem_unop function. Dies with op= %s @\n" (Unop.str op) + + + (* semantics of expression e according to environment env *) + let rec sem env e : Exp.t option * ItvPureCost.t option = + match e with + | Exp.BinOp (op, e1, e2) -> + let res1 = sem env e1 in + let res2 = sem env e2 in + sem_binop op res1 res2 + | Exp.Const Cint i -> + (None, Some (ItvPureCost.of_int_lit i)) + | Exp.Lvar _ | Exp.Var _ -> + (Some e, None) + | Exp.UnOp (op, e1, _) -> + let res1 = sem env e1 in + sem_unop op res1 + | _ -> + 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} + +let pp_summary fmt {post} = F.fprintf fmt "@\n Post: %a @\n" Cost.pp post diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 2662572d7..7597b5c7e 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -98,7 +98,11 @@ let all_checkers = ; {name= "SIOF"; active= Config.siof; callbacks= [(Procedure Siof.checker, Language.Clang)]} ; { name= "uninitialized variables" ; active= Config.uninit - ; callbacks= [(Procedure Uninit.checker, Language.Clang)] } ] + ; callbacks= [(Procedure Uninit.checker, Language.Clang)] } + ; { name= "cost analysis" + ; active= Config.cost + ; callbacks= [(Procedure Cost.checker, Language.Clang); (Procedure Cost.checker, Language.Java)] + } ] let get_active_checkers () = diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c new file mode 100644 index 000000000..eccc67a1b --- /dev/null +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -0,0 +1,76 @@ +/* + * 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. + */ +int foo() { + int i, j; + i = 17; + j = 31; + + return i + j + 3 + 7; +} + +int bar() { + + int j = 0; + + j++; + j++; + j++; + j = foo(); + j++; + + return j; +} + +int cond(int i) { + int x; + + if (i < 0) { + x = bar(); + } else { + x = 1; + } + return x; +} + +void alias() { + + int i, j; + + j = i; + i = ++i; +} + +void alias2() { + + int i, j, z; + + j = 1; + z = 2; + + j = i; + i = z; +} + +int loop0() { + + for (int i = 0; i < 100; i++) { + alias2(); + } + return 0; +} + +int main() { + + int k; + + cond(2); + k = bar() + foo() * 2; + + return 0; +}