Implement CMake build system #647

Timmmm · 2024-12-18T12:02:51Z

Switch from Makefiles to CMake. Some formal outputs are not yet fully supported by the CMake so the old Makefile is retained.

CMake has significant advantages:

IDE support is perfect, since it generates compile_commands.json. You can even go-to-definition to the generated code (I can demo this in the meeting if people want). Lots of IDEs also understand CMake and CTest.
Building all the emulators and running the tests is easy, parallel, and can generate an XML test result file (I haven't tested this though).
Better Windows support, e.g. CMake can generate Visual Studio project files.

This also adds a manual Github actions workflow to generate the JSON doc bundle, to allow inclusion of Sail snippets in the ISA manual.

emulator/riscv_sim_RV64

CMakeLists.txt

cmake/modules/FindGMP.cmake

emulator/CMakeLists.txt

arichardson

Overall this is looking good!
I've left a few CMake comments, but it's quite hard to review with the softfloat upgrade included here.

Timmmm · 2025-01-02T15:03:12Z

Thanks for the review! I've split the other changes out into separate commits, so the CMake stuff is just the last commit now and hopefully easier to review.

I might drop the upgrade to softfloat actually since it didn't really change the code and hopefully we'll remove it at some point anyway in favour of the pure Sail implementation.

jordancarlin · 2025-01-02T16:28:31Z

I think it probably makes sense to skip the softfloat upgrade for the reasons you mentioned, but if we do decide to keep it I have some suggestions so that you don’t have to modify their Makefile.

arichardson

Regarding the commit that suggests bundling GMP - we could also use https://cmake.org/cmake/help/latest/module/ExternalProject.html#examples to build a known version statically (either opt-in or by default).

arichardson · 2025-01-02T17:04:33Z

Makefile

@@ -1,428 +0,0 @@
-# Select architecture: RV32 or RV64.


Could keep the makefile for the targets that aren't supported yet and just defer to CMake by default?
e.g.

csim: $(BUILD_DIR) cmake -S . -B $(BUILD_DIR) -GNinja -DCMAKE_BUILD_TYPE=Release && ninja -C $(BUILD_DIR)

Or to avoid needing ninja:

csim: $(BUILD_DIR) cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release && $(MAKE) -C $(BUILD_DIR)

arichardson

A few minor comments but generally looks good to me.

.gitignore

CMakeLists.txt

emulator/CMakeLists.txt

CMakeLists.txt

cmake/extra_fast.cmake

Timmmm · 2025-01-03T09:51:41Z

if we do decide to keep it I have some suggestions so that you don’t have to modify their Makefile.

We aren't actually using their Makefile at all with the CMake version; I just kept the modifications so that it compiled as a standalone commit. I'll just remove the upgrade anyway though.

@arichardson I think you put a comment somewhere that I can't find now about keeping the Makefile. I think I'll just try and implement all of the features currently in the Makefile before merging this, rather than have two build systems...

arichardson

Adding all the other targets may take quite a while, maybe easiest for now to add CMake support and remove targets from the Makefile as we port them over?

E.g. this PR just removes the csim target (or rather have it defer to CMake cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release && $(MAKE) -C $(BUILD_DIR)) and then later commits add the extra features? Otherwise I worry this will be a long standing feature branch that never gets merged.

jrtc27 · 2025-01-09T19:19:53Z

Adding all the other targets may take quite a while, maybe easiest for now to add CMake support and remove targets from the Makefile as we port them over?

E.g. this PR just removes the csim target (or rather have it defer to CMake cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release && $(MAKE) -C $(BUILD_DIR)) and then later commits add the extra features? Otherwise I worry this will be a long standing feature branch that never gets merged.

Doing CMake incrementally makes sense to me, but I'd rather not incrementally remove things from Makefile. It's annoying to have to use both depending on what you want to do. I don't really see the benefit of it. Just leave Makefile alone until it's entirely subsumed by CMakeLists.txt and then delete it.

arichardson · 2025-01-09T20:11:45Z

Adding all the other targets may take quite a while, maybe easiest for now to add CMake support and remove targets from the Makefile as we port them over?
E.g. this PR just removes the csim target (or rather have it defer to CMake cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release && $(MAKE) -C $(BUILD_DIR)) and then later commits add the extra features? Otherwise I worry this will be a long standing feature branch that never gets merged.

Doing CMake incrementally makes sense to me, but I'd rather not incrementally remove things from Makefile. It's annoying to have to use both depending on what you want to do. I don't really see the benefit of it. Just leave Makefile alone until it's entirely subsumed by CMakeLists.txt and then delete it.

That sounds even better to me

billmcspadden-riscv · 2025-01-09T23:11:55Z

I agree.

…

On Thu, Jan 9, 2025 at 2:12 PM Alexander Richardson < ***@***.***> wrote: Adding all the other targets may take quite a while, maybe easiest for now to add CMake support and remove targets from the Makefile as we port them over? E.g. this PR just removes the csim target (or rather have it defer to CMake cmake -S . -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=Release && $(MAKE) -C $(BUILD_DIR)) and then later commits add the extra features? Otherwise I worry this will be a long standing feature branch that never gets merged. Doing CMake incrementally makes sense to me, but I'd rather not incrementally remove things from Makefile. It's annoying to have to use both depending on what you want to do. I don't really see the benefit of it. Just leave Makefile alone until it's entirely subsumed by CMakeLists.txt and then delete it. That sounds even better to me — Reply to this email directly, view it on GitHub <#647 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXROLOBMH4VMSUCF5IGWAX32J3JZ3AVCNFSM6AAAAABT2RMBV2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKOBRGE3DGMZRGE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

-- Bill McSpadden Formal Verification Engineer RISC-V International mobile: 503-807-9309

Timmmm · 2025-01-10T12:01:15Z

I've rebased it, removed the c_emulator rename and the softfloat update (we can do that later), and added RVFI support. I also updated the CI scripts.

I'm not sure I'm much of a fan of having two build systems during a transition. Verilator has exactly this - an old ./configure && make and an "experimental" CMake build system, and IMO it is quite confusing for users, and probably annoying for developers.

I reckon I can add the other targets without too much trouble, assuming they still work anyway! They aren't tested by CI and are presumably very rarely used.

arichardson · 2025-01-10T18:12:15Z

.pre-commit-config.yaml

@@ -1,6 +1,6 @@
 # See https://pre-commit.com for more information
 # See https://pre-commit.com/hooks.html for more hooks
-exclude: '^(prover_snapshots)|(generated_definitions)|(c_emulator/SoftFloat-3e)'
+exclude: '^(prover_snapshots)|(generated_definitions)|(dependencies/softfloat/berkeley-softfloat-3)'


I think we shouldn't run the checks on any dependencies? How about this:

Suggested change

exclude: '^(prover_snapshots)|(generated_definitions)|(dependencies/softfloat/berkeley-softfloat-3)'

exclude: '^(prover_snapshots)|(generated_definitions)|(dependencies)'

This is still open

Oops, fixed.

Oops sorry I forgot. It would still be nice to run pre-commit on the CMakeLists.txt file I added there, but I think something like this will work

exclude: '^(prover_snapshots)|(generated_definitions)|(dependencies/[^/]+/)'

arichardson · 2025-01-10T18:12:55Z

Makefile

@@ -1,428 +0,0 @@
-# Select architecture: RV32 or RV64.
-ARCH ?= RV64


Need to keep makefile for now for the prover stuff?

build_simulators.sh

arichardson · 2025-01-10T18:17:57Z

Makefile

-ifneq (,$(COVERAGE))
-C_FLAGS += --coverage -O1
-SAIL_FLAGS += -Oconstant_fold
-else
-C_FLAGS += -O3 -flto=auto
-endif
-
-ifneq (,$(SAILCOV))
-ALL_BRANCHES = generated_definitions/c/all_branches
-C_FLAGS += -DSAILCOV
-SAIL_FLAGS += -c_coverage $(ALL_BRANCHES) -c_include sail_coverage.h
-C_LIBS += $(SAIL_LIB_DIR)/coverage/libsail_coverage.a -lm -lpthread -ldl
-endif
-
-# Optionally link C_LIBS statically. Unlike -static this will not
-# link glibc statically which is generally a bad idea.
-ifneq (,$(STATIC))
-    UNAME_S := $(shell sh -c 'uname -s 2>/dev/null || echo not')
-    ifeq ($(UNAME_S),Darwin)
-        # Unfortunately the Mac linker does not support -Bstatic.
-        GMP_LIBS = $(shell pkg-config --variable=libdir gmp)/libgmp.a
-        C_LIBS_WRAPPED = $(C_LIBS)
-    else
-        C_LIBS_WRAPPED = -Wl,--push-state -Wl,-Bstatic $(C_LIBS) -Wl,--pop-state
-    endif
-else
-    C_LIBS_WRAPPED = $(C_LIBS)
-endif


I believe we have lost support for these options. I've used the sailcov option before, but not the other ones.

arichardson · 2025-01-10T18:19:50Z

Makefile

-riscv_hol: generated_definitions/hol4/$(ARCH)/riscvScript.sml
-riscv_hol_build: generated_definitions/hol4/$(ARCH)/riscvTheory.uo
-.PHONY: riscv_hol riscv_hol_build


Is the hol target still working? If so do we need to port it over to cmake?

arichardson · 2025-01-10T18:20:57Z

c_emulator/CMakeLists.txt

+    riscv_softfloat.h
+)
+
+foreach (arch IN ITEMS "rv32" "rv32d" "rv64" "rv64f" "rv32_rvfi" "rv32d_rvfi" "rv64_rvfi" "rv64f_rvfi")


