[herd] Follow suggestions (to be squashed later)

Author: maranget

herd/mem.ml

@@ -866,43 +866,10 @@ and get_written e = match E.written_of e with
 
 let map_loc_find loc m = U.LocEnv.safe_find [] loc m
 
-(* Event set ordered by to (generalised) program order *)
-
-module
-  EvtSetByPo
-    (I:sig val es : S.event_structure end) =
-struct
-
-  let is_before_strict = U.is_before_strict I.es
-
-  include Set.Make
-      (struct
-
-        type t = E.event
-
-        let compare e1 e2 =
-          if is_before_strict e1 e2 then -1
-          else if is_before_strict e2 e1 then 1
-          else
-            let () =
-              Printf.eprintf "Not ordered stores %a and %a\n" E.debug_event e1
-                E.debug_event e2
-            in
-            assert false
-
-      end)
-
-  let find_last_before set e =
-    find_last_opt (fun e' -> is_before_strict e' e) set
-
-  let find_first_after e set =
-    find_first_opt (fun e' -> is_before_strict e e') set
-
-end
 
 let match_reg_events add_eq es csn =
   let loc_loads_stores = U.collect_reg_loads_stores es in
-  let module StoreSet = EvtSetByPo(struct let es = es end) in
+  let module StoreSet = U.EvtSetByPo(struct let es = es end) in
   let add wt rf (rfm, csn) = (S.RFMap.add wt rf rfm, add_eq rfm wt rf csn) in
   (* For all loads find the right store, the one "just before" the load *)
   U.LocEnv.fold
@@ -1026,6 +993,11 @@ let get_rf_value test read =
                 S.simplify_vars_in_rfmap sol rfm,
                 csn )
       with Contradiction -> None
+         | e ->
+             let module PP = Pretty.Make(S) in
+             eprintf "Coucou\n%!" ;
+             PP.show_es_rfm test es S.RFMap.empty ;
+             raise e
 
     let solve_regs test es csn =
       profile "solve_regs" @@ fun () ->
@@ -1840,7 +1812,7 @@ let get_rf_value test read =
 
     let make_atomic_load_store es =
       let atms,spurious = U.collect_atomics es in
-      let module StoreSet = EvtSetByPo(struct let es = es end) in
+      let module StoreSet = U.EvtSetByPo(struct let es = es end) in
       let make_atomic_pairs es k =
         let rs,ws = List.partition E.is_load es in
         let ws = StoreSet.of_list ws

herd/memUtils.ml

@@ -58,7 +58,41 @@ module Make(S : SemExtra.S) = struct
        else (* e1 and e2 are from the same instruction *)
        E.EventRel.exists_path (e1,e2) iico)
 
-(* Fence *)
+(* Event set ordered by to (generalised) program order *)
+
+  module
+    EvtSetByPo
+      (I:sig val es : S.event_structure end) =
+  struct
+
+    let is_before_strict = is_before_strict I.es
+
+    include Set.Make
+        (struct
+
+          type t = E.event
+
+          let compare e1 e2 =
+            if E.po_strict e1 e2 then -1
+            else if E.po_strict e2 e1 then 1
+            else
+              let () =
+                Printf.eprintf "Not ordered stores %a and %a\n" E.debug_event e1
+                  E.debug_event e2 ;
+              in
+              assert false
+
+        end)
+
+    let find_last_before set e =
+      find_last_opt (fun e' -> is_before_strict e' e) set
+
+    let find_first_after e set =
+      find_first_opt (fun e' -> is_before_strict e e') set
+
+  end
+
+  (* Fence *)
   let po_fence_po po pred =
     let r1 =
       E.EventRel.restrict_domains E.is_mem pred po

herd/memUtils.mli

@@ -25,6 +25,32 @@ module Make : functor (S: SemExtra.S) -> sig
   val po_iico :  S.event_structure -> S.event_rel
 (* po union iico_data union iico_control *)
   val is_before_strict : S.event_structure -> S.event -> S.event -> bool
+
+(*
+ * Set of events ordered by  is_before_strict.
+ * Notice it is an error to add unrelated events
+ *  to this set.
+ *)
+  module
+    EvtSetByPo :
+    functor
+      (I:sig val es : S.event_structure end) ->
+    sig
+
+      (* Strict ordering, taking iico into account for effects
+         from the same instruction. *)
+      val is_before_strict : S.event -> S.event -> bool
+
+      include Set.S with type elt = S.event
+
+      (* [find_last_before set e] find maximal effect in [set] before [e] *)
+      val find_last_before : t -> S.event -> S.event option
+
+      (* [find_last_before set e] find minimal effect in [set] after [e] *)
+      val find_first_after : S.event -> t -> S.event option
+
+    end
+
 (* Fence like relations *)
   val po_fence_po : S.event_rel (* po *) -> (S.event -> bool) -> S.event_rel