diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 89a7d1000..3b25c4e7c 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -569,43 +569,44 @@ module TransferFunctions (CFG : ProcCfg.S) = struct exps ~init:accesses let expand_actuals actuals accesses pdesc = - let rec get_access_path = function - | HilExp.AccessPath ap - -> Some ap - | HilExp.Cast (_, e) | HilExp.Exception e - -> get_access_path e - | _ - -> None - in let open Domain in - let formals, _ = FormalMap.make pdesc |> FormalMap.get_formals_indexes |> List.unzip in - let n = min (List.length formals) (List.length actuals) in - let fmls_actls = - List.zip_exn (List.take formals n) (List.take actuals n) - |> List.filter_map ~f:(fun (fml, act) -> - match get_access_path act with Some path -> Some (fml, path) | _ -> None ) - in - let fmap = - List.fold fmls_actls ~init:AccessPath.BaseMap.empty ~f:(fun acc (fml, act) -> - AccessPath.BaseMap.add fml act acc ) - in - let expand_path (base, accesses as path) = - try - let actual = AccessPath.BaseMap.find base fmap in - AccessPath.append actual accesses - with Not_found -> path - in - let expand_pre accesses = - let sinks = - PathDomain.Sinks.fold - (fun elem acc -> - let new_elem = TraceElem.map ~f:expand_path elem in - PathDomain.Sinks.add new_elem acc) - (PathDomain.sinks accesses) PathDomain.Sinks.empty + if AccessDomain.is_empty accesses then accesses + else + let rec get_access_path = function + | HilExp.AccessPath ap + -> Some ap + | HilExp.Cast (_, e) | HilExp.Exception e + -> get_access_path e + | _ + -> None in - PathDomain.update_sinks accesses sinks - in - AccessDomain.map expand_pre accesses + let formal_map = FormalMap.make pdesc in + let expand_path (base, accesses as path) = + match FormalMap.get_formal_index base formal_map with + | Some formal_index -> ( + match List.nth actuals formal_index with + | Some actual_exp -> ( + match get_access_path actual_exp with + | Some actual + -> AccessPath.append actual accesses + | None + -> path ) + | None + -> path ) + | None + -> path + in + let expand_pre accesses = + let sinks = + PathDomain.Sinks.fold + (fun elem acc -> + let new_elem = TraceElem.map ~f:expand_path elem in + PathDomain.Sinks.add new_elem acc) + (PathDomain.sinks accesses) PathDomain.Sinks.empty + in + PathDomain.update_sinks accesses sinks + in + AccessDomain.map expand_pre accesses let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _ (instr: HilInstr.t) =