[gen] Introduce a new relaxation/edge/atom parser in diy tool.

Makefile

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

gen/alt.ml

@@ -301,7 +301,7 @@ module Make(C:Builder.S)
              |> String.concat list_list_sep )
         |> String.concat list_sep
 
-    let edges_ofs rs =
+    let edges_of_relax_list rs =
       List.map (fun r -> (r, edges_of r)) rs
 
 (* Functional for recursive call of generators *)
@@ -345,18 +345,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)
@@ -443,8 +441,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
 
       (* ********************************** *)
@@ -690,9 +688,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 ;
@@ -769,6 +764,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/common/ast.ml

@@ -0,0 +1,65 @@
+type 'prim t =
+  | One of 'prim
+  | Opt of 'prim t
+  | Seq of 'prim t list
+  | Choice of 'prim t list
+
+let rec normalise ast =
+  let normalise_seq_items items =
+    List.fold_right
+      (fun item acc ->
+        match normalise item with
+        | Seq nested -> nested @ acc
+        | item -> item :: acc)
+      items [] in
+  let normalise_choice_items items =
+    List.fold_right
+      (fun item acc ->
+        match normalise item with
+        | Choice nested -> nested @ acc
+        | item -> item :: acc)
+      items [] in
+  match ast with
+  | One _ -> ast
+  | Opt opt -> Opt (normalise opt)
+  | Seq ss -> Seq (normalise_seq_items ss)
+  | Choice ss -> Choice (normalise_choice_items ss)
+
+let rec bind ast func =
+  let bind_func ast = bind ast func in
+  match ast with
+  | One s -> func s
+  | Opt opt -> Opt (bind_func opt)
+  | Seq ss -> Seq (List.map bind_func ss)
+  | Choice ss -> Choice (List.map bind_func ss)
+
+let rec pp pp_prim ast =
+  let pp_with_prim = pp pp_prim in
+  let ast = normalise ast in
+  match ast with
+  | One s -> Printf.sprintf "%s" (pp_prim s)
+  | Opt opt -> Printf.sprintf "%s?" (pp_with_prim opt)
+  | Seq ss ->
+      Printf.sprintf "[%s]" (String.concat "," (List.map pp_with_prim ss))
+  | Choice ss ->
+      Printf.sprintf "[%s]" (String.concat "|" (List.map pp_with_prim ss))
+
+let list_cross_product_map f lhs rhs =
+  List.map ( fun l ->
+    List.map ( fun r ->
+      f l r
+    ) rhs
+  ) lhs
+  |> List.flatten
+
+let rec expand t =
+  let result = match t with
+  | One str -> [[str]]
+  | Opt opt -> [] :: expand opt
+  | Seq seq -> List.fold_left
+    ( fun acc s ->
+      expand s
+      |> list_cross_product_map ( @ ) acc
+    ) [[]] seq
+  | Choice choice -> List.map expand choice |> List.flatten in
+  result

gen/common/ast.mli

