[racerd] Instrumenting the concurrency analysis with tracking of access path stability.

Reviewed By: sblackshear

Differential Revision: D6414244

fbshipit-source-id: d2acc16

infer/src/concurrency/RacerD.ml

@@ -227,7 +227,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       ; threads= ThreadsDomain.empty
       ; accesses= callee_accesses
       ; return_ownership
-      ; return_attributes= AttributeSetDomain.empty }
+      ; return_attributes= AttributeSetDomain.empty
+      ; wobbly_paths= StabilityDomain.empty }
 
 
   let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate: Domain.astate) =
@@ -379,6 +380,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     AccessDomain.fold update_accesses accesses caller_astate.accesses
 
 
+  (***********************************************************************)
+  (*              Wobbly paths and where to find them.                   *)
+  (***********************************************************************)
+  (***********************************************************************)
+
   let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _
       (instr: HilInstr.t) =
     let open Domain in
@@ -393,7 +399,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let ownership =
           OwnershipDomain.add (ret_base, []) OwnershipAbstractValue.owned astate.ownership
         in
-        {astate with accesses; ownership}
+        (* Record all actuals as wobbly paths *)
+        let wobbly_paths = StabilityDomain.add_wobbly_actuals actuals astate.wobbly_paths in
+        {astate with accesses; ownership; wobbly_paths}
     | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc)
       -> (
         let accesses_with_unannotated_calls =
@@ -404,7 +412,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads
             astate.ownership proc_data
         in
-        let astate = {astate with accesses} in
+        let wobbly_paths = StabilityDomain.add_wobbly_actuals actuals astate.wobbly_paths in
+        let astate = {astate with accesses; wobbly_paths} in
         let astate =
           match Models.get_thread callee_pname with
           | BackgroundThread ->
@@ -472,7 +481,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                       in
                       {summary with accesses= rebased_accesses} )
                 with
-                | Some {threads; locks; accesses; return_ownership; return_attributes} ->
+                | Some
+                    { threads
+                    ; locks
+                    ; accesses
+                    ; return_ownership
+                    ; return_attributes
+                    ; wobbly_paths= callee_wps } ->
                     let locks = LocksDomain.join locks astate.locks in
                     let threads =
                       match (astate.threads, threads) with
@@ -490,7 +505,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     let ownership, attribute_map =
                       propagate_return ret_opt return_ownership return_attributes actuals astate
                     in
