-
Notifications
You must be signed in to change notification settings - Fork 178
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information
Showing
19 changed files
with
808 additions
and
329 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 test results | ||
| if: always() | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: riscv_model_rv64d.json | ||
| path: build/model/riscv_model_rv64d.json |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
|
|
||
|
|
@@ -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) | ||
|
|
||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,14 +1,8 @@ | ||
| #!/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 | ||
| mkdir -p build | ||
| cd build | ||
| cmake .. -DCMAKE_BUILD_TYPE=RelWithDebInfo | ||
| make -j2 csim |
Oops, something went wrong.