From bbd6820ca1a97bec6f8eda29755a075e379ac4fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 8 Jun 2018 10:39:48 -0700 Subject: [PATCH] Get rid of data dep analysis and localize it to single step Reviewed By: mbouaziz Differential Revision: D8330899 fbshipit-source-id: 84fb46c --- infer/src/IR/Procdesc.ml | 21 +++ infer/src/IR/Procdesc.mli | 3 + infer/src/IR/Var.ml | 5 + infer/src/IR/Var.mli | 3 + infer/src/backend/errdesc.ml | 31 +--- infer/src/checkers/control.ml | 145 +++++------------- infer/src/checkers/cost.ml | 16 +- .../codetoanalyze/java/performance/issues.exp | 13 +- 8 files changed, 89 insertions(+), 148 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 8d166d801..98d98fbbe 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -112,6 +112,27 @@ module Node = struct n |> get_instrs |> Instrs.last |> Option.value_map ~f:Sil.instr_get_loc ~default:n.loc + let find_in_node_or_preds = + let rec find ~f visited nodes = + match nodes with + | node :: nodes when not (NodeSet.mem node visited) + -> ( + let instrs = get_instrs node in + match Instrs.find_map ~f:(f node) instrs with + | Some res -> + Some res + | None -> + let nodes = get_preds node |> List.rev_append nodes in + let visited = NodeSet.add node visited in + find ~f visited nodes ) + | _ :: nodes -> + find ~f visited nodes + | _ -> + None + in + fun start_node ~f -> find ~f NodeSet.empty [start_node] + + let pp_id f id = F.pp_print_int f id let pp f node = pp_id f (get_id node) diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index e772dfca1..d9af63426 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -75,6 +75,9 @@ module Node : sig val get_last_loc : t -> Location.t (** Get the source location of the last instruction in the node *) + val find_in_node_or_preds : t -> f:(t -> Sil.instr -> 'a option) -> 'a option + (** Find in the given node or its predecessors *) + val get_loc : t -> Location.t (** Get the source location of the node *) diff --git a/infer/src/IR/Var.ml b/infer/src/IR/Var.ml index d128904a5..f6e2a4ac3 100644 --- a/infer/src/IR/Var.ml +++ b/infer/src/IR/Var.ml @@ -36,6 +36,11 @@ let is_return = function ProgramVar pvar -> Pvar.is_return pvar | LogicalVar _ - let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id +let get_all_vars_in_exp e = + let acc = Exp.free_vars e |> Sequence.map ~f:of_id in + Exp.program_vars e |> Sequence.map ~f:of_pvar |> Sequence.append acc + + let appears_in_source_code = function | LogicalVar _ -> false diff --git a/infer/src/IR/Var.mli b/infer/src/IR/Var.mli index 0d81ed1c1..94e447bba 100644 --- a/infer/src/IR/Var.mli +++ b/infer/src/IR/Var.mli @@ -22,6 +22,9 @@ val of_pvar : Pvar.t -> t val of_formal_index : int -> t (** Create a variable representing the ith formal of the current procedure *) +val get_all_vars_in_exp : Exp.t -> t Sequence.t +(** Get all free and program vars *) + val to_exp : t -> Exp.t val is_global : t -> bool diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 134a20200..65cdfc0f0 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -78,27 +78,6 @@ let explain_deallocate_constant_string s ra = let verbose = Config.trace_error -let find_in_node_or_preds = - let rec find ~f visited nodes = - match nodes with - | node :: nodes when not (Procdesc.NodeSet.mem node visited) - -> ( - let instrs = Procdesc.Node.get_instrs node in - match Instrs.find_map ~f:(f node) instrs with - | Some res -> - Some res - | None -> - let nodes = Procdesc.Node.get_preds node |> List.rev_append nodes in - let visited = Procdesc.NodeSet.add node visited in - find ~f visited nodes ) - | _ :: nodes -> - find ~f visited nodes - | _ -> - None - in - fun start_node ~f -> find ~f Procdesc.NodeSet.empty [start_node] - - (** Find the function call instruction used to initialize normal variable [id], and return the function name and arguments *) let find_normal_variable_funcall (node: Procdesc.Node.t) (id: Ident.t) @@ -109,7 +88,7 @@ let find_normal_variable_funcall (node: Procdesc.Node.t) (id: Ident.t) | _ -> None in - let res = find_in_node_or_preds node ~f:find_declaration in + let res = Procdesc.Node.find_in_node_or_preds node ~f:find_declaration in if verbose && is_none res then ( L.d_str ( "find_normal_variable_funcall could not find " ^ Ident.to_string id ^ " in node " @@ -126,7 +105,7 @@ let find_program_variable_assignment node pvar : (Procdesc.Node.t * Ident.t) opt | _ -> None in - find_in_node_or_preds node ~f:find_instr + Procdesc.Node.find_in_node_or_preds node ~f:find_instr (** Special case for C++, where we translate code like @@ -145,7 +124,7 @@ let find_struct_by_value_assignment node pvar = | _ -> None in - find_in_node_or_preds node ~f:find_instr + Procdesc.Node.find_in_node_or_preds node ~f:find_instr else None @@ -157,7 +136,7 @@ let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option = | _ -> None in - find_in_node_or_preds node ~f:find_instr + Procdesc.Node.find_in_node_or_preds node ~f:find_instr (** Find a boolean assignment to a temporary variable holding a boolean condition. @@ -224,7 +203,7 @@ let rec find_normal_variable_load_ tenv (seen: Exp.Set.t) node id : DExp.t optio | _ -> None in - let res = find_in_node_or_preds node ~f:find_declaration in + let res = Procdesc.Node.find_in_node_or_preds node ~f:find_declaration in if verbose && is_none res then ( L.d_str ( "find_normal_variable_load could not find " ^ Ident.to_string id ^ " in node " diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index b9f40bad0..693ec00ca 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -14,67 +14,11 @@ module L = Logging 1. perform a control flow dependency analysis by getting all the variables that appear in the control flow path up to that node. - 2. perform a data dependency analysis - - 3. for each control dependency per node, find its respective data - dependencies *) + 2. for each control dependency per node, find its respective data + dependency + *) module VarSet = AbstractDomain.FiniteSet (Var) -module DataDepSet = VarSet -module DataDepMap = AbstractDomain.Map (Var) (DataDepSet) - -(* forward transfer function for collecting data dependencies of a variable *) -module TransferFunctionsDataDeps (CFG : ProcCfg.S) = struct - module CFG = CFG - module Domain = DataDepMap - - type extras = ProcData.no_extras - - (* compute data the dependencies in an eager way, i.e. get the transitive closure *) - let add_data_dep_exp lhs_var exp astate = - let add_dependency_to_var lhs_var free_var astate_acc = - (* add lhs_var -> {free var} *) - let deps_of_free_var = - DataDepMap.find_opt free_var astate_acc |> Option.value ~default:DataDepSet.empty - in - DataDepMap.add lhs_var (DataDepSet.add free_var deps_of_free_var) astate_acc - in - let astate' = - Exp.free_vars exp - |> Sequence.fold ~init:astate ~f:(fun astate_acc id_var -> - add_dependency_to_var lhs_var (Var.of_id id_var) astate_acc ) - in - Exp.program_vars exp - |> Sequence.fold ~init:astate' ~f:(fun astate_acc pvar -> - add_dependency_to_var lhs_var (Var.of_pvar pvar) astate_acc ) - - - let exec_instr astate _ _ = function - | Sil.Load (lhs_id, _, _, _) when Ident.is_none lhs_id -> - (* dummy deref inserted by frontend--don't count as a read *) - astate - | Sil.Load (id, exp, _, _) -> - add_data_dep_exp (Var.of_id id) exp astate - | Sil.Store (exp_lhs, _, exp_rhs, _) -> - let astate' = - Exp.free_vars exp_lhs - |> Sequence.fold ~init:astate ~f:(fun astate_acc id -> - add_data_dep_exp (Var.of_id id) exp_rhs astate_acc ) - in - Exp.program_vars exp_lhs - |> Sequence.fold ~init:astate' ~f:(fun astate_acc pvar -> - add_data_dep_exp (Var.of_pvar pvar) exp_rhs astate_acc ) - | Sil.Call ((id, _), _, arg_list, _, _) -> - List.fold_left arg_list ~init:astate ~f:(fun astate_acc (exp, _) -> - add_data_dep_exp (Var.of_id id) exp astate_acc ) - | Sil.Prune _ | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> - astate - - - let pp_session_name node fmt = - F.fprintf fmt "data dependency analysis %a" CFG.Node.pp_id (CFG.Node.id node) -end - module ControlDepSet = VarSet module GuardNodes = AbstractDomain.FiniteSet (Procdesc.Node) @@ -94,27 +38,48 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct type extras = loop_control_maps - let get_vars_in_exp exp = - let aux f_free_vars f_to_var = - f_free_vars exp |> Sequence.map ~f:f_to_var |> Sequence.to_list |> ControlDepSet.of_list - in - assert (Domain.is_empty (aux Exp.program_vars Var.of_pvar)) ; + let collect_vars_in_exp exp = + Var.get_all_vars_in_exp exp + |> Sequence.fold ~init:ControlDepSet.empty ~f:(fun acc var -> ControlDepSet.add var acc) + + + let find_vars_in_decl id _ = function + | Sil.Load (lhs_id, exp, _, _) when Ident.equal lhs_id id -> + collect_vars_in_exp exp |> Option.some + | Sil.Call ((lhs_id, _), _, arg_list, _, _) when Ident.equal lhs_id id -> + List.fold_left arg_list ~init:ControlDepSet.empty ~f:(fun deps (exp, _) -> + collect_vars_in_exp exp |> ControlDepSet.union deps ) + |> Option.some + | _ -> + None + + + let get_vars_in_exp exp prune_node = + assert (Exp.program_vars exp |> Sequence.is_empty) ; (* We should never have program variables in prune nodes *) - aux Exp.free_vars Var.of_id + Exp.free_vars exp + |> Sequence.fold ~init:ControlDepSet.empty ~f:(fun acc id -> + match Procdesc.Node.find_in_node_or_preds prune_node ~f:(find_vars_in_decl id) with + | Some deps -> + ControlDepSet.union deps acc + | None -> + L.internal_error "Failed to get the definition of the control variable %a" Ident.pp + id ; + assert false ) (* extract vars from the prune instructions in the node *) let get_control_vars loop_nodes = GuardNodes.fold - (fun loop_node acc -> - let instrs = Procdesc.Node.get_instrs loop_node in + (fun prune_node acc -> + let instrs = Procdesc.Node.get_instrs prune_node in Instrs.fold ~init:acc ~f:(fun astate instr -> match instr with | Sil.Prune (exp, _, _, _) -> - Domain.union (get_vars_in_exp exp) astate + Domain.union (get_vars_in_exp exp prune_node) astate | _ -> - (* prune nodes include other instructions like REMOVE_TEMPS *) + (* prune nodes include other instructions like REMOVE_TEMPS or loads *) astate ) instrs ) loop_nodes Domain.empty @@ -148,30 +113,8 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct end module CFG = ProcCfg.Normal -module DataDepAnalyzer = AbstractInterpreter.Make (CFG) (TransferFunctionsDataDeps) module ControlDepAnalyzer = AbstractInterpreter.Make (CFG) (TransferFunctionsControlDeps) -let report_deps data_map = - Sequence.iter ~f:(fun x -> - match DataDepMap.find_opt x data_map with - | Some d_vars -> - L.(debug Analysis Medium) "@\n>>> var = %a --> %a @\n\n" Var.pp x DataDepSet.pp d_vars - | None -> - () ) - - -let report_data_deps data_map node = - Instrs.iter (Procdesc.Node.get_instrs node) ~f:(fun instr -> - List.iter (Sil.instr_get_exps instr) ~f:(fun exp -> - L.(debug Analysis Medium) - "@\n>>>Data dependencies of node = %a @\n" Procdesc.Node.pp node ; - let free_vars = Exp.free_vars exp |> Sequence.map ~f:Var.of_id in - let program_vars = Exp.program_vars exp |> Sequence.map ~f:Var.of_pvar in - L.(debug Analysis Medium) "@\n>>>for exp = %a : @\n\n" Exp.pp exp ; - report_deps data_map free_vars ; - report_deps data_map program_vars ) ) - - let report_control_deps control_map node = Instrs.iter (Procdesc.Node.get_instrs node) ~f:(fun instr -> L.(debug Analysis Medium) "@\n>>>Control dependencies of node = %a @\n" Procdesc.Node.pp node ; @@ -180,25 +123,11 @@ let report_control_deps control_map node = "@\n>>>for exp = %a : %a @\n\n" Exp.pp exp ControlDepSet.pp control_map ) ) -let gather_all_deps control_map data_map = - ControlDepSet.fold - (fun x deps -> - DataDepMap.find_opt x data_map - |> Option.map ~f:(fun data_deps -> - DataDepSet.filter Var.appears_in_source_code data_deps |> DataDepSet.union deps ) - |> Option.value ~default:deps ) - control_map VarSet.empty - - -let compute_all_deps data_invariant_map control_invariant_map node = +let compute_all_deps control_invariant_map node = let node_id = CFG.Node.id node in let deps = VarSet.empty in ControlDepAnalyzer.extract_post node_id control_invariant_map |> Option.map ~f:(fun control_deps -> - DataDepAnalyzer.extract_post node_id data_invariant_map - |> Option.map ~f:(fun data_deps -> - report_data_deps data_deps node ; - report_control_deps control_deps node ; - gather_all_deps control_deps data_deps ) - |> Option.value ~default:deps ) + report_control_deps control_deps node ; + control_deps ) |> Option.value ~default:deps diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index ce8f51623..50344ead6 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -142,8 +142,7 @@ module BoundMap = struct false - let compute_upperbound_map node_cfg inferbo_invariant_map data_invariant_map - control_invariant_map = + let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map = let pname = Procdesc.get_proc_name node_cfg in let formal_pvars = Procdesc.get_formals node_cfg |> List.map ~f:(fun (m, _) -> Pvar.mk m pname) @@ -161,9 +160,7 @@ module BoundMap = struct match exit_state_opt with | Some entry_mem -> (* compute all the dependencies, i.e. set of variables that affect the control flow upto the node *) - let all_deps = - Control.compute_all_deps data_invariant_map control_invariant_map node - in + let all_deps = Control.compute_all_deps control_invariant_map node in L.(debug Analysis Medium) "@\n>>> All dependencies for node = %a : %a @\n\n" Procdesc.Node.pp node Control.VarSet.pp all_deps ; @@ -986,15 +983,9 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = let inferbo_invariant_map, summary = BufferOverrunChecker.compute_invariant_map_and_check callback_args in - let proc_data = ProcData.make_default proc_desc tenv in let node_cfg = NodeCFG.from_pdesc proc_desc in (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) let control_maps = Loop_control.get_control_maps node_cfg in - (* computes the data dependencies: node -> (var -> var set) *) - let data_dep_invariant_map = - Control.DataDepAnalyzer.exec_cfg node_cfg proc_data ~initial:Control.DataDepMap.empty - ~debug:true - in (* computes the control dependencies: node -> var set *) let control_dep_invariant_map = let proc_data = ProcData.make proc_desc tenv control_maps in @@ -1010,8 +1001,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = in (* given the semantics computes the upper bound on the number of times a node could be executed *) let bound_map = - BoundMap.compute_upperbound_map node_cfg inferbo_invariant_map data_dep_invariant_map - control_dep_invariant_map + BoundMap.compute_upperbound_map node_cfg inferbo_invariant_map control_dep_invariant_map in let _ = ConstraintSolver.collect_constraints node_cfg in let constraints = StructuralConstraints.compute_structural_constraints node_cfg in diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index a1107ea4c..32389b096 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -43,5 +43,16 @@ codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.two_loops codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.two_loops(), 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545] codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608] codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 607] -codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,String), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 239] +codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,Object), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,boolean), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,double), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,long), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonMap.java, void JsonMap.addKeyToMap(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonString.java, JsonString.(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonUtils.java, StringBuilder JsonUtils.serialize(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.escape(StringBuilder,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.escape(StringBuilder,String), 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.serialize(StringBuilder,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []