Merge pull request #1808 from fsestini/fix-po-graphs

[herd] Fix placement of po edges in dot graphs

Author: fsestini

herd/Pretty.ml

@@ -827,7 +827,7 @@ module Make (S:SemExtra.S) : S with module S = S  = struct
   | E.IdSome ii ->
       fprintf chan "proc:%s poi:%i\\l"
         (Proc.pp ii.A.proc)
-        ii.A.static_poi
+        ii.A.program_order_index
 
 (*
   This complex function is not meant to be used directly,

herd/dune

@@ -1,4 +1,4 @@
-(dirs :standard \ tests libdir)
+(dirs :standard \ tests/instructions libdir)
 
 (rule
  (copy ../Version.ml Version.ml))

herd/prettyUtils.ml

@@ -23,7 +23,7 @@ module Make(S : SemExtra.S) = struct
     let by_po =
       E.EventSet.fold
         (fun e k ->
-          match E.static_poi e with
+          match E.progorder_of e with
             | None -> k
             | Some poi ->
                let es_poi = IntMap.safe_find []  poi k in

herd/tests/other/dune

@@ -0,0 +1,4 @@
+(cram
+ (deps
+  (source_tree libdir)
+  %{bin:herd7}))

herd/tests/other/libdir

@@ -0,0 +1 @@
+../../libdir

herd/tests/other/poi-loop.t/run.t

@@ -0,0 +1,17 @@
+Check that po indices/edges are assigned correctly in the presence of loops (only checks the last (longest) execution graph)
+  $ herd7 -set-libdir ../libdir -dumpes true -o - ./wait-flag.litmus | awk '/digraph G \{/ {block=""} {block = block $0 "\n"} END {printf "%s", block}' | grep -e 'poi' -e 'label="po"'
+  eiid0 [label="a: W[x]=1\lproc:P0 poi:1\lSTR W1,[X0]", shape="box", color="blue"];
+  eiid1 [label="b: R[x]=S1\lproc:P1 poi:0\lLDR W1,[X0]", shape="box", color="blue"];
+  eiid11 [label="l: Branching(bcc)\lproc:P1 poi:1\lCBZ W1,.-4", shape="box", color="blue"];
+  eiid2 [label="c: R[x]=S5\lproc:P1 poi:2\lLDR W1,[X0]", shape="box", color="blue"];
+  eiid15 [label="p: Branching(bcc)\lproc:P1 poi:3\lCBZ W1,.-4", shape="box", color="blue"];
+  eiid3 [label="d: R[x]=S9\lproc:P1 poi:4\lLDR W1,[X0]", shape="box", color="blue"];
+  eiid19 [label="t: Branching(bcc)\lproc:P1 poi:5\lCBZ W1,.-4", shape="box", color="blue"];
+  eiid20 [label="u: CutOff:L0\lproc:P1 poi:6\lLDR W1,[X0]", shape="box", color="blue"];
+  /* the poi edges */
+  eiid1 -> eiid11 [label="po", color="black", fontcolor="black"];
+  eiid2 -> eiid15 [label="po", color="black", fontcolor="black"];
+  eiid3 -> eiid19 [label="po", color="black", fontcolor="black"];
+  eiid11 -> eiid2 [label="po", color="black", fontcolor="black"];
+  eiid15 -> eiid3 [label="po", color="black", fontcolor="black"];
+  eiid19 -> eiid20 [label="po", color="black", fontcolor="black"];

herd/tests/other/poi-loop.t/wait-flag.litmus

@@ -0,0 +1,8 @@
+AArch64 wait-flag
+{
+   0:X0=x; 1:X0=x;
+}
+   P0          | P1          ;
+   MOV W1,#1   |L0:          ;
+   STR W1,[X0] | LDR W1,[X0] ;
+               | CBZ W1,L0   ;