diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml index f83adb82e..0905bdae2 100644 --- a/.github/workflows/compile.yml +++ b/.github/workflows/compile.yml @@ -65,11 +65,7 @@ jobs: # 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 -DFIRST_PARTY_TESTS=TRUE - # By default only the rv32d and rv64d emulators are built, - # but we want to build more targets here to ensure they - # can at least build without errors. - ninja -C build all riscv_sim_rv32f riscv_sim_rv64f generated_smt_rv64f generated_docs_rv64d - # These targets do not work with Sail 0.18: generated_rmem_rv32d_rmem generated_coq_rv64f_coq + ninja -C build all generated_sail_riscv_docs generated_smt_rv64d generated_smt_rv32d ctest --test-dir build --output-junit tests.xml --output-on-failure - name: Upload test results diff --git a/CMakeLists.txt b/CMakeLists.txt index 234db045f..875aba775 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -136,8 +136,6 @@ execute_process( ) message(STATUS "Sail library directory: ${sail_dir}") -set(DEFAULT_ARCHITECTURES "rv32d;rv64d" CACHE STRING "Architectures to build by default (rv32f|rv64f|rv32d|rv64d)? " ) - option(COVERAGE "Compile with Sail coverage collection enabled.") # Softfloat support. @@ -178,8 +176,8 @@ endif() include(CPack) # Convenience targets. -add_custom_target(csim DEPENDS riscv_sim_rv32d riscv_sim_rv64d) -add_custom_target(check DEPENDS generated_model_rv32d generated_model_rv64d) +add_custom_target(csim DEPENDS sail_riscv_sim) +add_custom_target(check DEPENDS generated_model_rv) # TODO: Add `interpret` target. # TODO: Add hol4 target. diff --git a/Makefile.old b/Makefile.old index c779d654f..e7b3422d0 100644 --- a/Makefile.old +++ b/Makefile.old @@ -139,7 +139,7 @@ SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS) $(SAIL_OTHER_COQ_SRCS)) SAIL_FLAGS += --require-version 0.19.1 -SAIL_FLAGS += --config config/default.json +SAIL_FLAGS += --config config/rv64d.json SAIL_FLAGS += --strict-var SAIL_FLAGS += -dno_cast SAIL_DOC_FLAGS ?= -doc_embed plain @@ -301,7 +301,7 @@ endif generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile.old mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) - $(SAIL) $(SAIL_FLAGS) --config config/default.json -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 $(SAIL_SRCS) + $(SAIL) $(SAIL_FLAGS) --config config/rv64d.json -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 $(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 diff --git a/README.md b/README.md index e9e581df9..9785dee2e 100644 --- a/README.md +++ b/README.md @@ -29,19 +29,10 @@ Install [Sail](https://github.com/rems-project/sail/). On Linux you can download $ ./build_simulators.sh ``` -will build the simulators in `build/c_emulator/riscv_sim_rv{32,64}d`. +will build the simulator at `build/c_emulator/sail_riscv_sim`. 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.19.1 or later. -By default the RV32D and RV64D emulators are built. -You can see a complete list of targets by running `make help` in the -build directory, then e.g. - -``` -$ cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo -DDOWNLOAD_GMP=TRUE -$ make -C build riscv_sim_rv64f -``` - By default `build_simulators.sh` will download and build [libgmp](https://gmplib.org/). To use a system installation of libgmp, run `env DOWNLOAD_GMP=FALSE ./build_simulators.sh` instead. @@ -50,7 +41,7 @@ To use a system installation of libgmp, run `env DOWNLOAD_GMP=FALSE ./build_simu The simulator can be used to execute small test binaries. ``` -$ build/c_emulator/riscv_sim_ +$ build/c_emulator/sail_riscv_sim ``` A suite of RV32 and RV64 test programs derived from the @@ -62,13 +53,13 @@ can be run using `make test` or `ctest` in the build directory. The model is configured using a JSON file specifying various tunable options. The default configuration used for the model can be examined -using `build/c_emulator/riscv_sim_ --print-default-config`. To +using `build/c_emulator/sail_riscv_sim --print-default-config`. To use a custom configuration, save the default configuration into a file, edit it as needed, and pass it to the simulator using the `--config` option. Information on other options for the simulator is available from -`build/c_emulator/riscv_sim_ -h`. +`build/c_emulator/sail_riscv_sim -h`. ### Booting OS images diff --git a/c_emulator/CMakeLists.txt b/c_emulator/CMakeLists.txt index 6db81bbb4..f3c072dab 100644 --- a/c_emulator/CMakeLists.txt +++ b/c_emulator/CMakeLists.txt @@ -18,73 +18,59 @@ set(EMULATOR_COMMON_SRCS config_utils.cpp ) -foreach (xlen IN ITEMS 32 64) - foreach (flen IN ITEMS 32 64) - set(arch "rv${xlen}") - if (flen EQUAL 32) - string(APPEND arch "f") - else() - string(APPEND arch "d") - endif() - - add_executable(riscv_sim_${arch} - "${CMAKE_BINARY_DIR}/riscv_model_${arch}.c" - "${CMAKE_BINARY_DIR}/riscv_model_${arch}.h" - ${EMULATOR_COMMON_SRCS} - ) - # The generated model is not warnings-clean, silence them. - set(_generated_c_warning_opt_out - -Wno-extra - -Wno-unused - -Wno-uninitialized - ) - set_source_files_properties("${CMAKE_BINARY_DIR}/riscv_model_${arch}.c" - PROPERTIES COMPILE_OPTIONS "${_generated_c_warning_opt_out}") - - if (NOT arch IN_LIST DEFAULT_ARCHITECTURES) - set_target_properties(riscv_sim_${arch} PROPERTIES EXCLUDE_FROM_ALL TRUE) - endif() +add_executable(sail_riscv_sim + "${CMAKE_BINARY_DIR}/sail_riscv_model.c" + "${CMAKE_BINARY_DIR}/sail_riscv_model.h" + ${EMULATOR_COMMON_SRCS} +) - add_dependencies(riscv_sim_${arch} generated_model_${arch}) +# The generated model is not warnings-clean, silence them. +# -Wno-self-assing is needed for `zhtif_tohost = zhtif_tohost` +# generated by the sail code to avoid optimizing the function out. +set(_generated_c_warning_opt_out + -Wno-extra + -Wno-unused + -Wno-uninitialized + $<$:-Wno-self-assign> +) +set_source_files_properties( + "${CMAKE_BINARY_DIR}/sail_riscv_model.c" + "${CMAKE_BINARY_DIR}/sail_riscv_model.h" + PROPERTIES COMPILE_OPTIONS "${_generated_c_warning_opt_out}" +) - target_link_libraries(riscv_sim_${arch} - PRIVATE softfloat sail_runtime default_config - ) +add_dependencies(sail_riscv_sim generated_sail_riscv_model) - target_include_directories(riscv_sim_${arch} - # So the generated C can find riscv_platform/prelude.h" - PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}" - # So we can find riscv_model_${arch}.h - "${CMAKE_BINARY_DIR}" - ) +target_link_libraries(sail_riscv_sim + PRIVATE softfloat sail_runtime default_config +) - # This is necessary so it can pick the right riscv_model_${arch}.h - # to #include. We can remove it when there is a single model with - # runtime xlen and flen. - target_compile_definitions(riscv_sim_${arch} - PRIVATE "RISCV_MODEL_HEADER=" - ) +target_include_directories(sail_riscv_sim + PRIVATE + # So the generated C can find riscv_platform/prelude.h" + "${CMAKE_CURRENT_SOURCE_DIR}" + # So `riscv_sail.h` can find `sail_riscv_model.h`. + "${CMAKE_BINARY_DIR}" +) - # Enable Sail coverage collection. - if (COVERAGE) - target_compile_definitions(riscv_sim_${arch} - PRIVATE "SAILCOV" - ) - endif() +# TODO: Enable warnings when we use the #include trick +# to include the generated Sail code. Currently it +# generates too many warnings to turn these on globally. - # TODO: Enable warnings when we use the #include trick - # to include the generated Sail code. Currently it - # generates too many warnings to turn these on globally. +# target_compile_options(sail_riscv_sim PRIVATE +# -Wall -Wextra +# # Too annoying at the moment. +# -Wno-unused-parameter +# ) - # target_compile_options(riscv_sim_${arch} PRIVATE - # -Wall -Wextra - # # Too annoying at the moment. - # -Wno-unused-parameter - # ) +# Enable Sail coverage collection. +if (COVERAGE) + target_compile_definitions(sail_riscv_sim + PRIVATE "SAILCOV" + ) +endif() - install(TARGETS riscv_sim_${arch} - OPTIONAL - RUNTIME DESTINATION "bin" - ) - endforeach() -endforeach() +install(TARGETS sail_riscv_sim + OPTIONAL + RUNTIME DESTINATION "bin" +) diff --git a/c_emulator/riscv_callbacks.cpp b/c_emulator/riscv_callbacks.cpp index 715aa7f42..4c0395bf9 100644 --- a/c_emulator/riscv_callbacks.cpp +++ b/c_emulator/riscv_callbacks.cpp @@ -21,12 +21,12 @@ void print_lbits_hex(lbits val, int length = 0) // Implementations of default callbacks for trace printing and RVFI. // The model assumes that these functions do not change the state of the model. -unit mem_write_callback(const char *type, uint64_t paddr, uint64_t width, +unit mem_write_callback(const char *type, sbits paddr, uint64_t width, lbits value) { if (config_print_mem_access) { fprintf(trace_log, "mem[%s,0x%0*" PRIX64 "] <- 0x", type, - static_cast((zphysaddrbits_len + 3) / 4), paddr); + static_cast((zphysaddrbits_len + 3) / 4), paddr.bits); print_lbits_hex(value, width); } if (config_enable_rvfi) { @@ -35,12 +35,12 @@ unit mem_write_callback(const char *type, uint64_t paddr, uint64_t width, return UNIT; } -unit mem_read_callback(const char *type, uint64_t paddr, uint64_t width, +unit mem_read_callback(const char *type, sbits paddr, uint64_t width, lbits value) { if (config_print_mem_access) { fprintf(trace_log, "mem[%s,0x%0*" PRIX64 "] -> 0x", type, - static_cast((zphysaddrbits_len + 3) / 4), paddr); + static_cast((zphysaddrbits_len + 3) / 4), paddr.bits); print_lbits_hex(value, width); } if (config_enable_rvfi) { @@ -53,7 +53,7 @@ unit mem_read_callback(const char *type, uint64_t paddr, uint64_t width, return UNIT; } -unit mem_exception_callback(uint64_t paddr, uint64_t num_of_exception) +unit mem_exception_callback(sbits paddr, uint64_t num_of_exception) { (void)num_of_exception; if (config_enable_rvfi) { @@ -63,15 +63,15 @@ unit mem_exception_callback(uint64_t paddr, uint64_t num_of_exception) } unit xreg_full_write_callback(const_sail_string abi_name, unsigned reg, - uint64_t value) + sbits value) { if (config_print_reg) { if (config_use_abi_names) { fprintf(trace_log, "%s <- 0x%0*" PRIX64 "\n", abi_name, - static_cast(zxlen / 4), value); + static_cast(zxlen / 4), value.bits); } else { fprintf(trace_log, "x%d <- 0x%0*" PRIX64 "\n", reg, - static_cast(zxlen / 4), value); + static_cast(zxlen / 4), value.bits); } } if (config_enable_rvfi) { @@ -80,34 +80,34 @@ unit xreg_full_write_callback(const_sail_string abi_name, unsigned reg, return UNIT; } -unit freg_write_callback(unsigned reg, uint64_t value) +unit freg_write_callback(unsigned reg, sbits value) { // TODO: will only print bits; should we print in floating point format? if (config_print_reg) { // TODO: Might need to change from PRIX64 to PRIX128 once the "Q" extension // is supported fprintf(trace_log, "f%d <- 0x%0*" PRIX64 "\n", reg, - static_cast(zflen / 4), value); + static_cast(zflen / 4), value.bits); } return UNIT; } unit csr_full_write_callback(const_sail_string csr_name, unsigned reg, - uint64_t value) + sbits value) { if (config_print_reg) { fprintf(trace_log, "CSR %s (0x%03X) <- 0x%016" PRIX64 "\n", csr_name, reg, - value); + value.bits); } return UNIT; } unit csr_full_read_callback(const_sail_string csr_name, unsigned reg, - uint64_t value) + sbits value) { if (config_print_reg) { fprintf(trace_log, "CSR %s (0x%03X) -> 0x%016" PRIX64 "\n", csr_name, reg, - value); + value.bits); } return UNIT; } @@ -124,7 +124,7 @@ unit vreg_write_callback(unsigned reg, lbits value) return UNIT; } -unit pc_write_callback(uint64_t value) +unit pc_write_callback(sbits value) { (void)value; return UNIT; diff --git a/c_emulator/riscv_callbacks.h b/c_emulator/riscv_callbacks.h index ac5fd9773..703c0a65c 100644 --- a/c_emulator/riscv_callbacks.h +++ b/c_emulator/riscv_callbacks.h @@ -5,30 +5,30 @@ extern "C" { #endif -unit mem_write_callback(const char *type, uint64_t paddr, uint64_t width, +unit mem_write_callback(const char *type, sbits paddr, uint64_t width, lbits value); -unit mem_read_callback(const char *type, uint64_t paddr, uint64_t width, +unit mem_read_callback(const char *type, sbits paddr, uint64_t width, lbits value); -unit mem_exception_callback(uint64_t paddr, uint64_t num_of_exception); +unit mem_exception_callback(sbits paddr, uint64_t num_of_exception); unit xreg_full_write_callback(const_sail_string abi_name, unsigned reg, - uint64_t value); -unit freg_write_callback(unsigned reg, uint64_t value); + sbits value); +unit freg_write_callback(unsigned reg, sbits value); // `full` indicates that the name and index of the CSR are provided. // 64 bit CSRs use a long_csr_write_callback Sail function that automatically // makes two csr_full_write_callback calls on RV32. unit csr_full_write_callback(const_sail_string csr_name, unsigned reg, - uint64_t value); + sbits value); unit csr_full_read_callback(const_sail_string csr_name, unsigned reg, - uint64_t value); + sbits value); unit vreg_write_callback(unsigned reg, lbits value); -unit pc_write_callback(uint64_t value); +unit pc_write_callback(sbits value); unit trap_callback(unit); // TODO: Move these implementations to C. -unit zrvfi_write(uint64_t paddr, int64_t width, lbits value); -unit zrvfi_read(uint64_t paddr, sail_int width, lbits value); -unit zrvfi_mem_exception(uint64_t paddr); -unit zrvfi_wX(int64_t reg, uint64_t value); +unit zrvfi_write(sbits paddr, int64_t width, lbits value); +unit zrvfi_read(sbits paddr, sail_int width, lbits value); +unit zrvfi_mem_exception(sbits paddr); +unit zrvfi_wX(int64_t reg, sbits value); unit zrvfi_trap(unit); #ifdef __cplusplus diff --git a/c_emulator/riscv_platform.cpp b/c_emulator/riscv_platform.cpp index eaec88de2..b64098e62 100644 --- a/c_emulator/riscv_platform.cpp +++ b/c_emulator/riscv_platform.cpp @@ -29,9 +29,9 @@ mach_bits plat_get_16_random_bits(unit) // either directly in `load_reservation()` or by callling // `cancel_reservation()`. -unit load_reservation(mach_bits addr) +unit load_reservation(sbits addr) { - reservation = addr; + reservation = addr.bits; reservation_valid = true; RESERVATION_DBG("reservation <- %0" PRIx64 "\n", reservation); return UNIT; @@ -42,10 +42,10 @@ static mach_bits check_mask() return (zxlen == 32) ? 0x00000000FFFFFFFF : -1; } -bool match_reservation(mach_bits addr) +bool match_reservation(sbits addr) { mach_bits mask = check_mask(); - bool ret = reservation_valid && (reservation & mask) == (addr & mask); + bool ret = reservation_valid && (reservation & mask) == (addr.bits & mask); RESERVATION_DBG("reservation(%c): %0" PRIx64 ", key=%0" PRIx64 ": %s\n", reservation_valid ? 'v' : 'i', reservation, addr, ret ? "ok" : "fail"); diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 42252b348..12ee84ea4 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -8,8 +8,8 @@ extern "C" { // Provides entropy for the scalar cryptography extension. mach_bits plat_get_16_random_bits(unit); -unit load_reservation(mach_bits); -bool match_reservation(mach_bits); +unit load_reservation(sbits); +bool match_reservation(sbits); unit cancel_reservation(unit); bool valid_reservation(unit); diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index bdb43bc41..f50949d8f 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -1,7 +1,7 @@ #pragma once // The header generated by Sail. -#include RISCV_MODEL_HEADER +#include "sail_riscv_model.h" #ifdef __cplusplus extern "C" { @@ -13,10 +13,10 @@ void model_fini(void); // The generated header does not include these variables. // TODO: We should avoid accessing variables directly. -extern mach_bits zxlen; -extern mach_bits zflen; -extern mach_bits zphysaddrbits_len; -extern mach_bits zVLEN; +extern uint64_t zxlen; +extern uint64_t zflen; +extern uint64_t zphysaddrbits_len; +extern uint64_t zVLEN; #ifdef __cplusplus } diff --git a/c_emulator/riscv_sim.cpp b/c_emulator/riscv_sim.cpp index a2cb77bc6..bb894a40f 100644 --- a/c_emulator/riscv_sim.cpp +++ b/c_emulator/riscv_sim.cpp @@ -440,7 +440,7 @@ void init_sail_reset_vector(uint64_t entry) } /* boot at reset vector */ - zPC = rom_base; + zforce_pc(rom_base); } void init_sail(uint64_t elf_entry, const char *config_file) @@ -456,15 +456,18 @@ void init_sail(uint64_t elf_entry, const char *config_file) rv_clint_size = UINT64_C(0); rv_htif_tohost = UINT64_C(0); */ - zPC = elf_entry; - } else + zforce_pc(elf_entry); + } else { init_sail_reset_vector(elf_entry); + } } /* reinitialize to clear state and memory, typically across tests runs */ void reinit_sail(uint64_t elf_entry, const char *config_file) { model_fini(); + sail_set_abstract_xlen(); + sail_set_abstract_ext_d_supported(); model_init(); init_sail(elf_entry, config_file); } @@ -666,6 +669,8 @@ int main(int argc, char **argv) { int files_start = process_args(argc, argv); + sail_set_abstract_xlen(); + sail_set_abstract_ext_d_supported(); model_init(); if (do_validate_config) { diff --git a/config/CMakeLists.txt b/config/CMakeLists.txt index e25205c93..7f7816948 100644 --- a/config/CMakeLists.txt +++ b/config/CMakeLists.txt @@ -1,11 +1,11 @@ - -file(READ "default.json" DEFAULT_JSON) +set(default_config_filename "rv64d.json") +file(READ ${default_config_filename} DEFAULT_JSON) configure_file("default_config.h.in" "default_config.h" @ONLY) -# Ensure this runs again if `default.json` is changed. -set_property(DIRECTORY APPEND PROPERTY CMAKE_CONFIGURE_DEPENDS "default.json;default_config.h.in") +# Ensure this runs again if the dependencies are changed. +set_property(DIRECTORY APPEND PROPERTY CMAKE_CONFIGURE_DEPENDS "${default_config_filename};default_config.h.in") add_library(default_config INTERFACE - "default_config.h" + "default_config.h" ) target_include_directories(default_config INTERFACE "${CMAKE_BINARY_DIR}/config") diff --git a/config/rv32d.json b/config/rv32d.json new file mode 100644 index 000000000..73325fe18 --- /dev/null +++ b/config/rv32d.json @@ -0,0 +1,261 @@ +{ + "base": { + "xlen": 32, + "writable_misa": true, + "writable_fiom": true, + "writable_hpm_counters": { + "len": 32, + "value": "0xFFFF_FFFF" + }, + "mtval_has_illegal_instruction_bits": false + }, + "memory": { + "pmp": { + "grain": 0, + "count": 16 + }, + "misaligned": { + "supported": true, + "byte_by_byte": false, + "order_decreasing": false, + "allowed_within_exp": 0 + }, + "translation": { + "dirty_update": false + } + }, + "platform": { + "vendorid": 0, + "archid": 0, + "impid": 0, + "hartid": 0, + "reset_vector": 4096, + "cache_block_size_exp": 6, + "ram": { + "base": 2147483648, + "size": 2147483648 + }, + "rom": { + "base": 4096, + "size": 4096 + }, + "clint": { + "base": 33554432, + "size": 786432 + }, + "clock_frequency": 1000000000, + "instructions_per_tick": 2, + "wfi_is_nop": true + }, + "extensions": { + "M": { + "supported": true + }, + "A": { + "supported": true + }, + "F": { + "supported": true + }, + "D": { + "supported": true + }, + "V": { + "supported": true, + "vlen_exp": 9, + "elen_exp": 6, + "vl_use_ceil": false + }, + "B": { + "supported": true + }, + "S": { + "supported": true + }, + "U": { + "supported": true + }, + "Zicbom": { + "supported": true + }, + "Zicboz": { + "supported": true + }, + "Zicond": { + "supported": true + }, + "Zicntr": { + "supported": true + }, + "Zicsr": { + "supported": true + }, + "Zifencei": { + "supported": true + }, + "Zihpm": { + "supported": true + }, + "Zimop": { + "supported": true + }, + "Zmmul": { + "supported": false + }, + "Zaamo": { + "supported": false + }, + "Zabha": { + "supported": true + }, + "Zalrsc": { + "supported": false + }, + "Zawrs": { + "supported": true, + "nto": { + "is_nop": false + }, + "sto": { + "is_nop": false + } + }, + "Zfa": { + "supported": true + }, + "Zfh": { + "supported": true + }, + "Zfhmin": { + "supported": false + }, + "Zfinx": { + "supported": false + }, + "Zca": { + "supported": true + }, + "Zcf": { + "supported": true + }, + "Zcd": { + "supported": true + }, + "Zcb": { + "supported": true + }, + "Zcmop": { + "supported": true + }, + "Zba": { + "supported": false + }, + "Zbb": { + "supported": false + }, + "Zbs": { + "supported": false + }, + "Zbc": { + "supported": true + }, + "Zbkb": { + "supported": true + }, + "Zbkc": { + "supported": true + }, + "Zbkx": { + "supported": true + }, + "Zknd": { + "supported": true + }, + "Zkne": { + "supported": true + }, + "Zknh": { + "supported": true + }, + "Zkr": { + "supported": true, + "sseed_reset_value": false, + "useed_reset_value": false, + "sseed_read_only_zero": false, + "useed_read_only_zero": false + }, + "Zksed": { + "supported": true + }, + "Zksh": { + "supported": true + }, + "Zkt": { + "supported": true + }, + "Zhinx": { + "supported": false + }, + "Zhinxmin": { + "supported": false + }, + "Zvbb": { + "supported": true + }, + "Zvbc": { + "supported": true + }, + "Zvkb": { + "supported": false + }, + "Zvkg": { + "supported": true + }, + "Zvkned": { + "supported": true + }, + "Zvknha": { + "supported": true + }, + "Zvknhb": { + "supported": true + }, + "Zvksed": { + "supported": true + }, + "Zvksh": { + "supported": true + }, + "Zvkt": { + "supported": true + }, + "Sscofpmf": { + "supported": true + }, + "Smcntrpmf": { + "supported": true + }, + "Sstc": { + "supported": true + }, + "Svinval": { + "supported": true + }, + "Svbare": { + "supported": true, + "sfence_vma_illegal_if_svbare_only": true + }, + "Sv32": { + "supported": true + }, + "Sv39": { + "supported": false + }, + "Sv48": { + "supported": false + }, + "Sv57": { + "supported": false + } + } +} diff --git a/config/default.json b/config/rv64d.json similarity index 97% rename from config/default.json rename to config/rv64d.json index e5a77bb51..9aeba4d38 100644 --- a/config/default.json +++ b/config/rv64d.json @@ -1,5 +1,6 @@ { "base": { + "xlen": 64, "writable_misa": true, "writable_fiom": true, "writable_hpm_counters": { @@ -53,7 +54,10 @@ "A": { "supported": true }, - "FD": { + "F": { + "supported": true + }, + "D": { "supported": true }, "V": { @@ -132,7 +136,7 @@ "supported": true }, "Zcf": { - "supported": true + "supported": false }, "Zcd": { "supported": true @@ -242,7 +246,7 @@ "sfence_vma_illegal_if_svbare_only": true }, "Sv32": { - "supported": true + "supported": false }, "Sv39": { "supported": true diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md index 5a6962c93..b6dbd7e3e 100644 --- a/doc/ReadingGuide.md +++ b/doc/ReadingGuide.md @@ -142,7 +142,7 @@ image into raw memory, including any ROM firmware such as the Berkeley boot loader and DeviceTree binary blobs, and initializes the memory map. -The generated C model `riscv_sim_$ARCH` is built from the Sail +The generated C model `sail_riscv_sim` is built from the Sail sources by the Sail compiler for the specified architecture $ARCH, either RV32 or RV64. It contains calls to the platform interface `riscv_platform` for platform-specific information; the latter is diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt index 61a58e193..c00aa8837 100644 --- a/model/CMakeLists.txt +++ b/model/CMakeLists.txt @@ -17,339 +17,321 @@ set(sail_common --require-version ${SAIL_REQUIRED_VER} ) -foreach (xlen IN ITEMS 32 64) - foreach (flen IN ITEMS 32 64) - foreach (variant IN ITEMS "" "rocq" "rmem" "lean" "lem" "isabelle") - set(arch "rv${xlen}") - if (flen EQUAL 32) - string(APPEND arch "f") - else() - string(APPEND arch "d") - endif() - - set(sail_xlen - "riscv_xlen${xlen}.sail" - "riscv_xlen.sail" - ) - - # TODO: Unfortunately 32 or 64 bit float support is a compile time. - # See https://github.com/riscv/sail-riscv/issues/348 - if (flen EQUAL 64) - set(sail_flen "riscv_flen_D.sail") - else() - set(sail_flen "riscv_flen_F.sail") - endif() - list(APPEND sail_flen "riscv_flen.sail") - - set(sail_vlen "riscv_vlen.sail") - - # Instruction sources, depending on target - set(sail_check_srcs - "riscv_addr_checks_common.sail" - "riscv_addr_checks.sail" - "riscv_misa_ext.sail" - ) - - set(vext_srcs - "riscv_insts_vext_utils.sail" - "riscv_insts_vext_fp_utils.sail" - "riscv_insts_vext_vset.sail" - "riscv_insts_vext_arith.sail" - "riscv_insts_vext_fp.sail" - "riscv_insts_vext_mem.sail" - "riscv_insts_vext_mask.sail" - "riscv_insts_vext_vm.sail" - "riscv_insts_vext_fp_vm.sail" - "riscv_insts_vext_red.sail" - "riscv_insts_vext_fp_red.sail" - ) - - set(sail_default_inst - "riscv_insts_base.sail" - "riscv_insts_zifencei.sail" - "riscv_insts_zaamo.sail" - "riscv_insts_zalrsc.sail" - "riscv_insts_zca.sail" - "riscv_insts_mext.sail" - "riscv_insts_zicsr.sail" - "riscv_insts_hext.sail" - "riscv_insts_reserved_fence.sail" - "riscv_insts_fext.sail" - "riscv_insts_zcf.sail" - "riscv_insts_dext.sail" - "riscv_insts_zcd.sail" - "riscv_insts_svinval.sail" - "riscv_insts_zba.sail" - "riscv_insts_zbb.sail" - "riscv_insts_zbc.sail" - "riscv_insts_zbs.sail" - "riscv_insts_zcb.sail" - "riscv_insts_zfh.sail" - # Zfa needs to be added after fext, dext and Zfh (as it needs - # definitions from those) - "riscv_insts_zfa.sail" - "riscv_insts_zkn.sail" - "riscv_insts_zks.sail" - "riscv_insts_zbkb.sail" - "riscv_insts_zbkx.sail" - "riscv_insts_zicond.sail" - ${vext_srcs} - "riscv_insts_zicbom.sail" - "riscv_insts_zicboz.sail" - "riscv_insts_zawrs.sail" - "riscv_insts_zvbb.sail" - "riscv_insts_zvbc.sail" - "riscv_insts_zvkg.sail" - "riscv_insts_zvkned.sail" - "riscv_insts_zvknhab.sail" - "riscv_insts_zvksed.sail" - "riscv_insts_zvksh.sail" - # Zimop and Zcmop should be at the end so they can be overridden by earlier extensions - "riscv_insts_zimop.sail" - "riscv_insts_zcmop.sail" - ) - - if (variant STREQUAL "rmem") - set(sail_seq_inst - ${sail_default_inst} - "riscv_jalr_rmem.sail" - "riscv_insts_rmem.sail" - ) - else() - set(sail_seq_inst - ${sail_default_inst} - "riscv_jalr_seq.sail" - ) - endif() - - set(sail_seq_inst_srcs - "riscv_insts_begin.sail" - ${sail_seq_inst} - "riscv_insts_end.sail" - "riscv_csr_end.sail" - ) - - set(sail_sys_srcs - "riscv_vext_control.sail" - "riscv_sys_exceptions.sail" - "riscv_sync_exception.sail" - "riscv_zihpm.sail" - "riscv_sscofpmf.sail" - "riscv_zkr_control.sail" - "riscv_zicntr_control.sail" - "riscv_softfloat_interface.sail" - "riscv_fdext_regs.sail" - "riscv_fdext_control.sail" - "riscv_smcntrpmf.sail" - "riscv_sys_reservation.sail" - "riscv_sys_control.sail" - ) - - set(sail_vm_srcs - "riscv_vmem_pte.sail" - "riscv_vmem_ptw.sail" - "riscv_vmem_tlb.sail" - "riscv_vmem.sail" - "riscv_vmem_utils.sail" - ) - - set(prelude - "prelude.sail" - "riscv_errors.sail" - ${sail_xlen} - ${sail_flen} - ${sail_vlen} - "prelude_mem_addrtype.sail" - "prelude_mem_metadata.sail" - "prelude_mem.sail" - "arithmetic.sail" - "rvfi_dii.sail" - "rvfi_dii_v1.sail" - "rvfi_dii_v2.sail" - ) - - set(sail_regs_srcs - "riscv_csr_begin.sail" - "riscv_callbacks.sail" - "riscv_reg_type.sail" - "riscv_freg_type.sail" - "riscv_regs.sail" - "riscv_pc_access.sail" - "riscv_sys_regs.sail" - "riscv_pmp_regs.sail" - "riscv_pmp_control.sail" - "riscv_ext_regs.sail" - ${sail_check_srcs} - "riscv_vreg_type.sail" - "riscv_vext_regs.sail" - ) - - set(sail_arch_srcs - ${prelude} - "riscv_extensions.sail" - "riscv_types_common.sail" - "riscv_types_ext.sail" - "riscv_types.sail" - "riscv_vmem_types.sail" - ${sail_regs_srcs} - ${sail_sys_srcs} - "riscv_platform.sail" - "riscv_sstc.sail" - "riscv_mem.sail" - "riscv_inst_retire.sail" - ${sail_vm_srcs} - # Shared/common code for the cryptography extension. - "riscv_types_kext.sail" - "riscv_zvk_utils.sail" - ) - - set(sail_step_srcs - "riscv_step_common.sail" - "riscv_step_ext.sail" - "riscv_decode_ext.sail" - "riscv_fetch_rvfi.sail" - "riscv_fetch.sail" - "riscv_step.sail" - ) - - if (variant STREQUAL "rocq" OR variant STREQUAL "lean") - list(APPEND sail_step_srcs - "riscv_termination.sail" - ) - endif() - - set(sail_cfg_srcs - "riscv_validate_config.sail" - "riscv_device_tree.sail" - ) - - set(sail_model_srcs - "riscv_model.sail" - ) - - # Final file list. - set(sail_srcs - ${sail_arch_srcs} - ${sail_seq_inst_srcs} - ${sail_step_srcs} - ${sail_cfg_srcs} - ${sail_model_srcs} - "main.sail" - ) - - # Convert to absolute paths, so we can run - - # Generate C code from Sail model - if (NOT variant) - set(c_model_no_ext "${CMAKE_BINARY_DIR}/riscv_model_${arch}") - set(c_model "${c_model_no_ext}.c") - set(c_model_header "${c_model_no_ext}.h") - - if (COVERAGE) - set(branch_info_file "${c_model_no_ext}.branch_info") - set(coverage_args "--c-coverage" ${branch_info_file}) - else() - set(branch_info_file) - set(coverage_args) - endif() - - add_custom_command( - DEPENDS ${sail_srcs} - OUTPUT ${c_model} ${c_model_header} ${branch_info_file} - VERBATIM - COMMENT "Building C code from Sail model (${arch})" - WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} - COMMAND - ${SAIL_BIN} - ${sail_common} - # Output file (without extension). - -o ${c_model_no_ext} - # Generate a file containing information about all possible branches. - # See https://github.com/rems-project/sail/blob/sail2/sailcov/README.md - ${coverage_args} - # Optimisations. - -O --Oconstant-fold - # Cache Z3 results in z3_problems file to speed up incremental compilation. - --memo-z3 - # Output C code. - -c - # Generate a C header too. - --c-generate-header - # Don't generate a main() function. - --c-no-main - # Extra #include's. - --c-include riscv_prelude.h - --c-include riscv_platform.h - --c-include riscv_callbacks.h - # Don't dead-code eliminate these functions. - --c-preserve init_model - --c-preserve try_step - --c-preserve tick_clock - --c-preserve generate_dts - --c-preserve config_is_valid - --c-preserve generate_canonical_isa_string - # Preserve RVFI functions. - --c-preserve rvfi_set_instr_packet - --c-preserve rvfi_get_cmd - --c-preserve rvfi_get_insn - --c-preserve rvfi_get_v2_trace_size - --c-preserve rvfi_get_v2_support_packet - --c-preserve rvfi_get_exec_packet_v1 - --c-preserve rvfi_get_exec_packet_v2 - --c-preserve rvfi_get_mem_data - --c-preserve rvfi_get_int_data - --c-preserve rvfi_zero_exec_packet - --c-preserve rvfi_halt_exec_packet - --c-preserve print_instr_packet - --c-preserve print_rvfi_exec - --c-preserve rvfi_write - --c-preserve rvfi_read - --c-preserve rvfi_mem_exception - --c-preserve rvfi_wX - --c-preserve rvfi_trap - # Input files. - ${sail_srcs} - ) - - add_custom_target(generated_model_${arch} DEPENDS ${c_model} ${c_model_header}) - endif() - - if (NOT variant) - # Generate JSON snippets file. - set(model_doc "riscv_model_${arch}.json") - - add_custom_command( - DEPENDS ${sail_srcs} - OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/${model_doc}" - VERBATIM - COMMENT "Building documentation JSON from Sail model (${arch})" - WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} - COMMAND - ${SAIL_BIN} - ${sail_common} - # Generate JSON documentation file. - --doc - # Format to interpret comments as. You can also use 'asciidoc' - # in which case it will interpret them as Markdown and output them - # as Asciidoc, but there's a bug in the Sail compiler so it can't - # parse the Markdown and it doesn't seem to output the comments - # anyway. - --doc-format identity - # Don't pretty-print the JSON output. It's too big to be readable anyway. - --doc-compact - # Actually embed the code snippets in the JSON as plain text rather - # than referencing them. The other option is base64. - --doc-embed plain - # The directory that the JSON will be saved in. - -o ${CMAKE_CURRENT_BINARY_DIR} - # The name of the JSON file. - --doc-bundle ${model_doc} - # Input files. - ${sail_srcs} - ) - - add_custom_target(generated_docs_${arch} DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/${model_doc}") - +foreach (variant IN ITEMS "" "smt" "rocq" "rmem" "lean" "lem" "isabelle") + + # Instruction sources, depending on target + set(sail_check_srcs + "riscv_addr_checks_common.sail" + "riscv_addr_checks.sail" + "riscv_misa_ext.sail" + ) + + set(vext_srcs + "riscv_insts_vext_utils.sail" + "riscv_insts_vext_fp_utils.sail" + "riscv_insts_vext_vset.sail" + "riscv_insts_vext_arith.sail" + "riscv_insts_vext_fp.sail" + "riscv_insts_vext_mem.sail" + "riscv_insts_vext_mask.sail" + "riscv_insts_vext_vm.sail" + "riscv_insts_vext_fp_vm.sail" + "riscv_insts_vext_red.sail" + "riscv_insts_vext_fp_red.sail" + ) + + set(sail_default_inst + "riscv_insts_base.sail" + "riscv_insts_zifencei.sail" + "riscv_insts_zaamo.sail" + "riscv_insts_zalrsc.sail" + "riscv_insts_zca.sail" + "riscv_insts_mext.sail" + "riscv_insts_zicsr.sail" + "riscv_insts_hext.sail" + "riscv_insts_reserved_fence.sail" + "riscv_insts_fext.sail" + "riscv_insts_zcf.sail" + "riscv_insts_dext.sail" + "riscv_insts_zcd.sail" + "riscv_insts_svinval.sail" + "riscv_insts_zba.sail" + "riscv_insts_zbb.sail" + "riscv_insts_zbc.sail" + "riscv_insts_zbs.sail" + "riscv_insts_zcb.sail" + "riscv_insts_zfh.sail" + # Zfa needs to be added after fext, dext and Zfh (as it needs + # definitions from those) + "riscv_insts_zfa.sail" + "riscv_insts_zkn.sail" + "riscv_insts_zks.sail" + "riscv_insts_zbkb.sail" + "riscv_insts_zbkx.sail" + "riscv_insts_zicond.sail" + ${vext_srcs} + "riscv_insts_zicbom.sail" + "riscv_insts_zicboz.sail" + "riscv_insts_zawrs.sail" + "riscv_insts_zvbb.sail" + "riscv_insts_zvbc.sail" + "riscv_insts_zvkg.sail" + "riscv_insts_zvkned.sail" + "riscv_insts_zvknhab.sail" + "riscv_insts_zvksed.sail" + "riscv_insts_zvksh.sail" + # Zimop and Zcmop should be at the end so they can be overridden by earlier extensions + "riscv_insts_zimop.sail" + "riscv_insts_zcmop.sail" + ) + + if (variant STREQUAL "rmem") + set(sail_seq_inst + ${sail_default_inst} + "riscv_jalr_rmem.sail" + "riscv_insts_rmem.sail" + ) + else() + set(sail_seq_inst + ${sail_default_inst} + "riscv_jalr_seq.sail" + ) + endif() + + set(sail_seq_inst_srcs + "riscv_insts_begin.sail" + ${sail_seq_inst} + "riscv_insts_end.sail" + "riscv_csr_end.sail" + ) + + set(sail_sys_srcs + "riscv_vext_control.sail" + "riscv_sys_exceptions.sail" + "riscv_sync_exception.sail" + "riscv_zihpm.sail" + "riscv_sscofpmf.sail" + "riscv_zkr_control.sail" + "riscv_zicntr_control.sail" + "riscv_softfloat_interface.sail" + "riscv_fdext_regs.sail" + "riscv_fdext_control.sail" + "riscv_smcntrpmf.sail" + "riscv_sys_reservation.sail" + "riscv_sys_control.sail" + ) + + set(sail_vm_srcs + "riscv_vmem_pte.sail" + "riscv_vmem_ptw.sail" + "riscv_vmem_tlb.sail" + "riscv_vmem.sail" + "riscv_vmem_utils.sail" + ) + + set(prelude + "prelude.sail" + "riscv_errors.sail" + "riscv_xlen.sail" + "riscv_flen.sail" + "riscv_vlen.sail" + "prelude_mem_addrtype.sail" + "prelude_mem_metadata.sail" + "prelude_mem.sail" + "arithmetic.sail" + "rvfi_dii.sail" + "rvfi_dii_v1.sail" + "rvfi_dii_v2.sail" + ) + + set(sail_regs_srcs + "riscv_csr_begin.sail" + "riscv_callbacks.sail" + "riscv_reg_type.sail" + "riscv_freg_type.sail" + "riscv_regs.sail" + "riscv_pc_access.sail" + "riscv_sys_regs.sail" + "riscv_pmp_regs.sail" + "riscv_pmp_control.sail" + "riscv_ext_regs.sail" + ${sail_check_srcs} + "riscv_vreg_type.sail" + "riscv_vext_regs.sail" + ) + + set(sail_arch_srcs + ${prelude} + "riscv_extensions.sail" + "riscv_types_common.sail" + "riscv_types_ext.sail" + "riscv_types.sail" + "riscv_vmem_types.sail" + ${sail_regs_srcs} + ${sail_sys_srcs} + "riscv_platform.sail" + "riscv_sstc.sail" + "riscv_mem.sail" + "riscv_inst_retire.sail" + ${sail_vm_srcs} + # Shared/common code for the cryptography extension. + "riscv_types_kext.sail" + "riscv_zvk_utils.sail" + ) + + set(sail_step_srcs + "riscv_step_common.sail" + "riscv_step_ext.sail" + "riscv_decode_ext.sail" + "riscv_fetch_rvfi.sail" + "riscv_fetch.sail" + "riscv_step.sail" + ) + + if (variant STREQUAL "rocq" OR variant STREQUAL "lean") + list(APPEND sail_step_srcs + "riscv_termination.sail" + ) + endif() + + set(sail_cfg_srcs + "riscv_validate_config.sail" + "riscv_device_tree.sail" + ) + + set(sail_model_srcs + "riscv_model.sail" + ) + + # Final file list. + set(sail_srcs + ${sail_arch_srcs} + ${sail_seq_inst_srcs} + ${sail_step_srcs} + ${sail_cfg_srcs} + ${sail_model_srcs} + "main.sail" + ) + + # Generate C code from Sail model + if (NOT variant) + set(c_model_no_ext "${CMAKE_BINARY_DIR}/sail_riscv_model") + set(c_model "${c_model_no_ext}.c") + set(c_model_header "${c_model_no_ext}.h") + + if (COVERAGE) + set(branch_info_file "${c_model_no_ext}.branch_info") + set(coverage_args "--c-coverage" ${branch_info_file}) + else() + set(branch_info_file) + set(coverage_args) + endif() + + add_custom_command( + DEPENDS ${sail_srcs} + OUTPUT ${c_model} ${c_model_header} ${branch_info_file} + VERBATIM + COMMENT "Building C code from Sail model" + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + COMMAND + ${SAIL_BIN} + ${sail_common} + # Output file (without extension). + -o ${c_model_no_ext} + # Generate a file containing information about all possible branches. + # See https://github.com/rems-project/sail/blob/sail2/sailcov/README.md + ${coverage_args} + # Optimisations. + -O --Oconstant-fold + # Cache Z3 results in z3_problems file to speed up incremental compilation. + --memo-z3 + # Output C code. + -c + # Generate a C header too. + --c-generate-header + # Don't generate a main() function. + --c-no-main + # Extra #include's. + --c-include riscv_prelude.h + --c-include riscv_platform.h + --c-include riscv_callbacks.h + # Don't dead-code eliminate these functions. + --c-preserve init_model + --c-preserve try_step + --c-preserve tick_clock + --c-preserve force_pc + --c-preserve generate_dts + --c-preserve config_is_valid + --c-preserve generate_canonical_isa_string + # Preserve RVFI functions. + --c-preserve rvfi_set_instr_packet + --c-preserve rvfi_get_cmd + --c-preserve rvfi_get_insn + --c-preserve rvfi_get_v2_trace_size + --c-preserve rvfi_get_v2_support_packet + --c-preserve rvfi_get_exec_packet_v1 + --c-preserve rvfi_get_exec_packet_v2 + --c-preserve rvfi_get_mem_data + --c-preserve rvfi_get_int_data + --c-preserve rvfi_zero_exec_packet + --c-preserve rvfi_halt_exec_packet + --c-preserve print_instr_packet + --c-preserve print_rvfi_exec + --c-preserve rvfi_write + --c-preserve rvfi_read + --c-preserve rvfi_mem_exception + --c-preserve rvfi_wX + --c-preserve rvfi_trap + # Input files. + ${sail_srcs} + ) + + add_custom_target(generated_sail_riscv_model DEPENDS ${c_model} ${c_model_header}) + endif() + + if (NOT variant) + # Generate JSON snippets file. + set(model_doc "sail_riscv_model.json") + + add_custom_command( + DEPENDS ${sail_srcs} + OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/${model_doc}" + VERBATIM + COMMENT "Building documentation JSON from Sail model" + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + COMMAND + ${SAIL_BIN} + ${sail_common} + # Generate JSON documentation file. + --doc + # Format to interpret comments as. You can also use 'asciidoc' + # in which case it will interpret them as Markdown and output them + # as Asciidoc, but there's a bug in the Sail compiler so it can't + # parse the Markdown and it doesn't seem to output the comments + # anyway. + --doc-format identity + # Don't pretty-print the JSON output. It's too big to be readable anyway. + --doc-compact + # Actually embed the code snippets in the JSON as plain text rather + # than referencing them. The other option is base64. + --doc-embed plain + # The directory that the JSON will be saved in. + -o ${CMAKE_CURRENT_BINARY_DIR} + # The name of the JSON file. + --doc-bundle ${model_doc} + # Input files. + ${sail_srcs} + ) + + add_custom_target(generated_sail_riscv_docs DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/${model_doc}") + endif() + + if (variant) + # Theorem prover backends require compile time configuration. + foreach (arch IN ITEMS "rv32d" "rv64d") + set(config_file "${CMAKE_SOURCE_DIR}/config/${arch}.json") + + if (variant STREQUAL "smt") # Generate smtlib2 code from the Sail code. # A separate .smt2 file is created for each $property or $counterexample. # Since the true output files are unknown we need to manually @@ -368,7 +350,7 @@ foreach (xlen IN ITEMS 32 64) --smt # The prefix of the output files. -o "${CMAKE_CURRENT_BINARY_DIR}/model" - --config ${CMAKE_SOURCE_DIR}/config/default.json + --config ${config_file} # Input files. ${sail_srcs} COMMAND ${CMAKE_COMMAND} -E touch ${smt_stamp_file} @@ -402,6 +384,7 @@ foreach (xlen IN ITEMS 32 64) --isa-output-dir ${CMAKE_CURRENT_BINARY_DIR} # The prefix of the output files. -o "lem_${arch}" + --config ${config_file} # Input files. ${sail_srcs} ) @@ -420,6 +403,7 @@ foreach (xlen IN ITEMS 32 64) --tofrominterp-output-dir ${CMAKE_CURRENT_BINARY_DIR} # The prefix of the output files. -o "rmem_${arch}" + --config ${config_file} # Input files. ${sail_srcs} ) @@ -435,6 +419,7 @@ foreach (xlen IN ITEMS 32 64) --marshal # The prefix of the output files. -o "rmem_${arch}" + --config ${config_file} # Input files. ${sail_srcs} ) @@ -464,7 +449,7 @@ foreach (xlen IN ITEMS 32 64) --coq-output-dir "${CMAKE_BINARY_DIR}/rocq" # The prefix of the output files. -o "${arch}" - --config ${CMAKE_SOURCE_DIR}/config/default.json + --config ${config_file} # Input files. ${sail_srcs} ) @@ -491,12 +476,13 @@ foreach (xlen IN ITEMS 32 64) if (variant STREQUAL "lean") string(TOUPPER ${arch} arch_uppercase) set(lean_sail_common - --config ${CMAKE_SOURCE_DIR}/config/default.json - --lean - --memo-z3 - --lean-output-dir ${CMAKE_CURRENT_BINARY_DIR} - --lean-force-output - --lean-non-beq-type ast) + --config ${config_file} + --lean + --memo-z3 + --lean-output-dir ${CMAKE_CURRENT_BINARY_DIR} + --lean-force-output + --lean-non-beq-type ast + ) set(lean_sail_default --lean-noncomputable --lean-noncomputable-function encdec_forwards @@ -508,14 +494,12 @@ foreach (xlen IN ITEMS 32 64) --lean-noncomputable-function encdec_compressed_forwards_matches --lean-noncomputable-function encdec_compressed_backwards_matches --lean-import-file ../handwritten_support/RiscvExtras.lean - -o "Lean_${arch_uppercase}") - set(lean_sail_executable - --lean-import-file ../handwritten_support/RiscvExtrasExecutable.lean - -o "Lean_${arch_uppercase}_executable") + -o "Lean_${arch_uppercase}" + ) add_custom_command( DEPENDS ${sail_srcs} - ${CMAKE_SOURCE_DIR}/config/default.json + ${config_file} ${CMAKE_SOURCE_DIR}/handwritten_support/RiscvExtrasExecutable.lean VERBATIM OUTPUT "lean_${arch_uppercase}.lean" @@ -531,7 +515,7 @@ foreach (xlen IN ITEMS 32 64) add_custom_command( DEPENDS ${sail_srcs} - ${CMAKE_SOURCE_DIR}/config/default.json + ${config_file} ${CMAKE_SOURCE_DIR}/handwritten_support/RiscvExtras.lean VERBATIM OUTPUT "lean_executable_${arch_uppercase}.lean" @@ -553,7 +537,7 @@ foreach (xlen IN ITEMS 32 64) if (variant STREQUAL "lem") string_upper_initial("${arch}" arch_thy) add_custom_command( - DEPENDS ${sail_srcs} ${CMAKE_SOURCE_DIR}/config/default.json + DEPENDS ${sail_srcs} ${config_file} VERBATIM OUTPUT "${arch}.lem" "${arch}_types.lem" "${CMAKE_BINARY_DIR}/isabelle/${arch}/${arch_thy}_lemmas.thy" COMMENT "Building Lem definitions from Sail model (${arch})" @@ -569,7 +553,7 @@ foreach (xlen IN ITEMS 32 64) --isa-output-dir "${CMAKE_BINARY_DIR}/isabelle/${arch}" # The prefix of the output files. -o "${arch}" - --config ${CMAKE_SOURCE_DIR}/config/default.json + --config ${config_file} # Input files. ${sail_srcs} COMMAND @@ -635,5 +619,5 @@ foreach (xlen IN ITEMS 32 64) add_custom_target(generated_isabelle_${arch} DEPENDS "${CMAKE_BINARY_DIR}/isabelle/${arch}/${arch_thy}.thy") endif() endforeach() - endforeach() + endif() endforeach() diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail index a931fc66b..4a8e52118 100644 --- a/model/riscv_extensions.sail +++ b/model/riscv_extensions.sail @@ -44,11 +44,13 @@ function clause hartSupports(Ext_A) = config extensions.A.supported // Single-Precision Floating-Point enum clause extension = Ext_F mapping clause extensionName = Ext_F <-> "f" -function clause hartSupports(Ext_F) = config extensions.FD.supported +function clause hartSupports(Ext_F) = config extensions.F.supported // Double-Precision Floating-Point +// TODO: Ideally we'd use `config extensions.D.supported` here but it doesn't +// work due to https://github.com/rems-project/sail/issues/1255 enum clause extension = Ext_D mapping clause extensionName = Ext_D <-> "d" -function clause hartSupports(Ext_D) = config extensions.FD.supported // TODO: Separate F and D supported flags +function clause hartSupports(Ext_D) = constraint(ext_d_supported) & hartSupports(Ext_F) // Bit Manipulation enum clause extension = Ext_B mapping clause extensionName = Ext_B <-> "b" diff --git a/model/riscv_flen.sail b/model/riscv_flen.sail index 99d9a85e5..30458e879 100644 --- a/model/riscv_flen.sail +++ b/model/riscv_flen.sail @@ -6,6 +6,11 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ +// This is only a type because `if (config extensions.D.supported : bool) then 8 else 4` +// gives a syntax error: https://github.com/rems-project/sail/issues/1256 +type ext_d_supported : Bool = config extensions.D.supported +type flen_bytes : Int = if ext_d_supported then 8 else 4 + type flen : Int = flen_bytes * 8 type flenbits = bits(flen) diff --git a/model/riscv_flen_D.sail b/model/riscv_flen_D.sail deleted file mode 100644 index 613bd07ff..000000000 --- a/model/riscv_flen_D.sail +++ /dev/null @@ -1,11 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -/* Define the FLEN value for the 'D' extension. */ - -type flen_bytes : Int = 8 diff --git a/model/riscv_flen_F.sail b/model/riscv_flen_F.sail deleted file mode 100644 index b3fdeecaf..000000000 --- a/model/riscv_flen_F.sail +++ /dev/null @@ -1,11 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -/* Define the FLEN value for the 'F' extension. */ - -type flen_bytes : Int = 4 diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index 58908bb2d..c302ad654 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -31,3 +31,8 @@ function tick_pc() = { PC = nextPC; pc_write_callback(PC); } + +// For forcing PC from C. This is ugly. +function force_pc(pc : bits(64)) -> unit = { + PC = truncate(pc, xlen); +} diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 1bece362a..52d2a1de5 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -64,8 +64,9 @@ register plat_clint_size : physaddrbits = to_bits_checked(config platform.clint. val plat_enable_htif = pure "plat_enable_htif" : unit -> bool /* Location of HTIF ports */ -val plat_htif_tohost = pure {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> physaddrbits -function plat_htif_tohost () = zeros() +val plat_htif_tohost = pure {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> bits(64) +function htif_tohost_base() -> physaddrbits = trunc(plat_htif_tohost()) + // todo: fromhost /* Physical memory map predicates */ @@ -111,10 +112,10 @@ function within_clint forall 'n, 0 < 'n <= max_mem_access . (Physaddr(addr) : ph } function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (Physaddr(addr) : physaddr, width : int('n)) -> bool = - plat_enable_htif() & (plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4)) + plat_enable_htif() & (htif_tohost_base() == addr | (htif_tohost_base() + 4 == addr & width == 4)) function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (Physaddr(addr) : physaddr, width : int('n)) -> bool = - plat_enable_htif() & (plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4)) + plat_enable_htif() & (htif_tohost_base() == addr | (htif_tohost_base() + 4 == addr & width == 4)) /* CLINT (Core Local Interruptor), based on Spike. */ @@ -332,11 +333,11 @@ function htif_load(t, Physaddr(paddr), width) = { if get_config_print_platform() then print_platform("htif[" ^ hex_bits_str(paddr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ - if width == 8 & (paddr == plat_htif_tohost()) + if width == 8 & (paddr == htif_tohost_base()) then Ok(zero_extend(64, htif_tohost)) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else if width == 4 & paddr == plat_htif_tohost() + else if width == 4 & paddr == htif_tohost_base() then Ok(zero_extend(32, htif_tohost[31..0])) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else if width == 4 & paddr == plat_htif_tohost() + 4 + else if width == 4 & paddr == htif_tohost_base() + 4 then Ok(zero_extend(32, htif_tohost[63..32])) /* FIXME: Redundant zero_extend currently required by Lem backend */ else match t { InstructionFetch() => Err(E_Fetch_Access_Fault()), @@ -354,12 +355,12 @@ function htif_store(Physaddr(paddr), width, data) = { then { htif_cmd_write = bitone; htif_payload_writes = htif_payload_writes + 1; htif_tohost = zero_extend(data) } - else if width == 4 & paddr == plat_htif_tohost() + else if width == 4 & paddr == htif_tohost_base() then { if data == htif_tohost[31 .. 0] then htif_payload_writes = htif_payload_writes + 1 else htif_payload_writes = 0x1; htif_tohost = vector_update_subrange(htif_tohost, 31, 0, data) } - else if width == 4 & paddr == plat_htif_tohost() + 4 + else if width == 4 & paddr == htif_tohost_base() + 4 then { if data[15 .. 0] == htif_tohost[47 .. 32] then htif_payload_writes = htif_payload_writes + 1 else htif_payload_writes = 0x1; diff --git a/model/riscv_termination.sail b/model/riscv_termination.sail index 1b8acb178..d8f6117d9 100644 --- a/model/riscv_termination.sail +++ b/model/riscv_termination.sail @@ -91,7 +91,8 @@ termination_measure virtual_memory_supported(_) = 3 function hartSupports_measure(ext : extension) -> int = match ext { - Ext_C => 1, + Ext_C => 2, + Ext_D => 1, _ => 0, } diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail index 7b51f3f8d..6b83489a8 100644 --- a/model/riscv_xlen.sail +++ b/model/riscv_xlen.sail @@ -6,18 +6,32 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -type log2_xlen : Int = log2_xlen_bytes + 3 -type xlen_bytes : Int = 2 ^ log2_xlen_bytes -type xlen : Int = xlen_bytes * 8 -type xlenbits = bits(xlen) +// Define the XLEN value for the architecture. +// This is done using the smallest/most logarithmic possible value since Sail's +// type system works well for multiply and 2^ but not divide and log2. + +type xlen : Int = config base.xlen +constraint xlen in {32, 64} + +type log2_xlen : Int = if xlen == 32 then 5 else 6 +type xlen_bytes : Int = if xlen == 32 then 4 else 8 + +// TODO: Allow configuring a lower number of physical address bits. +// For example it is unlikely that serious RV64 implementations really +// have 64 physical address bits. +type physaddrbits_len : Int = if xlen == 32 then 34 else 64 + +// This is the maximum; designs can implement shorter ASIDLENs. +// TODO: Allow configuring shorter ASIDLENs. +type asidlen : Int = if xlen == 32 then 9 else 16 // Variable versions of the above types. Variables and types // are disjoint in Sail so they are allowed to have the same name. // This saves typing `sizeof()` everywhere. let log2_xlen = sizeof(log2_xlen) -let log2_xlen_bytes = sizeof(log2_xlen_bytes) let xlen_bytes = sizeof(xlen_bytes) let xlen = sizeof(xlen) +let asidlen = sizeof(asidlen) -let asidlen = sizeof(asidlen) -type asidbits = bits(asidlen) +type xlenbits = bits(xlen) +type asidbits = bits(asidlen) diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail deleted file mode 100644 index 38dc8c6ce..000000000 --- a/model/riscv_xlen32.sail +++ /dev/null @@ -1,17 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -// Define the XLEN value for the architecture. -// This is done using the smallest/most logarithmic possible value since Sail's -// type system works well for multiply and 2^ but not divide and log2. -type log2_xlen_bytes : Int = 2 - -type physaddrbits_len : Int = 34 - -// This is the maximum; designs can implement shorter ASIDLENs. -type asidlen : Int = 9 diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail deleted file mode 100644 index 5d92cb625..000000000 --- a/model/riscv_xlen64.sail +++ /dev/null @@ -1,17 +0,0 @@ -/*=======================================================================================*/ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except where otherwise noted is subject the BSD */ -/* two-clause license in the LICENSE file. */ -/* */ -/* SPDX-License-Identifier: BSD-2-Clause */ -/*=======================================================================================*/ - -// Define the XLEN value for the architecture. -// This is done using the smallest/most logarithmic possible value since Sail's -// type system works well for multiply and 2^ but not divide and log2. -type log2_xlen_bytes : Int = 3 - -type physaddrbits_len : Int = 64 - -// This is the maximum; designs can implement shorter ASIDLENs. -type asidlen : Int = 16 diff --git a/os-boot/README.md b/os-boot/README.md index 772011d9f..3a39f2cc4 100644 --- a/os-boot/README.md +++ b/os-boot/README.md @@ -25,7 +25,7 @@ a DTB (device-tree blob) file describing the platform (say in the file the model should be run as: ``` -$ ./c_emulator/riscv_sim_ -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & +$ ./c_emulator/sail_riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & $ tail -f console.log ``` @@ -53,6 +53,6 @@ device-tree blob for a 64MB RV64 machine using `dtc`: ``` dtc < os-boot/rv64-64mb.dts > os-boot/rv64-64mb.dtb -./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/rv64-linux-4.15.0-gcc-7.2.0-64mb.bbl > >(gzip -c > execution-trace.log.gz) 2>&1 +./c_emulator/sail_riscv_sim -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/rv64-linux-4.15.0-gcc-7.2.0-64mb.bbl > >(gzip -c > execution-trace.log.gz) 2>&1 tail -f /tmp/console.log ``` diff --git a/os-boot/image-notes.txt b/os-boot/image-notes.txt index f517f878b..4e60dcc74 100644 --- a/os-boot/image-notes.txt +++ b/os-boot/image-notes.txt @@ -20,19 +20,19 @@ dtc < os-boot/rv64-64mb.dts > os-boot/rv64-64mb.dtb The 64-bit Linux image can then be booted as: ``` -./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/linux-rv64-64mb.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1 +./c_emulator/sail_riscv_sim -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/linux-rv64-64mb.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1 tail -f /tmp/console.log ``` The 64-bit FreeBSD image requires hardware PTE update support (`-d`): ``` -./c_emulator/riscv_sim_RV64 -d -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/freebsd-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1 +./c_emulator/sail_riscv_sim -d -b os-boot/rv64-64mb.dtb -t /tmp/console.log os-boot/freebsd-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1 ``` The 64-bit seL4 image runs its test-suite and requires more memory (`-z`): ``` dtc < os-boot/rv64-2gb.dts > os-boot/rv64-2gb.dtb -./c_emulator/riscv_sim_RV64 -z 2048 -b os-boot/rv64-2gb.dtb -t /tmp/console.log os-boot/sel4-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1 +./c_emulator/sail_riscv_sim -z 2048 -b os-boot/rv64-2gb.dtb -t /tmp/console.log os-boot/sel4-rv64.bbl > >(gzip -c - > /tmp/exec-trace.log.gz) 2>&1 ``` Note that the consistency of the `-z` argument and the contents of the diff --git a/test/first_party/CMakeLists.txt b/test/first_party/CMakeLists.txt index bc6ad56a5..5baeab947 100644 --- a/test/first_party/CMakeLists.txt +++ b/test/first_party/CMakeLists.txt @@ -88,15 +88,17 @@ set(tests "test_pmp_access.c" ) + foreach (xlen IN ITEMS 32 64) - foreach (test_source IN LISTS tests) - set(arch "rv${xlen}d") - if (xlen EQUAL 32) - set(mabi "ilp32") - else() - set(mabi "lp64") - endif() + set(arch "rv${xlen}d") + if (xlen EQUAL 32) + set(mabi "ilp32") + else() + set(mabi "lp64") + endif() + set(default_config "${CMAKE_SOURCE_DIR}/config/${arch}.json") + foreach (test_source IN LISTS tests) set(elf "${arch}_${test_source}.elf") set(config "${arch}_${test_source}.json") @@ -145,11 +147,11 @@ foreach (xlen IN ITEMS 32 64) add_custom_command( OUTPUT ${config} DEPENDS - "${CMAKE_SOURCE_DIR}/config/default.json" + ${default_config} "${CMAKE_CURRENT_SOURCE_DIR}/src/${test_source}.filter" COMMAND jq -f "${CMAKE_CURRENT_SOURCE_DIR}/src/${test_source}.filter" - "${CMAKE_SOURCE_DIR}/config/default.json" + ${default_config} > ${config} VERBATIM COMMENT "Creating ${config}" @@ -158,9 +160,9 @@ foreach (xlen IN ITEMS 32 64) add_custom_command( OUTPUT ${config} DEPENDS - "${CMAKE_SOURCE_DIR}/config/default.json" + ${default_config} COMMAND ${CMAKE_COMMAND} -E copy - "${CMAKE_SOURCE_DIR}/config/default.json" + ${default_config} "${config}" VERBATIM ) @@ -170,7 +172,7 @@ foreach (xlen IN ITEMS 32 64) add_test( NAME "first_party_${arch}_${test_source}" - COMMAND $ --config ${config} ${elf} + COMMAND $ --config ${config} ${elf} ) endforeach() endforeach() diff --git a/test/riscv-tests/CMakeLists.txt b/test/riscv-tests/CMakeLists.txt index 031f32531..aa2c202ce 100644 --- a/test/riscv-tests/CMakeLists.txt +++ b/test/riscv-tests/CMakeLists.txt @@ -13,8 +13,8 @@ foreach (arch IN ITEMS "rv32d" "rv64d") add_test( NAME "${arch}_${elf_name}" COMMAND - $ - --config "${CMAKE_SOURCE_DIR}/config/default.json" + $ + --config "${CMAKE_SOURCE_DIR}/config/${arch}.json" ${elf} ) endforeach()