@@ -0,0 +1,34 @@
+(* Abstract syntax tree for the relax-input grammar.
+   The type parameter `'prim` is the leaf token type produced by the parser.
+   - `One x` is a single primitive token.
+   - `Opt t` is an optional sub-expression, i.e., `(t)?`.
+   - `Seq ts` is an ordered sequence of sub-expressions, i.e., `A B C`
+     or `A,B,C`.
+   - `Choice ts` is a choice between alternatives, i.e., `A|B|C`. *)
+type 'prim t =
+  | One of 'prim
+  | Opt of 'prim t
+  | Seq of 'prim t list
+  | Choice of 'prim t list
+
+val bind : 'a t -> ('a -> 'b t) -> 'b t
+val pp : ('a -> string) -> 'a t -> string
+
+(* Flatten the AST into the list of concrete sequences.
+   - `One x` expands to `[[x]]`.
+   - `Opt t` expands to the alternatives of `t`, plus the empty sequence.
+   - `Choice list` concatenates the expansions of each alternative.
+     For example, `Choice [A; B]` becomes `[[A]; [B]]`.
+   - `Seq list` computes the ordered cross-product.
+     If `A` expands to `[[X; Y]; [Z]]` and `B` to `[[K]; [M; N]]`,
+     then `Seq [A; B]` expands to
+     `[ [X; Y; K]; [X; Y; M; N]; [Z; K]; [Z; M; N] ]`.
+   A concrete example is
+   `Seq [Choice [One x; One y]; Opt (Seq [One z; One k])]`,
+   which expands to `[[x]; [x; z; k]; [y]; [y; z; k]]`, where:
+   - `[x]` comes from `One x` followed by the empty alternative of `Opt`.
+   - `[x; z; k]` comes from `One x` followed by `Seq [One z; One k]`.
+   - `[y]` comes from `One y` followed by the empty alternative of `Opt`.
+   - `[y; z; k]` comes from `One y` followed by `Seq [One z; One k]`.
+   *)
+val expand : 'a t -> 'a list list

gen/common/config.ml

@@ -141,6 +141,28 @@ let parse_cumul = function
   | "true" -> All
   | s -> Set s
 
+let parser_syntax_doc =
+  "For the input cycle or cycle segments: '[...]' groups expressions, '|' means choice, and '?' makes the preceding expression optional.\n\
+   Inside '[...]', both whitespace and ',' mean sequence, so '[A B,C]' and '[A,B C]' all have canonical form '[A,B,C]'.\n\
+   At top level, plain whitespace and ',' may denote either choice or sequence, depending on the context."
+
+let diyone_parser_syntax_doc =
+  parser_syntax_doc ^ "\n\
+   In `diyone7`, each argument denotes one unique relaxation, and the full command line has canonical form as one top-level sequence.\n\
+   For example, `diyone7 A '[B C]' D` has canonical form `[A,[B,C],D]` and eventually denotes the single cycle `A,B,C,D`.\n\
+   After expansion, the input must denote exactly one concrete cycle, so using `|` or `?` leads to a user error."
+
+let diycross_parser_syntax_doc =
+  parser_syntax_doc ^ "\n\
+   In `diycross7`, each argument denotes a group of relaxations, and the full command line has canonical form as one top-level sequence.\n\
+   For example, `diycross7 A 'B,[C D E?]'` and `diycross7 A 'B [C D E?]'` have canonical form `[A,[B|[C,D,E?]]]`, which expands to the cycles `A,B`, `A,C,D`, and `A,C,D,E`."
+
+let with_parser_syntax_doc doc =
+  doc ^ " " ^ parser_syntax_doc
+
+let with_top_level_choice_doc doc =
+  doc ^ " At top level, plain separators denote choice, so '[A B] C [D E]' has canonical form '[[A,B]|C|[D,E]]'."
+
 
 (* Helpers *)
 
@@ -316,7 +338,8 @@ let diy_spec () =
       (Code.pp_check !mode)
    )::
    ("-cumul", Arg.String (fun b -> cumul := parse_cumul b),
-    "<s> allow non-explicit fence cumulativity for specified fenced (default all)")::
+    with_top_level_choice_doc
+      "<s> allow non-explicit fence cumulativity for specified fenced (default all)")::
    ("-conf", Arg.String (fun s -> conf := Some s), "<file> read configuration file")::
    ("-size", Arg.Int (fun n -> size := n),
     sprintf
@@ -335,7 +358,7 @@ let diy_spec () =
   ("-prefix", Arg.String (fun s -> prefix := s :: !prefix),
     "<relax-list> specify a prefix for cycles, can be repeated")::
    ("-relax", Arg.String (fun s -> relaxs := !relaxs @ [s]),
-    "<relax-list> specify a relax list")::
+    with_top_level_choice_doc "<relax-list> specify a relax list")::
    ("-mix", Arg.Bool (fun b -> mix := b),
     sprintf
       "<bool> mix relaxations when several are given (default %b)" !mix)::
@@ -344,9 +367,9 @@ let diy_spec () =
    ("-minrelax",   Arg.Int (fun n -> mix := true ; min_relax := n),
     sprintf "<n> test relaxations considering <n> or more different relaxations (default %i). Implies -mix true." !min_relax)::
    ("-safe", Arg.String (fun s -> safes := !safes @ [s]),
-    "<relax-list> specify a safe list")::
+    with_top_level_choice_doc "<relax-list> specify a safe list")::
    ("-relaxlist", Arg.String (fun s -> safes := !safes @[s]),
-    "<relax-list> specify a list of relaxations of interest (alias for -safe)")::
+    with_top_level_choice_doc "<relax-list> specify a list of relaxations of interest (alias for -safe)")::
    ("-rejectlist", Arg.String (fun s -> rejects := Some s),
    "<reject-list> specify a list of relaxation combinations to reject from generation")::
    stdout_spec false ::

gen/common/dune

@@ -1,5 +1,8 @@
 (ocamllex lexUtil)
 
+(menhir
+ (modules parser))
+
 (rule
  (copy ../../Version.ml Version.ml))
 

gen/common/edge.ml

@@ -198,6 +198,15 @@ and module RMW = A.RMW = struct
 
   type value = A.Value.v
 
+  let pre_parse_string s =
+    let parsed_result = Lexing.from_string (String.trim s)
+    |> LexUtil.parse Parser.main
+    |> Ast.expand in
+    match parsed_result with
+      | [x] -> x
+      | _ ->
+        Warn.user_error "only accepts exactly one input cycle."
+
   let compute_rmw rmw old operand =
     Value.from_int @@ RMW.compute_rmw rmw ~old:(Value.to_int old) ~operand:(Value.to_int operand)
 
@@ -555,15 +564,12 @@ let fold_tedges f r =
     with Not_found -> Warn.fatal "Bad atom: %s" s
 
   let parse_atoms xs =
-    try
-      List.fold_left
-        (fun k x ->
-          List.fold_left
-            (fun k s -> parse_atom s::k)
-            k (LexUtil.just_split x))
-        [] xs
-    with LexUtil.Error msg ->
-      Warn.fatal "bad atoms list (%s)" msg
+    List.map
+      ( fun x ->
+        pre_parse_string x
+        |> List.map parse_atom
+      ) xs
+    |> List.flatten
 
   let get_access_atom = A.get_access_atom
 
@@ -659,7 +665,8 @@ let fold_tedges f r =
     try Hashtbl.find t s
     with Not_found -> Warn.fatal "Bad edge: %s" s
 
-  let parse_edges s = List.map parse_edge (LexUtil.just_split s)
+  let parse_edges s =
+    pre_parse_string s |> List.map parse_edge
 
   let pp_edges es = String.concat " " (List.map pp_edge es)