[racerd][3/n] improve domain interface and consolidate access validity checking

Summary:
For historical reasons, the record of an access is a three-level record:
1. `AccessSnapshot`, a record with info such as ownership and lock status, including
2. `TraceElem`, a record with a trace and an element which is
3. Access, the abstract addressed accessed and the type of access.

This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3.

This diff improves the domain interface and consolidates all the various validity invariant checking for accesses inside their constructors.

Reviewed By: skcho

Differential Revision: D20668611

fbshipit-source-id: 45806d40d

infer/src/concurrency/RacerD.ml

@@ -163,16 +163,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     if is_box callee_pname then
       match actuals with
-      | HilExp.AccessExpression actual_access_expr :: _ ->
-          if AttributeMapDomain.has_attribute actual_access_expr Functional astate.attribute_map
-          then
-            (* TODO: check for constants, which are functional? *)
-            let attribute_map =
-              AttributeMapDomain.add (AccessExpression.base ret_base) Functional
-                astate.attribute_map
-            in
-            {astate with attribute_map}
-          else astate
+      | HilExp.AccessExpression actual_access_expr :: _
+        when AttributeMapDomain.is_functional astate.attribute_map actual_access_expr ->
+          (* TODO: check for constants, which are functional? *)
+          let attribute_map =
+            AttributeMapDomain.add (AccessExpression.base ret_base) Functional astate.attribute_map
+          in
+          {astate with attribute_map}
       | _ ->
           astate
     else if should_assume_returns_ownership callee_pname call_flags actuals then
@@ -264,11 +261,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         match get_lock_effect callee_pname actuals with
         | Lock _ | GuardLock _ | GuardConstruct {acquire_now= true} ->
             { astate with
-              locks= LocksDomain.acquire_lock astate.locks
+              locks= LockDomain.acquire_lock astate.locks
             ; threads= update_for_lock_use astate.threads }
         | Unlock _ | GuardDestroy _ | GuardUnlock _ ->
             { astate with
-              locks= LocksDomain.release_lock astate.locks
+              locks= LockDomain.release_lock astate.locks
             ; threads= update_for_lock_use astate.threads }
         | LockedIfTrue _ | GuardLockedIfTrue _ ->
             let attribute_map =
@@ -290,7 +287,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             match rebased_summary_opt with
             | Some {threads; locks; accesses; return_ownership; return_attribute} ->
                 let locks =
-                  LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks
+                  LockDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks
                 in
                 let accesses =
                   add_callee_accesses extras astate accesses locks threads actuals callee_pname loc
@@ -337,8 +334,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in
     let is_functional =
       (not (List.is_empty rhs_access_exprs))
-      && List.for_all rhs_access_exprs ~f:(fun access_exp ->
-             AttributeMapDomain.has_attribute access_exp Functional astate.attribute_map )
+      && List.for_all rhs_access_exprs ~f:(AttributeMapDomain.is_functional astate.attribute_map)
       &&
       match AccessExpression.get_typ lhs_access_exp tenv with
       | Some {Typ.desc= Typ.Tint ILong | Tfloat FDouble} ->
@@ -370,8 +366,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let apply_choice bool_value (acc : Domain.t) = function
       | Attribute.LockHeld ->
           let locks =
-            if bool_value then LocksDomain.acquire_lock acc.locks
-            else LocksDomain.release_lock acc.locks
+            if bool_value then LockDomain.acquire_lock acc.locks
+            else LockDomain.release_lock acc.locks
           in
           {acc with locks}
       | Attribute.OnMainThread ->
@@ -444,8 +440,8 @@ let analyze_procedure {Callbacks.exe_env; summary} =
     let proc_data = ProcData.make summary tenv (FormalMap.make proc_desc) in
     let initial =
       let locks =
-        if Procdesc.is_java_synchronized proc_desc then LocksDomain.(acquire_lock bottom)
-        else LocksDomain.bottom
+        if Procdesc.is_java_synchronized proc_desc then LockDomain.(acquire_lock bottom)
+        else LockDomain.bottom
       in
       let threads =
         if
@@ -521,7 +517,7 @@ let analyze_procedure {Callbacks.exe_env; summary} =
         let return_attribute = AttributeMapDomain.find return_var_exp attribute_map in
         let locks =
           (* if method is [synchronized] released the lock once. *)
-          if Procdesc.is_java_synchronized proc_desc then LocksDomain.release_lock locks else locks
+          if Procdesc.is_java_synchronized proc_desc then LockDomain.release_lock locks else locks
         in
         let post = {threads; locks; accesses; return_ownership; return_attribute} in
         Payload.update_summary post summary
