[WIP][gen] Remove locally-order-before in baseline configuration file.

Makefile

@@ -716,6 +716,7 @@ diyone-basic-test:
 	@ echo
 	dune test gen/tests
 	@ echo "diy* basic test: OK"
+
 diy-test:: diy-baseline-cycleonly
 diy-baseline-cycleonly::
 	@ echo

gen/alt.ml

@@ -237,16 +237,18 @@ struct
           else x
     let last_non_insert xs = hd_non_insert (List.rev xs)
 
-    (* Check whether relaxation list `xs` can precede relaxation list `ys`.
-       This uses the effective boundary edges of the two sequences,
-       ignoring insert/store pseudo-edges when necessary, and checks:
-       - whether the boundary edges are compatible via `Edge.can_precede`
-       - whether the mode-specific rule holds *)
-    let can_precede safes po_safe xs ys =
-      let e1 = last_non_insert xs in
-      let e2 = hd_non_insert ys in
-      C.E.can_precede e1 e2
-      && match e1.edge,e2.edge with
+	    (* Check whether relaxation list `xs` can precede relaxation list `ys`.
+	       This uses the effective boundary edges of the two sequences,
+	       ignoring insert/store pseudo-edges when necessary, and checks:
+	       - whether the boundary edges are compatible via `Edge.can_precede`
+	       - whether the mode-specific rule holds *)
+	    let can_precede safes po_safe xs ys =
+	      if xs = [] || ys = [] then false
+	      else
+	      let e1 = last_non_insert xs in
+	      let e2 = hd_non_insert ys in
+	      C.E.can_precede e1 e2
+	      && match e1.edge,e2.edge with
 (*
   First reject some of hb' ; hb'
  *)
@@ -295,9 +297,6 @@ module Make(C:Builder.S)
     | [] -> true
     | (_,ys)::_ -> FilterImpl.can_precede safes po_safe xs ys
 
-    (* List.is_empty only supports for ocaml 5.1 afterwards *)
-    let is_empty_list l = (l = [])
-
     let pp_ess ess =
       let list_sep = " " in
       let list_list_sep = " " in
@@ -307,7 +306,80 @@ module Make(C:Builder.S)
              |> String.concat list_list_sep )
         |> String.concat list_sep
 
-    let edges_ofs rs =
+    (* check if `list` starts with `expected` based on predicate `pred` *)
+    let rec starts_with pred list expected =
+      match list, expected with
+      | _, [] -> true
+      | [], _::_  -> false
+      | hd :: tail, hd_expected :: tail_expected ->
+          pred hd hd_expected
+          && starts_with pred tail tail_expected
+
+    (* check if `list` starts with `expected` based on predicate `pred` *)
+    let ends_with pred list expected =
+      starts_with pred (List.rev list) (List.rev expected)
+
+    (* Given `next = [....; after(..); after(..)]` and
+       `exist = [before(..); before(..); ....]`,
+       where `after` and `before` are optional,
+       function checks whether the predicates can merge with the concrete
+       boundary:
+         - `before` merges with concrete if edge matches.
+         - `after` merges with concrete if edge matches.
+         - `before` pairing with `after` fails. *)
+	    let merge_predicate next exist =
+	      (* Separate the tailing `after` predicate from `next` *)
+	      let after =
+	        List.fold_right ( fun e (after,seen_non_after) ->
+	          match seen_non_after, C.E.get_predicate e = Some C.E.After with
+	          | true, _ | _, false -> after, true
+	          | false, true -> e :: after, false ) next ([],false)
+	        |> fst in
+	      (* Separate the beginning `before` predicate from `exist` *)
+	      let before =
+	        List.fold_left ( fun (before,seen_non_before) e ->
+	          match seen_non_before, C.E.get_predicate e = Some C.E.Before with
+	          | true, _ | _, false -> before, true
+	          | false, true -> e :: before, false ) ([],false) exist
+	        |> fst |> List.rev in
+      (* Merge `after` and `before` if find *)
+      match after, before with
+      | [], [] -> true
+      | after, [] ->
+          starts_with C.E.equal_edge_atoms exist after
+      | [], before ->
+          ends_with C.E.equal_edge_atoms next before
+      (* error on `after` hits `before` predicate *)
+      | _, _ -> false
+
+    (* List.is_empty only supports for ocaml 5.1 afterwards *)
+    let is_empty_list l = (l = [])
+
+	    let needs_merge next_edges exist_edges =
+	      match List.rev next_edges, exist_edges with
+	      | next_last::_, exist_first::_ ->
+	          C.E.get_predicate next_last = Some C.E.After ||
+	          C.E.get_predicate exist_first = Some C.E.Before
+	      | _ -> false
+
+    let check_precede can_precede next_edges exist_edges =
+      if O.verbose > 2 then
+        eprintf "next: %s, exists: %s\n"
+          (C.E.pp_edges next_edges) (C.E.pp_edges exist_edges);
+	      if needs_merge next_edges exist_edges then
+	        merge_predicate next_edges exist_edges
+	      else
+	        can_precede next_edges exist_edges
+
+	    let precede_relax_edge_list safes po_safe next exist =
+	      match exist with
+	      | [] -> true
+	      | (_,exist_edges) :: _ ->
+	          check_precede
+	            (FilterImpl.can_precede safes po_safe)
+	            (snd next) exist_edges
+
+    let edges_of_relax_list rs =
       List.map (fun r -> (r, edges_of r)) rs
 
 (* Functional for recursive call of generators *)
