Merge pull request #595 from goblint/mhp-analysis

Extract MHP analysis, simplify printing in race output

Author: michael-schwarz

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 (* only unique threads *)
+      | _, _ -> 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

@@ -9,7 +9,22 @@ type t = {
 } [@@deriving eq, ord, hash]
 
 let pretty () {tid; created; must_joined} =
-  Pretty.dprintf "{ tid=%a; created=%a; must_joined=%a }" ThreadIdDomain.ThreadLifted.pretty tid ConcDomain.ThreadSet.pretty created ConcDomain.ThreadSet.pretty must_joined
+  let tid_doc = Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid) in
+  (* avoid useless empty sets in race output *)
+  let created_doc =
+    if ConcDomain.ThreadSet.is_empty created then
+      None
+    else
+      Some (Pretty.dprintf "created=%a" ConcDomain.ThreadSet.pretty created)
+  in
+  let must_joined_doc =
+    if ConcDomain.ThreadSet.is_empty must_joined then
+      None
+    else
+      Some (Pretty.dprintf "must_joined=%a" ConcDomain.ThreadSet.pretty must_joined)
+  in
+  let docs = List.filter_map (fun doc -> doc) [tid_doc; created_doc; must_joined_doc] in
+  Pretty.dprintf "{%a}" (Pretty.d_list "; " Pretty.insert) docs
 
 include Printable.SimplePretty (
   struct

src/cdomains/mHP.ml

@@ -98,6 +98,15 @@ struct
   end
   include Printable.Prod (P) (S)
 
+  let pretty () (p, s) =
+    let p = List.rev p in (* show in "unreversed" order *)
+    if S.is_empty s then
+      P.pretty () p (* hide empty set *)
+    else
+      Pretty.dprintf "%a, %a" P.pretty p S.pretty s
+
+  let show x = Pretty.sprint ~width:max_int (pretty () x)
+
   module D =
   struct
     include S

src/cdomains/threadIdDomain.ml

@@ -256,7 +256,7 @@
           "items": { "type": "string" },
           "default": [
             "expRelation", "base", "threadid", "threadflag", "threadreturn",
-            "escape", "mutex", "access", "mallocWrapper"
+            "escape", "mutex", "access", "mallocWrapper", "mhp"
           ]
         },
         "path_sens": {

src/util/options.schema.json

@@ -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>