pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Extending analysis to parametric case

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D7179463

fbshipit-source-id: 1711a0e
master
Dino Distefano 7 years ago committed by Facebook Github Bot
parent 1977fefaab
commit d2cc5e72f7
7 changed files with 209 additions and 84 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -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

6
infer/src/bufferoverrun/bufferOverrunChecker.mli
Unescape View File

@ -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

145
infer/src/checkers/cost.ml
Unescape View File

@ -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 =
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 not (Domain.( <= ) ~lhs:cost ~rhs:expensive_threshold) ->
| 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 " Domain.pp cost
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
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 not (Domain.( <= ) ~lhs:cost ~rhs:expensive_threshold) ->
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)" Domain.pp cost
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
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 (

4
infer/src/checkers/costDomain.ml
Unescape View File

@ -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}

20
infer/tests/codetoanalyze/c/performance/Makefile
Unescape View File

@ -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)

56
infer/tests/codetoanalyze/c/performance/cost_test.c
Unescape View File

@ -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;
}

7
infer/tests/codetoanalyze/c/performance/issues.exp
Unescape View File

@ -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, []
Write Preview
Loading…
Cancel
Save