Isolated inlined C code into source and header files

dirs-and-confs.txt

@@ -7,4 +7,4 @@
 ./herd/tests/instructions/AArch64.self ./herd/tests/instructions/AArch64.self/self.cfg
 ./herd/tests/instructions/AArch64.kvm ./herd/tests/instructions/AArch64.kvm/kvm.cfg
 ./herd/tests/instructions/AArch64.vmsa+mte ./herd/tests/instructions/AArch64.vmsa+mte/vmsa+mte.cfg
-catalogue/aarch64-ifetch/tests catalogue/aarch64-ifetch/cfgs/new-web.cfg
+catalogue/aarch64-ifetch/tests catalogue/aarch64-ifetch/cfgs/new-web.cfg

litmus/dumpRun.ml

@@ -125,6 +125,15 @@ end = struct
         (List.rev sources) ;
       fprintf chan "\n"
     end ;
+    begin
+      begin match Cfg.mode with
+        | Mode.Kvm -> ()
+        | Mode.Std | Mode.PreSi ->
+           fprintf chan "SRCDIR = $(CURDIR)\n"
+      end ;
+      fprintf chan "SHARED_SRC_DIR = $(CURDIR)/lib\n" ;
+      fprintf chan "GCCOPTS += -I $(SHARED_SRC_DIR)\n\n"
+    end ;
     begin
       match Cfg.mode with
       | Mode.Std|Mode.PreSi -> ()
@@ -143,9 +152,15 @@ end = struct
            if flags.Flags.pac then
              "auth.o"::utils
            else utils in
-         fprintf chan "UTILS=%s\n"
+         fprintf chan "UTILS = %s\n\n"
            (String.concat " " utils)
     end ;
+    begin
+      fprintf chan "UTILS_SRC = $(wildcard $(SHARED_SRC_DIR)/*.c)\n\n"
+    end ;
+    begin
+      fprintf chan "UTILS_OBJ = $(UTILS_SRC:.c=.o)\n\n"
+    end ;
     ()
 
   let makefile_clean chan extra =
@@ -167,10 +182,10 @@ end = struct
             b :: k
           else k) utils [] in
     List.iter
-      (fun u ->
+      (fun u -> 
         let src = u ^ ".c" and obj = u ^ ".o" in
         fprintf chan "%s: %s\n" obj src ;
-        fprintf chan "\t$(GCC) $(GCCOPTS) %s-O2 -c %s\n"
+        fprintf chan "\t$(GCC) $(GCCOPTS) %s-O2 -c -o $@ %s\n"
           (if
             TargetOS.is_freebsd Cfg.targetos &&
             u = "affinity"
@@ -180,9 +195,11 @@ end = struct
         fprintf chan "\n")
       utils ;
 (* UTIL objs *)
+    fprintf chan "$(SHARED_SRC_DIR)/%%.o: $(SHARED_SRC_DIR)/%%.c\n";
+    fprintf chan "\t$(GCC) $(GCCOPTS) -O2 -c -o $@ $<\n\n" ;
     let utils_objs =
       String.concat " " (List.map (fun s -> s ^ ".o") utils) in
-    fprintf chan "UTILS=%s\n\n" utils_objs ;
+    fprintf chan "UTILS = %s\n\n" utils_objs ;
     ()
 ;;
 
@@ -477,9 +494,9 @@ let dump_shell_cont arch flags sources utils =
           | TargetOS.Linux|TargetOS.AIX
           | TargetOS.FreeBsd|TargetOS.Android8
             -> 's' in
-          fprintf chan "%%.exe:%%.%c $(UTILS)\n" src_ext ;
+          fprintf chan "%%.exe:%%.%c $(UTILS) $(UTILS_OBJ)\n" src_ext ;
           fprintf chan
-            "\t$(GCC) $(GCCOPTS) $(LINKOPTS) -o $@ $(UTILS) $<\n" ;
+            "\t$(GCC) $(GCCOPTS) $(LINKOPTS) -o $@ $(UTILS) $(UTILS_OBJ) $<\n" ;
           fprintf chan "\n" ;
 (* .s pattern rule *)
           fprintf chan "%%.s:%%.c\n" ;
@@ -668,12 +685,12 @@ let dump_c_cont xcode arch flags sources utils nts =
             fprintf chan "\tsed -e 's|.c$$|.o|g' < src > obj\n\n"
           end ;
           let o1 =
-            if infile then "$(UTILS) obj run.o"
-            else "$(UTILS) $(OBJ) run.o" in
+            if infile then "$(UTILS) $(UTILS_OBJ) obj run.o"
+            else "$(UTILS) $(UTILS_OBJ) $(OBJ) run.o" in
           let o2 =
-            if infile then "$(UTILS) @obj run.o"
+            if infile then "$(UTILS) $(UTILS_OBJ) @obj run.o"
             else o1 in
-          fprintf chan "$(EXE): %s\n" o1 ;
+          fprintf chan "$(EXE): %s\n" o1;
           fprintf chan "\t$(GCC)  $(GCCOPTS) $(LINKOPTS) -o $@ %s\n" o2 ;
           fprintf chan "\n" ;
           (* .o pattern rule *)

litmus/libdir/_aarch64/_memtag.c

@@ -14,9 +14,6 @@
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
 
-#ifndef _MEMTAG_H
-#define _MEMTAG_H 1
-
 #include "kvm-headers.h"
 #include "memtag.h"
 
@@ -109,5 +106,3 @@ void mte_init(tag_check_key tag_check)
     set_tcr_el1(tcr); // also issues isb and flushes tlb
   }
 }