@@ -351,18 +423,16 @@ module Make(C:Builder.S)
     let minint suff = c_minint 0 suff
 
 (* Prefix *)
-    let prefix_expanded = List.flatten (List.map C.R.expand_relax_seq O.prefix)
-
     let () =
       if O.verbose > 0 && O.prefix <> [] then begin
         eprintf "Prefixes:\n" ;
         List.iter
           (fun rs ->
             eprintf "  %s\n" (C.R.pp_relax_list rs))
-          prefix_expanded
+          O.prefix
       end
 
-    let prefixes = List.map edges_ofs prefix_expanded
+    let prefixes = List.map edges_of_relax_list O.prefix
 
     let rec mk_can_prefix = function
       | [] -> (fun _ _ -> true)
@@ -382,40 +452,64 @@ module Make(C:Builder.S)
       let rsuff = List.split rsuff |> snd |> List.concat in
       not (List.exists (fun rl -> is_prefix rsuff rl) rl)
 
-
     (* This function is used `zyva` *)
-    let call_rec_base prefix f0 safes po_safe over n r suff f_rec k ?(reject=[])=
-      if
-        can_precede safes po_safe r suff &&
-        minprocs suff <= O.nprocs &&
-        minint (r::suff) <= O.max_ins-1 &&
-        check_cycle (r::suff) reject
-      then
-        let suff = r::suff
-        and n = n-sz r in
-        if O.verbose > 2 then eprintf "CALL: %i %s\n%!" n (pp_ess suff) ;
-        let k =
-          if
-            over &&
-            (n = 0 || (n > 0 && O.upto)) &&
-            can_prefix prefix (can_precede safes po_safe) suff
-          then begin
-            let tr =  prefix@suff in
-            if O.verbose > 2 then
-            eprintf "TRY: '%s'\n"
-              (C.E.pp_edges (List.flatten (List.map snd tr))) ;
-            try f0 po_safe tr k
-            with  Misc.Exit -> k
-            | Misc.Fatal msg |Misc.UserError msg ->
-                eprintf "Marche pas: '%s'\n" msg ;
+    let call_rec_base prefix test_generator safes po_safe over n r suff f_rec k ?(reject=[])=
+	      (* check if `r` is compatible with `suff` *)
+	      if not (precede_relax_edge_list safes po_safe r suff) then k
+	      else
+	        (* The next possible candidate cycle *)
+	        let r_suff = r::suff in
+	          if O.verbose > 2 then eprintf "CALL: %i %s\n%!" n (pp_ess r_suff) ;
+	        (* size only decreases when there is at least one non-insert edge in `r` *)
+	        let n = n-sz r in
+	        (* Update the accumulator `k` if a possible candidate cycle was found;
+	           otherwise keep it unchanged. *)
+	        let k =
+	          if
+	            (* Check whether the tail `r_suff` is compatible with its head, and
+	               hence forms a possible candidate cycle. *)
+	            precede_relax_edge_list safes po_safe (Misc.last r_suff) r_suff
+	            (* Check whether the environment and configuration are compatible with
+	               the candidate cycle. *)
+	            && over
+	            (* cycle size `n` is still within bound *)
+	            && (n = 0 || (n > 0 && O.upto))
+	            (* user-defined `prefix` can be added *)
+	            && can_prefix prefix (can_precede safes po_safe) r_suff
+		          then
+	              (* Find a candidate cycle, add `prefix`,
+	                 remove all predicates since they have already been checked,
+                   and then call `test_generator`. *)
+		            let candidate_cycle = List.map ( fun (relax, edges) ->
+	                let edges = List.filter ( function
+	                  | { pred = Some _; _ } -> false
+	                  | _ -> true ) edges in
+	                (relax,edges)
+	              ) (prefix @ r_suff) in
+	            if O.verbose > 2 then
+	            eprintf "TRY: '%s'\n"
+	              (C.E.pp_edges (List.flatten (List.map snd candidate_cycle))) ;
+	            try test_generator po_safe candidate_cycle k
+            (* `test_generator` fails, however, surpresses some expected error *)
+            with Misc.Exit -> k
+            | Misc.Fatal msg | Misc.UserError msg ->
+                eprintf "try test generator but fail: '%s'\n" msg ;
                 k
-            | e ->
-              eprintf "Exc in F0: '%s'\n" (Printexc.to_string e) ;
-              raise e
-          end else k in
-        if n <= 0 then k
-        else f_rec n suff k
-      else k
+	            | e ->
+	                eprintf "unexpected error in test generator: '%s'\n"
+	                  (Printexc.to_string e) ;
+	                raise e
+	          else k in
+        (* recursive call *)
+        let is_continue_search =
+          (* Check procedure number *)
+          minprocs suff <= O.nprocs
+          (* Check instruction number *)
+          && minint r_suff <= O.max_ins-1
+          (* Check if the cycle is rejected by `reject` *)
+          && check_cycle r_suff reject in
+        if is_continue_search && n > 0 then f_rec n r_suff k
+        else k
     (* END of call_rec_base *)
 
     module SdDir2Set =
@@ -449,8 +543,8 @@ module Make(C:Builder.S)
 
     let zyva prefix aset relax safe reject n f =
 (*      let safes = C.R.Set.of_list safe in *)
-      let relax = edges_ofs relax in
-      let safe = edges_ofs safe in
+      let relax = edges_of_relax_list relax in
+      let safe = edges_of_relax_list safe in
       let po_safe = extract_po safe in
 
       (* ********************************** *)
@@ -696,9 +790,6 @@ module Make(C:Builder.S)
 
     let parse_input ~relax ~safe ~reject =
       let r_nempty = Misc.consp relax in
-      let relax = expand_relaxs C.ppo relax
-      and safe = expand_relaxs C.ppo safe
-      and reject = expand_relaxs C.ppo reject in
       if Misc.nilp relax then if r_nempty then begin
         Warn.fatal "relaxations provided in relaxlist could not be used to generate cycles"
       end ;
@@ -775,6 +866,6 @@ module Make(C:Builder.S)
     let filter_check ~relax ~safe lhs rhs =
       let safe,_,_ = parse_input ~relax ~safe ~reject:[] in
       let safe_set = C.R.Set.of_list safe in
-      let po_safe = edges_ofs safe |> extract_po in
+      let po_safe = edges_of_relax_list safe |> extract_po in
       FilterImpl.can_precede safe_set po_safe lhs rhs
   end

gen/atomize.ml

@@ -25,6 +25,7 @@ let opts = [Util.arch_opt arch]
 module Make (F:Fence.S)(A:Atom.S) =
     struct
       module E = Edge.Make(Edge.Config)(F)(A)
+      module Relax = Relax.Make(F)(E)
       module Namer = Namer.Make(F)(A)(E)
       module Normer =
         Normaliser.Make(struct let lowercase = false end)(E)
@@ -87,21 +88,22 @@ module Make (F:Fence.S)(A:Atom.S) =
         done with End_of_file -> ()
 
       let zyva_argv es =
-        let es = List.map E.parse_edge es in
-        let es = atomize es in
+        let es = E.parse_edges es |> atomize in
         printf "%s\n" (pp_edges es)
 
       let zyva = function
         | [] -> zyva_stdin ()
-        | es ->  zyva_argv es
+        | es ->  String.concat "," es |> zyva_argv
     end
 
 let pp_es = ref []
 
 let () =
   Util.parse_cmdline
     opts
-    (fun x -> pp_es := x :: !pp_es)
+    (fun x ->
+      let segment = String.trim x in
+      if segment <> "" then pp_es := segment :: !pp_es)
 
 let pp_es = List.rev !pp_es
 

gen/autoArch.ml

@@ -23,12 +23,19 @@ end
 module Make(A:Arch_gen.S) : S
 = struct
   module A = A
-  module E = Edge.Make(Edge.Config)(A)
+  module EdgeConfig = struct
+    include Edge.Config
+    let wildcard = true
+  end
+  module E = Edge.Make(EdgeConfig)(A)(A)
   module R = Relax.Make(A) (E)
 
   module LogInput = struct
     type relax = R.relax
-    let parse = R.parse_relax
+    let parse ast =
+      match R.parse_expand_relaxs ast with
+      | [r] -> r
+      | _ -> Warn.fatal "input is not a singleton relaxation"
   end
 
 

gen/autoOpt.ml

@@ -171,11 +171,12 @@ let get_nprocs a cfg = match cfg.nprocs with
       | `PPC -> 4
       | `X86|`X86_64
       | `ARM
+      | `BPF
       | `MIPS
       | `LISA
       | `AArch64
       | `RISCV -> 2
-      | `C | `CPP -> 2
+      | `C | `CPP | `JAVA | `ASL -> 2
     end
 | Some i -> i
 

gen/cat2config/translation.ml

@@ -40,7 +40,7 @@ let get_ie edge =
   let open Code in
   match edge with
   | Id | Po _ | Dp _ | Fenced _ | Rmw _ -> Int
-  | Rf ie | Fr ie | Ws ie -> ie
+  | Rf ie | Fr ie | Ws ie | Coms ie -> ie
   | Leave _ | Back _ | Hat -> Ext
   | Insert _ | Store | Node _ -> Int
 
@@ -54,7 +54,7 @@ let set_ie ie (edge : E.tedge) =
 let get_sd (edge : E.tedge) =
   match edge with
   | Po (sd, _, _) | Dp (_, sd, _) | Fenced (_, sd, _, _) -> sd
-  | Leave _ | Back _ | Hat | Id | Rf _ | Fr _ | Ws _ | Rmw _ -> Same
+  | Leave _ | Back _ | Hat | Id | Rf _ | Fr _ | Ws _ | Coms _ | Rmw _ -> Same
   | Insert _ | Store | Node _ -> raise (Invalid_argument "Unexpected edge kind")
 
 let set_sd sd (edge : E.tedge) =
@@ -262,7 +262,7 @@ let try_match_edge (left : prim_set list) (core : seq_item list)
   let relaxs =
     tedges
     |> List.map (fun (Tedge { edge; insert }) ->
-        let edge = E.{ edge; a1 = left.atom; a2 = right.atom } in
+        let edge = E.{ edge; a1 = left.atom; a2 = right.atom; pred = None } in
         let edge = set_src left.extr edge in
         let edge = set_tgt right.extr edge in
         let edges =