[racerd] move some domain operations into domain module

Summary: As per title, plus minor improvements in interfaces and a couple of FIXMEs.

Reviewed By: skcho

Differential Revision: D24836125

fbshipit-source-id: f7a4dc196

infer/src/concurrency/RacerD.ml

@@ -20,75 +20,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   type nonrec analysis_data = analysis_data
 
-  let rec get_access_exp = function
-    | HilExp.AccessExpression access_expr ->
-        Some access_expr
-    | HilExp.Cast (_, e) | HilExp.Exception e ->
-        get_access_exp e
-    | _ ->
-        None
-
-
-  let get_first_actual actuals = List.hd actuals |> Option.bind ~f:get_access_exp
-
-  let apply_to_first_actual ~f astate actuals =
-    get_first_actual actuals |> Option.value_map ~default:astate ~f
-
-
-  let add_access formals loc ~is_write_access locks threads ownership tenv access_domain exp =
-    let open Domain in
-    let rec add_field_accesses prefix_path acc = function
-      | [] ->
-          acc
-      | access :: access_list ->
-          let prefix_path' = Option.value_exn (AccessExpression.add_access prefix_path access) in
-          if
-            (not (HilExp.Access.is_field_or_array_access access))
-            || RacerDModels.is_safe_access access prefix_path tenv
-          then add_field_accesses prefix_path' acc access_list
-          else
-            let is_write = List.is_empty access_list && is_write_access in
-            let pre = OwnershipDomain.get_owned prefix_path ownership in
-            let snapshot_opt =
-              AccessSnapshot.make_access formals prefix_path' ~is_write loc locks threads pre
-            in
-            let access_acc' = AccessDomain.add_opt snapshot_opt acc in
-            add_field_accesses prefix_path' access_acc' access_list
-    in
-    List.fold (HilExp.get_access_exprs exp) ~init:access_domain ~f:(fun acc access_expr ->
-        let base, accesses = AccessExpression.to_accesses access_expr in
-        add_field_accesses base acc accesses )
-
-
-  let make_container_access {interproc= {tenv}; formals} ret_base callee_pname ~is_write receiver_ap
-      callee_loc (astate : Domain.t) =
-    let open Domain in
-    if
-      AttributeMapDomain.is_synchronized astate.attribute_map receiver_ap
-      || RacerDModels.is_synchronized_container callee_pname receiver_ap tenv
-    then astate
-    else
-      let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in
-      let callee_access =
-        AccessSnapshot.make_container_access formals receiver_ap ~is_write callee_pname callee_loc
-          astate.locks astate.threads ownership_pre
-      in
-      let ownership =
-        OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership
-      in
-      let accesses = AccessDomain.add_opt callee_access astate.accesses in
-      {astate with accesses; ownership}
-
-
-  let add_reads formals exps loc ({accesses; locks; threads; ownership} as astate : Domain.t) tenv =
-    let accesses =
-      List.fold exps ~init:accesses
-        ~f:(add_access formals loc ~is_write_access:false locks threads ownership tenv)
-    in
-    {astate with accesses}
-
-
   let expand_actuals formals actuals accesses pdesc =
+    (* FIXME fix quadratic order with an array-backed substitution *)
     let open Domain in
     if AccessDomain.is_empty accesses then accesses
     else