-
-#endif /* _MEMTAG_H */

litmus/libdir/_aarch64/_memtag.h

@@ -13,6 +13,8 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef _MEMTAG_H
+#define _MEMTAG_H 1
 
 typedef enum
 { tag_check_Off = 0b0000,
@@ -22,3 +24,4 @@ typedef enum
 } tag_check_key;
 
 void mte_init(tag_check_key tag_check);
+#endif

litmus/libdir/_aarch64/asmhandler.c

@@ -1,4 +1,21 @@
-static void exceptions_init_test(void *p) {
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#include <asmhandler.h>
+
+void exceptions_init_test(void *p) {
   asm __volatile__ (
 "msr vbar_el1,%0\n\t"
 "isb\n"

litmus/libdir/_aarch64/asmhandler.h

@@ -0,0 +1,19 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef ASMHANDLER_H
+#define ASMHANDLER_H 1
+void exceptions_init_test(void *p);
+#endif

litmus/libdir/_aarch64/barrier.c

@@ -16,14 +16,9 @@
 /**********************/
 /* User level barrier */
 /**********************/
+#include "barrier.h"
 
-
-typedef struct {
-  volatile int c,sense;
-  int n ;
-} sense_t;
-
-static void barrier_init (sense_t *p,int n) {
+void barrier_init (sense_t *p,int n) {
   p->n = p->c = n;
   p->sense = 0;
 }
@@ -53,7 +48,7 @@ static void barrier_init (sense_t *p,int n) {
 	dmb	ish
 	ret
 */
-static void barrier_wait(sense_t *p) {
+void barrier_wait(sense_t *p) {
   int sense = p->sense ;
   int r1,r3 ;
 asm __volatile (
@@ -87,7 +82,7 @@ asm __volatile (
 }
 #if 0
 /* C version */
-static void barrier_wait(sense_t *p) {
+void barrier_wait(sense_t *p) {
   int sense = p->sense ;
   __sync_synchronize() ;
   int rem = __sync_add_and_fetch(&p->c,-1) ;

litmus/libdir/_aarch64/barrier.h

@@ -0,0 +1,30 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+/**********************/
+/* User level barrier */
+/**********************/
+#ifndef BARRIER_H
+#define BARRIER_H 1
+
+typedef struct {
+  volatile int c,sense;
+  int n ;
+} sense_t;
+
+void barrier_init (sense_t *p,int n);
+
+void barrier_wait(sense_t *p);
+#endif

litmus/libdir/_aarch64/instruction.h

@@ -1 +1,22 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef INSTRUCTION_H
+#define INSTRUCTION_H
+#include <stdint.h>
+
 typedef uint32_t ins_t; /* Type of instructions */
+#endif

litmus/libdir/_aarch64/intrinsics.h

@@ -1,3 +1,19 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
 #ifdef __ARM_NEON
 #include <arm_neon.h>
 #define cast(v)			\

litmus/libdir/_aarch64/kvm-headers.h

@@ -13,6 +13,8 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef KVM_HEADERS_H
+#define KVM_HEADERS_H 1
 
 #include <vmalloc.h>
 #include <alloc_page.h>
@@ -355,3 +357,4 @@ inline static parel1_t pack_par_el1(int pa, parel1_t p) {
     ((parel1_t)pa << OA_PACKED) |
     pack_flag(p, msk_f, 0);
 }
+#endif

litmus/libdir/_aarch64/kvm-self.c

@@ -16,20 +16,40 @@
 /* Authors:                                                                 */
 /* Nikos Nikoleris, Arm Limited.                                            */
 /****************************************************************************/
+#include <kvm-self.h>
+#include <_find_ins.h>
+#include <../kvm-headers.h>
 
-static void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
+static ins_t getret(void) {
+  ins_t *x1;
+  ins_t r;
+  asm __volatile__ (
+  "adr %[x1],0f\n\t"
+  "ldr %w[x2],[%[x1]]\n\t"
+  "b 1f\n"
+  "0:\n\t"
+  "ret\n"
+  "1:\n"
+:[x1] "=&r" (x1),[x2] "=&r" (r)
+:
+: "cc","memory"
+);
+  return r;
+}
+
+void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
 {
   while (vaddr < vaddr_end) {
     selfbar((void *)vaddr);
     vaddr += cache_line_size;
   }
 }
 
-static size_t code_size(ins_t *p,int skip) {
+size_t code_size(ins_t *p,int skip) {
   return (find_ins(getret(), p, skip) + 1) * sizeof(ins_t);
 }
 
-static void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end)
+void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end)
 {
   while (vaddr < vaddr_end) {
     pteval_t *pte = litmus_tr_pte((void *)vaddr);
@@ -43,7 +63,7 @@ static void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end)
   );
 }
 
-static void code_init(void *code, void *src, size_t sz)
+void code_init(void *code, void *src, size_t sz)
 {
   memcpy(code, src, sz);
   litmus_icache_sync((uintptr_t)code, (uintptr_t)code + sz);

litmus/libdir/_aarch64/kvm-self.h

@@ -0,0 +1,31 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef KVM_SELF_H
+#define KVM_SELF_H 1
+
+#include <stdint.h>
+#include <stddef.h>
+#include <instruction.h>
+#include <self.h>
+
+void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end);
+
+size_t code_size(ins_t *p,int skip);
+
+void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end);
+
+void code_init(void *code, void *src, size_t sz);
+#endif

litmus/libdir/_aarch64/kvm.c.rules

@@ -1,5 +1,5 @@
 clean:
-	/bin/rm -f *.o *.s *.t *.elf *.flat *~ *.t $(H)
+	/bin/rm -f *.o lib/*.o *.s *.t *.elf *.flat *~ *.t $(H)
 
 %.s: %.c
 	$(CC) -DASS $(GCCOPTS) -S $<
@@ -15,7 +15,7 @@ clean:
 
 %.elf: LDFLAGS = -nostdlib -pie -n
 
-run.elf: run.o $(OBJ) $(UTILS) $(FLATLIBS) $(SRCDIR)/arm/flat.lds $(cstart.o)
+run.elf: run.o $(OBJ) $(UTILS) $(UTILS_OBJ) $(FLATLIBS) $(SRCDIR)/arm/flat.lds $(cstart.o)
 	$(CC) $(CFLAGS) -c -o $(@:.elf=.aux.o) $(SRCDIR)/lib/auxinfo.c \
 		-DPROGNAME=\"$(@:.elf=.flat)\" -DAUXFLAGS=$(AUXFLAGS)
 	$(LD) $(LDFLAGS) -o $@ -T $(SRCDIR)/arm/flat.lds \