diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 9f0dbb8f9..38c25acbf 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -358,10 +358,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ownership = OwnershipDomain.add (ret_base, []) OwnershipAbstractValue.owned astate.ownership in - (* Record all actuals as wobbly paths *) - let wobbly_paths = - StabilityDomain.add_wobbly_actuals actuals astate.wobbly_paths |> add_base ret_base - in + let wobbly_paths = add_base ret_base astate.wobbly_paths in {astate with accesses; ownership; wobbly_paths} | Call (ret_access_path, Direct callee_pname, actuals, call_flags, loc) -> let accesses_with_unannotated_calls = @@ -372,10 +369,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads astate.ownership proc_data in - let wobbly_paths = - StabilityDomain.add_wobbly_actuals actuals astate.wobbly_paths - |> add_base ret_access_path - in + let wobbly_paths = add_base ret_access_path astate.wobbly_paths in let astate = {astate with accesses; wobbly_paths} in let astate = match Models.get_thread callee_pname with @@ -451,13 +445,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct propagate_return ret_access_path return_ownership return_attributes actuals astate in - (* Remapping wobble paths; also bases that are not in caller's wobbly paths, i.e., callee's locals *) - let callee_wps_rebased = - Option.value_map ~default:callee_wps - ~f:(fun summary -> StabilityDomain.rebase_paths actuals summary callee_wps) - callee_pdesc + let wobbly_paths = + StabilityDomain.integrate_summary actuals callee_pdesc ~callee:callee_wps + ~caller:wobbly_paths in - let wobbly_paths = StabilityDomain.join wobbly_paths callee_wps_rebased in let threads = ThreadsDomain.integrate_summary ~caller_astate:astate.threads ~callee_astate:threads @@ -553,15 +544,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let attribute_map = AttributeMapDomain.propagate_assignment lhs_access_path rhs_exp astate.attribute_map in - (* [TODO] Do not add this path as wobbly, if it's the _first_ - initialization of a local variable (e.g. A z = getA(); --> - now z is considered wobbly). - - At the moment, I don't know how to distinguish those from - plain re-assignnments, so a lot of spurious wobbly paths is - negerated. *) let wobbly_paths = - StabilityDomain.add_wobbly_paths_assign lhs_access_path rhs_exp astate.wobbly_paths + StabilityDomain.add_assign lhs_access_path rhs_exp astate.wobbly_paths in {astate with accesses; ownership; attribute_map; wobbly_paths} | Assume (assume_exp, _, _, loc) -> @@ -924,33 +908,15 @@ let ignore_var v = Var.is_global v || Var.is_return v (* Checking for a wobbly path *) let get_contaminated_race_message access wobbly_paths = let open RacerDDomain in - let wobbly_path_opt = - match TraceElem.kind access with - | TraceElem.Kind.Read access_path - | Write access_path - (* Access paths rooted in static variables are always race-prone, - hence do not complain about contamination. *) - when not (access_path |> fst |> fst |> ignore_var) -> - let proper_prefix_path, _ = AccessPath.truncate access_path in - let base, accesses = proper_prefix_path in - let rec prefix_in_wobbly_paths prefix = function - | [] -> - let wobbly = (base, []) in - if StabilityDomain.mem (AccessPath.Abs.Exact wobbly) wobbly_paths then - Some (wobbly, access_path) - else None - | access :: accesses -> - let prefix' = prefix @ [access] in - let candidate = (base, prefix') in - if StabilityDomain.mem (AccessPath.Abs.Exact candidate) wobbly_paths then - Some (candidate, access_path) - else prefix_in_wobbly_paths prefix' accesses - in - prefix_in_wobbly_paths [] accesses - | _ -> - None - in - Option.map wobbly_path_opt ~f:(fun _ -> " [wob]") + match TraceElem.kind access with + | TraceElem.Kind.Read access_path + | Write access_path + (* Access paths rooted in static variables are always race-prone, + hence do not complain about contamination. *) + when not (access_path |> fst |> fst |> ignore_var) -> + if StabilityDomain.exists_proper_prefix access_path wobbly_paths then Some " [wob]" else None + | _ -> + None let log_issue current_pname ~loc ~ltr ~access exn = diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index e7772851c..cec4dcaa3 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -506,106 +506,81 @@ module AttributeMapDomain = struct end module StabilityDomain = struct - include AccessTree.PathSet (AccessTree.DefaultConfig) + include AbstractDomain.FiniteSet (AccessPath) - let get_all_paths t = - fold - (fun paths z _ -> - match z with AccessPath.Abs.Abstracted p | AccessPath.Abs.Exact p -> p :: paths ) - t [] + let is_prefix (base, accesses) (base', accesses') = + AccessPath.equal_base base base' + && List.is_prefix ~equal:AccessPath.equal_access ~prefix:accesses accesses' - let add_path (access_path: AccessPath.t) t = - let (base, _), accesses = access_path in - (* Without this check, short prefixes will override longer paths in the tree *) - if should_skip_var base || mem (AccessPath.Abs.Abstracted access_path) t then t - else - match (base, accesses) with - (* Do not add a vanilla "this" as a prefix *) - | Var.ProgramVar pvar, [] - when Pvar.is_this pvar -> - t - | _ -> - let ap_abs = AccessPath.Abs.Exact access_path in - add_trace ap_abs true t - - - let add_wobbly_path_exp exp paths = - let access_paths = AccessExpression.to_access_paths (HilExp.get_access_exprs exp) in - List.fold ~f:(fun acc p -> add_path p acc) access_paths ~init:paths - - - let add_wobbly_actuals exps paths = - (* Checking conditions for inter-procedural stability: - automatically add duplicating actuals, "deep" stability - checking will be handled by processing the method's footprint - and rebasing (see StabilityDomain.rebase_paths). *) - let is_dup_access_path e = - List.count exps ~f:(fun x -> - match (x, e) with - | HilExp.AccessExpression ae1, HilExp.AccessExpression ae2 -> - AccessPath.equal - (AccessExpression.to_access_path ae1) - (AccessExpression.to_access_path ae2) - | _, _ -> - false ) - > 1 - in - let is_prefix_exp x e = - match (x, e) with - | HilExp.AccessExpression ae1, HilExp.AccessExpression ae2 -> - let open AccessExpression in - let ap1, ap2 = (to_access_path ae1, to_access_path ae2) in - AccessPath.is_prefix ap1 ap2 && not (AccessPath.equal ap1 ap2) - | _ -> + let is_proper_prefix (base, accesses) (base', accesses') = + let rec aux xs ys = + match (xs, ys) with + | [], _ -> + not (List.is_empty ys) + | _, [] -> false + | w :: ws, z :: zs -> + AccessPath.equal_access w z && aux ws zs in - let find_all_prefixes e = List.filter exps ~f:(fun x -> is_prefix_exp x e) in - let with_duplicates = - List.fold exps ~init:paths ~f:(fun acc e -> - if is_dup_access_path e then add_wobbly_path_exp e acc else acc ) - in - let with_prefixes = - List.fold exps ~init:with_duplicates ~f:(fun acc_paths e -> - List.fold (find_all_prefixes e) ~init:acc_paths ~f:(fun acc1 e1 -> - add_wobbly_path_exp e1 acc1 ) ) - in - with_prefixes + AccessPath.equal_base base base' && aux accesses accesses' + + + let exists_prefix path_to_check t = exists (fun path -> is_prefix path path_to_check) t + + let exists_proper_prefix path_to_check t = + exists (fun path -> is_proper_prefix path path_to_check) t + + let add_path path_to_add t = + if should_skip_var (fst path_to_add |> fst) || exists_prefix path_to_add t then t + else filter (fun path -> is_prefix path_to_add path |> not) t |> add path_to_add - let add_wobbly_paths_assign lhs_path rhs_exp paths = - let paths_with_lhs = add_path lhs_path paths in - let paths_with_lsh_rhs = add_wobbly_path_exp rhs_exp paths_with_lhs in - paths_with_lsh_rhs + let add_exp exp paths = + AccessExpression.to_access_paths (HilExp.get_access_exprs exp) + |> List.fold ~f:(fun acc p -> add_path p acc) ~init:paths - let rebase_paths actuals pdesc t = + + let add_assign lhs_path rhs_exp paths = add_path lhs_path paths |> add_exp rhs_exp + + let actual_to_access_path actual_exp = + match HilExp.get_access_exprs actual_exp with + | [actual] -> + Some (AccessExpression.to_access_path actual) + | _ -> + None + + + let rebase actuals pdesc t = let formal_map = FormalMap.make pdesc in - let remove_pure_formals paths = - List.filter paths ~f:(fun p -> - match p with - | base, [] when FormalMap.get_formal_index base formal_map |> Option.is_some -> - false - | _ -> - true ) + let expand_path ((base, accesses) as p) = + FormalMap.get_formal_index base formal_map |> Option.bind ~f:(List.nth actuals) + |> Option.bind ~f:actual_to_access_path + |> Option.value_map ~default:p ~f:(fun ap -> AccessPath.append ap accesses) + in + fold + (fun ((_, accesses) as path) acc -> + if List.is_empty accesses then acc else add_path (expand_path path) acc ) + t empty + + + let integrate_summary actuals pdesc_opt ~callee ~caller = + let rebased = + Option.value_map pdesc_opt ~default:callee ~f:(fun pdesc -> rebase actuals pdesc callee) 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 HilExp.get_access_exprs actual_exp with - | [actual] -> - AccessPath.append (AccessExpression.to_access_path actual) accesses - | _ -> - path ) - | None -> - path ) - | None -> - path + let joined = join rebased caller in + let actual_aps = List.filter_map actuals ~f:actual_to_access_path in + let rec aux acc left right = + match right with + | [] -> + acc + | ap :: aps -> + let all = List.rev_append left aps in + let acc' = if List.exists all ~f:(is_prefix ap) then add_path ap acc else acc in + aux acc' (ap :: left) aps in - get_all_paths t |> remove_pure_formals |> List.map ~f:expand_path - |> List.fold ~f:(fun acc p -> add_path p acc) ~init:empty + aux joined [] actual_aps end type astate = diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 5e7413906..1859b39d4 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -196,15 +196,16 @@ module AttributeMapDomain : sig end module StabilityDomain : sig - include module type of AccessTree.PathSet (AccessTree.DefaultConfig) + include AbstractDomain.WithBottom - val rebase_paths : HilExp.t list -> Procdesc.t -> t -> t + val add_assign : AccessPath.t -> HilExp.t -> astate -> astate - val add_wobbly_paths_assign : AccessPath.t -> HilExp.t -> t -> t + val add_path : AccessPath.t -> astate -> astate - val add_path : AccessPath.t -> t -> t + val exists_proper_prefix : AccessPath.t -> astate -> bool - val add_wobbly_actuals : HilExp.t list -> t -> t + val integrate_summary : + HilExp.t list -> Procdesc.t option -> callee:astate -> caller:astate -> astate end type astate = diff --git a/infer/tests/codetoanalyze/cpp/racerd/issues.exp b/infer/tests/codetoanalyze/cpp/racerd/issues.exp index 9a3ebdc03..0a73b7125 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/issues.exp +++ b/infer/tests/codetoanalyze/cpp/racerd/issues.exp @@ -2,9 +2,9 @@ codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get2, 36, LOCK_CONSISTENCY_VI codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get4, 43, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,access to `this.suspiciously_read`,,access to `this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to basics::Basic_get_private_suspiciously_read,access to `this.suspiciously_read`,,access to `this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 81, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,access to `this.single_lock_suspiciously_read`,,access to `this.single_lock_suspiciously_read`] -codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`] -codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`] diff --git a/infer/tests/codetoanalyze/java/stability/Intraprocedural.java b/infer/tests/codetoanalyze/java/stability/Intraprocedural.java index 7d6df3553..24e638b0a 100644 --- a/infer/tests/codetoanalyze/java/stability/Intraprocedural.java +++ b/infer/tests/codetoanalyze/java/stability/Intraprocedural.java @@ -33,7 +33,7 @@ static class Field { x = a.f.g; } - public void stable_bad() { + public void FN_stable_bad() { int x = 42; synchronized (this) { a.f.g = 101; diff --git a/infer/tests/codetoanalyze/java/stability/issues.exp b/infer/tests/codetoanalyze/java/stability/issues.exp index 50efb8588..4022221c5 100644 --- a/infer/tests/codetoanalyze/java/stability/issues.exp +++ b/infer/tests/codetoanalyze/java/stability/issues.exp @@ -1,5 +1,3 @@ -codetoanalyze/java/stability/Interprocedural.java, void Interprocedural$Field.stable_bad(), 45, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.codetoanalyze.java.checkers.Interprocedural$Field.a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,,access to `this.codetoanalyze.java.checkers.Interprocedural$Field.a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`] codetoanalyze/java/stability/Interprocedural.java, void Interprocedural$Param.stable_bad(Interprocedural$A), 72, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`] codetoanalyze/java/stability/Interprocedural.java, void Interprocedural$Param2.stable_bad(Interprocedural$A), 90, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`] -codetoanalyze/java/stability/Intraprocedural.java, void Intraprocedural$Field.stable_bad(), 41, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.codetoanalyze.java.checkers.Intraprocedural$Field.a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,,access to `this.codetoanalyze.java.checkers.Intraprocedural$Field.a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`] codetoanalyze/java/stability/Intraprocedural.java, void Intraprocedural$Param.stable_bad(Intraprocedural$A), 61, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,,access to `a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`]