-                    {locks; threads; accesses; ownership; attribute_map}
+                    (* 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
+                    in
+                    let wobbly_paths = StabilityDomain.join wobbly_paths callee_wps_rebased in
+                    {locks; threads; accesses; ownership; attribute_map; wobbly_paths}
                 | None ->
                     let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
                       (* assume non-interface methods with no summary and no parameters return
@@ -582,7 +604,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         in
         let ownership = propagate_ownership lhs_access_path rhs_exp astate.ownership in
         let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in
-        {astate with accesses; ownership; attribute_map}
+        (* [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
+        in
+        {astate with accesses; ownership; attribute_map; wobbly_paths}
     | Assume (assume_exp, _, _, loc) ->
         let rec eval_binop op var e1 e2 =
           match (eval_bexp var e1, eval_bexp var e2) with
@@ -662,7 +694,8 @@ let empty_post : RacerDDomain.summary =
   ; locks= RacerDDomain.LocksDomain.empty
   ; accesses= RacerDDomain.AccessDomain.empty
   ; return_ownership= RacerDDomain.OwnershipAbstractValue.unowned
-  ; return_attributes= RacerDDomain.AttributeSetDomain.empty }
+  ; return_attributes= RacerDDomain.AttributeSetDomain.empty
+  ; wobbly_paths= RacerDDomain.StabilityDomain.empty }
 
 
 let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
@@ -736,7 +769,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
         {RacerDDomain.empty with ownership; threads}
     in
     match Analyzer.compute_post proc_data ~initial with
-    | Some {threads; locks; accesses; ownership; attribute_map} ->
+    | Some {threads; locks; accesses; ownership; attribute_map; wobbly_paths} ->
         let return_var_ap =
           AccessPath.of_pvar
             (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
@@ -747,7 +780,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
           try AttributeMapDomain.find return_var_ap attribute_map with Not_found ->
             AttributeSetDomain.empty
         in
-        let post = {threads; locks; accesses; return_ownership; return_attributes} in
+        let post = {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} in
         Summary.update_summary post summary
     | None ->
         summary
@@ -919,7 +952,45 @@ let make_trace ~report_kind original_path pdesc =
       (original_trace, original_end, None)
 
 
-let report_thread_safety_violation tenv pdesc ~make_description ~report_kind access thread =
+let ignore_var v = Var.is_global v || Var.is_return v
+
+(* Checking for a wobbly path *)
+let contaminated_race_msg 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 (wobbly_path, access_path) ->
+      F.asprintf
+        "@\n\nNote that the prefix path %a has been contaminated during the execution, so the reported race on %a might be a false positive.@\n\n"
+        AccessPath.pp wobbly_path AccessPath.pp access_path )
+
+
+let report_thread_safety_violation tenv pdesc ~make_description ~report_kind access thread
+    wobbly_paths =
   let open RacerDDomain in
   let pname = Procdesc.get_proc_name pdesc in
   let report_one_path ((_, sinks) as path) =
@@ -952,7 +1023,12 @@ let report_thread_safety_violation tenv pdesc ~make_description ~report_kind acc
       (* why we are reporting it *)
       let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in
       let error_message = F.sprintf "%s%s" description explanation in
-      let exn = Exceptions.Checkers (issue_type, Localise.verbatim_desc error_message) in
+      let contaminated = contaminated_race_msg access wobbly_paths in
+      let exn =
+        Exceptions.Checkers
+          ( issue_type
+          , Localise.verbatim_desc (error_message ^ Option.value contaminated ~default:"") )
+      in
       let end_locs = Option.to_list original_end @ Option.to_list conflict_end in
       let access = IssueAuxData.encode (pname, access, end_locs) in
       Reporting.log_error_deprecated ~store_summary:true pname ~loc ~ltr ~access exn
@@ -971,7 +1047,7 @@ let report_unannotated_interface_violation tenv pdesc access thread reported_pna
           class_name MF.pp_monospaced "@ThreadSafe"
       in
       report_thread_safety_violation tenv pdesc ~make_description ~report_kind:UnannotatedInterface
-        access thread
+        access thread RacerDDomain.StabilityDomain.empty
   | _ ->
       (* skip reporting on C++ *)
       ()
@@ -1000,7 +1076,8 @@ type reported_access =
   ; threads: RacerDDomain.ThreadsDomain.astate
   ; precondition: RacerDDomain.AccessData.t
   ; tenv: Tenv.t
-  ; procdesc: Procdesc.t }
+  ; procdesc: Procdesc.t
+  ; wobbly_paths: RacerDDomain.StabilityDomain.astate }
 
 let make_read_write_race_description ~read_is_sync (conflict: reported_access) pname
     final_sink_site initial_sink_site final_sink =
@@ -1095,7 +1172,8 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
           reported
     else reported
   in
-  let report_unsafe_access {access; precondition; threads; tenv; procdesc} accesses reported_acc =
+  let report_unsafe_access {access; precondition; threads; tenv; procdesc; wobbly_paths} accesses
+      reported_acc =
     let pname = Procdesc.get_proc_name procdesc in
     if is_duplicate_report access pname reported_acc then reported_acc
     else
@@ -1133,7 +1211,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
               let conflict = List.hd writes_on_background_thread in
               report_thread_safety_violation tenv procdesc
                 ~make_description:make_unprotected_write_description
-                ~report_kind:(WriteWriteRace conflict) access threads ;
+                ~report_kind:(WriteWriteRace conflict) access threads wobbly_paths ;
               update_reported access pname reported_acc
             else reported_acc
         | _ ->
@@ -1163,7 +1241,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
             let conflict = List.hd_exn all_writes in
             report_thread_safety_violation tenv procdesc
               ~make_description:(make_read_write_race_description ~read_is_sync:false conflict)
-              ~report_kind:(ReadWriteRace conflict.access) access threads ;
+              ~report_kind:(ReadWriteRace conflict.access) access threads wobbly_paths ;
             update_reported access pname reported_acc
           else reported_acc
       | Access.Read _ | ContainerRead _ ->
@@ -1191,7 +1269,7 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
             (* protected read with conflicting unprotected write(s). warn. *)
             report_thread_safety_violation tenv procdesc
               ~make_description:(make_read_write_race_description ~read_is_sync:true conflict)
