diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 30120e556..65ead5bc7 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -174,7 +174,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> attribute_map - let add_path_to_state access_kind exp typ loc path_state id_map attribute_map tenv = + let is_unprotected is_locked pdesc = + not is_locked && not (Procdesc.is_java_synchronized pdesc) + + let add_access + exp + loc + access_kind + (astate : Domain.astate) + ~f_resolve_id + (proc_data : FormalMap.t ProcData.t) = + let get_formal_index exp typ = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with + | Some (base, _) -> FormalMap.get_formal_index base proc_data.extras + | None -> None in (* we don't want to warn on writes to the field if it is (a) thread-confined, or (b) volatile *) let is_safe_write access_path tenv = let is_thread_safe_write accesses tenv = @@ -195,77 +207,28 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> false in is_thread_safe_write (snd access_path) tenv in - let f_resolve_id = resolve_id id_map in - - if is_constant exp - then - path_state - else - List.fold - ~f:(fun acc rawpath -> - if not (is_owned (AccessPath.Raw.truncate rawpath) attribute_map) && - not (is_safe_write rawpath tenv) - then Domain.PathDomain.add_sink (Domain.make_access rawpath access_kind loc) acc - else acc) - ~init:path_state - (AccessPath.of_exp exp typ ~f_resolve_id) - - let is_unprotected is_locked pdesc = - not is_locked && not (Procdesc.is_java_synchronized pdesc) - let add_access - exp - loc - access_kind - (astate : Domain.astate) - ~f_resolve_id - (proc_data : FormalMap.t ProcData.t) = - let get_formal_index exp typ = match AccessPath.of_lhs_exp exp typ ~f_resolve_id with - | Some (base, _) -> FormalMap.get_formal_index base proc_data.extras - | None -> None in match exp with | Exp.Lfield (base_exp, _, typ) -> let open Domain in - if is_unprotected astate.locks proc_data.pdesc - then - match get_formal_index base_exp typ with - | Some formal_index -> - let pre = AccessPrecondition.Unprotected (Some formal_index) in - let conditional_accesses_for_pre = - add_path_to_state - access_kind - exp - typ - loc - (AccessDomain.get_accesses pre astate.accesses) - astate.id_map - astate.attribute_map - proc_data.tenv in - AccessDomain.add pre conditional_accesses_for_pre astate.accesses - | None -> - let unsafe_accesses = - add_path_to_state - access_kind - exp - typ - loc - (AccessDomain.get_accesses AccessPrecondition.unprotected astate.accesses) - astate.id_map - astate.attribute_map - proc_data.tenv in - AccessDomain.add AccessPrecondition.unprotected unsafe_accesses astate.accesses - else - let safe_accesses = - add_path_to_state - access_kind - exp - typ - loc - (AccessDomain.get_accesses Protected astate.accesses) - astate.id_map - astate.attribute_map - proc_data.tenv in - AccessDomain.add Protected safe_accesses astate.accesses + let pre = + if is_unprotected astate.locks proc_data.pdesc + then + match get_formal_index base_exp typ with + | Some formal_index -> AccessPrecondition.Unprotected (Some formal_index) + | None -> AccessPrecondition.unprotected + else + AccessPrecondition.Protected in + let accesses = + List.fold + ~f:(fun acc rawpath -> + if not (is_owned (AccessPath.Raw.truncate rawpath) astate.attribute_map) && + not (is_safe_write rawpath proc_data.tenv) + then PathDomain.add_sink (make_access rawpath access_kind loc) acc + else acc) + ~init:(AccessDomain.get_accesses pre astate.accesses) + (AccessPath.of_exp exp typ ~f_resolve_id) in + AccessDomain.add pre accesses astate.accesses | _ -> astate.accesses