[herd,litmus] Initial support for translating addresses of instructions

Makefile

@@ -682,6 +682,18 @@ test.vmsa+mte:
 		$(REGRESSION_TEST_MODE)
 	@ echo "herd7 AArch64 VMSA+MTE instructions tests: OK"
 
+test:: test.vmsa+ifetch
+test-local:: test.vmsa+ifetch
+test.vmsa+ifetch:
+	@ echo
+	$(HERD_REGRESSION_TEST) \
+		-herd-path $(HERD) \
+		-libdir-path ./herd/libdir \
+		-litmus-dir ./herd/tests/instructions/AArch64.vmsa+ifetch \
+		-conf ./herd/tests/instructions/AArch64.vmsa+ifetch/vmsa+ifetch.cfg \
+		$(REGRESSION_TEST_MODE)
+	@ echo "herd7 AArch64 VMSA+ifetch instructions tests: OK"
+
 ### Diy tests, includes
 ### - A `diy7` with `cycleonly` instance checks the cycle generations
 ### - Several `diycross7` + `herd7` instances, check if the generated litmus tests

diymicro/compile.ml

@@ -260,6 +260,9 @@ let rec dump_pseudo = function
   | A.Macro (m, args) :: rem ->
       Printf.sprintf "%s(%s)" m (String.concat "," (List.map A.pp_reg args))
       :: dump_pseudo rem
+  | A.Pagealign :: _ -> Warn.fatal "Page alignment not available in diymicro"
+  | A.Skip _ :: _ ->
+      Warn.fatal "Page alignment placeholders not available in diymicro"
 
 let fmt_cols =
   let rec fmt_col p k = function

gen/final.ml

@@ -250,6 +250,7 @@ module Make : functor (O:Config) -> functor (C:ArchRun.S) ->
       type fault_type = FaultType.t
       let pp_fault_type = FaultType.pp
       let fault_type_compare = FaultType.compare
+      let fault_type_matches = FaultType.matches
     end
 
     include Fault.Make(FaultArg)

gen/top_gen.ml

@@ -940,6 +940,8 @@ let rec dump_pseudo = function
         (String.concat ","
            (List.map A.pp_reg args))::
       dump_pseudo rem
+  | A.Pagealign::_ -> assert false (* support for .pagealign not implemented yet*)
+  | A.Skip _::_ -> assert false (* used internally in herd7 only *)
 
 let fmt_cols =
   let rec fmt_col p k = function

herd/AArch64ASLSem.ml

@@ -1407,7 +1407,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
             match act with
             | Act.Access
                 (dir,A.Location_global loc,_,_,
-                 AArch64Explicit.Exp,_,Access.(PHY_PTE|PTE))
+                 AArch64Explicit.Exp,_,Access.(PHY_PTE|PTE DISide.Data))
               when dir_ok dir
               ->
                 Some loc