-              ~report_kind:(ReadWriteRace conflict.access) access threads ;
+              ~report_kind:(ReadWriteRace conflict.access) access threads wobbly_paths ;
             update_reported access pname reported_acc
           else reported_acc
   in
@@ -1331,8 +1409,8 @@ module MayAliasQuotientedAccessListMap : QuotientedAccessListMap = struct
           AccessPath.equal p1 p2
 
 
-  (* equivalence relation computing whether two access paths may refer to the
-     same heap location. *)
+  (* equivalence relation computing whether two access paths may refer
+     to the same heap location. *)
   let may_alias tenv p1 p2 =
     let open Typ in
     let open AccessPath in
@@ -1403,12 +1481,13 @@ let should_filter_access access =
       false
 
 
-(* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for
-   now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells
+(* create a map from [abstraction of a memory loc] -> accesses that
+   may touch that memory loc. for now, our abstraction is an access
+   path like x.f.g whose concretization is the set of memory cells
    that x.f.g may point to during execution *)
 let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env =
   let open RacerDDomain in
-  let aggregate_post {threads; accesses} tenv procdesc acc =
+  let aggregate_post {threads; accesses; wobbly_paths} tenv procdesc acc =
     AccessDomain.fold
       (fun precondition accesses acc ->
         PathDomain.Sinks.fold
@@ -1416,7 +1495,9 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env
             let access_kind = TraceElem.kind access in
             if should_filter_access access_kind then acc
             else
-              let reported_access = {access; precondition; threads; tenv; procdesc} in
+              let reported_access : reported_access =
+                {access; threads; precondition; tenv; procdesc; wobbly_paths}
+              in
               AccessListMap.add access_kind reported_access acc )
           (PathDomain.sinks accesses) acc )
       accesses acc
@@ -1431,8 +1512,8 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env
   List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty |> AccessListMap.quotient
 
 
-(* aggregate all of the procedures in the file env by their declaring class. this lets us analyze
-   each class individually *)
+(* aggregate all of the procedures in the file env by their declaring
+   class. this lets us analyze each class individually *)
 let aggregate_by_class file_env =
   List.fold file_env
     ~f:(fun acc ((_, pdesc) as proc) ->
@@ -1449,8 +1530,9 @@ let aggregate_by_class file_env =
     ~init:String.Map.empty
 
 
-(* Gathers results by analyzing all the methods in a file, then post-processes the results to check
-   an (approximation of) thread safety *)
+(* Gathers results by analyzing all the methods in a file, then
+   post-processes the results to check an (approximation of) thread
+   safety *)
 let file_analysis {Callbacks.procedures} =
   String.Map.iter
     ~f:(fun class_env ->

infer/src/concurrency/RacerDDomain.ml

@@ -431,12 +431,116 @@ module AccessDomain = struct
   let get_accesses precondition t = try find precondition t with Not_found -> PathDomain.empty
 end
 
+module StabilityDomain = struct
+  include AccessTree.PathSet (AccessTree.DefaultConfig)
+
+  let get_all_paths t =
+    fold
+      (fun paths z _ ->
+        match z with AccessPath.Abs.Abstracted p | AccessPath.Abs.Exact p -> p :: paths )
+      t []
+
+
+  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 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 = HilExp.get_access_paths 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)
+      | _ ->
+          false
+    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
+
+
+  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 rebase_paths 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 )
+    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_paths actual_exp with
+          | [actual] ->
+              AccessPath.append actual accesses
+          | _ ->
+              path )
+        | None ->
+            path )
+      | None ->
+          path
+    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
+end
+
 type astate =
   { threads: ThreadsDomain.astate
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; ownership: OwnershipDomain.astate
-  ; attribute_map: AttributeMapDomain.astate }
+  ; attribute_map: AttributeMapDomain.astate
+  ; wobbly_paths: StabilityDomain.astate }
 
 let empty =
   let threads = ThreadsDomain.empty in
@@ -444,12 +548,14 @@ let empty =
   let accesses = AccessDomain.empty in
   let ownership = OwnershipDomain.empty in
   let attribute_map = AttributeMapDomain.empty in
