From 7a04ed32f50b9e49d62fbc9ab5d25bca8e8d1420 Mon Sep 17 00:00:00 2001 From: Peter O'Hearn Date: Tue, 15 Nov 2016 12:05:37 -0800 Subject: [PATCH] [threadsafety] interprocedural Summary: Refactoring to make thread safety checker interpocedural. This should not change funcitonality, and will only set things up for making the interprocedural part more serious. Reviewed By: sblackshear Differential Revision: D4124316 fbshipit-source-id: 6721953 --- infer/src/backend/specs.ml | 7 ++- infer/src/backend/specs.mli | 1 + infer/src/checkers/ThreadSafety.ml | 63 ++++++++++++++---------- infer/src/checkers/ThreadSafetyDomain.ml | 23 +++++++++ 4 files changed, 65 insertions(+), 29 deletions(-) create mode 100644 infer/src/checkers/ThreadSafetyDomain.ml diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 572cc483a..4cd8d1e63 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -327,6 +327,7 @@ type payload = (** Proc location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; siof : SiofDomain.astate option; + threadsafety : ThreadSafetyDomain.astate option; } type summary = @@ -449,16 +450,17 @@ let pp_summary_no_stats_specs fmt summary = F.fprintf fmt "%a@\n" pp_pair (describe_phase summary); F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map -let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof } = +let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety } = let pp_opt pp fmt = function | Some x -> pp fmt x | None -> () in - F.fprintf fmt "%a%a%a%a%a" + F.fprintf fmt "%a%a%a%a%a%a" (pp_specs pe) (get_specs_from_preposts preposts) (pp_opt (TypeState.pp TypeState.unit_ext)) typestate (pp_opt Crashcontext.pp_stacktree) crashcontext_frame (pp_opt QuandarySummary.pp) quandary (pp_opt SiofDomain.pp) siof + (pp_opt ThreadSafetyDomain.pp) threadsafety let pp_summary_text ~whole_seconds fmt summary = @@ -768,6 +770,7 @@ let empty_payload = crashcontext_frame = None; quandary = None; siof = None; + threadsafety = None; } (** [init_summary (depend_list, nodes, diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 1e6b8c5d3..061899f63 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -131,6 +131,7 @@ type payload = (** Procedure location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; siof : SiofDomain.astate option; + threadsafety : ThreadSafetyDomain.astate option; } (** Procedure summary *) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index db29d2f1f..4045cd97e 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -12,25 +12,21 @@ open! Utils module F = Format module L = Logging -module PPrawpath = PrettyPrintable.MakePPSet(struct - type t = AccessPath.raw - let compare = AccessPath.raw_compare - let pp_element = AccessPath.pp_raw - end) - -module LocksDomain = AbstractDomain.FiniteSet(StringPPSet) -module PathDomain = AbstractDomain.FiniteSet(PPrawpath) +module Summary = Summary.Make (struct + type summary = ThreadSafetyDomain.astate -module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain) + let update_payload astate payload = + { payload with Specs.threadsafety = Some astate } -module CombinedDomain = AbstractDomain.Pair (LocksDomain) (ReadWriteDomain) -(* a typical element is (){locked}, {vars and fields}) *) + let read_from_payload payload = + payload.Specs.threadsafety + end) module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG - module Domain = CombinedDomain + module Domain = ThreadSafetyDomain type extras = ProcData.no_extras let is_lock_procedure pn = Procname.equal pn BuiltinDecl.__set_locked_attribute @@ -39,22 +35,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_path_to_state exp typ pathdomainstate = IList.fold_left - (fun pathdomainstate_acc rawpath -> PathDomain.add rawpath pathdomainstate_acc) + (fun pathdomainstate_acc rawpath -> ThreadSafetyDomain.PathDomain.add + rawpath pathdomainstate_acc) pathdomainstate (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) let exec_instr ((lockstate,(readstate,writestate)) as astate) { ProcData.pdesc; } _ = let is_unprotected lockstate = - (not (Procdesc.is_java_synchronized pdesc)) && (LocksDomain.is_empty lockstate) + (not (Procdesc.is_java_synchronized pdesc)) && + (ThreadSafetyDomain.LocksDomain.is_empty lockstate) in function | Sil.Call (_, Const (Cfun pn), _, _, _) -> if is_lock_procedure pn then - ((LocksDomain.add "locked" lockstate), (readstate,writestate)) + ((ThreadSafetyDomain.LocksDomain.add "locked" lockstate), (readstate,writestate)) else if is_unlock_procedure pn then - ((LocksDomain.remove "locked" lockstate) , (readstate,writestate)) + ((ThreadSafetyDomain.LocksDomain.remove "locked" lockstate) , (readstate,writestate)) else astate @@ -83,19 +81,25 @@ module Analyzer = (Scheduler.ReversePostorder) (TransferFunctions) -let method_analysis { Callbacks.proc_desc; tenv; } = - match Analyzer.compute_post (ProcData.make_default proc_desc tenv) with +module Interprocedural = Analyzer.Interprocedural (Summary) + +(*This is a "checker"*) +let method_analysis callback = + let proc_desc = callback.Callbacks.proc_desc in + let opost = Interprocedural.checker callback ProcData.empty_extras in + match opost with | Some post -> (* I am printing to commandline and out to cater to javac and buck*) (L.stdout "\n Procedure: %s@ " (Procname.to_string (Procdesc.get_proc_name proc_desc) ) ); - L.stdout "\n POST: %a\n" CombinedDomain.pp post; + L.stdout "\n POST: %a\n" ThreadSafetyDomain.pp post; (L.out "\n Procedure: %s@ " (Procname.to_string (Procdesc.get_proc_name proc_desc) ) ); - L.out "\n POST: %a\n" CombinedDomain.pp post + L.out "\n POST: %a\n" ThreadSafetyDomain.pp post | None -> () + (* a results table is a Map where a key is an a procedure environment, i.e., something of type Idenv.t * Tenv.t * Procname.t * Procdesc.t *) @@ -111,8 +115,9 @@ let should_analyze_proc (_,tenv,proc_name,proc_desc) = not (Procname.is_class_initializer proc_name) && Procdesc.get_access proc_desc <> PredSymb.Private + (* creates a map from proc_envs to postconditions *) -let make_results_table file_env = +let make_results_table get_proc_desc file_env = let procs_to_analyze = IList.filter should_analyze_proc file_env in (* make a Map sending each element e of list l to (f e) *) @@ -121,10 +126,13 @@ let make_results_table file_env = ) ResultsTableType.empty l in let compute_post_for_procedure = (* takes proc_env as arg *) - fun (_, tenv, _, proc_desc) -> - match Analyzer.compute_post (ProcData.make_default proc_desc tenv) with + fun (idenv, tenv, proc_name, proc_desc) -> + let callback_arg = + {Callbacks.get_proc_desc; get_procs_in_file = (fun _ -> []); + idenv; tenv; proc_name; proc_desc} in + match Interprocedural.checker callback_arg ProcData.empty_extras with | Some post -> post - | None -> CombinedDomain.initial + | None -> ThreadSafetyDomain.initial in map_post_computation_over_procs compute_post_for_procedure procs_to_analyze @@ -165,7 +173,7 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate = (Procdesc.get_loc pdesc) description in - IList.iter report_one_error (IList.map snd (PathDomain.elements writestate)) + IList.iter report_one_error (IList.map snd (ThreadSafetyDomain.PathDomain.elements writestate)) (* For now, just checks if there is one active element amongst the posts of the analyzed methods. @@ -188,13 +196,14 @@ let should_analyze_file file_env = in IList.exists current_class_or_super_marked_threadsafe file_env +(*This is a "cluster checker" *) (*Gathers results by analyzing all the methods in a file, then post-processes the results to check (approximation of) thread safety *) (* file_env: (Idenv.t * Tenv.t * Procname.t * Procdesc.t) list *) -let file_analysis _ _ _ file_env = +let file_analysis _ _ get_procdesc file_env = if should_analyze_file file_env then process_results_table - (make_results_table file_env) + (make_results_table get_procdesc file_env) (* Todo: diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml new file mode 100644 index 000000000..0376c6299 --- /dev/null +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -0,0 +1,23 @@ +(* + * 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. + *) +module PPrawpath = PrettyPrintable.MakePPSet(struct + type t = AccessPath.raw + let compare = AccessPath.raw_compare + let pp_element = AccessPath.pp_raw + end) + +module LocksDomain = AbstractDomain.FiniteSet(Utils.StringPPSet) + +module PathDomain = AbstractDomain.FiniteSet(PPrawpath) + +module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain) + +include AbstractDomain.Pair (LocksDomain) (ReadWriteDomain) +(* This is the ThreadSafety abstract domain *) +(* a typical element is (){locked}, {vars and fields}) *)