[RacerD] Fix stability implementation

Summary:
- Do not add actuals of a call as unstable.
- Replace access trie with simple set of paths, which is easier to debug/argue correct.
- Fix bug where a prefix path was searched, as opposed to a *proper* prefix.
- Restrict interface to the minimum so that alternative implementations are easier.

Reviewed By: ilyasergey

Differential Revision: D8573792

fbshipit-source-id: 4c4e174

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
+      if StabilityDomain.exists_proper_prefix access_path wobbly_paths then Some " [wob]" else None
   | _ ->
       None
-  in
-  Option.map wobbly_path_opt ~f:(fun _ -> " [wob]")
 
 
 let log_issue current_pname ~loc ~ltr ~access exn =

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 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 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 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 -> (
+
+  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_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 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] ->
-              AccessPath.append (AccessExpression.to_access_path actual) accesses
+        Some (AccessExpression.to_access_path actual)
     | _ ->
-              path )
-        | None ->
-            path )
-      | None ->
-          path
+        None
+
+
+  let rebase actuals pdesc t =
+    let formal_map = FormalMap.make pdesc in
+    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 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 =

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 =

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, [<Read trace>,access to `this.suspiciously_read`,<Write trace>,access to `this.suspiciously_read`]
 codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to basics::Basic_get_private_suspiciously_read,access to `this.suspiciously_read`,<Write trace>,access to `this.suspiciously_read`]
 codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 81, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.single_lock_suspiciously_read`,<Write trace>,access to `this.single_lock_suspiciously_read`]
-codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,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, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`]

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;

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, [<Read trace>,access to `this.codetoanalyze.java.checkers.Interprocedural$Field.a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `this.codetoanalyze.java.checkers.Intraprocedural$Field.a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,<Write trace>,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, [<Read trace>,access to `a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,<Write trace>,access to `a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`]