Isolated inlined C code into source and header files by z5146542 · Pull Request #1699 · herd/herdtools7

z5146542 · 2026-02-05T17:02:03Z

This pull request now separates the inlined C code from the generated C code into a separate source and header file (e.g., barrier.c and barrier.h) respecitvely.
Previosuly, when the C code is generated, all relevant files are created within the specified root directory:

root/
root/test1.c
root/test2.c
root/run.c
root/utils.c
root/utils.h
root/Makefile
root/README
...

Now, the generated C code results in the following:

root/
root/test1.c
root/test2.c
root/run.c
root/utils.c
root/utils.h
root/Makefile
root/README
root/lib/
root/lib/barrier.c
root/lib/barrier.h
...

For all tests included in the batch (e.g. test1.c and test2.c), barrier.c is no longer inlined and is replaced with #include <barrier.h>. The same applies for most of the other inlined code.

For some previously inlined functions and variables with dependencies based on specific test cases (e.g. functions depending on macros that may differ depending on the test cases), they remain static for the time being. The plan is to remove this dependency after this change is incorporated.

diaolo01

Thanks Simon, please squash all commits into a single one.

I notice there are three types of drivers: C, XCode and Shell. I tried running a test using presi and driver shell and it is unable to link the barrier.o.
I used the following to test:
./herdtools7/_build/install/default/bin/litmus7 -v -set-libdir ./herdtools7/litmus/libdir/ -mach aarch64 -a 1 -s 100 -r 100 ./herdtools7/herd/tests/instructions/AArch64/A04.litmus -driver shell -mode presi -o ./kvm-unit-tests/A014
It’s unclear what driver shell is for, but if we keep it, this PR should work across all driver types (C/XCode/Shell).

Could you tell me why there is a need for a separate lib folder for barrier files?

z5146542 · 2026-02-09T19:24:30Z

Thanks for the comment, and thanks for catching the make error -- this is now fixed, and hopefully this is the last error fix I need to do relating to Makefile (Edit: it seems like driver shell is the default driver mode when this field is unspecified).

For now, I created a separate lib directory for the C files generated from preSi.ml (as opposed to files generated from dumpRun.ml, which is responsible for the creation of Makefile). Currently, dumpRun.ml enumerates the relevant source and header files used by the test and adds each case one by one to Makefile. I tried not to touch this part of the code as much as possible, and I did not want to also enumerate the C files generated from preSi.ml one by one, which may differ depending on the test case. The following line:

$(SHARED_SRC_DIR)/%.c: $(SHARED_SRC_DIR)/%.o
	$(GCC) $(GCCOPT) -O2 -c -o $@ $<

...ensures that all C files generated by preSi.ml are compiled without having to manually enumerate every single source and header file generated from preSi.ml.

Regarding squashing commits, I will get this fixed very soon.

z5146542 · 2026-02-19T13:35:55Z

@diaolo01 I have now isolated all inlined C files, and I have squashed all the commits. Please let me know if the changes look all good.

litmus/libdir/_aarch64/instruction.h

litmus/libdir/_aarch64/asmhandler.h

litmus/libdir/_aarch64/kvm_fault_handler.h

litmus/libdir/_arm/instruction.h

relokin

$ make litmus-cata-aarch64-test-presi
fails, can you please have a look.

z5146542 · 2026-03-03T09:15:25Z

@relokin Thanks for this. The issue is now fixed. make litmus-aarch-test - as a whole - should now pass.

diaolo01

I tried running make litmus-aarch64-test and I am getting all sorts of errors. Mostly to do with inclusion and definition of the right headers. Please, can you look into it? You mentioned you were able to successfully run this on your end. If that is the case, I can share my local errors.

General minor comment: all lines
"Copyright year-present Institut National de Recherche en Informatique et "
Need to be
"Copyright 2026-present Institut National de Recherche en Informatique et "

litmus/libdir/_aarch64/kvm-self.h

litmus/libdir/_aarch64/presi-self.h

litmus/libdir/_mips/instruction.h

litmus/libdir/_ppc/instruction.h