@@ -98,7 +31,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         | Some formal_index -> (
           match List.nth actuals formal_index with
           | Some actual_exp -> (
-            match get_access_exp actual_exp with
+            match accexp_of_hilexp actual_exp with
             | Some actual ->
                 AccessExpression.append ~onto:actual exp |> Option.value ~default:exp
             | None ->
@@ -152,7 +85,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let open RacerDModels in
     let open RacerDDomain in
     if RacerDModels.is_synchronized_container_constructor tenv callee_pname actuals then
-      apply_to_first_actual astate actuals ~f:(fun receiver ->
+      apply_to_first_actual actuals astate ~f:(fun receiver ->
           let attribute_map = AttributeMapDomain.add receiver Synchronized astate.attribute_map in
           {astate with attribute_map} )
     else if RacerDModels.is_converter_to_synchronized_container tenv callee_pname actuals then
@@ -161,7 +94,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       in
       {astate with attribute_map}
     else if is_box callee_pname then
-      apply_to_first_actual astate actuals ~f:(fun actual_access_expr ->
+      apply_to_first_actual actuals astate ~f:(fun actual_access_expr ->
           if AttributeMapDomain.is_functional astate.attribute_map actual_access_expr then
             (* TODO: check for constants, which are functional? *)
             let attribute_map =
@@ -187,16 +120,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     {astate with ownership}
 
 
-  let do_container_access ~is_write ret_base callee_pname actuals loc analysis_data astate =
-    match get_first_actual actuals with
-    | Some receiver_expr ->
-        make_container_access analysis_data ret_base callee_pname ~is_write receiver_expr loc astate
-    | None ->
-        L.internal_error "Call to %a is marked as a container access, but has no receiver"
-          Procname.pp callee_pname ;
-        astate
-
-
   let do_proc_call ret_base callee_pname actuals call_flags loc
       {interproc= {tenv; analyze_dependency}; formals} (astate : Domain.t) =
     let open Domain in
@@ -303,10 +226,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let do_assignment lhs_access_exp rhs_exp loc {interproc= {tenv}; formals} (astate : Domain.t) =
     let open Domain in
-    let rhs_accesses =
-      add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership
-        tenv astate.accesses rhs_exp
-    in
+    let astate = add_access tenv formals loc ~is_write:false astate rhs_exp in
     let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in
     let is_functional =
       (not (List.is_empty rhs_access_exprs))
@@ -321,20 +241,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | _ ->
           true
     in
-    let accesses =
+    let astate =
       if is_functional then
         (* we want to forget about writes to @Functional fields altogether, otherwise we'll
            report spurious read/write races *)
-        rhs_accesses
+        astate
       else
-        add_access formals loc ~is_write_access:true astate.locks astate.threads astate.ownership
-          tenv rhs_accesses (HilExp.AccessExpression lhs_access_exp)
+        add_access tenv formals loc ~is_write:true astate (HilExp.AccessExpression lhs_access_exp)
     in
     let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in
     let attribute_map =
       AttributeMapDomain.propagate_assignment lhs_access_exp rhs_exp astate.attribute_map
     in
-    {astate with accesses; ownership; attribute_map}
+    {astate with ownership; attribute_map}
 
 
   let do_assume formals assume_exp loc tenv (astate : Domain.t) =
@@ -354,35 +273,31 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | Attribute.(Functional | Nothing | Synchronized) ->
           acc
     in
-    let accesses =
-      add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership
-        tenv astate.accesses assume_exp
-    in
-    let astate' =
-      match HilExp.get_access_exprs assume_exp with
-      | [access_expr] ->
-          HilExp.eval_boolean_exp access_expr assume_exp
-          |> Option.value_map ~default:astate ~f:(fun bool_value ->
-                 (* prune (prune_exp) can only evaluate to true if the choice is [bool_value].
-                    add the constraint that the choice must be [bool_value] to the state *)
-                 AttributeMapDomain.get access_expr astate.attribute_map
-                 |> apply_choice bool_value astate )
-      | _ ->
-          astate
-    in
-    {astate' with accesses}
+    let astate = add_access tenv formals loc ~is_write:false astate assume_exp in
+    match HilExp.get_access_exprs assume_exp with
+    | [access_expr] ->
+        HilExp.eval_boolean_exp access_expr assume_exp
+        |> Option.value_map ~default:astate ~f:(fun bool_value ->
+               (* prune (prune_exp) can only evaluate to true if the choice is [bool_value].
+                  add the constraint that the choice must be [bool_value] to the state *)
+               AttributeMapDomain.get access_expr astate.attribute_map
+               |> apply_choice bool_value astate )
+    | _ ->
+        astate
 
 
   let exec_instr astate ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ instr =
     match (instr : HilInstr.t) with
     | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
-        let astate = add_reads formals actuals loc astate tenv in
+        let astate = Domain.add_reads_of_hilexps tenv formals actuals loc astate in
         if RacerDModels.acquires_ownership callee_pname tenv then
           do_call_acquiring_ownership ret_base astate
         else if RacerDModels.is_container_write tenv callee_pname then
-          do_container_access ~is_write:true ret_base callee_pname actuals loc analysis_data astate
+          Domain.add_container_access tenv formals ~is_write:true ret_base callee_pname actuals loc
+            astate
         else if RacerDModels.is_container_read tenv callee_pname then
-          do_container_access ~is_write:false ret_base callee_pname actuals loc analysis_data astate
+          Domain.add_container_access tenv formals ~is_write:false ret_base callee_pname actuals loc
+            astate
         else do_proc_call ret_base callee_pname actuals call_flags loc analysis_data astate
     | Call (_, Indirect _, _, _, _) ->
         if Procname.is_java (Procdesc.get_proc_name proc_desc) then

infer/src/concurrency/RacerDDomain.ml

@@ -8,8 +8,25 @@
 open! IStd
 module AccessExpression = HilExp.AccessExpression
 module F = Format
+module L = Logging
 module MF = MarkupFormatter
 
+let rec accexp_of_hilexp hil_exp =
+  match (hil_exp : HilExp.t) with
+  | AccessExpression access_expr ->
+      Some access_expr
+  | Cast (_, e) | Exception e ->
+      accexp_of_hilexp e
+  | _ ->
+      None
+
+
+let accexp_of_first_hilexp actuals = List.hd actuals |> Option.bind ~f:accexp_of_hilexp
+
+let apply_to_first_actual actuals astate ~f =
+  accexp_of_first_hilexp actuals |> Option.value_map ~default:astate ~f
+
+
 let pp_exp fmt exp =
   match !Language.curr_language with
   | Clang ->
@@ -349,8 +366,7 @@ module OwnershipDomain = struct
           get_owned prefix astate )
 
 
-  let rec ownership_of_expr expr ownership =
-    let open HilExp in
+  let rec ownership_of_expr (expr : HilExp.t) ownership =
     match expr with
     | AccessExpression access_expr ->
         get_owned access_expr ownership
@@ -544,20 +560,13 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} =
 
 
 let add_unannotated_call_access formals pname actuals loc (astate : t) =
-  match actuals with
-  | [] ->
-      astate
-  | receiver_hilexp :: _ -> (
-    match HilExp.get_access_exprs receiver_hilexp with
-    | [] | _ :: _ :: _ ->
-        (* if no access exps involved, or if more than one (should be impossible), ignore *)
-        astate
-    | [receiver] ->
-        let snapshot =
-          AccessSnapshot.make_unannotated_call_access formals receiver pname astate.locks
-            astate.threads Unowned loc
-        in
-        {astate with accesses= AccessDomain.add_opt snapshot astate.accesses} )
+  apply_to_first_actual actuals astate ~f:(fun receiver ->
+      let access_opt =
+        (* FIXME this should use the ownership of the receiver! *)
+        AccessSnapshot.make_unannotated_call_access formals receiver pname astate.locks
+          astate.threads Unowned loc
+      in
+      {astate with accesses= AccessDomain.add_opt access_opt astate.accesses} )
 
 
 let astate_to_summary proc_desc formals {threads; locks; accesses; ownership; attribute_map} =
@@ -582,3 +591,58 @@ let astate_to_summary proc_desc formals {threads; locks; accesses; ownership; at
     else AttributeMapDomain.top
   in
   {threads; locks; accesses; return_ownership; return_attribute; attributes}
+
+
+let add_access tenv formals loc ~is_write (astate : t) exp =
+  let rec add_field_accesses prefix_path acc = function
+    | [] ->
+        acc
+    | access :: access_list ->
+        let prefix_path' = Option.value_exn (AccessExpression.add_access prefix_path access) in
+        if
+          (not (HilExp.Access.is_field_or_array_access access))
+          || RacerDModels.is_safe_access access prefix_path tenv
+        then add_field_accesses prefix_path' acc access_list
+        else
+          let is_write = is_write && List.is_empty access_list in
+          let pre = OwnershipDomain.get_owned prefix_path astate.ownership in
+          let snapshot_opt =
+            AccessSnapshot.make_access formals prefix_path' ~is_write loc astate.locks
+              astate.threads pre
+          in
+          let access_acc' = AccessDomain.add_opt snapshot_opt acc in
+          add_field_accesses prefix_path' access_acc' access_list
+  in
+  let accesses =
+    List.fold (HilExp.get_access_exprs exp) ~init:astate.accesses ~f:(fun acc access_expr ->
+        let base, accesses = AccessExpression.to_accesses access_expr in
+        add_field_accesses base acc accesses )
+  in
+  {astate with accesses}
+
+
+let add_container_access tenv formals ~is_write ret_base callee_pname actuals loc (astate : t) =
+  match accexp_of_first_hilexp actuals with
+  | None ->
+      L.internal_error "Call to %a is marked as a container access, but has no receiver" Procname.pp
+        callee_pname ;
+      astate
+  | Some receiver_expr
+    when AttributeMapDomain.is_synchronized astate.attribute_map receiver_expr
+         || RacerDModels.is_synchronized_container callee_pname receiver_expr tenv ->
+      astate
+  | Some receiver_expr ->
+      let ownership_pre = OwnershipDomain.get_owned receiver_expr astate.ownership in
+      let callee_access_opt =
+        AccessSnapshot.make_container_access formals receiver_expr ~is_write callee_pname loc
+          astate.locks astate.threads ownership_pre
+      in
+      let ownership =
+        OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership
+      in
+      let accesses = AccessDomain.add_opt callee_access_opt astate.accesses in
+      {astate with accesses; ownership}
+
+
+let add_reads_of_hilexps tenv formals exps loc astate =
+  List.fold exps ~init:astate ~f:(add_access tenv formals loc ~is_write:false)

infer/src/concurrency/RacerDDomain.mli

@@ -9,6 +9,10 @@ open! IStd
 module AccessExpression = HilExp.AccessExpression
 module F = Format
 
+val accexp_of_hilexp : HilExp.t -> HilExp.access_expression option
+
+val apply_to_first_actual : HilExp.t list -> 'a -> f:(HilExp.access_expression -> 'a) -> 'a
+
 val pp_exp : F.formatter -> AccessExpression.t -> unit
 (** language sensitive pretty-printer *)
 
@@ -27,7 +31,7 @@ module Access : sig
   val get_access_exp : t -> AccessExpression.t
 end
 
-(** Overapproximation of number of time the lock has been acquired *)
+(** Overapproximation of number of times the lock has been acquired *)
 module LockDomain : sig
   include AbstractDomain.WithBottom
 
@@ -99,27 +103,6 @@ module AccessSnapshot : sig
 
   val get_loc : t -> Location.t
 
-  val make_access :
-       FormalMap.t
-    -> AccessExpression.t
-    -> is_write:bool
-    -> Location.t
-    -> LockDomain.t
-    -> ThreadsDomain.t
-    -> OwnershipAbstractValue.t
-    -> t option
-
-  val make_container_access :
-       FormalMap.t
-    -> AccessExpression.t
-    -> is_write:bool
-    -> Procname.t
-    -> Location.t
-    -> LockDomain.t
-    -> ThreadsDomain.t
-    -> OwnershipAbstractValue.t
-    -> t option
-
   val is_unprotected : t -> bool
   (** return true if not protected by lock, thread, or ownership *)
 
@@ -148,8 +131,6 @@ module OwnershipDomain : sig
 
   val add : AccessExpression.t -> OwnershipAbstractValue.t -> t -> t
 
-  val get_owned : AccessExpression.t -> t -> OwnershipAbstractValue.t
-
   val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t
 
   val propagate_return : AccessExpression.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t
@@ -175,8 +156,6 @@ module AttributeMapDomain : sig
 
   val is_functional : t -> AccessExpression.t -> bool
 
-  val is_synchronized : 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 *)
 end
@@ -210,3 +189,18 @@ val empty_summary : summary
 val pp_summary : F.formatter -> summary -> unit
 
 val astate_to_summary : Procdesc.t -> FormalMap.t -> t -> summary
+
+val add_access : Tenv.t -> FormalMap.t -> Location.t -> is_write:bool -> t -> HilExp.t -> t
+
+val add_container_access :
+     Tenv.t
+  -> FormalMap.t
+  -> is_write:bool
+  -> AccessPath.base
+  -> Procname.t
+  -> HilExp.t list
+  -> Location.t
+  -> t
+  -> t
+
+val add_reads_of_hilexps : Tenv.t -> FormalMap.t -> HilExp.t list -> Location.t -> t -> t