Should we use variants here as well to make it easier to add the other targets in the future?

arichardson

Overall I still think this is a great change. A few things that were supported are no longer there.

I wonder if we should keep the Makefile for now and add something like the following to the top:

ifndef I_REALLY_NEED_TO_USE_MAKE
$(error The Makefile build system is deprecated, please use CMake instead. If you are using a target that does not exist there yet, please file and issue and re-run make with I_REALLY_NEED_TO_USE_MAKE=1 until this has been fixed)
endif

arichardson · 2025-01-10T18:24:33Z

I've rebased it, removed the c_emulator rename and the softfloat update (we can do that later), and added RVFI support. I also updated the CI scripts.

I'm not sure I'm much of a fan of having two build systems during a transition. Verilator has exactly this - an old ./configure && make and an "experimental" CMake build system, and IMO it is quite confusing for users, and probably annoying for developers.

I reckon I can add the other targets without too much trouble, assuming they still work anyway! They aren't tested by CI and are presumably very rarely used.

I agree that having multiple build systems is annoying and confusing. What do you think of my suggestion to add a (opt-out) error to the makefile to point people towards CMake.

We should probably also update the README.

jrtc27 · 2025-01-10T18:25:15Z

CMakeLists.txt

+    message(FATAL_ERROR "Sail not found. See README.md for installation instructions.")
+endif()
+
+set(DEFAULT_ARCHITECTURES "rv32;rv64" CACHE STRING "Architectures to build by default (rv32|rv64|rv32d|rv64f)(_rvfi)? " )


