Implement CMake build system

.github/workflows/compile.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
     - name: Install packages
-      run: sudo apt install -y --no-install-recommends zlib1g-dev pkg-config libgmp-dev curl
+      run: sudo apt install -y --no-install-recommends zlib1g-dev pkg-config libgmp-dev curl ninja-build
     - name: Check out repository code
       uses: actions/checkout@HEAD
       with:
@@ -19,13 +19,23 @@ jobs:
         sudo mkdir -p /usr/local
         curl --location https://github.com/rems-project/sail/releases/download/0.18-linux-binary/sail.tar.gz | sudo tar xvz --directory=/usr/local --strip-components=1
     - name: Build and test simulators
-      run: test/run_tests.sh
+      run: |
+        # Ninja is used because the CMake Makefile generator doesn't
+        # build top-level targets in parallel unfortunately.
+        cmake -S . -B build -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo
+        # 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 build all riscv_sim_rv32d_rvfi generated_smt_rv64f generated_docs_rv64d
+        # These targets do not work with Sail 0.18: generated_rmem_rv32d_rmem generated_coq_rv64f_coq
+        ctest --test-dir build --output-junit tests.xml
     - name: Upload test results
       if: always()
       uses: actions/upload-artifact@v4
       with:
         name: tests.xml
-        path: test/tests.xml
+        path: build/tests.xml
+        if-no-files-found: error
     - name: Upload event payload
       if: always()
       uses: actions/upload-artifact@v4

.github/workflows/generate-json.yml

@@ -0,0 +1,30 @@
+name: Generate Doc JSON
+
+on: [workflow_dispatch]
+
+jobs:
+  build:
+    runs-on: ubuntu-22.04
+    steps:
+    - name: Install packages
+      run: sudo apt install -y --no-install-recommends zlib1g-dev pkg-config libgmp-dev curl ninja-build
+    - name: Check out repository code
+      uses: actions/checkout@HEAD
+      with:
+        submodules: true
+    - name: Install sail from binary
+      run: |
+        sudo mkdir -p /usr/local
+        curl --location https://github.com/rems-project/sail/releases/download/0.18-linux-binary/sail.tar.gz | sudo tar xvz --directory=/usr/local --strip-components=1
+    - name: Build JSON doc bundle
+      run: |
+        mkdir build
+        cd build
+        cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..
+        ninja generated_docs_rv64d
+    - name: Upload JSON doc bundle
+      uses: actions/upload-artifact@v4
+      with:
+        name: riscv_model_rv64d.json
+        path: build/model/riscv_model_rv64d.json
+        if-no-files-found: error

.gitignore

@@ -6,4 +6,9 @@ _build/
 _sbuild/
 *.o
 *.a
-/z3_problems
+z3_problems
+
+# Typical CMake build directory.
+/build
+# CMake build directories used by CLion.
+/cmake-build-*

.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/[^/]+/)'
 minimum_pre_commit_version: 2.10.0
 repos:
 -   repo: https://github.com/pre-commit/pre-commit-hooks

CMakeLists.txt

@@ -0,0 +1,95 @@
+cmake_minimum_required(VERSION 3.20)
+
+project(sail_riscv)
+
+# Make users explicitly pick a build type so they don't get
+# surprised when the default gives a very slow emulator.
+if (NOT CMAKE_BUILD_TYPE AND NOT CMAKE_CONFIGURATION_TYPES)
+    message(FATAL_ERROR "
+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.")
+endif()
+
+# Enable CTest
+enable_testing()
+
+# Export compile_commands.json for IDE support.
+set(CMAKE_EXPORT_COMPILE_COMMANDS TRUE)
+
+# Always use Position Independent Code. By default it is only used for
+# shared libraries (which require it), but you also need it for static
+# libraries if you link them into shared libraries.
+# Generally it just simplifies everything for a negligable performance cost.
+set(CMAKE_POSITION_INDEPENDENT_CODE TRUE)
+
+# Don't allow undefined symbols. This is generally a pain.
+include(CheckLinkerFlag)
+
+check_linker_flag(C "-Wl,--no-undefined" LINKER_SUPPORTS_NO_UNDEFINED)
+if (LINKER_SUPPORTS_NO_UNDEFINED)
+    add_link_options("-Wl,--no-undefined")
+endif()
+
+# Extra CMake files.
+set(CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake/modules")
+
+# These are the main requirements.
+# Don't use `REQUIRED` so that we can print custom help messages.
+find_package(ZLIB)
+if (NOT ZLIB_FOUND)
+    if (APPLE)
+        message(FATAL_ERROR "Zlib not found. Try 'brew install zlib'.")
+    elseif (UNIX)
+        message(FATAL_ERROR "Zlib not found. Try 'sudo apt install zlib1g-dev' or 'sudo dnf install zlib-devel'.")
+    else()
+        message(FATAL_ERROR "Zlib not found.")
+    endif()
+endif()
+
+find_package(GMP)
+if (NOT GMP_FOUND)
+    if (APPLE)
+        message(FATAL_ERROR "GMP not found. Try 'brew install gmp'.")
+    elseif (UNIX)
+        message(FATAL_ERROR "GMP not found. Try 'sudo apt install libgmp-dev' or 'sudo dnf install gmp-devel'.")
+    else()
+        message(FATAL_ERROR "GMP not found.")
+    endif()
+endif()
+
+find_program(SAIL_BIN "sail")
+if (NOT SAIL_BIN)
+    message(FATAL_ERROR "Sail not found. See README.md for installation instructions.")
+endif()
+
+set(DEFAULT_ARCHITECTURES "rv32d;rv64d" CACHE STRING "Architectures to build by default (rv32f|rv64f|rv32d|rv64d)(_rvfi)? " )
+
+option(COVERAGE "Compile with Sail coverage collection enabled.")
+
+# Softfloat support.
+add_subdirectory("dependencies/softfloat")
+
+# Sail C runtime.
+add_subdirectory("sail_runtime")
+
+# Sail model generated C code.
+add_subdirectory("model")
+
+# Emulator binary.
+add_subdirectory("c_emulator")
+
+# Old pre-compiled riscv-tests.
+add_subdirectory("test/riscv-tests")
+
+# Convenience targets.
+add_custom_target(csim DEPENDS riscv_sim_rv32d riscv_sim_rv64d)
+add_custom_target(check DEPENDS generated_model_rv32d generated_model_rv64d)
+
+# TODO: Support static linking.
+# TODO: Add `interpret` target.
+# TODO: Add isabelle target.
+# TODO: Add lem target.
+# TODO: Add hol4 target.

Makefile → Makefile.old

@@ -1,3 +1,9 @@
+# WARNING! This Makefile is deprecated and has been *mostly* replaced by CMake.
+# There are some targets related to formal backends (Coq, Hol4, etc.) that have
+# not been fully transitioned, so this is kept for posterity.
+#
+# To build the emulators you can use the usual CMake flow, or `./build_simulators.sh`.
+
 # Select architecture: RV32 or RV64.
 ARCH ?= RV64
 
@@ -148,7 +154,7 @@ C_WARNINGS ?=
 C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h)
 C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c)
 
