[thread-safety][cleanup] use record for summary type

Reviewed By: peterogithub

Differential Revision: D5636060

fbshipit-source-id: 5e25a28

infer/src/checkers/ThreadSafety.ml

@@ -499,13 +499,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
              we own the container *)
     let escapee_formals = List.length actuals |> List.range 0 |> FormalsDomain.of_list in
     Some
-      ( true
+      { thumbs_up= true
-      , false
+      ; locks= false
-      , false
+      ; threads= false
-      , callee_accesses
+      ; accesses= callee_accesses
-      , OwnershipAbstractValue.unowned
+      ; return_ownership= OwnershipAbstractValue.unowned
-      , AttributeSetDomain.empty
+      ; return_attributes= AttributeSetDomain.empty
-      , escapee_formals )
+      ; escapee_formals }
 
   let get_summary caller_pdesc callee_pname actuals callee_loc tenv =
     let get_receiver_ap actuals =
@@ -627,13 +627,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             | NoEffect ->
               match get_summary pdesc callee_pname actuals loc tenv with
               | Some
-                  ( callee_thumbs_up
+                  { thumbs_up
-                  , callee_threads
+                  ; threads
-                  , callee_locks
+                  ; locks
-                  , callee_accesses
+                  ; accesses
-                  , return_ownership
+                  ; return_ownership
-                  , return_attributes
+                  ; return_attributes
-                  , escapee_formals )
+                  ; escapee_formals }
                -> let update_caller_accesses pre callee_accesses caller_accesses =
                     let combined_accesses =
                       PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
@@ -641,9 +641,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     in
                     AccessDomain.add pre combined_accesses caller_accesses
                   in
-                  let thumbs_up = callee_thumbs_up && astate.thumbs_up in
+                  let thumbs_up = thumbs_up && astate.thumbs_up in
-                  let locks = callee_locks || astate.locks in
+                  let locks = locks || astate.locks in
-                  let threads = callee_threads || astate.threads in
+                  let threads = threads || astate.threads in
                   let unprotected = is_unprotected locks threads pdesc in
                   (* add [ownership_accesses] to the [accesses_acc] with a protected pre if
                        [exp] is owned, and an appropriate unprotected pre otherwise *)
@@ -707,7 +707,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                               add_ownership_access callee_accesses (List.nth_exn actuals index) acc)
                             formal_indexes accesses_acc
                     in
-                    AccessDomain.fold update_accesses callee_accesses astate.accesses
+                    AccessDomain.fold update_accesses accesses astate.accesses
                   in
                   let ownership, attribute_map =
                     propagate_return ret_opt return_ownership return_attributes actuals astate
@@ -841,7 +841,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
            -> (* non-boolean expression; can't evaluate it *)
               None
         in
-        let add_choice bool_value acc = function
+        let add_choice bool_value (acc: Domain.astate) = function
           | Choice.LockHeld
            -> let locks = bool_value in
               {acc with locks}
@@ -963,20 +963,14 @@ let is_thread_safe_method pdesc tenv =
         is_thread_safe)
     tenv (Procdesc.get_proc_name pdesc)
 
-let empty_post =
+let empty_post : ThreadSafetyDomain.summary =
-  let initial_thumbs_up = true
+  { ThreadSafetyDomain.thumbs_up= true
-  and initial_known_on_ui_thread = false
+  ; threads= false
-  and has_lock = false
+  ; locks= false
-  and return_ownership = ThreadSafetyDomain.OwnershipAbstractValue.unowned
+  ; accesses= ThreadSafetyDomain.AccessDomain.empty
-  and return_attrs = ThreadSafetyDomain.AttributeSetDomain.empty
+  ; return_ownership= ThreadSafetyDomain.OwnershipAbstractValue.unowned
-  and escapee_formals = ThreadSafetyDomain.FormalsDomain.empty in
+  ; return_attributes= ThreadSafetyDomain.AttributeSetDomain.empty
-  ( initial_thumbs_up
+  ; escapee_formals= ThreadSafetyDomain.FormalsDomain.empty }
-  , initial_known_on_ui_thread
-  , has_lock
-  , ThreadSafetyDomain.AccessDomain.empty
-  , return_ownership
-  , return_attrs
-  , escapee_formals )
 
 let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
   let is_initializer tenv proc_name =
@@ -1035,13 +1029,13 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
         in
         let escapee_formals = FormalsDomain.of_escapees escapees in
         let post =
-          ( thumbs_up
+          { thumbs_up
-          , threads
+          ; threads
-          , locks
+          ; locks
-          , accesses
+          ; accesses
-          , return_ownership
+          ; return_ownership
-          , return_attributes
+          ; return_attributes
-          , escapee_formals )
+          ; escapee_formals }
         in
         Summary.update_summary post summary
     | None
