From 257e684392b55f2941d05f1e7755bdc0ccc11016 Mon Sep 17 00:00:00 2001 From: Jia Chen Date: Thu, 29 Jun 2017 18:43:19 -0700 Subject: [PATCH] [infer][checker] Put AnnotationSpec.sink_predicate and AnnotationSpec.sanitizer_predicate into actual use for annotation reachability checker Reviewed By: jeremydubreil Differential Revision: D5296631 fbshipit-source-id: 885969b --- infer/src/checkers/annotationReachability.ml | 239 +++++++++---------- 1 file changed, 114 insertions(+), 125 deletions(-) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 1d53e873b..4ad14a87f 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -15,33 +15,6 @@ module MF = MarkupFormatter let dummy_constructor_annot = "__infer_is_constructor" -let annotation_of_str annot_str = - { Annot.class_name = annot_str; parameters = []; } - -(* parse user-defined specs from .inferconfig *) -let parse_user_defined_specs = function - | `List user_specs -> - let parse_user_spec json = - let open Yojson.Basic in - let sources = Util.member "sources" json |> Util.to_list |> List.map ~f:Util.to_string in - let sinks = Util.member "sink" json |> Util.to_string in - sources, sinks in - List.map ~f:parse_user_spec user_specs - | _ -> - [] - -let src_snk_pairs = - let specs = - ([Annotations.performance_critical], Annotations.expensive) :: - ([Annotations.no_allocation], dummy_constructor_annot) :: - ([Annotations.any_thread; Annotations.for_non_ui_thread], Annotations.ui_thread) :: - ([Annotations.ui_thread; Annotations.for_ui_thread], Annotations.for_non_ui_thread) :: - (parse_user_defined_specs Config.annotation_reachability_custom_pairs) in - List.map - ~f:(fun (src_annot_str_list, snk_annot_str) -> - List.map ~f:annotation_of_str src_annot_str_list, annotation_of_str snk_annot_str) - specs - module Domain = struct module TrackingVar = AbstractDomain.FiniteSet (Var) module TrackingDomain = AbstractDomain.BottomLifted (TrackingVar) @@ -253,100 +226,6 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si with Not_found -> ()) sink_map -let method_has_ignore_allocation_annot tenv pname = - check_attributes Annotations.ia_is_ignore_allocations tenv pname - -(* TODO: generalize this to allow sanitizers for other annotation types, store it in [extras] so - we can compute it just once *) -let method_is_sanitizer annot tenv pname = - if String.equal annot.Annot.class_name dummy_constructor_annot - then method_has_ignore_allocation_annot tenv pname - else false - -module TransferFunctions (CFG : ProcCfg.S) = struct - module CFG = CFG - module Domain = Domain - type extras = ProcData.no_extras - - (* 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 = - List.fold - ~init:astate - ~f:(fun astate (_, annot) -> - if method_has_annot annot tenv callee_pname && - not (method_is_sanitizer annot tenv caller_pname) - then Domain.add_call_site annot callee_pname call_site astate - else astate) - src_snk_pairs - - let merge_callee_map call_site pdesc callee_pname astate = - match Summary.read_summary pdesc callee_pname with - | None -> astate - | Some callee_call_map -> - let add_call_site annot sink calls astate = - if AnnotReachabilityDomain.CallSites.is_empty calls - then astate - else Domain.add_call_site annot sink call_site astate in - AnnotReachabilityDomain.fold - (fun annot sink_map astate -> - AnnotReachabilityDomain.SinkMap.fold - (add_call_site annot) - sink_map - astate) - callee_call_map - astate - - let exec_instr astate { ProcData.pdesc; tenv; } _ = function - | Sil.Call (Some (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 = Procdesc.get_proc_name pdesc in - let call_site = CallSite.make callee_pname call_loc in - check_call tenv callee_pname caller_pname call_site astate - |> merge_callee_map call_site pdesc callee_pname - | 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 - | Sil.Call (None, _, _, _, _) -> - failwith "Expecting a return identifier" - | _ -> - astate -end - -module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) - let report_src_snk_path { Callbacks.proc_desc; tenv; summary } sink_map snk_annot src_annot = let proc_name = Procdesc.get_proc_name proc_desc in let loc = Procdesc.get_loc proc_desc in @@ -370,6 +249,9 @@ let report_src_snk_paths proc_data annot_map src_annot_list snk_annot = (* New implementation starts here *) +let annotation_of_str annot_str = + { Annot.class_name = annot_str; parameters = []; } + module AnnotationSpec = struct type predicate = Tenv.t -> Typ.Procname.t -> bool @@ -377,6 +259,7 @@ module AnnotationSpec = struct source_predicate: predicate; sink_predicate: predicate; sanitizer_predicate: predicate; + sink_annotation: Annot.t; report: Callbacks.proc_callback_args -> AnnotReachabilityDomain.astate -> unit; } @@ -391,8 +274,12 @@ module StandardAnnotationSpec = struct let from_annotations src_annots snk_annot = AnnotationSpec.{ source_predicate = (fun tenv pname -> List.exists src_annots ~f:(fun a -> method_overrides_annot a tenv pname)); - sink_predicate = (method_has_annot snk_annot); + sink_predicate = (fun tenv pname -> + let has_annot ia = Annotations.ia_ends_with ia snk_annot.Annot.class_name in + check_attributes has_annot tenv pname + ); sanitizer_predicate = default_sanitizer; + sink_annotation = snk_annot; report = (fun proc_data annot_map -> report_src_snk_paths proc_data annot_map src_annots snk_annot) } @@ -405,8 +292,11 @@ module NoAllocationAnnotationSpec = struct let spec = AnnotationSpec.{ source_predicate = (fun tenv pname -> method_overrides_annot no_allocation_annot tenv pname); - sink_predicate = (method_has_annot constructor_annot); - sanitizer_predicate = method_has_ignore_allocation_annot; + sink_predicate = (fun tenv pname -> + is_allocator tenv pname); + sanitizer_predicate = (fun tenv pname -> + check_attributes Annotations.ia_is_ignore_allocations tenv pname); + sink_annotation = constructor_annot; report = (fun proc_data annot_map -> report_src_snk_paths proc_data annot_map [no_allocation_annot] constructor_annot); } @@ -439,8 +329,12 @@ module ExpensiveAnnotationSpec = struct let spec = AnnotationSpec.{ source_predicate = is_expensive; - sink_predicate = (method_has_annot expensive_annot); + sink_predicate = (fun tenv pname -> + let has_annot ia = Annotations.ia_ends_with ia expensive_annot.class_name in + check_attributes has_annot tenv pname || is_modeled_expensive tenv pname + ); sanitizer_predicate = default_sanitizer; + sink_annotation = expensive_annot; report = (fun ({ Callbacks.tenv; proc_desc } as proc_data) astate -> let proc_name = Procdesc.get_proc_name proc_desc in if is_expensive tenv proc_name then @@ -450,6 +344,18 @@ module ExpensiveAnnotationSpec = struct } end +(* parse user-defined specs from .inferconfig *) +let parse_user_defined_specs = function + | `List user_specs -> + let parse_user_spec json = + let open Yojson.Basic in + let sources = Util.member "sources" json |> Util.to_list |> List.map ~f:Util.to_string in + let sinks = Util.member "sink" json |> Util.to_string in + sources, sinks in + List.map ~f:parse_user_spec user_specs + | _ -> + [] + let annot_specs = let user_defined_specs = let specs = parse_user_defined_specs Config.annotation_reachability_custom_pairs in @@ -467,6 +373,89 @@ let annot_specs = (annotation_of_str Annotations.for_non_ui_thread)) :: user_defined_specs +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain + type extras = ProcData.no_extras + + (* 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 = + List.fold + ~init:astate + ~f:(fun astate (spec: AnnotationSpec.t) -> + if spec.sink_predicate tenv callee_pname && + not (spec.sanitizer_predicate tenv caller_pname) + then Domain.add_call_site spec.sink_annotation callee_pname call_site astate + else astate) + annot_specs + + let merge_callee_map call_site pdesc callee_pname astate = + match Summary.read_summary pdesc callee_pname with + | None -> astate + | Some callee_call_map -> + let add_call_site annot sink calls astate = + if AnnotReachabilityDomain.CallSites.is_empty calls + then astate + else Domain.add_call_site annot sink call_site astate in + AnnotReachabilityDomain.fold + (fun annot sink_map astate -> + AnnotReachabilityDomain.SinkMap.fold + (add_call_site annot) + sink_map + astate) + callee_call_map + astate + + let exec_instr astate { ProcData.pdesc; tenv; } _ = function + | Sil.Call (Some (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 = Procdesc.get_proc_name pdesc in + let call_site = CallSite.make callee_pname call_loc in + check_call tenv callee_pname caller_pname call_site astate + |> merge_callee_map call_site pdesc callee_pname + | 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 + | Sil.Call (None, _, _, _, _) -> + failwith "Expecting a return identifier" + | _ -> + astate +end + +module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) let checker ({ Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary = let initial = (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in