Use C header generated by Sail

c_emulator/CMakeLists.txt

@@ -29,6 +29,7 @@ foreach (xlen IN ITEMS 32 64)
 
         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.
@@ -53,6 +54,15 @@ foreach (xlen IN ITEMS 32 64)
         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}"
+        )
+
+        # 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=<riscv_model_${arch}.h>"
         )
 
         # TODO: Enable warnings when we use the #include trick

c_emulator/riscv_sail.h

@@ -1,79 +1,23 @@
-/* Top-level interfaces to the Sail model.
-   Ideally, this would be autogenerated.
- */
+#pragma once
+
+// The header generated by Sail.
+#include RISCV_MODEL_HEADER
 
 #ifdef __cplusplus
 extern "C" {
 #endif
 
-typedef int unit;
-#define UNIT 0
-typedef uint64_t mach_bits;
-
-struct zMisa {
-  mach_bits zMisa_chunk_0;
-};
-extern struct zMisa zmisa;
-
+// The generated header does not include these functions.
 void model_init(void);
 void model_fini(void);
 
-unit zinit_model(const_sail_string);
-bool ztry_step(sail_int, bool);
-unit ztick_clock(unit);
-
-bool zconfig_is_valid(unit);
-void zgenerate_dts(sail_string *out, unit);
-
-unit zrvfi_set_instr_packet(mach_bits);
-mach_bits zrvfi_get_cmd(unit);
-mach_bits zrvfi_get_insn(unit);
-bool zrvfi_step(sail_int);
-unit zrvfi_zzero_exec_packet(unit);
-unit zrvfi_halt_exec_packet(unit);
-void zrvfi_get_exec_packet_v1(sail_bits *rop, unit);
-void zrvfi_get_exec_packet_v2(sail_bits *rop, unit);
-extern bool zrvfi_int_data_present;
-void zrvfi_get_int_data(sail_bits *rop, unit);
-extern bool zrvfi_mem_data_present;
-void zrvfi_get_mem_data(sail_bits *rop, unit);
-void zrvfi_get_v2_support_packet(sail_bits *rop, unit);
-
-// Debugging prints
-unit zprint_rvfi_exec(unit);
-unit zprint_instr_packet(uint64_t);
-
+// 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 bool zhtif_done;
-extern mach_bits zhtif_exit_code;
-extern bool have_exception;
-
-/* machine state */
-
-extern uint32_t zcur_privilege;
-
-extern mach_bits zPC;
-
-extern mach_bits zx1, zx2, zx3, zx4, zx5, zx6, zx7, zx8, zx9, zx10, zx11, zx12,
-    zx13, zx14, zx15, zx16, zx17, zx18, zx19, zx20, zx21, zx22, zx23, zx24,
-    zx25, zx26, zx27, zx28, zx29, zx30, zx31;
-
-extern mach_bits zmstatus;
-extern mach_bits zmepc, zmtval;
-extern mach_bits zsepc, zstval;
-
-extern mach_bits zfloat_result, zfloat_fflags;
-
-struct zMcause {
-  mach_bits zMcause_chunk_0;
-};
-extern struct zMcause zmcause, zscause;
-
-extern mach_bits zminstret;
 
 #ifdef __cplusplus
-} // extern "C"
+}
 #endif

model/CMakeLists.txt

@@ -227,6 +227,7 @@ foreach (xlen IN ITEMS 32 64)
             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")
@@ -238,7 +239,7 @@ foreach (xlen IN ITEMS 32 64)
 
                 add_custom_command(
                     DEPENDS ${sail_srcs}
-                    OUTPUT ${c_model} ${branch_info_file}
+                    OUTPUT ${c_model} ${c_model_header} ${branch_info_file}
                     VERBATIM
                     COMMENT "Building C code from Sail model (${arch})"
                     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
@@ -262,14 +263,15 @@ foreach (xlen IN ITEMS 32 64)
                         --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. These should match the
-                        # ones used from riscv_sail.h
+                        # Don't dead-code eliminate these functions.
                         --c-preserve init_model
                         --c-preserve try_step
                         --c-preserve tick_clock
@@ -298,7 +300,7 @@ foreach (xlen IN ITEMS 32 64)
                         ${sail_srcs}
                 )
 
-                add_custom_target(generated_model_${arch} DEPENDS ${c_model})
+                add_custom_target(generated_model_${arch} DEPENDS ${c_model} ${c_model_header})
             endif()
 
             if (NOT variant)