It's not clear to me on first read what these things mean. My initial interpretation was:
rv32: no float
rv64: no float
rv32d: FLEN=64
rv64f: FLEN=32

But then that's odd because FLEN=64 is a sensible configuration for RV64 (more so than FLEN=32, even), and of course that's not actually what's going on, there's a default non-zero FLEN and then the suffixed ones are overrides. But those names are confusing and weird.

On top of that, this is a behavioural change. The current Makefile build always defaults to FLEN=64 even for RV32, but you've changed that default to be FLEN=32.

You're right - I've changed it to rv32f, rv32d, rv64f, rv64d with the obvious meanings, and rv32d and rv64d are the defaults. I didn't add no-float configs since you can do that via a runtime option (the float length has to be compile-time currently).

arichardson · 2025-01-10T18:25:24Z

Once this lands, I am happy to submit some follow-up improvements to support static builds and builds that build GMP from source as part of the build process to avoid any system dependencies.

jrtc27 · 2025-01-10T18:28:30Z

I've rebased it, removed the c_emulator rename and the softfloat update (we can do that later), and added RVFI support. I also updated the CI scripts.
I'm not sure I'm much of a fan of having two build systems during a transition. Verilator has exactly this - an old ./configure && make and an "experimental" CMake build system, and IMO it is quite confusing for users, and probably annoying for developers.
I reckon I can add the other targets without too much trouble, assuming they still work anyway! They aren't tested by CI and are presumably very rarely used.