-  {threads; locks; accesses; ownership; attribute_map}
+  let wobbly_paths = StabilityDomain.empty in
+  {threads; locks; accesses; ownership; attribute_map; wobbly_paths}
 
 
-let is_empty {threads; locks; accesses; ownership; attribute_map} =
+let is_empty {threads; locks; accesses; ownership; attribute_map; wobbly_paths} =
   ThreadsDomain.is_empty threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses
   && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map
+  && StabilityDomain.is_empty wobbly_paths
 
 
 let ( <= ) ~lhs ~rhs =
@@ -459,6 +565,7 @@ let ( <= ) ~lhs ~rhs =
     && LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks
     && AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses
     && AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map
+    && StabilityDomain.( <= ) ~lhs:lhs.wobbly_paths ~rhs:rhs.wobbly_paths
 
 
 let join astate1 astate2 =
@@ -469,7 +576,8 @@ let join astate1 astate2 =
     let accesses = AccessDomain.join astate1.accesses astate2.accesses in
     let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in
     let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
-    {threads; locks; accesses; ownership; attribute_map}
+    let wobbly_paths = StabilityDomain.join astate1.wobbly_paths astate2.wobbly_paths in
+    {threads; locks; accesses; ownership; attribute_map; wobbly_paths}
 
 
 let widen ~prev ~next ~num_iters =
@@ -482,7 +590,10 @@ let widen ~prev ~next ~num_iters =
     let attribute_map =
       AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters
     in
-    {threads; locks; accesses; ownership; attribute_map}
+    let wobbly_paths =
+      StabilityDomain.widen ~prev:prev.wobbly_paths ~next:next.wobbly_paths ~num_iters
+    in
+    {threads; locks; accesses; ownership; attribute_map; wobbly_paths}
 
 
 type summary =
@@ -490,19 +601,22 @@ type summary =
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; return_ownership: OwnershipAbstractValue.astate
-  ; return_attributes: AttributeSetDomain.astate }
+  ; return_attributes: AttributeSetDomain.astate
+  ; wobbly_paths: StabilityDomain.astate }
 
-let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes} =
+let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} =
   F.fprintf fmt
-    "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n"
+    "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\nWobbly Paths: %a@\n"
     ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses
     OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes
+    StabilityDomain.pp wobbly_paths
 
 
-let pp fmt {threads; locks; accesses; ownership; attribute_map} =
-  F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\n"
+let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} =
+  F.fprintf fmt
+    "Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\nNon-stable Paths: %a@\n"
     ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp
-    ownership AttributeMapDomain.pp attribute_map
+    ownership AttributeMapDomain.pp attribute_map StabilityDomain.pp wobbly_paths
 
 
 let rec attributes_of_expr attribute_map e =

infer/src/concurrency/RacerDDomain.mli

@@ -190,6 +190,16 @@ module AccessDomain : sig
   (** get all accesses with the given precondition *)
 end
 
+module StabilityDomain : sig
+  include module type of AccessTree.PathSet (AccessTree.DefaultConfig)
+
+  val rebase_paths : HilExp.t list -> Procdesc.t -> t -> t
+
+  val add_wobbly_paths_assign : AccessPath.t -> HilExp.t -> t -> t
+
+  val add_wobbly_actuals : HilExp.t list -> t -> t
+end
+
 type astate =
   { threads: ThreadsDomain.astate  (** current thread: main, background, or unknown *)
   ; locks: LocksDomain.astate  (** boolean that is true if a lock must currently be held *)
@@ -197,7 +207,9 @@ type astate =
         (** read and writes accesses performed without ownership permissions *)
   ; ownership: OwnershipDomain.astate  (** map of access paths to ownership predicates *)
   ; attribute_map: AttributeMapDomain.astate
-        (** map of access paths to attributes such as owned, functional, ... *) }
+        (** map of access paths to attributes such as owned, functional, ... *)
+  ; wobbly_paths: StabilityDomain.astate
+        (** Record the "touched" paths that can compromise the race detection **) }
 
 (** same as astate, but without [attribute_map] (since these involve locals) and with the addition
     of the ownership/attributes associated with the return value as well as the set of formals which
@@ -207,7 +219,8 @@ type summary =
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; return_ownership: OwnershipAbstractValue.astate
-  ; return_attributes: AttributeSetDomain.astate }
+  ; return_attributes: AttributeSetDomain.astate
+  ; wobbly_paths: StabilityDomain.astate }
 
 include AbstractDomain.WithBottom with type astate := astate