Reviewed By: mbouaziz Differential Revision: D7586777 fbshipit-source-id: 8752679master
Ezgi Çiçek
7 years ago
committed by
Facebook Github Bot
parent
cfa2dd5f83
commit
76300d55c7
@ -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
|
||||||
@ -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;
|
||||||
|
}
|
||||||
Loading…
Reference in new issue