diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml new file mode 100644 index 000000000..dce8e07be --- /dev/null +++ b/infer/src/checkers/control.ml @@ -0,0 +1,166 @@ +(* + * Copyright (c) 2016 - 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 +(* forward dependency analysis for computing set of variables that affect the control flow at each program point + 1. perform a control flow dependency analysis CF 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 *) + +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 (lhs, _, arg_list, _, _) -> ( + match lhs with + | Some (id, _) -> + List.fold_left arg_list ~init:astate ~f:(fun astate_acc (exp, _) -> + add_data_dep_exp (Var.of_id id) exp astate_acc ) + | None -> + astate ) + | Sil.Prune _ | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> + astate + + + let pp_session_name node fmt = + F.fprintf fmt "data depenedency analysis %a" CFG.pp_id (CFG.id node) +end + +module ControlDepSet = VarSet + +(* forward transfer function for control dependencies *) +module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = ControlDepSet + + type extras = ProcData.no_extras + + let exec_instr astate _ _ instr = + match instr with + | Sil.Prune (exp, _, _, _) -> + let astate' = + Exp.free_vars exp |> Sequence.map ~f:Var.of_id |> Sequence.to_list + |> ControlDepSet.of_list |> Domain.union astate + in + Exp.program_vars exp |> Sequence.map ~f:Var.of_pvar |> Sequence.to_list + |> ControlDepSet.of_list |> Domain.union astate' + | Sil.Load _ + | Sil.Store _ + | Sil.Call _ + | Declare_locals _ + | Remove_temps _ + | Abstract _ + | Nullify _ -> + astate + + + let pp_session_name node fmt = + F.fprintf fmt "control depenedency analysis %a" CFG.pp_id (CFG.id node) +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 = + List.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 = + List.iter (Procdesc.Node.get_instrs node) ~f:(fun instr -> + L.(debug Analysis Medium) "@\n>>>Control dependencies of node = %a @\n" Procdesc.Node.pp node ; + List.iter (Sil.instr_get_exps instr) ~f:(fun exp -> + L.(debug Analysis Medium) + "@\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 und_node = CFG.underlying_node node in + let node_id = Procdesc.Node.get_id und_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 ) + |> Option.value ~default:deps diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index a4bec0f95..935d19352 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -147,7 +147,8 @@ module BoundMap = struct env - let compute_upperbound_map pdesc invariant_map_NodesBasicCost = + let compute_upperbound_map pdesc invariant_map_NodesBasicCost data_invariant_map + control_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 @@ -163,6 +164,13 @@ module BoundMap = struct match entry_state_opt with | Some (entry_mem, _) -> let env = convert entry_mem in + (* 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 + L.(debug Analysis Medium) + "@\n>>> All dependencies for node = %a : %a @\n\n" Procdesc.Node.pp node + Control.VarSet.pp all_deps ; (* bound = env(v1) *... * env(vn) *) let bound = CostDomain.EnvDomainBO.fold @@ -175,8 +183,11 @@ module BoundMap = struct | Exp.Lvar _ when List.mem fparam' exp ~equal:Exp.equal -> Itv.one - | Exp.Lvar _ -> + | Exp.Lvar pvar when Control.VarSet.mem (Var.of_pvar pvar) all_deps -> itv + | Exp.Lvar _ -> + (* For a var that doesn't affect control flow directly or indirectly, we give [1,1] so it doesn't count *) + Itv.one | _ -> assert false in @@ -556,12 +567,24 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = Preanal.do_preanalysis proc_desc tenv ; let proc_data = ProcData.make_default proc_desc tenv in let cfg = CFG.from_pdesc proc_desc in + (* computes the data dependencies: node -> (var -> var set) *) + let data_dep_invariant_map = + Control.DataDepAnalyzer.exec_cfg cfg proc_data ~initial:Control.DataDepMap.empty ~debug:true + in + (* computes the control dependencies: node -> var set *) + let control_dep_invariant_map = + Control.ControlDepAnalyzer.exec_cfg cfg proc_data ~initial:Control.ControlDepSet.empty + ~debug:true + in let invariant_map_NodesBasicCost = (*compute_WCET cfg invariant_map min_trees in *) AnalyzerNodesBasicCost.exec_cfg cfg proc_data ~initial:NodesBasicCostDomain.init ~debug:true 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 cfg invariant_map_NodesBasicCost in + let bound_map = + BoundMap.compute_upperbound_map cfg invariant_map_NodesBasicCost data_dep_invariant_map + control_dep_invariant_map + in let constraints = StructuralConstraints.compute_structural_constraints cfg in let min_trees = MinTree.compute_trees_from_contraints bound_map cfg constraints in let trees_valuation = diff --git a/infer/tests/codetoanalyze/c/performance/cost_test_deps.c b/infer/tests/codetoanalyze/c/performance/cost_test_deps.c new file mode 100644 index 000000000..85d0fa32f --- /dev/null +++ b/infer/tests/codetoanalyze/c/performance/cost_test_deps.c @@ -0,0 +1,98 @@ +/* + * 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 that exercise precision of the analysis on control variables + +// -- We computed infinity before for the following two tests-- + +// Loop's execution count doesn't depend on values of p,t,k +int loop_no_dep1(int k) { + int p = 0; + int t = 2 + k; + for (int i = 0; i < 100; i++) { + p++; + } + return p; +} + +int foo(int i, int j) { return i + j; } + +// Loop's execution count doesn't depend on values of p,t,k +int loop_no_dep2(int k) { + int p = 0; + int t = foo(p, k); + for (int i = 0; i < 100; i++) { + p++; + } + return p; +} + +// -- Below examples should have worked, but due to the imprecision of CF +// analysis, they don't +// +// This example doesn't work since for the loop +// control vars={p,j} and since j in [-oo.+oo], we get oo count. +int if_bad(int j) { + int p = 10; + int i = 0; + if (p < 10 + j) { + p++; + } else { + p = j + 3; + for (int k = 0; k < 100; k++) { + j += 3; + } + } + return p; +} + +// We get +oo for this program, but if you take the first loop out, +// fake dependency disappears and we can get a proper bound +// +int two_loops() { + int p = 10; + int k = 3; + int t = 2 + k; + for (int j = 0; j < 6; j++) { + k++; + } + for (int i = 0; i < 100; i++) { + p = 3; + } + return p; +} + +// We can't get program point A's execution count as 5 due to the weakness in CF +// analysis +int nested_loop() { + int k = 0; + for (int i = 0; i < 5; i++) { + A: + k = 0; + for (int j = 0; j < 100; j++) { + k = 3; + } + } + return k; +} + +// Unlike the above program, B will be inside the inner loop, hence executed +int simulated_nested_loop(int p) { + int k = 0; + int t = 5; + int j = 0; + for (int i = 0; i < 5; i++) { + B: + t = 3; + j++; + if (j < 100) + goto B; // continue; + } + return k; +} diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index db69c9772..642113c72 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -7,3 +7,13 @@ codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_ codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104] codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1106] codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 212] +codetoanalyze/c/performance/cost_test_deps.c, if_bad, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 605] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 605] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 608] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 609] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 609] +codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep2, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 612] +codetoanalyze/c/performance/cost_test_deps.c, nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, simulated_nested_loop, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test_deps.c, two_loops, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []