From 2386bc8f67f5ed72d84b897a3582ca7f43b6bde8 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 12 Dec 2016 19:32:40 -0800 Subject: [PATCH] [thread-safety] use record type in domain Summary: We're about to add another element to the abstract domain, and a 4-tuple is a bit too cumbersome to work with. Reviewed By: jberdine Differential Revision: D4315292 fbshipit-source-id: d04699f --- infer/src/checkers/ThreadSafety.ml | 57 ++++++++++++++---------- infer/src/checkers/ThreadSafetyDomain.ml | 47 +++++++++++++++++-- 2 files changed, 76 insertions(+), 28 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index b9c7f203c..3796a9398 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -83,7 +83,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct path_state (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) - let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; tenv; } _ = + let exec_instr + ({ ThreadSafetyDomain.locks; reads; writes; } as astate) + { ProcData.pdesc; tenv; } _ = + let is_unprotected is_locked = not is_locked && not (Procdesc.is_java_synchronized pdesc) in function @@ -92,41 +95,44 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* assuming that modeled procedures do not have useful summaries *) match get_lock_model pn with | Lock -> - true, snd astate + { astate with locks = true; } | Unlock -> - false, snd astate + { astate with locks = false; } | None -> begin match Summary.read_summary pdesc pn with - | Some (callee_lockstate, (callee_reads, callee_writes)) -> - let lockstate' = callee_lockstate || lockstate in - let _, read_writestate' = + | Some callee_astate -> + let locks' = callee_astate.locks || locks in + let astate' = (* TODO (14842325): report on constructors that aren't threadsafe (e.g., constructors that access static fields) *) - if is_unprotected lockstate' && + if is_unprotected locks' && not (is_initializer tenv pn) && not (is_call_to_builder_class_method pn) then let call_site = CallSite.make pn loc in - let callee_readstate = - ThreadSafetyDomain.PathDomain.with_callsite callee_reads call_site in - let callee_writestate = - ThreadSafetyDomain.PathDomain.with_callsite callee_writes call_site in - let callee_astate = - callee_lockstate, (callee_readstate, callee_writestate) in - ThreadSafetyDomain.join callee_astate astate + 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 else astate in - lockstate', read_writestate' + { astate' with locks = locks' } | None -> astate end end | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, loc) -> - if is_unprotected lockstate then (* abstracts no lock being held*) - (lockstate, (readstate, add_path_to_state lhsfield typ loc writestate)) - else astate + if is_unprotected locks (* abstracts no lock being held *) + then + let writes' = add_path_to_state lhsfield typ loc writes in + { astate with writes = writes'; } + else + astate (* Note: it appears that the third arg of Store is never an Lfield in the targets of, our translations, which is why we have not covered that case. *) @@ -134,9 +140,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct failwith "Unexpected store instruction with rhs field" | Sil.Load (_, (Lfield ( _, _, typ) as rhsfield) , _, loc) -> - if is_unprotected lockstate then (* abstracts no lock being held*) - (lockstate, (add_path_to_state rhsfield typ loc readstate, writestate)) - else astate + 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 | _ -> astate @@ -224,7 +233,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 (_, (_, callee_trace)) -> callee_trace + | Some astate -> astate.writes | _ -> PathDomain.initial in let report_one_path ((_, sinks) as path) = let pp_accesses fmt sink = @@ -261,9 +270,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 ( _,( _, writestate)) -> + (fun proc_env (astate : ThreadSafetyDomain.astate) -> if should_report_on_proc proc_env then - report_thread_safety_errors proc_env writestate + report_thread_safety_errors proc_env astate.writes else () ) tab diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index f7c12c069..e7a031d38 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -54,8 +54,47 @@ module LocksDomain = AbstractDomain.BooleanAnd module PathDomain = SinkTrace.Make(TraceElem) -module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain) +type astate = + { locks : LocksDomain.astate; + reads : PathDomain.astate; + writes : PathDomain.astate; + } -include AbstractDomain.Pair (LocksDomain) (ReadWriteDomain) -(* This is the ThreadSafety abstract domain *) -(* a typical element is (){locked}, {vars and fields}) *) +let initial = + let locks = LocksDomain.initial in + let reads = PathDomain.initial in + let writes = PathDomain.initial in + { locks; reads; writes; } + +let (<=) ~lhs ~rhs = + if phys_equal lhs rhs + then true + else + LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && + PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads && + PathDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes + +let join astate1 astate2 = + if phys_equal astate1 astate2 + then + astate1 + else + 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 widen ~prev ~next ~num_iters = + if phys_equal prev next + then + prev + else + 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 pp fmt { locks; reads; writes; } = + F.fprintf + fmt + "Locks: %a Reads: %a Writes: %a" LocksDomain.pp locks PathDomain.pp reads PathDomain.pp writes