@@ -746,20 +742,6 @@ let empty_reported =
   {reported_sites; reported_reads; reported_writes; reported_unannotated_calls}
 
 
-(* decide if we should throw away an access before doing safety analysis
-   for now, just check for whether the access is within a switch-map
-   that is auto-generated by Java. *)
-let should_filter_access exp_opt =
-  let check_access = function
-    | HilExp.Access.FieldAccess fld ->
-        String.is_substring ~substring:"$SwitchMap" (Fieldname.to_string fld)
-    | _ ->
-        false
-  in
-  Option.exists exp_opt ~f:(fun exp ->
-      AccessExpression.to_accesses exp |> snd |> List.exists ~f:check_access )
-
-
 (** Map containing reported accesses, which groups them in lists, by abstract location. The
     equivalence relation used for grouping them is equality of access paths. This is slightly
     complicated because local variables contain the pname of the function declaring them. Here we
@@ -806,10 +788,8 @@ end = struct
 
   let add (rep : reported_access) map =
     let access = rep.snapshot.elem.access in
-    if RacerDDomain.Access.get_access_exp access |> should_filter_access then map
-    else
-      let k = Key.of_access access in
-      M.update k (function None -> Some [rep] | Some reps -> Some (rep :: reps)) map
+    let k = Key.of_access access in
+    M.update k (function None -> Some [rep] | Some reps -> Some (rep :: reps)) map
 
 
   let fold f map a =

infer/src/concurrency/RacerDDomain.ml

@@ -10,17 +10,6 @@ module AccessExpression = HilExp.AccessExpression
 module F = Format
 module MF = MarkupFormatter
 
-(** Master function for deciding whether RacerD should completely ignore a variable as the root of
-    an access expression. Currently fires on *static locals* and any variable which does not appear
-    in source code (eg, temporary variables and frontend introduced variables). This is because
-    currently reports on these variables would not be easily actionable.
-
-    This is here and not in RacerDModels to avoid dependency cycles. *)
-let should_skip_var v =
-  (not (Var.appears_in_source_code v))
-  || match v with Var.ProgramVar pvar -> Pvar.is_static_local pvar | _ -> false
-
-
 let pp_exp fmt exp =
   match !Language.curr_language with
   | Clang ->
@@ -68,16 +57,21 @@ module Access = struct
 
 
   let should_keep formals access =
-    match get_access_exp access with
-    | None ->
-        true
-    | Some acc_exp -> (
-        let ((root, _) as base) = AccessExpression.get_base acc_exp in
-        match root with
-        | Var.LogicalVar _ ->
-            false
-        | Var.ProgramVar pvar ->
-            Pvar.is_global pvar || FormalMap.is_formal base formals )
+    let rec check_access (exp : AccessExpression.t) =
+      match exp with
+      | FieldOffset (prefix, fld) ->
+          (not (String.is_substring ~substring:"$SwitchMap" (Fieldname.get_field_name fld)))
+          && check_access prefix
+      | ArrayOffset (prefix, _, _) | AddressOf prefix | Dereference prefix ->
+          check_access prefix
+      | Base (LogicalVar _, _) ->
+          false
+      | Base (((ProgramVar pvar as var), _) as base) ->
+          Var.appears_in_source_code var
+          && (not (Pvar.is_static_local pvar))
+          && (Pvar.is_global pvar || FormalMap.is_formal base formals)
+    in
+    match get_access_exp access with None -> true | Some acc_exp -> check_access acc_exp
 
 
   let map ~f access =
@@ -132,7 +126,7 @@ module CallPrinter = struct
   let pp fmt cs = F.fprintf fmt "call to %a" Procname.pp (CallSite.pname cs)
 end
 
-module LocksDomain = struct
+module LockDomain = struct
   include AbstractDomain.CountDomain (struct
     (** arbitrary threshold for max locks we expect to be held simultaneously *)
     let max = 5
@@ -216,7 +210,7 @@ module OwnershipAbstractValue = struct
 
   let owned = OwnedIf IntSet.empty
 
-  let is_owned = function OwnedIf set -> IntSet.is_empty set | _ -> false
+  let is_owned = function OwnedIf set -> IntSet.is_empty set | Unowned -> false
 
   let unowned = Unowned
 
@@ -293,20 +287,20 @@ module AccessSnapshot = struct
 
 
   let make_unannotated_call_access formals pname lock ownership loc =
-    let lock = LocksDomain.is_locked lock in
+    let lock = LockDomain.is_locked lock in
     let access = Access.make_unannotated_call_access pname in
     make_if_not_owned formals access lock ownership loc
 
 
   let make_access formals acc_exp ~is_write loc lock thread ownership_precondition =
-    let lock = LocksDomain.is_locked lock in
+    let lock = LockDomain.is_locked lock in
     let access = Access.make_field_access acc_exp ~is_write in
     make_if_not_owned formals access lock thread ownership_precondition loc
 
 
   let make_container_access formals acc_exp ~is_write callee loc lock thread ownership_precondition
       =
-    let lock = LocksDomain.is_locked lock in
+    let lock = LockDomain.is_locked lock in
     let access = Access.make_container_access acc_exp callee ~is_write in
     make_if_not_owned formals access lock thread ownership_precondition loc
 
@@ -319,7 +313,7 @@ module AccessSnapshot = struct
     let thread =
       ThreadsDomain.integrate_summary ~callee_astate:snapshot.elem.thread ~caller_astate:threads
     in
-    let lock = snapshot.elem.lock || LocksDomain.is_locked locks in
+    let lock = snapshot.elem.lock || LockDomain.is_locked locks in
     with_callsite snapshot callsite
     |> map ~f:(fun elem -> {elem with lock; thread; ownership_precondition})
     |> filter formals
@@ -334,14 +328,6 @@ end
 module AccessDomain = struct
   include AbstractDomain.FiniteSet (AccessSnapshot)
 
-  let add ({AccessSnapshot.elem= {access}} as s) astate =
-    let skip =
-      Access.get_access_exp access
-      |> Option.exists ~f:(fun exp -> AccessExpression.get_base exp |> fst |> should_skip_var)
-    in
-    if skip then astate else add s astate
-
-
   let add_opt snapshot_opt astate =
     Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc)
 end
@@ -435,8 +421,8 @@ module AttributeMapDomain = struct
 
   let find acc_exp t = find_opt acc_exp t |> Option.value ~default:Attribute.top
 
-  let has_attribute access_expression attribute t =
-    find_opt access_expression t |> Option.exists ~f:(Attribute.equal attribute)
+  let is_functional t access_expression =
+    match find_opt access_expression t with Some Functional -> true | _ -> false
 
 
   let rec attribute_of_expr attribute_map (e : HilExp.t) =
@@ -464,14 +450,14 @@ end
 
 type t =
   { threads: ThreadsDomain.t
-  ; locks: LocksDomain.t
+  ; locks: LockDomain.t
   ; accesses: AccessDomain.t
   ; ownership: OwnershipDomain.t
   ; attribute_map: AttributeMapDomain.t }
 
 let bottom =
   let threads = ThreadsDomain.bottom in
-  let locks = LocksDomain.bottom in
+  let locks = LockDomain.bottom in
   let accesses = AccessDomain.empty in
   let ownership = OwnershipDomain.empty in
   let attribute_map = AttributeMapDomain.empty in
@@ -479,7 +465,7 @@ let bottom =
 
 
 let is_bottom {threads; locks; accesses; ownership; attribute_map} =
-  ThreadsDomain.is_bottom threads && LocksDomain.is_bottom locks && AccessDomain.is_empty accesses
+  ThreadsDomain.is_bottom threads && LockDomain.is_bottom locks && AccessDomain.is_empty accesses
   && OwnershipDomain.is_empty ownership
   && AttributeMapDomain.is_empty attribute_map
 
@@ -488,7 +474,7 @@ let leq ~lhs ~rhs =
   if phys_equal lhs rhs then true
   else
     ThreadsDomain.leq ~lhs:lhs.threads ~rhs:rhs.threads
-    && LocksDomain.leq ~lhs:lhs.locks ~rhs:rhs.locks
+    && LockDomain.leq ~lhs:lhs.locks ~rhs:rhs.locks
     && AccessDomain.leq ~lhs:lhs.accesses ~rhs:rhs.accesses
     && AttributeMapDomain.leq ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map
 
@@ -497,7 +483,7 @@ let join astate1 astate2 =
   if phys_equal astate1 astate2 then astate1
   else
     let threads = ThreadsDomain.join astate1.threads astate2.threads in
-    let locks = LocksDomain.join astate1.locks astate2.locks in
+    let locks = LockDomain.join astate1.locks astate2.locks in
     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
@@ -508,7 +494,7 @@ let widen ~prev ~next ~num_iters =
   if phys_equal prev next then prev
   else
     let threads = ThreadsDomain.widen ~prev:prev.threads ~next:next.threads ~num_iters in
-    let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in
+    let locks = LockDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in
     let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in
     let ownership = OwnershipDomain.widen ~prev:prev.ownership ~next:next.ownership ~num_iters in
     let attribute_map =
@@ -519,15 +505,15 @@ let widen ~prev ~next ~num_iters =
 
 type summary =
   { threads: ThreadsDomain.t
-  ; locks: LocksDomain.t
+  ; locks: LockDomain.t
   ; accesses: AccessDomain.t
   ; return_ownership: OwnershipAbstractValue.t
   ; return_attribute: Attribute.t }
 
 let empty_summary =
   { threads= ThreadsDomain.bottom
-  ; locks= LocksDomain.bottom
-  ; accesses= AccessDomain.empty
+  ; locks= LockDomain.bottom
+  ; accesses= AccessDomain.bottom
   ; return_ownership= OwnershipAbstractValue.unowned
   ; return_attribute= Attribute.top }
 
@@ -535,13 +521,13 @@ let empty_summary =
 let pp_summary fmt {threads; locks; accesses; return_ownership; return_attribute} =
   F.fprintf fmt
     "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n"
-    ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipAbstractValue.pp
+    ThreadsDomain.pp threads LockDomain.pp locks AccessDomain.pp accesses OwnershipAbstractValue.pp
     return_ownership Attribute.pp return_attribute
 
 
 let pp fmt {threads; locks; accesses; ownership; attribute_map} =
   F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nAttributes: %a @\n"
-    ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp
+    ThreadsDomain.pp threads LockDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp
     ownership AttributeMapDomain.pp attribute_map
 
 

infer/src/concurrency/RacerDDomain.mli

@@ -21,18 +21,15 @@ module Access : sig
         (** Write to container object *)
     | InterfaceCall of Procname.t
         (** Call to method of interface not annotated with [@ThreadSafe] *)
-  [@@deriving compare]
 
-  include ExplicitTrace.Element with type t := t
+  val pp : F.formatter -> t -> unit
 
   val get_access_exp : t -> AccessExpression.t option
 end
 
-(** Overapproximation of number of locks that are currently held *)
-module LocksDomain : sig
-  type t
-
-  val bottom : t
+(** Overapproximation of number of time the lock has been acquired *)
+module LockDomain : sig
+  include AbstractDomain.WithBottom
 
   val acquire_lock : t -> t
   (** record acquisition of a lock *)
@@ -77,6 +74,8 @@ module OwnershipAbstractValue : sig
 
   val owned : t
 
+  val unowned : t
+
   val make_owned_if : int -> t
 
   val join : t -> t -> t
@@ -107,7 +106,7 @@ module AccessSnapshot : sig
     -> AccessExpression.t
     -> is_write:bool
     -> Location.t
-    -> LocksDomain.t
+    -> LockDomain.t
     -> ThreadsDomain.t
     -> OwnershipAbstractValue.t
     -> t option
@@ -118,7 +117,7 @@ module AccessSnapshot : sig
     -> is_write:bool
     -> Procname.t
     -> Location.t
-    -> LocksDomain.t
+    -> LockDomain.t
     -> ThreadsDomain.t
     -> OwnershipAbstractValue.t
     -> t option
@@ -134,7 +133,7 @@ module AccessSnapshot : sig
     -> CallSite.t
     -> OwnershipAbstractValue.t
     -> ThreadsDomain.t
-    -> LocksDomain.t
+    -> LockDomain.t
     -> t option
 end
 
@@ -175,7 +174,7 @@ module AttributeMapDomain : sig
 
   val add : AccessExpression.t -> Attribute.t -> t -> t
 
-  val has_attribute : AccessExpression.t -> Attribute.t -> t -> bool
+  val is_functional : t -> AccessExpression.t -> bool
 
   val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t
   (** propagate attributes from the leaves to the root of an RHS Hil expression *)
@@ -183,7 +182,7 @@ end
 
 type t =
   { threads: ThreadsDomain.t  (** current thread: main, background, or unknown *)
-  ; locks: LocksDomain.t  (** boolean that is true if a lock must currently be held *)
+  ; locks: LockDomain.t  (** boolean that is true if a lock must currently be held *)
   ; accesses: AccessDomain.t
         (** read and writes accesses performed without ownership permissions *)
   ; ownership: OwnershipDomain.t  (** map of access paths to ownership predicates *)
@@ -199,7 +198,7 @@ val add_unannotated_call_access : FormalMap.t -> Procname.t -> Location.t -> t -
     may escape *)
 type summary =
   { threads: ThreadsDomain.t
-  ; locks: LocksDomain.t
+  ; locks: LockDomain.t
   ; accesses: AccessDomain.t
   ; return_ownership: OwnershipAbstractValue.t
   ; return_attribute: Attribute.t }