From 8e212f046881fdf821e0e1cc3f5efb96b6d73d66 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 14 Dec 2016 09:17:41 -0800 Subject: [PATCH] [thread-safety] use id map to decompile tmp vars into access paths Summary: This is required to maintain a set of owned access paths in a subsequent diff. Reviewed By: jberdine Differential Revision: D4318859 fbshipit-source-id: bd1a9fa --- infer/src/backend/specs.ml | 4 +- infer/src/backend/specs.mli | 2 +- infer/src/checkers/ThreadSafety.ml | 114 +++++++++++++---------- infer/src/checkers/ThreadSafetyDomain.ml | 37 ++++++-- 4 files changed, 96 insertions(+), 61 deletions(-) diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 731b3ccf8..9b6230350 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -321,7 +321,7 @@ type payload = (** Proc location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; siof : SiofDomain.astate option; - threadsafety : ThreadSafetyDomain.astate option; + threadsafety : ThreadSafetyDomain.summary option; } type summary = @@ -456,7 +456,7 @@ let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; (pp_opt Crashcontext.pp_stacktree) crashcontext_frame (pp_opt QuandarySummary.pp) quandary (pp_opt SiofDomain.pp) siof - (pp_opt ThreadSafetyDomain.pp) threadsafety + (pp_opt ThreadSafetyDomain.pp_summary) threadsafety let pp_summary_text ~whole_seconds fmt summary = diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index f7c06c090..6eef3255d 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -133,7 +133,7 @@ type payload = (** Procedure location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; siof : SiofDomain.astate option; - threadsafety : ThreadSafetyDomain.astate option; + threadsafety : ThreadSafetyDomain.summary option; } (** Procedure summary *) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index fd06b5225..e03e8a98d 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -14,10 +14,10 @@ module L = Logging module Summary = Summary.Make (struct - type summary = ThreadSafetyDomain.astate + type summary = ThreadSafetyDomain.summary - let update_payload astate payload = - { payload with Specs.threadsafety = Some astate } + let update_payload summary payload = + { payload with Specs.threadsafety = Some summary } let read_from_payload payload = payload.Specs.threadsafety @@ -47,7 +47,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type lock_model = | Lock | Unlock - | None + | NoEffect let get_lock_model = function | Procname.Java java_pname -> @@ -67,24 +67,35 @@ module TransferFunctions (CFG : ProcCfg.S) = struct "unlock" -> Unlock | _ -> - None + NoEffect end | pname when Procname.equal pname BuiltinDecl.__set_locked_attribute -> Lock | pname when Procname.equal pname BuiltinDecl.__delete_locked_attribute -> Unlock | _ -> - None + NoEffect - let add_path_to_state exp typ loc path_state = + let resolve_id (id_map : IdAccessPathMapDomain.astate) id = + try Some (IdAccessPathMapDomain.find id id_map) + with Not_found -> None + + let add_path_to_state exp typ loc path_state id_map = + let f_resolve_id = resolve_id id_map in IList.fold_left (fun acc rawpath -> ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc) path_state - (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) + (AccessPath.of_exp exp typ ~f_resolve_id) + + let analyze_id_assignment lhs_id rhs_exp rhs_typ { ThreadSafetyDomain.id_map; } = + let f_resolve_id = resolve_id id_map in + match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with + | Some rhs_access_path -> IdAccessPathMapDomain.add lhs_id rhs_access_path id_map + | None -> id_map let exec_instr - ({ ThreadSafetyDomain.locks; reads; writes; } as astate) + ({ ThreadSafetyDomain.locks; reads; writes; id_map; } as astate) { ProcData.pdesc; tenv; } _ = let is_unprotected is_locked = @@ -98,11 +109,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with locks = true; } | Unlock -> { astate with locks = false; } - | None -> + | NoEffect -> begin match Summary.read_summary pdesc pn with - | Some callee_astate -> - let locks' = callee_astate.locks || locks in + | Some (callee_locks, callee_reads, callee_writes) -> + let locks' = callee_locks || locks in let astate' = (* TODO (14842325): report on constructors that aren't threadsafe (e.g., constructors that access static fields) *) @@ -111,13 +122,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct not (is_call_to_builder_class_method pn) then let call_site = CallSite.make pn loc in - let callee_reads = - ThreadSafetyDomain.PathDomain.with_callsite callee_astate.reads call_site in - let callee_writes = - ThreadSafetyDomain.PathDomain.with_callsite callee_astate.writes call_site in - let callee_astate' = - { callee_astate with ThreadSafetyDomain.reads = callee_reads; writes = callee_writes; } in - ThreadSafetyDomain.join callee_astate' astate + let reads' = + ThreadSafetyDomain.PathDomain.with_callsite callee_reads call_site + |> ThreadSafetyDomain.PathDomain.join reads in + let writes' = + ThreadSafetyDomain.PathDomain.with_callsite callee_writes call_site + |> ThreadSafetyDomain.PathDomain.join writes in + { astate with reads = reads'; writes = writes'; } else astate in { astate' with locks = locks' } @@ -126,10 +137,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end end + | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _) when Pvar.is_frontend_tmp lhs_pvar -> + let id_map' = analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate in + { astate with id_map = id_map'; } + | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, loc) -> if is_unprotected locks (* abstracts no lock being held *) then - let writes' = add_path_to_state lhsfield typ loc writes in + let writes' = add_path_to_state lhsfield typ loc writes id_map in { astate with writes = writes'; } else astate @@ -139,14 +154,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.Store (_, _, Lfield _, _) -> failwith "Unexpected store instruction with rhs field" - | Sil.Load (_, (Lfield ( _, _, typ) as rhsfield) , _, loc) -> - if is_unprotected locks (* abstracts no lock being held *) - then - let reads' = add_path_to_state rhsfield typ loc reads in - { astate with reads = reads'; } - else - astate - + | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) -> + let id_map' = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in + let reads' = + match rhs_exp with + | Lfield ( _, _, typ) when is_unprotected locks -> + add_path_to_state rhs_exp typ loc reads id_map + | _ -> + reads in + { astate with Domain.reads = reads'; id_map = id_map'; } | _ -> astate end @@ -159,26 +175,19 @@ module Analyzer = module Interprocedural = AbstractInterpreter.Interprocedural (Summary) +(* convert the abstract state to a summary by dropping the id map *) +let compute_post pdesc = + match Analyzer.compute_post pdesc with + | Some { locks; reads; writes; } -> Some (locks, reads, writes) + | None -> None + (*This is a "checker"*) let method_analysis callback = - let proc_desc = callback.Callbacks.proc_desc in - let opost = - Interprocedural.compute_and_store_post - ~compute_post:Analyzer.compute_post - ~make_extras:ProcData.make_empty_extras - callback 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" ThreadSafetyDomain.pp post; - (L.out "\n Procedure: %s@ " - (Procname.to_string (Procdesc.get_proc_name proc_desc) ) - ); - L.out "\n POST: %a\n" ThreadSafetyDomain.pp post - | None -> () - + Interprocedural.compute_and_store_post + ~compute_post + ~make_extras:ProcData.make_empty_extras + callback + |> ignore (* 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 @@ -207,11 +216,14 @@ let make_results_table get_proc_desc file_env = idenv; tenv; proc_name; proc_desc} in match Interprocedural.compute_and_store_post - ~compute_post:Analyzer.compute_post + ~compute_post ~make_extras:ProcData.make_empty_extras callback_arg with | Some post -> post - | None -> ThreadSafetyDomain.initial + | None -> + ThreadSafetyDomain.LocksDomain.initial, + ThreadSafetyDomain.PathDomain.initial, + ThreadSafetyDomain.PathDomain.initial in map_post_computation_over_procs compute_post_for_procedure file_env @@ -241,7 +253,7 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) trace = let open ThreadSafetyDomain in let trace_of_pname callee_pname = match Summary.read_summary pdesc callee_pname with - | Some astate -> astate.writes + | Some (_, _, writes) -> writes | _ -> PathDomain.initial in let report_one_path ((_, sinks) as path) = let pp_accesses fmt sink = @@ -278,9 +290,9 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) trace = This indicates that the method races with itself. To be refined later. *) let process_results_table tab = ResultsTableType.iter (* report errors for each method *) - (fun proc_env (astate : ThreadSafetyDomain.astate) -> + (fun proc_env (_, _, writes) -> if should_report_on_proc proc_env then - report_thread_safety_errors proc_env astate.writes + report_thread_safety_errors proc_env writes else () ) tab diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index e7a031d38..f0e15fac3 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -55,16 +55,26 @@ module LocksDomain = AbstractDomain.BooleanAnd module PathDomain = SinkTrace.Make(TraceElem) type astate = - { locks : LocksDomain.astate; + { + locks : LocksDomain.astate; + (** boolean that is true if a lock must currently be held *) reads : PathDomain.astate; + (** access paths read outside of synchronization *) writes : PathDomain.astate; + (** access paths written outside of synchronization *) + id_map : IdAccessPathMapDomain.astate; + (** map used to decompile temporary variables into access paths *) } +(** same as astate, but without [id_map] (since it's local) *) +type summary = LocksDomain.astate * PathDomain.astate * PathDomain.astate + let initial = let locks = LocksDomain.initial in let reads = PathDomain.initial in let writes = PathDomain.initial in - { locks; reads; writes; } + let id_map = IdAccessPathMapDomain.initial in + { locks; reads; writes; id_map; } let (<=) ~lhs ~rhs = if phys_equal lhs rhs @@ -72,7 +82,8 @@ let (<=) ~lhs ~rhs = else LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads && - PathDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes + PathDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes && + IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map let join astate1 astate2 = if phys_equal astate1 astate2 @@ -82,7 +93,8 @@ let join astate1 astate2 = let locks = LocksDomain.join astate1.locks astate2.locks in let reads = PathDomain.join astate1.reads astate2.reads in let writes = PathDomain.join astate1.writes astate2.writes in - { locks; reads; writes; } + let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in + { locks; reads; writes; id_map; } let widen ~prev ~next ~num_iters = if phys_equal prev next @@ -92,9 +104,20 @@ let widen ~prev ~next ~num_iters = let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in let reads = PathDomain.widen ~prev:prev.reads ~next:next.reads ~num_iters in let writes = PathDomain.widen ~prev:prev.writes ~next:next.writes ~num_iters in - { locks; reads; writes; } + let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in + { locks; reads; writes; id_map; } + +let pp_summary fmt (locks, reads, writes) = + F.fprintf + fmt + "Locks: %a Reads: %a Writes: %a" + LocksDomain.pp locks + PathDomain.pp reads + PathDomain.pp writes -let pp fmt { locks; reads; writes; } = +let pp fmt { locks; reads; writes; id_map; } = F.fprintf fmt - "Locks: %a Reads: %a Writes: %a" LocksDomain.pp locks PathDomain.pp reads PathDomain.pp writes + "%a Id Map: %a" + pp_summary (locks, reads, writes) + IdAccessPathMapDomain.pp id_map