[gen] Rework on printing generated litmus tests

Makefile

@@ -694,10 +694,16 @@ test.vmsa+ifetch:
 	@ echo "herd7 AArch64 VMSA+ifetch instructions tests: OK"
 
 ### Diy tests, includes
+### - A `diyone7` generated syntax check
 ### - A `diy7` with `cycleonly` instance checks the cycle generations
 ### - Several `diycross7` + `herd7` instances, check if the generated litmus tests
 ###   are equivalent based on `herd7` result.
 diy-test:: | build
+diy-test:: diyone-basic-test
+diyone-basic-test:
+	@ echo
+	dune test gen/tests
+	@ echo "diyone7 basic test: OK"
 diy-test:: diy-baseline-cycleonly
 diy-baseline-cycleonly::
 	@ echo

gen/AArch64Compile_gen.ml

@@ -527,7 +527,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
 
     let next_reg_sz st p sz =
       let r,st = next_reg st in
-      let loc = A.Reg (p,r) in
+      let loc = A.of_reg p r in
       let st = A.add_type loc (type_of_sz sz) st in
       r,st
 
@@ -943,7 +943,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
     let do_emit_mov_sz emit_mov_sz sz st p init v =
       let rA,init,csi,st = emit_mov_sz sz st p init v in
       let st =
-        let loc = A.Reg (p,rA) in
+        let loc = A.of_reg p rA in
         let t = type_of_sz sz in
         A.add_type loc t st in
       rA,init,csi,st

gen/ARMArch_gen.ml

@@ -90,7 +90,6 @@ let pp_dp = function
         | _ -> false
 
       let pp_reg = pp_reg
-      let pp_i _ = assert false
       let free_registers = allowed_for_symb
       type arch_atom = atom
       module Value = Value

gen/BellArch_gen.ml

@@ -272,7 +272,6 @@ include
       let is_symbolic _ = false
 
       let pp_reg = pp_reg
-      let pp_i _ = assert false
       let free_registers = allowed_for_symb
       type arch_atom = atom
       module Value = Value

gen/CCompile_gen.ml

@@ -818,17 +818,18 @@ module Make(O:Config) : Builder.S
                   obsc@cs,(m,f@fs),ios
                 else Warn.fatal "Last minute check"
               else  Warn.fatal "Too many procs" in
-            let f =
+            let empty_faults = (F.FaultAtomSet.empty,F.FaultAtomSet.empty) in
+            let fc flts =
               match O.cond with
               | Unicond ->
                   let evts =
                     List.map
                       (List.map (fun n -> n.C.evt))
                       splitted in
-                  F.run evts m
-              | Cycle -> F.check f
-              | Observe -> F.observe f in
-            (add_args env c,f (F.FaultSet.empty,F.FaultSet.empty)),
+                  F.forall_condition evts m flts
+              | Cycle -> F.exists_condition ~is_pos:(not O.neg) f flts
+              | Observe -> F.observe_condition in
+            (add_args env c,fc empty_faults),
             (U.compile_prefetch_ios (List.length obsc) ios,
              U.compile_coms splitted),
             env
@@ -1006,7 +1007,6 @@ module Make(O:Config) : Builder.S
       let get_name t = t.name
       let set_name t n = { t with name=n; }
       let set_scope _t _sc = Warn.fatal "No scope for C"
-      let add_info t k i = { t with info = (k,i)::t.info; }
       let extract_edges t = t.edges
 
       let dump_c_test_channel chan t =
@@ -1019,7 +1019,7 @@ module Make(O:Config) : Builder.S
         (* Empty init *)
         dump_init chan t.prog ;
         dump_code chan t.prog ;
