From 4f46567fa75c679547eddda7e872d715d28873ae Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Sat, 13 Jul 2019 02:53:26 -0700 Subject: [PATCH] [annotreach] kill custom path sensitivity Summary: The domain supported path sensitivity wrt to a specific boolean guard `Branch.unlikely`. This isn't used in actual code, so remove it. Also - add an .mli to the domain; - unabbreviate domain name to match analyser name; - use Payload.read instead of calling Ondemand directly; - adjust tests. Reviewed By: mbouaziz Differential Revision: D16203953 fbshipit-source-id: 743aa4400 --- infer/src/backend/Payloads.ml | 4 +- infer/src/backend/Payloads.mli | 2 +- infer/src/checkers/AnnotReachabilityDomain.ml | 11 -- infer/src/checkers/annotationReachability.ml | 124 +++--------------- .../checkers/annotationReachabilityDomain.ml | 18 +++ .../checkers/annotationReachabilityDomain.mli | 16 +++ .../codetoanalyze/java/annotreach/Branch.java | 15 --- .../java/annotreach/ExpensiveCallExample.java | 48 ------- .../java/annotreach/NoAllocationExample.java | 20 --- .../codetoanalyze/java/annotreach/issues.exp | 4 - 10 files changed, 54 insertions(+), 208 deletions(-) delete mode 100644 infer/src/checkers/AnnotReachabilityDomain.ml create mode 100644 infer/src/checkers/annotationReachabilityDomain.ml create mode 100644 infer/src/checkers/annotationReachabilityDomain.mli delete mode 100644 infer/tests/codetoanalyze/java/annotreach/Branch.java diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 46ba2768e..3369341ef 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -9,7 +9,7 @@ open! IStd module F = Format type t = - { annot_map: AnnotReachabilityDomain.t option + { annot_map: AnnotationReachabilityDomain.t option ; biabduction: BiabductionSummary.t option ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option @@ -37,7 +37,7 @@ let fields = let mk field name pp = F {field; name; pp= (fun _ -> pp)} in let mk_pe field name pp = F {field; name; pp} in Fields.to_list - ~annot_map:(fun f -> mk f "AnnotationReachability" AnnotReachabilityDomain.pp) + ~annot_map:(fun f -> mk f "AnnotationReachability" AnnotationReachabilityDomain.pp) ~biabduction:(fun f -> mk_pe f "Biabduction" BiabductionSummary.pp) ~buffer_overrun_analysis:(fun f -> mk f "BufferOverrunAnalysis" BufferOverrunAnalysisSummary.pp) ~buffer_overrun_checker:(fun f -> mk f "BufferOverrunChecker" BufferOverrunCheckerSummary.pp) diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 249b882d2..48d2cf30a 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -14,7 +14,7 @@ include (** analysis results *) type t = - { annot_map: AnnotReachabilityDomain.t option + { annot_map: AnnotationReachabilityDomain.t option ; biabduction: BiabductionSummary.t option ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option diff --git a/infer/src/checkers/AnnotReachabilityDomain.ml b/infer/src/checkers/AnnotReachabilityDomain.ml deleted file mode 100644 index ae1cbc1ef..000000000 --- a/infer/src/checkers/AnnotReachabilityDomain.ml +++ /dev/null @@ -1,11 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -module CallSites = AbstractDomain.FiniteSet (CallSite) -module SinkMap = AbstractDomain.Map (Typ.Procname) (CallSites) -include AbstractDomain.Map (Annot) (SinkMap) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 07e20f1bb..edb8cf276 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -6,61 +6,16 @@ *) open! IStd -open! AbstractDomain.Types module F = Format module MF = MarkupFormatter module U = Utils let dummy_constructor_annot = "__infer_is_constructor" -module Domain = struct - module TrackingVar = AbstractDomain.FiniteSet (Var) - module TrackingDomain = AbstractDomain.BottomLifted (TrackingVar) - include AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingDomain) - - let add_call_site annot sink call_site ((annot_map, previous_vstate) as astate) = - match previous_vstate with - | Bottom -> - astate - | NonBottom _ -> - let sink_map = - try AnnotReachabilityDomain.find annot annot_map - with Caml.Not_found -> AnnotReachabilityDomain.SinkMap.empty - in - let sink_map' = - if AnnotReachabilityDomain.SinkMap.mem sink sink_map then sink_map - else - let singleton = AnnotReachabilityDomain.CallSites.singleton call_site in - AnnotReachabilityDomain.SinkMap.singleton sink singleton - in - if phys_equal sink_map' sink_map then astate - else (AnnotReachabilityDomain.add annot sink_map' annot_map, previous_vstate) - - - let stop_tracking ((annot_map, _) : t) = (annot_map, Bottom) - - let add_tracking_var var ((annot_map, previous_vstate) as astate) = - match previous_vstate with - | Bottom -> - astate - | NonBottom vars -> - (annot_map, NonBottom (TrackingVar.add var vars)) - - - let remove_tracking_var var ((annot_map, previous_vstate) as astate) = - match previous_vstate with - | Bottom -> - astate - | NonBottom vars -> - (annot_map, NonBottom (TrackingVar.remove var vars)) - - - let is_tracked_var var (_, vstate) = - match vstate with Bottom -> false | NonBottom vars -> TrackingVar.mem var vars -end +module Domain = AnnotationReachabilityDomain module Payload = SummaryPayload.Make (struct - type t = AnnotReachabilityDomain.t + type t = Domain.t let field = Payloads.Fields.annot_map end) @@ -114,12 +69,9 @@ let method_has_annot annot tenv pname = let method_overrides_annot annot tenv pname = method_overrides (method_has_annot annot) tenv pname let lookup_annotation_calls ~caller_summary annot pname = - match Ondemand.analyze_proc_name ~caller_summary pname with - | Some {Summary.payloads= {Payloads.annot_map= Some annot_map}} -> ( - try AnnotReachabilityDomain.find annot annot_map - with Caml.Not_found -> AnnotReachabilityDomain.SinkMap.empty ) - | _ -> - AnnotReachabilityDomain.SinkMap.empty + Payload.read ~caller_summary ~callee_pname:pname + |> Option.bind ~f:(Domain.find_opt annot) + |> Option.value ~default:Domain.SinkMap.empty let update_trace loc trace = @@ -189,10 +141,10 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si in let new_trace = update_trace call_loc trace |> update_trace callee_def_loc in let unseen_callees, updated_callees = - AnnotReachabilityDomain.SinkMap.fold + Domain.SinkMap.fold (fun _ call_sites ((unseen, visited) as accu) -> try - let call_site = AnnotReachabilityDomain.CallSites.min_elt call_sites in + let call_site = Domain.CallSites.min_elt call_sites in let p = CallSite.pname call_site in let loc = CallSite.loc call_site in if Typ.Procname.Set.mem p visited then accu @@ -202,10 +154,10 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si in List.iter ~f:(loop fst_call_loc updated_callees (new_trace, new_stack_str)) unseen_callees in - AnnotReachabilityDomain.SinkMap.iter + Domain.SinkMap.iter (fun _ call_sites -> try - let fst_call_site = AnnotReachabilityDomain.CallSites.min_elt call_sites in + let fst_call_site = Domain.CallSites.min_elt call_sites in let fst_callee_pname = CallSite.pname fst_call_site in let fst_call_loc = CallSite.loc fst_call_site in let start_trace = update_trace (CallSite.loc call_site) [] in @@ -228,13 +180,11 @@ let report_src_snk_path {Callbacks.exe_env; summary} sink_map snk_annot src_anno let report_src_snk_paths proc_data annot_map src_annot_list snk_annot = try - let sink_map = AnnotReachabilityDomain.find snk_annot annot_map in + let sink_map = Domain.find snk_annot annot_map in List.iter ~f:(report_src_snk_path proc_data sink_map snk_annot) src_annot_list with Caml.Not_found -> () -(* New implementation starts here *) - let annotation_of_str annot_str = {Annot.class_name= annot_str; parameters= []} module AnnotationSpec = struct @@ -245,7 +195,7 @@ module AnnotationSpec = struct ; sink_predicate: predicate ; sanitizer_predicate: predicate ; sink_annotation: Annot.t - ; report: Callbacks.proc_callback_args -> AnnotReachabilityDomain.t -> unit } + ; report: Callbacks.proc_callback_args -> Domain.t -> unit } (* The default sanitizer does not sanitize anything *) let default_sanitizer _ _ = false @@ -381,7 +331,7 @@ module CxxAnnotationSpecs = struct if src_pred proc_name then let loc = Procdesc.get_loc proc_desc in try - let sink_map = AnnotReachabilityDomain.find snk_annot annot_map in + let sink_map = Domain.find snk_annot annot_map in report_call_stack proc_data.Callbacks.summary snk_pred ~string_of_pname:cxx_string_of_pname ~call_str (lookup_annotation_calls ~caller_summary:proc_data.Callbacks.summary snk_annot) @@ -530,35 +480,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = AnnotationSpec.t list - (* This is specific to the @NoAllocation and @PerformanceCritical checker - and the "unlikely" method is used to guard branches that are expected to run sufficiently - rarely to not affect the performances *) - let is_unlikely pname = - match pname with - | Typ.Procname.Java java_pname -> - String.equal (Typ.Procname.Java.get_method java_pname) "unlikely" - | _ -> - false - - - let is_tracking_exp astate = function - | Exp.Var id -> - Domain.is_tracked_var (Var.of_id id) astate - | Exp.Lvar pvar -> - Domain.is_tracked_var (Var.of_pvar pvar) astate - | _ -> - false - - - let prunes_tracking_var astate = function - | Exp.BinOp (Binop.Eq, lhs, rhs) when is_tracking_exp astate lhs -> - Exp.equal rhs Exp.one - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, lhs, rhs), _) when is_tracking_exp astate lhs -> - Exp.equal rhs Exp.zero - | _ -> - false - - let check_call tenv callee_pname caller_pname call_site astate specs = List.fold ~init:astate ~f:(fun astate (spec : AnnotationSpec.t) -> @@ -575,7 +496,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate | Some callee_call_map -> let add_call_site annot sink calls astate = - if AnnotReachabilityDomain.CallSites.is_empty calls then astate + if Domain.CallSites.is_empty calls then astate else let pname = Summary.get_proc_name summary in List.fold @@ -584,28 +505,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else Domain.add_call_site annot sink call_site astate ) ~init:astate specs in - AnnotReachabilityDomain.fold - (fun annot sink_map astate -> - AnnotReachabilityDomain.SinkMap.fold (add_call_site annot) sink_map astate ) + Domain.fold + (fun annot sink_map astate -> Domain.SinkMap.fold (add_call_site annot) sink_map astate) callee_call_map astate let exec_instr astate {ProcData.summary; tenv; ProcData.extras} _ = function - | Sil.Call ((id, _), Const (Cfun callee_pname), _, _, _) when is_unlikely callee_pname -> - Domain.add_tracking_var (Var.of_id id) astate | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> let caller_pname = Summary.get_proc_name summary in let call_site = CallSite.make callee_pname call_loc in check_call tenv callee_pname caller_pname call_site astate extras |> merge_callee_map call_site summary callee_pname tenv extras - | Sil.Load (id, exp, _, _) when is_tracking_exp astate exp -> - Domain.add_tracking_var (Var.of_id id) astate - | Sil.Store (Exp.Lvar pvar, _, exp, _) when is_tracking_exp astate exp -> - Domain.add_tracking_var (Var.of_pvar pvar) astate - | Sil.Store (Exp.Lvar pvar, _, _, _) -> - Domain.remove_tracking_var (Var.of_pvar pvar) astate - | Sil.Prune (exp, _, _, _) when prunes_tracking_var astate exp -> - Domain.stop_tracking astate | _ -> astate @@ -618,11 +528,11 @@ module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Except let checker ({Callbacks.exe_env; summary} as callback) : Summary.t = let proc_name = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env proc_name in - let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in + let initial = Domain.empty in let specs = get_annot_specs proc_name in let proc_data = ProcData.make summary tenv specs in match Analyzer.compute_post proc_data ~initial with - | Some (annot_map, _) -> + | Some annot_map -> List.iter specs ~f:(fun spec -> spec.AnnotationSpec.report callback annot_map) ; Payload.update_summary annot_map summary | None -> diff --git a/infer/src/checkers/annotationReachabilityDomain.ml b/infer/src/checkers/annotationReachabilityDomain.ml new file mode 100644 index 000000000..3c303896d --- /dev/null +++ b/infer/src/checkers/annotationReachabilityDomain.ml @@ -0,0 +1,18 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module CallSites = AbstractDomain.FiniteSetOfPPSet (CallSite.Set) +module SinkMap = AbstractDomain.MapOfPPMap (Typ.Procname.Map) (CallSites) +include AbstractDomain.Map (Annot) (SinkMap) + +let add_call_site annot sink call_site annot_map = + let sink_map = find_opt annot annot_map |> Option.value ~default:SinkMap.empty in + if SinkMap.mem sink sink_map then annot_map + else + let sink_map' = SinkMap.singleton sink (CallSites.singleton call_site) in + add annot sink_map' annot_map diff --git a/infer/src/checkers/annotationReachabilityDomain.mli b/infer/src/checkers/annotationReachabilityDomain.mli new file mode 100644 index 000000000..efcfa4476 --- /dev/null +++ b/infer/src/checkers/annotationReachabilityDomain.mli @@ -0,0 +1,16 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +module CallSites : AbstractDomain.FiniteSetS with type elt = CallSite.t + +module SinkMap : AbstractDomain.MapS with type key = Typ.Procname.t and type value = CallSites.t + +include AbstractDomain.MapS with type key = Annot.t and type value = SinkMap.t + +val add_call_site : Annot.t -> Typ.Procname.t -> CallSite.t -> t -> t diff --git a/infer/tests/codetoanalyze/java/annotreach/Branch.java b/infer/tests/codetoanalyze/java/annotreach/Branch.java deleted file mode 100644 index 397312b9d..000000000 --- a/infer/tests/codetoanalyze/java/annotreach/Branch.java +++ /dev/null @@ -1,15 +0,0 @@ -/* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ - -package codetoanalyze.java.checkers; - -public class Branch { - - public static boolean unlikely(boolean value) { - return value; - } -} diff --git a/infer/tests/codetoanalyze/java/annotreach/ExpensiveCallExample.java b/infer/tests/codetoanalyze/java/annotreach/ExpensiveCallExample.java index c7f5d0c56..7a8b1bc8d 100644 --- a/infer/tests/codetoanalyze/java/annotreach/ExpensiveCallExample.java +++ b/infer/tests/codetoanalyze/java/annotreach/ExpensiveCallExample.java @@ -146,56 +146,8 @@ public class ExpensiveCallExample implements AnnotatedInterface { mOther.callsExpensive1(); } - @PerformanceCritical - void callExpensiveMethodWithUnlikely() { - if (Branch.unlikely(mOther != null)) { - mOther.callsExpensive1(); - } - } - - @PerformanceCritical - void onlyOneExpensiveCallUsingUnlikely() { - if (Branch.unlikely(mOther != null)) { - mOther.callsExpensive1(); - } - expensiveMethod(); - } - - @PerformanceCritical - void callsExpensiveInTheUnlikelyElseBranch() { - if (Branch.unlikely(mOther != null)) { - // Do nothing - } else { - expensiveMethod(); - } - } - native boolean test(); - @PerformanceCritical - void callsExpensiveWithDisjunctionAfterUnlikely() { - if (Branch.unlikely(mOther != null) || test()) { - expensiveMethod(); - } - } - - @PerformanceCritical - void callsExpensiveWithUnlikelyInLocalVariable() { - boolean b = Branch.unlikely(mOther != null); - if (b) { - expensiveMethod(); - } - } - - @PerformanceCritical - void callsExpensiveWithOverriddenUnlikelyCondition() { - boolean b = Branch.unlikely(mOther != null); - b = test(); - if (b) { - expensiveMethod(); - } - } - @PerformanceCritical void callsExpensiveInConditionalBranch() { if (test()) { diff --git a/infer/tests/codetoanalyze/java/annotreach/NoAllocationExample.java b/infer/tests/codetoanalyze/java/annotreach/NoAllocationExample.java index dde13566e..4afdede3d 100644 --- a/infer/tests/codetoanalyze/java/annotreach/NoAllocationExample.java +++ b/infer/tests/codetoanalyze/java/annotreach/NoAllocationExample.java @@ -63,24 +63,4 @@ public class NoAllocationExample { void onlyAllocatesInAcceptableWay() { acceptableAllocation(); } - - native boolean rareCase(); - - @NoAllocation - void onlyAllocatesUsingUnlikely() { - if (Branch.unlikely(rareCase())) { - allocates(); - } - } - - native boolean anotherRareCase(); - - @NoAllocation - void nestedUnlikely() { - if (Branch.unlikely(rareCase())) { - if (!Branch.unlikely(anotherRareCase())) { - allocates(); - } - } - } } diff --git a/infer/tests/codetoanalyze/java/annotreach/issues.exp b/infer/tests/codetoanalyze/java/annotreach/issues.exp index 1def3cc25..127d3677a 100644 --- a/infer/tests/codetoanalyze/java/annotreach/issues.exp +++ b/infer/tests/codetoanalyze/java/annotreach/issues.exp @@ -6,15 +6,11 @@ codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.chec codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callMethodOnExpensiveClass(codetoanalyze.java.checkers.ExpensiveClass):void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callingExpensiveMethodFromInterface(codetoanalyze.java.checkers.ExpensiveInterfaceExample):void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callsExpensiveInConditionalBranch():void, 2, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] -codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callsExpensiveInTheUnlikelyElseBranch():void, 4, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] -codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callsExpensiveWithDisjunctionAfterUnlikely():void, 2, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] -codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callsExpensiveWithOverriddenUnlikelyCondition():void, 4, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callsFindViewByIdFromActivity(android.support.v4.app.FragmentActivity,int):android.view.View, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.callsFindViewByIdFromView(android.widget.ImageView,int):android.view.View, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.directlyCallingExpensiveMethod():void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.indirectlyCallingExpensiveMethod():void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.longerCallStackToExpensive():void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] -codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.ExpensiveCallExample.onlyOneExpensiveCallUsingUnlikely():void, 4, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.PerformanceCriticalClass.performanceCriticalMethod1(codetoanalyze.java.checkers.ExpensiveClass):void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.PerformanceCriticalClass.performanceCriticalMethod2(codetoanalyze.java.checkers.Other):void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, [] codetoanalyze/java/annotreach/ExpensiveCallExample.java, codetoanalyze.java.checkers.PerformanceCriticalClass.performanceCriticalMethod3(codetoanalyze.java.checkers.Other):void, 1, CHECKERS_CALLS_EXPENSIVE_METHOD, no_bucket, ERROR, []