Atomicity analysis

- Local atomicity violations (not actual violations because the functions with
  these violations are always called under the lock higher in the call
  hierarchy) are reported only as warnings.

- The atomic sets file is moved from 'infer-out/atomic-sets' to 'atomic-sets'.

- Definition of a type 't' and including of the 'PrettyPrintable.PrintableType'
  module in modules are replaced with including the
  'PrettyPrintable.PrintableEquatableOrderedType' module.

infer/src/atomicity/AtomicSets.ml

@@ -119,10 +119,8 @@ let analyse_procedure (analysis_data : Domain.Summary.t InterproceduralAnalysis.
           Procname.pp pName
 
 
-let print_atomic_sets (analysis_data : AtomicSetsDomain.Summary.t InterproceduralAnalysis.file_t) :
-    IssueLog.t =
-  (* Create a directory for printing. *)
-  Utils.create_dir inferDir ;
+let print_atomic_sets (analysis_data : Domain.Summary.t InterproceduralAnalysis.file_t) : IssueLog.t
+    =
   (* Print to a file. *)
   let oc : Out_channel.t =
     Out_channel.create ~binary:false ~append:Config.atomic_sets_file_append ~fail_if_exists:false

infer/src/atomicity/AtomicSetsDomain.mli

@@ -7,8 +7,7 @@ module F = Format
 
 (* ************************************ Astate ************************************************** *)
 
-(** An abstract state of a function. *)
-type t [@@deriving compare, equal]
+include PrettyPrintable.PrintableEquatableOrderedType
 
 (** An alias for the type 't'. *)
 type astate = t [@@deriving compare, equal]
@@ -43,10 +42,7 @@ val update_at_the_end_of_function : t -> t
 
 (** A module that encapsulates a summary of a function. *)
 module Summary : sig
-  (** A summary of a function. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val create : astate -> t
   (** Converts an abstract state to a summary. *)

infer/src/atomicity/AtomicityUtils.ml

@@ -43,7 +43,7 @@ module Lock = struct
       else if is_top lock then F.pp_print_string fmt SpecialChars.down_tack
       else F.pp_print_int fmt level
     in
-    F.fprintf fmt "%a (%a): " AccessPath.pp path pp_level lock
+    F.fprintf fmt "%a (%a)" AccessPath.pp path pp_level lock
 
 
   let lock ((path, level) as lock : t) : t = if is_top lock then lock else (path, level + 1)
@@ -63,8 +63,7 @@ module Guards = struct
 
   type t = AccessPath.t list GuardMap.t [@@deriving compare, equal]
 
-  let pp (fmt : F.formatter) (guards : t) : unit =
-    F.pp_print_string fmt "\t{\n" ;
+  let pp (fmt : F.formatter) : t -> unit =
     let print_guards (guard : AccessPath.t) : AccessPath.t list -> unit =
       let pp_locks (fmt : F.formatter) (locks : AccessPath.t list) : unit =
         let lastLock : AccessPath.t option = List.last locks in
@@ -76,8 +75,7 @@ module Guards = struct
       in
       F.fprintf fmt "\t\t%a: {%a};\n" AccessPath.pp guard pp_locks
     in
-    GuardMap.iter print_guards guards ;
-    F.pp_print_string fmt "\t};\n"
+    GuardMap.iter print_guards
 
 
   let empty : t = GuardMap.empty
@@ -98,9 +96,7 @@ end
 
 (* ************************************ Constants *********************************************** *)
 
-let inferDir : string = CommandLineOption.init_work_dir ^ "/infer-atomicity-out"
-
-let atomicSetsFile : string = inferDir ^ "/atomic-sets"
+let atomicSetsFile : string = CommandLineOption.init_work_dir ^ "/atomic-sets"
 
 let fileCommentChar : char = '#'
 

infer/src/atomicity/AtomicityUtils.mli

@@ -14,10 +14,7 @@ module SSet : module type of Set.Make (String)
 (** A module that represents a lock's access path with the number of times the lock has been
     acquired. *)
 module Lock : sig
-  (** A representation of a lock. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val lock : t -> t
   (** Increases the number of times the lock has been acquired. *)
@@ -37,10 +34,7 @@ end
 
 (** A module that represents associations between lock guards and locks. *)
 module Guards : sig
-  (** A representation of associations between lock guards and locks. *)
-  type t [@@deriving compare, equal]
-
-  include PrettyPrintable.PrintableType with type t := t
+  include PrettyPrintable.PrintableEquatableOrderedType
 
   val empty : t
   (** Creates an empty module. *)
@@ -60,9 +54,6 @@ end
 
 (* ************************************ Constants *********************************************** *)
 
-val inferDir : string
-(** The Infer work directory. *)
-
 val atomicSetsFile : string
 (** A file for storing atomic sets. *)
 

infer/src/atomicity/AtomicityViolations.ml

@@ -111,12 +111,36 @@ let analyse_procedure (analysis_data : Domain.Summary.t InterproceduralAnalysis.
         F.fprintf fmt "\n\nFunction: %a\n%a%a\n\n" Procname.pp pName Domain.pp post
           Domain.Summary.pp summary ;
         L.debug Capture Verbose "%s" (F.flush_str_formatter ()) ;
-        (* Report atomicity violations. *)
-        Domain.report_atomicity_violations post ~f:(fun (loc : Location.t) ~(msg : string) : unit ->
-            Reporting.log_issue analysis_data.proc_desc analysis_data.err_log ~loc
-              AtomicityViolations IssueType.atomicity_violation msg) ;
         Some summary
     | None ->
         L.die InternalError
           "The detection of atomicity violations failed to compute a post for '%a'." Procname.pp
           pName
+
+
+let report_atomicity_violations (analysis_data : Domain.Summary.t InterproceduralAnalysis.file_t) :
+    IssueLog.t =
+  let summaries : (Procname.t * Domain.Summary.t) list =
+    let mapper (pName : Procname.t) : (Procname.t * Domain.Summary.t) option =
+      match analysis_data.analyze_file_dependency pName with
+      | Some ((_ : Procdesc.t), (summary : Domain.Summary.t)) ->
+          Some (pName, summary)
+      | None ->
+          None
+    in
+    List.filter_map ~f:mapper analysis_data.procedures
+  in
+  let fold (issueLog : IssueLog.t) ((pName : Procname.t), (summary : Domain.Summary.t)) : IssueLog.t
+      =
+    if not (Domain.Summary.is_top_level_fun pName summaries) then issueLog
+    else
+      (* Report atomicity violations. *)
+      let report (loc : Location.t) ~(msg : string) (issueType : IssueType.t)
+          (issueLog : IssueLog.t) : IssueLog.t =
+        Reporting.log_issue_external pName ~issue_log:issueLog ~loc
+          ~ltr:[Errlog.make_trace_element 0 loc msg []]
+          AtomicityViolations issueType msg
+      in
+      Domain.Summary.report_atomicity_violations summary issueLog ~f:report
+  in
+  List.fold summaries ~init:IssueLog.empty ~f:fold

infer/src/atomicity/AtomicityViolations.mli

@@ -8,3 +8,7 @@ module Domain = AtomicityViolationsDomain
 val analyse_procedure : Domain.Summary.t InterproceduralAnalysis.t -> Domain.Summary.t option
 (** An atomicity violations detection entry point. Produces a summary for a given function. Should
     be invoked for each function in the analysed program. Reports atomicity violations. *)
+
+val report_atomicity_violations : Domain.Summary.t InterproceduralAnalysis.file_t -> IssueLog.t
+(** Should be invoked after the atomicity violations detection of all functions in the analysed
+    program. Reports atomicity violations from summaries from all analysed functions. *)