I agree that having multiple build systems is annoying and confusing. What do you think of my suggestion to add a (opt-out) error to the makefile to point people towards CMake.

We should probably also update the README.

I mean, if the Makefile is needed in some cases then it shouldn't be an error to use it. And if it's not needed then it can be deleted.

It's not confusing at all to have both, provided the CMake one is clearly labelled as experimental and in-progress. What's confusing is when there are two documented ways of building (or one documented but the other one isn't clearly labelled as "don't use yet unless you really want to").

arichardson · 2025-01-10T18:30:49Z

I've rebased it, removed the c_emulator rename and the softfloat update (we can do that later), and added RVFI support. I also updated the CI scripts.
I'm not sure I'm much of a fan of having two build systems during a transition. Verilator has exactly this - an old ./configure && make and an "experimental" CMake build system, and IMO it is quite confusing for users, and probably annoying for developers.
I reckon I can add the other targets without too much trouble, assuming they still work anyway! They aren't tested by CI and are presumably very rarely used.

I agree that having multiple build systems is annoying and confusing. What do you think of my suggestion to add a (opt-out) error to the makefile to point people towards CMake.
We should probably also update the README.

I mean, if the Makefile is needed in some cases then it shouldn't be an error to use it. And if it's not needed then it can be deleted.

It's not confusing at all to have both, provided the CMake one is clearly labelled as experimental and in-progress. What's confusing is when there are two documented ways of building (or one documented but the other one isn't clearly labelled as "don't use yet unless you really want to").

I agree it shouldn't be an error when it's needed. I was just suggesting making it an error that you can override to find out if anyone is using the targets that don't exist in the CMkae world yet.

If we just add a deprecation warning or keep the makefile around unchanged no one is going to report it until it becomes an error.

Timmmm · 2025-01-17T13:17:18Z

Ok I've done some updates:

Change float naming scheme as suggested by Jessica.
Add support for -DCOVERAGE=TRUE to enable Sail branch coverage support.
Change the c_emulator/CMakelists.txt variant list to use the same loop as in model/CMakeLists.txt. I really hope some of these compile time options will go away in future when Alasdair finishes the new config system.
Compile a few more variants in CI, to make sure they don't break.
I removed all of the whitelisted riscv-tests tests. We removed them because they don't work for some of the configs we use, but they do work for the default one so it makes sense to leave them for now I guess.
Added build_simulators.sh back for convenience.
Added the Makefile back and fixed an SMT argument.
Added support for rmem, and part of coq... but they're kind of incomplete because they don't actually compile at the moment - even with the original Makefile I run into various compilation errors, some in .sail files in the "standard library".
Add support for smt output. It compiles, but currently there are no $propertys so it doesn't output anything.

Given rmem and coq are broken anyway I think maybe it is best to do what Alex/Jessica were suggesting and keep the Makefile but add a warning to use CMake instead.

arichardson

I think this looks great now and since the Makefile is still there for now I don't see any reason to not merge it (once CI is happy).

Spotted a few minor things

arichardson · 2025-01-17T17:30:34Z

.pre-commit-config.yaml

@@ -1,6 +1,6 @@
 # See https://pre-commit.com for more information
 # See https://pre-commit.com/hooks.html for more hooks
-exclude: '^(prover_snapshots)|(generated_definitions)|(c_emulator/SoftFloat-3e)'
+exclude: '^(prover_snapshots)|(generated_definitions)|(dependencies/softfloat/berkeley-softfloat-3)'


This is still open

arichardson · 2025-01-17T17:31:24Z

.github/workflows/compile.yml

+        # By default only the rv32d and rv64d emulators are build,
+        # but we want to build more targets here to ensure they
+        # can at least build without errors.
+        ninja c_emulator_rv32d c_emulator_rv64d c_emulator_rv32d_rvfi generated_smt_rv64f


IMO we should just build ninja all since that is what most people will be using.
If we add EXCLUDE_FROM_ALL to certain targets in CMake we can change that to be a sensible subset.

I see EXCLUDE_FROM_ALL is already handled - I'd suggest using ninja + ninja <additional targets>

Also no need to cd here, use cmake -B and ninja -C.

@arichardson I didn't use ninja all (or just ninja which is the same) because it only builds rv32d and rv64d. If we do ninja && ninja <other targets> then they won't run in parallel optimally. I can do ninja all <other targets> though; I think that makes the most sense.

@jrtc27 I had a go but I can't see how to get ctest to run without cd - you can do ninja -C build test but then you can't pass the junit argument.

ctest --test-dir?

Yeah I tried that, and a couple of other ....dir options. Didn't work I'm afraid.

arichardson · 2025-01-17T17:32:50Z

CMakeLists.txt

+# TODO: Add isabelle target.
+# TODO: Add lem target.
+# TODO: Add hol4 target.
+# TODO: Add latex target.


Not sure we still care about the latex output now that all the docs are asciidoc?

I assume ISAv10 will still need them to embed our own research extensions, and possibly the standard part too? Not sure if we've thought through how exactly ISAv10 will look in this world though.

Yeah but that target would exist in sail-cheri-riscv and not here? Although maybe by ISAv10 it would just be a fork of this repo?

I don't know what the expectation is for integrating these build system bits into sail-cheri-riscv. Maybe we don't bother because the Makefile works just fine for us...

Yeah very good question. We should probably discuss it on Thursday. I'll remove the todo here anyway.

build_simulators.sh

c_emulator/CMakeLists.txt

arichardson · 2025-01-17T17:54:16Z

sail_runtime/CMakeLists.txt

+if (COVERAGE)
+    find_package(Threads REQUIRED)
+
+    # Note, you must run `make` in the ${sail_dir}/lib/coverage


Probably worth improving this in the future (e.g. building it automatically if not present), but not for this PR.

Yes, definitely! See rems-project/sail#893

c_emulator/CMakeLists.txt

.github/workflows/compile.yml

jrtc27 · 2025-01-20T16:34:58Z

CMakeLists.txt

+# Don't use `REQUIRED` so that we can print custom help messages.
+find_package(ZLIB)
+if (NOT ZLIB_FOUND)
+    message(FATAL_ERROR "Zlib not found. Try 'sudo apt install zlib1g-dev' or 'sudo dnf install zlib-devel'.")


I'd bet that an inexperienced user on macOS will turn up, hit one of these messages and try to run the commands given, then complain that it doesn't work...

Fair point, and actually we can easily customise the message for the OS - I'll do that.

This is done - I added brew messages for mac, and don't suggest anything for windows.

CMakeLists.txt

jrtc27 · 2025-01-20T16:41:56Z

.github/workflows/compile.yml

+        cd build
+        # Ninja is used because the CMake Makefile generator doesn't
+        # build top-level targets in parallel unfortunately.
+        cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..


RelWithDebInfo is the correct choice for most use cases, not Release. But I also wonder if we should have the default be that, rather than Debug. Otherwise I fear people will just do cmake && make, end up with Debug builds and get the impression the model is slow when it's not (or at least not that slow), it's just user error.

Hmm yeah. That is quite a problem in the Rust community too actually - people think it's slow because they did cargo build rather than cargo build --release.

I'm not sure we can change the default though with CMake? It's the default in build_simulators.sh at least though. (I'll change both to RelWithDebInfo).

if(NOT CMAKE_BUILD_TYPE) set(CMAKE_BUILD_TYPE RelWithDebInfo) endif()

?

Hmm yeah that makes me a bit nervous - CMake's build type is... weird in a few ways - there are multi-config build systems (MSVC and optionally Ninja) where it doesn't select a build type until build time (normally it's configure time) so you also need to check CMAKE_CONFIGURATION_TYPES.

I found this code which probably works, but even there one of the comments suggests that the default empty-string build type was intended for distros that build everything from source and set custom flags (tbf I'm not sure we really care about that).

Anyway, do you mind if we defer this to a future PR? It might never be an issue if people don't make that mistake...

I mean, you've seen the kinds of questions that some people post on this repo...

Can we at least do what LLVM does and require you to explicitly set the build type?

https://github.com/llvm/llvm-project/blob/e6c9cd9c060c1fa8343398b9556a5a6c0f35d515/llvm/CMakeLists.txt#L89-L99

Good idea, I've copied that. It looks like this:

❯ cmake .. CMake Error at CMakeLists.txt:6 (message): No build type selected. You need to pass -DCMAKE_BUILD_TYPE=<type> in order to configure the build. * -DCMAKE_BUILD_TYPE=Release - Optimized build with no debug info. * -DCMAKE_BUILD_TYPE=RelWithDebInfo - Optimized build with debug info. * -DCMAKE_BUILD_TYPE=Debug - Unoptimized build with debug info. * -DCMAKE_BUILD_TYPE=MinSizeRel - Optimized for size instead of speed. -- Configuring incomplete, errors occurred!

Timmmm · 2025-01-20T21:22:34Z

Update:

Per-OS error messages when GMP and Zlib aren't found.
Update README
Rename Makefile to Makefile.old to make it obvious at a glance that you shouldn't use the Makefile.

I think this is basically ready at this point. Probably any more improvements could be done in future PRs (and I'm starting to lose track of all the threads!)

jordancarlin · 2025-01-20T21:32:42Z

The Makefile is still pointing at the old location for softfloat. I know we want to encourage everyone to use the new CMake flow, but if we are going to keep the old Makefile around I think we should make sure it is still functional. Or remove the c emulator targets from it and only leave the formal backends.

Timmmm · 2025-01-20T22:14:36Z

Good point, I'll fix that. Also I think I forgot to do the RelWithDebInfo change - I'll do that in the morning.

jordancarlin · 2025-01-20T22:19:48Z

My other concern is changing the name of the generated executable itself. Currently it's riscv_sim_ARCH, which makes it clear what it is if copied to a bin directory. The switch to c_emulator_ARCH removes this easy recognition and doesn't seem to provide much benefit. If we want to explicitly call out that it is the c emulator (as opposed to the SystemVerilog one) maybe something like riscv_csim_ARCH would be better.

Makefile.old

Move the softfloat library to a dependencies directory. In future we can add GMP there too to reduce the number of external dependencies needed and to support static linking. The directory was renamed from `SoftFloat-3e` to `berkeley-softfloat-3` because that's how the latest version is named. It hasn't been upgraded in this commit to make it simpler to review and help Git track history. A future commit will upgrade it.

Switch from Makefiles to CMake. Some formal outputs are not yet fully supported by the CMake so the old Makefile is retained. This also adds a manual Github actions workflow to generate the JSON doc bundle, to allow inclusion of Sail snippets in the ISA manual.

Timmmm · 2025-01-27T10:13:12Z

I rebased it, updated it for the Coq output (which now builds with the latest sail2 compiler, but it doesn't do everything the Makefile does), and also added a Github actions workflow to generate the JSON docs.

My aim for the latter is to run it manually and make a Github Release with it attached, so we can start including Sail snippets in the ISA manual (as we do for CHERI).

Timmmm mentioned this pull request Dec 18, 2024

Switch to CMake #551

Open