Extract MHP access collecting to mhp analysis (issue #571)

Author: sim642

src/analyses/mHPAnalysis.ml

@@ -0,0 +1,27 @@
+(** MHP access analysis. *)
+open Prelude.Ana
+open Analyses
+
+module Spec =
+struct
+  include UnitAnalysis.Spec
+  let name () = "mhp"
+
+  module A =
+  struct
+    include MHP
+    let name () = "mhp"
+    let may_race = MHP.may_happen_in_parallel
+    let should_print _ = true
+  end
+
+  let access ctx e vo w: MHP.t =
+    {
+      tid = ctx.ask CurrentThreadId;
+      created = ctx.ask CreatedThreads;
+      must_joined = ctx.ask MustJoinedThreads
+    }
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/analyses/threadId.ml

@@ -96,25 +96,20 @@ struct
 
   module A =
   struct
-    (* Also contains MHP in addition to unique thread. *)
-    include Printable.Prod (Printable.Option (ThreadLifted) (struct let name = "nonunique" end)) (MHP)
-    let name () = "thread * mhp"
+    include Printable.Option (ThreadLifted) (struct let name = "nonunique" end)
+    let name () = "thread"
     let may_race (t1: t) (t2: t) = match t1, t2 with
-      | (Some t1, _), (Some t2, _) when ThreadLifted.equal t1 t2 -> false
-      | (_, mhp1), (_, mhp2) when not (MHP.may_happen_in_parallel mhp1 mhp2) -> false
-      | (_, _), (_, _) -> true
-    let should_print _ = true
+      | Some t1, Some t2 when ThreadLifted.equal t1 t2 -> false
+      | _, _ -> true
+    let should_print = Option.is_some
   end
+
   let access ctx e vo w =
-    let unique =
-      if is_unique ctx then
-        let tid = fst ctx.local in
-        Some tid
-      else
-        None
-    in
-    let mhp: MHP.t = {tid = fst ctx.local; created = created ctx.local; must_joined = ctx.ask MustJoinedThreads} in
-    (unique, mhp)
+    if is_unique ctx then
+      let tid = fst ctx.local in
+      Some tid
+    else
+      None
 
   let threadenter ctx lval f args =
     let+ tid = create_tid ctx.local ctx.prev_node f in

src/analyses/tutorials/unit.ml renamed to src/analyses/tutorials/unitAnalysis.ml

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] threadJoins
+// PARAM: --set ana.activated[+] mhp --set ana.activated[+] threadJoins
 #include <pthread.h>
 #include <stdio.h>
 

tests/regression/10-synch/13-two_threads_nr.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] threadJoins
+// PARAM: --set ana.activated[+] mhp --set ana.activated[+] threadJoins
 #include <pthread.h>
 #include <stdio.h>
 

tests/regression/10-synch/15-join_other_nr.c

@@ -1,3 +1,4 @@
+// PARAM: --set ana.activated[+] mhp
 #include <pthread.h>
 #include <assert.h>
 

tests/regression/53-races-mhp/01-not-created.c

@@ -1,4 +1,4 @@
-//PARAM: --set ana.activated[+] threadJoins
+//PARAM: --set ana.activated[+] mhp --set ana.activated[+] threadJoins
 #include <pthread.h>
 #include <assert.h>
 

tests/regression/53-races-mhp/02-join.c

@@ -1,3 +1,4 @@
+// PARAM: --set ana.activated[+] mhp
 #include <pthread.h>
 #include <stdio.h>