-SOFTFLOAT_DIR    = c_emulator/SoftFloat-3e
+SOFTFLOAT_DIR    = dependencies/softfloat/berkeley-softfloat-3
 SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include
 SOFTFLOAT_LIBDIR = $(SOFTFLOAT_DIR)/build/Linux-RISCV-GCC
 SOFTFLOAT_FLAGS  = -I $(SOFTFLOAT_INCDIR)
@@ -220,7 +226,7 @@ all: c_emulator/riscv_sim_$(ARCH)
 # break future builds if sail exits badly
 .DELETE_ON_ERROR: generated_definitions/c/%.c
 
-check: $(SAIL_SRCS) model/main.sail Makefile
+check: $(SAIL_SRCS) model/main.sail Makefile.old
 	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
 interpret: $(SAIL_SRCS) model/main.sail
@@ -230,15 +236,15 @@ sail_doc/riscv_$(ARCH).json: $(SAIL_SRCS) model/main.sail
 	$(SAIL) -doc -doc_bundle riscv_$(ARCH).json -o sail_doc $(SAIL_FLAGS) $(SAIL_DOC_FLAGS) $(SAIL_SRCS) model/main.sail
 
 riscv.smt_model: $(SAIL_SRCS)
-	$(SAIL) -smt_serialize $(SAIL_FLAGS) $(SAIL_SRCS) -o riscv
+	$(SAIL) -smt $(SAIL_FLAGS) $(SAIL_SRCS) -o riscv
 
 cloc:
 	cloc --by-file --force-lang C,sail $(SAIL_SRCS)
 
 gcovr:
 	gcovr -r . --html --html-detail -o index.html
 
-generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
+generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile.old
 	mkdir -p generated_definitions/c
 	$(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
 
@@ -251,7 +257,7 @@ csim: c_emulator/riscv_sim_$(ARCH)
 .PHONY: rvfi
 rvfi: c_emulator/riscv_rvfi_$(ARCH)
 
-c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
+c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile.old
 	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS_WRAPPED) -o $@
 
 # Note: We have to add -c_preserve since the functions might be optimized out otherwise
@@ -270,16 +276,16 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
   -c_preserve print_rvfi_exec
 
 # sed -i isn't posix compliant, unfortunately
-generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
+generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile.old
 	mkdir -p generated_definitions/c
 	$(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
 	sed -e '/^[[:space:]]*$$/d' $@ > [email protected]
 	mv [email protected] $@
 
-c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
+c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile.old
 	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS_WRAPPED) -o $@
 
-latex: $(SAIL_SRCS) Makefile
+latex: $(SAIL_SRCS) Makefile.old
 	mkdir -p generated_definitions/latex
 	$(SAIL) -latex -latex_prefix sail -o generated_definitions/latex $(SAIL_SRCS)
 
@@ -299,13 +305,13 @@ endif
 
 .PHONY: riscv_isa riscv_isa_build
 
-generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile
+generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile.old
 	mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
 	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
 	echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem
 
 # sed -i isn't posix compliant, unfortunately
-generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile
+generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile.old
 	lem -wl ign -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
 		$(RISCV_EXTRAS_LEM) \
 		generated_definitions/lem/$(ARCH)/riscv_types.lem \
@@ -348,7 +354,7 @@ riscv_coq: $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v)
 riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo
 .PHONY: riscv_coq riscv_coq_build
 
-$(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile
+$(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile.old
 	mkdir -p generated_definitions/coq/$(ARCH)
 	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras -coq_lib mem_metadata $(SAIL_COQ_SRCS)
 

README.md

@@ -47,53 +47,38 @@ Getting started
 Install [Sail](https://github.com/rems-project/sail/). On Linux you can download a [binary release](https://github.com/rems-project/sail/releases) (strongly recommended), or you can install from source [using opam](https://github.com/rems-project/sail/blob/sail2/INSTALL.md). Then:
 
 ```
-$ make
+$ ./build_simulators.sh
 ```
 
-will build the simulator in `c_emulator/riscv_sim_RV64`.
+will build the simulators in `build/c_emulator/riscv_sim_rv{32,64}d`.
 
 If you get an error message saying `sail: unknown option '--require-version'.` it's because your Sail compiler is too old. You need version 0.18 or later.
 
-One can build either the RV32 or the RV64 model by specifying
-`ARCH=RV32` or `ARCH=RV64` on the `make` line, and using the matching
-target suffix.  RV64 is built by default, but the RV32 model can be
-built using:
+By default the RV32D and RV64D emulators are built, without RVFI-DII support.
+You can see a complete list of targets by running `make help` in the
+build directory, then e.g.
 
 ```
-$ ARCH=RV32 make
+$ make -C build riscv_sim_rv64f_rvfi
 ```
 
-which creates the simulator in `c_emulator/riscv_sim_RV32`.
-
-The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and
-`riscv_hol_build` invoke the respective prover to process the
-definitions and produce the Isabelle model in
-`generated_definitions/isabelle/RV64/Riscv.thy`, the Coq model in
-`generated_definitions/coq/RV64/riscv.v`, or the HOL4 model in
-`generated_definitions/hol4/RV64/riscvScript.sml` respectively.
-We have tested Isabelle 2018, Coq 8.8.1, and HOL4
-Kananaskis-12.  When building these targets, please make sure the
-corresponding prover libraries in the Sail directory
-(`$SAIL_DIR/lib/$prover`) are up-to-date and built, e.g. by running
-`make` in those directories.
-
 ### Executing test binaries
 
 The simulator can be used to execute small test binaries.
 
 ```
-$ ./c_emulator/riscv_sim_<arch> <elf-file>
+$ build/c_emulator/riscv_sim_<arch> <elf-file>
 ```
 
 A suite of RV32 and RV64 test programs derived from the
 [`riscv-tests`](https://github.com/riscv/riscv-tests) test-suite is
 included under [test/riscv-tests/](test/riscv-tests/).  The test-suite
-can be run using `test/run_tests.sh`.
+can be run using `make test` or `ctest` in the build directory.
 
 ### Configuring platform options
 
 Information on configuration options for the simulator is available from
-`./c_emulator/riscv_sim_<arch> -h`.
+`build/c_emulator/riscv_sim_<arch> -h`.
 
 Some useful options are: configuring whether misaligned accesses trap
 (`--enable-misaligned`), and
@@ -104,10 +89,6 @@ whether page-table walks update PTE bits (`--enable-dirty-update`).
 For booting operating system images, see the information under the
 [os-boot/](os-boot/) subdirectory.
 
-### Using development versions of Sail
-
-Rarely, the release version of Sail may not meet your needs. This could happen if you need a bug fix or new feature not yet in the released Sail version, or you are actively working on Sail. In this case you can tell the `sail-riscv` `Makefile` to use a local copy of Sail by setting `SAIL_DIR` to the root of a checkout of the Sail repo when you invoke `make`. Alternatively, you can use `opam pin` to install Sail from a local checkout of the Sail repo as described in the Sail installation instructions.
-
 Supported RISC-V ISA features
 -----------------------------
 #### The Sail specification currently captures the following ISA extensions and features:
@@ -330,13 +311,6 @@ Directory Structure
 ```
 sail-riscv
 - model                   // Sail specification modules
-- generated_definitions   // files generated by Sail, in RV32 and RV64 subdirectories
-  -  c
-  -  lem
-  -  isabelle
-  -  coq
-  -  hol4
-  -  latex
 - prover_snapshots        // snapshots of generated theorem prover definitions
 - handwritten_support     // prover support files
 - c_emulator              // supporting platform files for C emulator

build_simulators.sh

@@ -1,14 +1,6 @@
 #!/bin/bash
 
-function test_build () {
-    declare -i rc=0
-    eval $*
-    rc=$?
-    if [ $rc -ne 0 ]; then
-        echo "Failure to execute: $*"
-        exit $rc
-    fi
-}
+set -e
 
-test_build make ARCH=RV32 c_emulator/riscv_sim_RV32
-test_build make ARCH=RV64 c_emulator/riscv_sim_RV64
+cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo
+cmake --build build -j2