From f8aea424cf289d464aca7b7ee22166727707afa5 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 27 Mar 2017 11:23:49 -0700 Subject: [PATCH] [thread-safety] use aggregated access table as results table Summary: We only need one "global" view of all the summaries in a file. Reviewed By: peterogithub Differential Revision: D4773646 fbshipit-source-id: 29e5316 --- infer/src/checkers/ThreadSafety.ml | 101 +++++++++++------------------ 1 file changed, 37 insertions(+), 64 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index a35a2ae6a..582e70987 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -697,17 +697,6 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) module Interprocedural = AbstractInterpreter.Interprocedural (Summary) -(* a results table is a Map where a key is an a procedure environment, - i.e., something of type Idenv.t * Tenv.t * Typ.Procname.t * Procdesc.t -*) -module ResultsTableType = Caml.Map.Make (struct - type t = Tenv.t * Procdesc.t - let compare (_, pd1) (_, pd2) = - let pn1 = Procdesc.get_proc_name pd1 - and pn2 = Procdesc.get_proc_name pd2 in - Typ.Procname.compare pn1 pn2 - end) - (* we want to consider Builder classes and other safe immutablility-ensuring patterns as thread-safe. we are overly friendly about this for now; any class whose name ends with `Builder` is assumed to be thread-safe. in the future, we can ask for builder classes to be annotated with @@ -894,22 +883,14 @@ let checker ({ Callbacks.summary } as callback_args) : Specs.summary = ignore (analyze_procedure callback_args); Specs.get_summary_unsafe "ThreadSafety.checker" proc_name -(* creates a map from proc_envs to postconditions *) -let make_results_table file_env = - (* make a Map sending each element e of list l to (f e) *) - let map_post_computation_over_procs f l = - List.fold - ~f:(fun m ((_, tenv, _, proc_desc) as p) -> - let key = (tenv, proc_desc) in - ResultsTableType.add key (f p) m) - ~init:ResultsTableType.empty - l in - let compute_post_for_procedure = (* takes proc_env as arg *) - fun (_, _, proc_name, proc_desc) -> - match Summary.read_summary proc_desc proc_name with - | Some summ -> summ - | None -> empty_post in - map_post_computation_over_procs compute_post_for_procedure file_env +(* we assume two access paths can alias if their access parts are equal (we ignore the base). *) +let can_alias access_path1 access_path2 = + List.compare AccessPath.compare_access (snd access_path1) (snd access_path2) + +module AccessListMap = Caml.Map.Make(struct + type t = AccessPath.Raw.t [@@deriving compare] + let compare = can_alias + end) let get_current_class_and_threadsafe_superclasses tenv pname = match pname with @@ -966,15 +947,6 @@ let get_possibly_unsafe_reads = get_unprotected_accesses Read let get_possibly_unsafe_writes = get_unprotected_accesses Write -(* we assume two access paths can alias if their access parts are equal (we ignore the base). *) -let can_alias access_path1 access_path2 = - List.compare AccessPath.compare_access (snd access_path1) (snd access_path2) - -module AccessListMap = Caml.Map.Make(struct - type t = AccessPath.Raw.t [@@deriving compare] - let compare = can_alias - end) - (*A helper function used in the error reporting*) let pp_accesses_sink fmt ~is_write_access sink = let access_path, _ = ThreadSafetyDomain.PathDomain.Sink.kind sink in @@ -1134,31 +1106,6 @@ let report_unsafe_accesses ~should_report aggregated_access_map = CallSite.Set.empty |> ignore -(* group accesses that may touch the same memory *) -let aggregate_accesses tab = - let open ThreadSafetyDomain in - let aggregate (threaded, _, accesses, _) tenv pdesc acc = - AccessDomain.fold - (fun pre accesses acc -> - PathDomain.Sinks.fold - (fun access acc -> - let access_path, _ = TraceElem.kind access in - let grouped_accesses = - try AccessListMap.find access_path acc - with Not_found -> [] in - AccessListMap.add - access_path - ((access, pre, threaded, tenv, pdesc) :: grouped_accesses) - acc) - (PathDomain.sinks accesses) - acc) - accesses - acc in - ResultsTableType.fold - (fun (tenv, pdesc) summary acc -> aggregate summary tenv pdesc acc) - tab - AccessListMap.empty - (* Currently we analyze if there is an @ThreadSafe annotation on at least one of the classes in a file. This might be tightened in future or even broadened in future based on other criteria *) @@ -1177,6 +1124,34 @@ let should_report_on_file file_env = not (List.exists ~f:current_class_marked_not_threadsafe file_env) && List.exists ~f:current_class_or_super_marked_threadsafe file_env +(* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for + now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells + that x.f.g may point to during execution *) +let make_results_table file_env = + let aggregate_post (threaded, _, accesses, _) tenv pdesc acc = + let open ThreadSafetyDomain in + AccessDomain.fold + (fun pre accesses acc -> + PathDomain.Sinks.fold + (fun access acc -> + let access_path, _ = TraceElem.kind access in + let grouped_accesses = + try AccessListMap.find access_path acc + with Not_found -> [] in + AccessListMap.add + access_path + ((access, pre, threaded, tenv, pdesc) :: grouped_accesses) + acc) + (PathDomain.sinks accesses) + acc) + accesses + acc in + let aggregate_posts acc (_, tenv, proc_name, proc_desc) = + match Summary.read_summary proc_desc proc_name with + | Some summary -> aggregate_post summary tenv proc_desc acc + | None -> acc in + List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty + (** Principles for race reporting. Two accesses are excluded if they are both protetected by the same lock or @@ -1208,9 +1183,7 @@ let process_results_table file_env tab = let should_report pdesc tenv = (should_report_on_all_procs && should_report_on_proc pdesc tenv) || is_thread_safe_method pdesc tenv in - - aggregate_accesses tab - |> report_unsafe_accesses ~should_report + report_unsafe_accesses ~should_report tab (* Gathers results by analyzing all the methods in a file, then post-processes the results to check an (approximation of) thread safety *)