litmus/libdir/_aarch64/self.h

z5146542 · 2026-03-20T17:44:37Z

@diaolo01 Thanks for this. all the cata-aarch64-kvm-related cases should compile without errors now.

diaolo01 · 2026-03-23T10:54:14Z

Thanks @z5146542, the PR now passes make litmus-aarch64-test once rebased on top of #1753.
Is there any reason timebase.h is not moved to lib/ like the other inlined code?
make clean does not remove the lib files, it would be good to update that too.

z5146542 · 2026-03-23T12:51:22Z

Hi @diaolo01, I have fixed the make clean issue - now, all the .o files in lib should be deleted when make clean is called.

timebase.h should now also move to lib.

litmus/libdir/_aarch64/kvm_timebase.h

litmus/dumpRun.ml

litmus/preSi.ml

remove the template file for now litmus now isolates shared files to a shared library directory platform_io source and header is now also copied to shared library platform_io copy works correctly now progress on inline porting removed duplicate copy methods and fixed aarch64 std mode makefile config fixed x86_64 makefile config fixed confs isolated inlined barrier code fixed makefile config fixed issue with makefile on shell mode isoated all inlined files reverted changes relating to isolating config some minor changes some minor changes

potential fix to instruction port problem fixed aarch64 std and presi instruction.h error fixed kvm self mode compilation error added missing header fixed kvm self mode compilation error kvm-self.h fixed self.h dependency issue added kvm headers for fix fixed header issue getret added kvm-self.h fixed self.h dependency issue getret added

…d readability of some code

remove the template file for now litmus now isolates shared files to a shared library directory platform_io source and header is now also copied to shared library platform_io copy works correctly now progress on inline porting removed duplicate copy methods and fixed aarch64 std mode makefile config fixed x86_64 makefile config fixed confs isolated inlined barrier code fixed makefile config fixed issue with makefile on shell mode isoated all inlined files reverted changes relating to isolating config some minor changes some minor changes

potential fix to instruction port problem fixed aarch64 std and presi instruction.h error fixed kvm self mode compilation error added missing header fixed kvm self mode compilation error kvm-self.h fixed self.h dependency issue added kvm headers for fix fixed header issue getret added kvm-self.h fixed self.h dependency issue getret added

…d readability of some code

litmus/libdir/_aarch64/_auth.h

litmus/libdir/_aarch64/_memtag.h

litmus/libdir/_aarch64/asmhandler.c

litmus/libdir/_aarch64/asmhandler.h

relokin · 2026-03-24T14:22:09Z

litmus/libdir/_aarch64/kvm-self.c

 /* Nikos Nikoleris, Arm Limited.                                            */
 /****************************************************************************/
+#include <kvm-self.h>
+#include <_find_ins.h>


if this is going to be a real header file should we remove the _?

I tried to preserve the file names as much as possible for now, but if you think that these files should be renamed I will do so.

relokin

I think we have to be a little more careful about the copyright headers. Especially in cases where you don't introduce it, there is no need to change it.

relokin · 2026-03-24T14:35:16Z

litmus/libdir/_aarch64/presi-self.c

do we need this to be different to kvm-self.c?

I'm not sure. These two files existed separately to begin with, so I only made minimal changes to both files.

litmus/libdir/_aarch64/presi-self.c

relokin · 2026-03-24T14:37:48Z

litmus/libdir/_aarch64/instruction.h

is this now a file that is both a standalone header and we might also inline?

it is a standalone header yes. instruction.h is now no longer inlined.

relokin

There are still cases where litmus won't work, for example:

litmus7 fails when I run a test directly:

$> litmus7 catalogue/aarch64/tests/MP.litmus
/var/folders/cl/7m7_nx7j0yn5tnsnwydtglcr0000gn/T/dir47895d.tmp/MP.c:114:10: fatal error: 'instruction.h' file not found