-        F.dump_final chan t.final ;
+        fprintf chan "%s" (F.dump_constr t.final);
         ()
 
 (*

gen/MIPSArch_gen.ml

@@ -102,7 +102,6 @@ include
         | Symbolic_reg _ -> true
         | _ -> false
       let pp_reg = pp_reg
-      let pp_i _ = assert false
       let free_registers = allowed_for_symb
       type arch_atom = atom
       module Value = Value

gen/PPCArch_gen.ml

@@ -103,7 +103,6 @@ module Make(C:Config)  =
             | Symbolic_reg _ -> true
             | _ -> false
           let pp_reg = pp_reg
-          let pp_i _ = assert false
           let free_registers = allowed_for_symb
           type arch_atom = atom
           module Value = Value

gen/RISCVArch_gen.ml

@@ -224,8 +224,6 @@ include
         | _ -> false
 
       let pp_reg = pp_reg
-      let pp_i _ = assert false
-
       let free_registers = allowed_for_symb
       type arch_atom = atom
       module Value = Value

gen/RISCVCompile_gen.ml

@@ -124,7 +124,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S  =
     | 0 -> zero,init,st
     | _ ->
         let r,st = next_reg st in
-        r,(Reg (p,r),Some (A.S (Printf.sprintf "0x%x" v)))::init,st
+        r,((of_reg p r),Some (A.S (Printf.sprintf "0x%x" v)))::init,st
 
 
 

gen/X86Arch_gen.ml

@@ -126,7 +126,6 @@ include
         | Symbolic_reg _ -> true
         | _ -> false
       let pp_reg = pp_reg
-      let pp_i _ = assert false
       let free_registers = allowed_for_symb
       type arch_atom = atom
       module Value = Value

gen/X86_64Arch_gen.ml

@@ -252,7 +252,6 @@ module Make
               | Symbolic_reg _ -> true
               | _ -> false
             let pp_reg = pp_reg
-            let pp_i _ = assert false
             let free_registers = allowed_for_symb
             type special = xmm
             type special2

gen/archLoc.mli

@@ -26,5 +26,4 @@ module type S = sig
   val location_compare : location -> location -> int
   val pp_location : location -> string
   val pp_location_brk : location -> string
-  val pp_i : int -> string
 end

gen/builder.mli

@@ -29,7 +29,6 @@ module type S = sig
   val get_name : test -> string
   val set_name : test -> string -> test
   val set_scope : test -> BellInfo.scopes -> test
-  val add_info : test -> string -> string -> test
 
   type node = C.node
   type edge = E.edge

gen/common/AArch64Arch_gen.ml

@@ -1089,7 +1089,6 @@ include
         | _ -> false
 
       let pp_reg = pp_reg
-      let pp_i = pp_i
       let free_registers = allowed_for_symb
 
       type special = reg

gen/common/archExtra_gen.ml

@@ -31,7 +31,6 @@ module type I = sig
   val specials : special list
   val specials2 : special2 list
   val specials3 : special3 list
-  val pp_i : int -> string
   module Value:Value_gen.S with type atom = arch_atom
 end
 
@@ -41,16 +40,14 @@ module type S = sig
   type arch_reg
 
   module Value : Value_gen.S with type atom = arch_atom
+  module Location : Location.S with type loc_reg = arch_reg and type loc_global = string
 
 (* Locations *)
-  type location =
-    | Reg of Code.proc * arch_reg
-    | Loc of string
+  type location = Location.location
 
   val of_loc : Code.loc -> location
   val of_reg : Code.proc -> arch_reg -> location
 
-  val pp_i : int -> string
   val pp_location : location -> string
   val pp_location_brk : location -> string
   val location_compare : location -> location -> int
@@ -124,38 +121,43 @@ and module Value := I.Value
   type arch_reg = I.arch_reg
   type arch_atom = I.arch_atom
 
-  type location =
-    | Reg of int * arch_reg
-    | Loc of string
-
   let pp_symbol loc =
     match Misc.tr_pte loc with
     | Some s -> Misc.pp_pte s
     | None -> loc
 
-  let pp_location = function
-    | Reg (i,r) ->
-        if I.is_symbolic r then I.pp_reg r
-        else sprintf "%i:%s" i (I.pp_reg r)
-    | Loc loc -> pp_symbol loc
-
-  let pp_location_brk = function
-    | Reg (i,r) ->
-        if I.is_symbolic r then I.pp_reg r
-        else sprintf "%i:%s" i (I.pp_reg r)
-    | Loc loc -> sprintf "[%s]" (pp_symbol loc)
-
-  let pp_i = I.pp_i
-
-  let location_compare loc1 loc2 = match loc1,loc2 with
-  | Reg _,Loc _ -> -1
-  | Loc _,Reg _ -> 1
-  | Reg (p1,r1),Reg (p2,r2) ->
-      begin match Misc.int_compare p1 p2 with
-      | 0 -> compare r1 r2
-      | r -> r
-      end
-  | Loc loc1,Loc loc2 -> compare loc1 loc2
+  module Location = Location.Make(
+    struct
+      type arch_reg = I.arch_reg
+      let pp_reg = I.pp_reg
+      let reg_compare = compare
+
+      type arch_global = string
+      let pp_global loc =
+        if Misc.tr_pte loc <> None then
+          sprintf "%s" (pp_symbol loc)
+        else loc
+      let global_compare lhs rhs =
+        (* Order `x` > `tag(x)` > `pte(x)` > `y`.
+         The helper function extract the actual location, and
+         the bank of the location, i.e. Tag, Pte or Ord. The bank
+         is used to order when actual location is the same. *)
+        let get_actual_location_bank loc =
+          match Misc.tr_atag loc with
+          | Some x -> x,Code.Tag
+          | None -> match Misc.tr_pte loc with
+              | Some x -> x,Code.Pte
+              | None -> loc,Code.Ord in
+        compare (get_actual_location_bank lhs) (get_actual_location_bank rhs)
+    end)
+
+  type location = Location.location
+
+  let pp_location = Location.pp_location
+
+  let pp_location_brk = Location.pp_location_brk
+
+  let location_compare = Location.location_compare
 
   module Value = I.Value
 
@@ -167,8 +169,8 @@ and module Value := I.Value
   module LocSet = MySet.Make(LocOrd)
   module LocMap = MyMap.Make(LocOrd)
 
-  let of_loc loc = Loc (Code.as_data loc)
-  let of_reg p r = Reg (p,r)
+  let of_loc loc = Location.Location_global (Code.as_data loc)
+  let of_reg p r = Location.Location_reg (p,r)
 
   (* - S of a plain value, a pte_* address or a phy_* address
      - P of a PteVal *)
@@ -216,19 +218,19 @@ and module Value := I.Value
       (* Add the locs `loc` and values `v` inside `iv` to `i` *)
       List.fold_left
         (fun env (loc,v) ->
-          if Misc.is_pte loc then (Loc loc,Some (P (Value.to_pte v)))::env
+          if Misc.is_pte loc then (Location.Location_global loc,Some (P (Value.to_pte v)))::env
           (* Do not include if the value is default zero *)
           else if Value.to_int v = 0 then env
-          else (Loc loc,Some (S (Value.pp_v ~hexa:hexa v)))::env
+          else (Location.Location_global loc,Some (S (Value.pp_v ~hexa:hexa v)))::env
         ) i iv in
     let already_here =
       List.fold_left
         (fun k (loc,v) ->
           let k = match loc with
           (* Add Loc `s` into `k` if `s` is not a pte address nor a number *)
-          | Loc s -> add_some (as_virtual s) k
+          | Location.Location_global s -> add_some (as_virtual s) k
           (* No process on register *)
-          | Reg _  -> k in
+          | Location.Location_reg _  -> k in
           let k = match v with
           (* Add value `s` into `k` if `s` is not a pte nor a number *)
           | Some (S s) -> add_some (as_virtual s) k
@@ -240,9 +242,9 @@ and module Value := I.Value
         (fun k (loc,v) ->
           let k = match loc with
           (* Add Loc `s` into `k` if `s` is a pte or physical address *)
-          | Loc s -> add_some (refers_virtual s) k
+          | Location.Location_global s -> add_some (refers_virtual s) k
           (* No process on register *)
-          | Reg _ -> k in
+          | Location.Location_reg _ -> k in
           let k = match v with
           (* Add value `s` into `k` if `s` is a pte or physical address *)
           | Some (S s) -> add_some (refers_virtual s) k
@@ -255,7 +257,7 @@ and module Value := I.Value
        then add it into init state `i` *)
     let i =
       StringSet.fold
-        (fun x i -> (Loc x,None)::i)
+        (fun x i -> (Location.Location_global x,None)::i)
         (StringSet.diff refer already_here)
         i in
     i
@@ -298,7 +300,7 @@ and module Value := I.Value
 
   let used_register init =
     List.filter_map ( function
-      | (Reg (_,r),Some _) -> Some r
+      | (Location.Location_reg (_,r),Some _) -> Some r
       | _ -> None ) init
 
   let remove_reg_allocator st remove =

gen/common/variant_gen.ml

@@ -52,6 +52,11 @@ let tags =
    "NoVolatile"; "Morello"; "VMSA(KVM)"; "NoFault";
    "Neon"; "ConstrainedUnpredictable"; ]
 
+let all_t =
+  [ AsAmo ; ConstsInInit ; Mixed ; FullMixed ; MixedDisjoint ; MixedStrictOverlap ;
+    Self ; MemTag ; NoVolatile ; Morello ; KVM ; NoFault ;
+    Neon ; SVE ; SME ; ConstrainedUnpredictable ]
+
 let parse tag = match Misc.lowercase tag with
 | "asamo" -> Some AsAmo
 | "constsininit" -> Some ConstsInInit
@@ -89,5 +94,17 @@ let pp = function
   | SME -> "sme"
   | ConstrainedUnpredictable -> "ConstrainedUnpredictable"
 
+let pp_herd_variant = function
+  | AsAmo | ConstsInInit | NoVolatile | NoFault -> None
+  | Neon -> Some "neon"
+  | SVE -> Some "sve"
+  | SME -> Some "sme"
+  | Mixed | FullMixed | MixedDisjoint | MixedStrictOverlap -> Some "mixed"
+  | Self -> Some "ifetch"
+  | MemTag -> Some "memtag"
+  | Morello -> Some "morello"
+  | KVM  -> Some "vmsa"
+  | ConstrainedUnpredictable -> Some "ConstrainedUnpredictable"
+
 let is_mixed v = v Mixed || v FullMixed
 let is_kvm v = v KVM

gen/common/variant_gen.mli

@@ -49,10 +49,12 @@ type t =
   | ConstrainedUnpredictable
 
 val tags : string list
+val all_t : t list
 
 val parse : string -> t option
 
 val pp : t -> string
+val pp_herd_variant : t -> string option
 
 val is_mixed : (t -> bool) -> bool
 val is_kvm : (t -> bool) -> bool

gen/compileCommon.ml

@@ -91,11 +91,11 @@ module Make(C:Config) (A:Arch_gen.S) = struct
       let ok,st = A.ok_reg st in
 (* Add explict `int` type for `ok<n>` variables *)
       let ok_loc = Code.as_data (Code.myok_proc p) in
-      let st = A.add_type (A.Loc ok_loc) TypBase.Int st in
+      let st = A.add_type (A.Location.Location_global ok_loc) TypBase.Int st in
       let init,cs_store,st = emit_store_reg st p init ok_loc ok in
       let csok = A.Label (Label.last p,A.Nop)::cs_store in
 (* Add explict initialvalue of zero for `ok<n>` variables *)
-      (A.Loc ok_loc,Some (A.S "0"))::init,cs@csok,st
+      (A.Location.Location_global ok_loc,Some (A.S "0"))::init,cs@csok,st
     else
       init,cs,st