@@ -1141,10 +1135,10 @@ let trace_of_pname orig_sink orig_pdesc callee_pname =
   let open ThreadSafetyDomain in
   let orig_access = PathDomain.Sink.kind orig_sink in
   match Summary.read_summary orig_pdesc callee_pname with
-  | Some (_, _, _, access_map, _, _, _)
+  | Some {accesses}
    -> get_all_accesses
         (fun access -> Int.equal (Access.compare (PathDomain.Sink.kind access) orig_access) 0)
-        access_map
+        accesses
   | _
    -> PathDomain.empty
 
@@ -1578,8 +1572,8 @@ let should_filter_access access =
    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 file_env =
-  let aggregate_post (_, threaded, _, accesses, _, _, _) tenv pdesc acc =
+  let open ThreadSafetyDomain in
-    let open ThreadSafetyDomain in
+  let aggregate_post {threads; accesses} tenv pdesc acc =
     AccessDomain.fold
       (fun pre accesses acc ->
         PathDomain.Sinks.fold
@@ -1592,7 +1586,7 @@ let make_results_table file_env =
                 with Not_found -> []
               in
               AccessListMap.add access_kind
-                ((access, pre, threaded, tenv, pdesc) :: grouped_accesses) acc)
+                ((access, pre, threads, tenv, pdesc) :: grouped_accesses) acc)
           (PathDomain.sinks accesses) acc)
       accesses acc
   in

infer/src/checkers/ThreadSafetyDomain.ml

@@ -318,15 +318,6 @@ type astate =
   ; attribute_map: AttributeMapDomain.astate
   ; escapees: EscapeeDomain.astate }
 
-type summary =
-  ThumbsUpDomain.astate
-  * ThreadsDomain.astate
-  * LocksDomain.astate
-  * AccessDomain.astate
-  * OwnershipAbstractValue.astate
-  * AttributeSetDomain.astate
-  * FormalsDomain.astate
-
 let empty =
   let thumbs_up = true in
   let threads = false in
@@ -371,12 +362,21 @@ let widen ~prev ~next ~num_iters =
     let escapees = EscapeeDomain.widen ~prev:prev.escapees ~next:next.escapees ~num_iters in
     {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}
 
+type summary =
+  { thumbs_up: ThumbsUpDomain.astate
+  ; threads: ThreadsDomain.astate
+  ; locks: LocksDomain.astate
+  ; accesses: AccessDomain.astate
+  ; return_ownership: OwnershipAbstractValue.astate
+  ; return_attributes: AttributeSetDomain.astate
+  ; escapee_formals: FormalsDomain.astate }
+
 let pp_summary fmt
-    (thumbs_up, threads, locks, accesses, ownership, return_attributes, escapee_formals) =
+    {thumbs_up; threads; locks; accesses; return_ownership; return_attributes; escapee_formals} =
   F.fprintf fmt
     "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\nEscapee Formals: %a @\n"
     ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp
-    accesses OwnershipAbstractValue.pp ownership AttributeSetDomain.pp return_attributes
+    accesses OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes
     FormalsDomain.pp escapee_formals
 
 let pp fmt {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees} =

infer/src/checkers/ThreadSafetyDomain.mli

@@ -186,17 +186,17 @@ type astate =
         (** map of access paths to attributes such as owned, functional, ... *)
   ; escapees: EscapeeDomain.astate  (** set of formals and locals that may escape *) }
 
-(** same as astate, but without [attribute_map] (since these involve locals)
+(** same as astate, but without [attribute_map] (since these involve locals) and with the addition
-    and with the addition of the attributes associated with the return value
+    of the ownership/attributes associated with the return value as well as the set of formals which
-    as well as the set of formals which may escape *)
+    may escape *)
 type summary =
-  ThumbsUpDomain.astate
+  { thumbs_up: ThumbsUpDomain.astate
-  * ThreadsDomain.astate
+  ; threads: ThreadsDomain.astate
-  * LocksDomain.astate
+  ; locks: LocksDomain.astate
-  * AccessDomain.astate
+  ; accesses: AccessDomain.astate
-  * OwnershipAbstractValue.astate
+  ; return_ownership: OwnershipAbstractValue.astate
-  * AttributeSetDomain.astate
+  ; return_attributes: AttributeSetDomain.astate
-  * FormalsDomain.astate
+  ; escapee_formals: FormalsDomain.astate }
 
 include AbstractDomain.WithBottom with type astate := astate