$> mkdir /tmp/t
$> litmus7 catalogue/aarch64/tests/MP.litmus -variant self -mode presi -a 4 -o /tmp/t
$> cd /tmp/t
$> make
....
MP.c:562:3: error: use of undeclared identifier 'cache_line_size'
562 | cache_line_size = getcachelinesize();
| ^~~~~~~~~~~~~~~
MP.c:562:21: error: call to undeclared function 'getcachelinesize'; ISO C99 and later do not support implicit function declarations
[-Wimplicit-function-declaration]
562 | cache_line_size = getcachelinesize();
| ^
2 errors generated.
make: *** [MP.s] Error 1


Independently, now we have some .c .h files which are still placed outside the libdir can we move them to the libdir?

relokin · 2026-04-01T22:07:07Z

litmus/libdir/_find_ins.h

Can we please rename this to find_ins.h (remove the _)?

relokin · 2026-04-01T22:07:19Z

litmus/libdir/_hash.h

Can we please rename this to hash.h (remove the _)?

relokin · 2026-04-01T22:07:34Z

litmus/libdir/_instance.h

Can we please rename this to instance.h (remove the _)?

relokin · 2026-04-01T22:08:28Z

litmus/libdir/_prelude_size.c

@@ -1,2 +1 @@
 static size_t prelude_size(ins_t *p) { return find_ins(nop,p,0); }
-


please revert this change.

relokin · 2026-04-01T22:14:02Z

litmus/libdir/kvm-aarch64.cfg

 delay = 32
 makevar = AUXFLAGS=0x0
-makevar = SRCDIR=$(PWD)/..
+makevar = SRCDIR=$(CURDIR)/..


can you please make a similar change to:

litmus/libdir/kvm-aarch64-qemu.cfg
litmus/libdir/kvm-armv8.1+rcpc.cfg
litmus/libdir/kvm-armv8.1.cfg:
litmus/libdir/kvm-armv8.5-a+memtag.cfg
litmus/libdir/kvm-m1.cfg
litmus/libdir/kvm-x86_64.cfg

relokin · 2026-04-01T22:14:28Z

litmus/objUtil.ml

      fnames

+(* Reference to the shared library *)
+    let libdir = "lib/"


Can we please rename this to litmus?

relokin · 2026-04-01T22:18:20Z

litmus/libdir/_aarch64/_memtag.c

Can we rename this to memtag.c?

relokin · 2026-04-01T22:18:31Z

litmus/libdir/_aarch64/_memtag.h

Can we rename this to memtag.h?

relokin · 2026-04-01T22:20:14Z

litmus/libdir/_aarch64/kvm-self.c

+#include <../kvm-headers.h>

-static void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
+static ins_t getret(void) {


Does this remain static?

relokin · 2026-04-01T22:20:40Z

litmus/libdir/_aarch64/kvm-self.c

 /****************************************************************************/
+#include <kvm-self.h>
+#include <_find_ins.h>
+#include <../kvm-headers.h>


This is not great can we please move kvm-headers into the libdir?

diaolo01 reviewed Feb 9, 2026

View reviewed changes

z5146542 force-pushed the inlineport branch from f9d9ecd to 4f1f0e8 Compare February 19, 2026 12:33

z5146542 changed the title ~~Isolated inlined code for barrier into source and header files~~ Isolated inlined C code into source and header files Feb 19, 2026

z5146542 marked this pull request as ready for review February 19, 2026 13:36

relokin requested changes Feb 23, 2026

View reviewed changes

litmus/libdir/_aarch64/instruction.h Outdated Show resolved Hide resolved

litmus/libdir/_aarch64/asmhandler.h Show resolved Hide resolved

litmus/libdir/_aarch64/kvm_fault_handler.h Show resolved Hide resolved

litmus/libdir/_arm/instruction.h Outdated Show resolved Hide resolved

z5146542 requested a review from relokin February 24, 2026 16:00

relokin reviewed Feb 27, 2026

View reviewed changes

z5146542 mentioned this pull request Mar 3, 2026

Isolated additional inlined C code as non-static C source and header files. #1739

Open

diaolo01 reviewed Mar 18, 2026

View reviewed changes

z5146542 force-pushed the inlineport branch 3 times, most recently from 41bef5d to 2dd8205 Compare March 19, 2026 16:55