Skip to content

Commit a606ebe

Browse files
pmundkurpmundkur
authored
Add a configuration validation function to the model. (riscv#1005)
This is a start and can be extended to check more invariants of a valid configuration. Configuration validation is done when the model is initialized in `init_model()`. `init_model()` and `reset()` are moved out of `riscv_step.sail` into a new file `riscv_model.sail` to manage the dependency on `riscv_validate_config.sail`. Addresses riscv#860.
1 parent 733accf commit a606ebe

File tree

7 files changed

+193
-44
lines changed

7 files changed

+193
-44
lines changed

‎c_emulator/riscv_sail.h‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,11 @@ extern struct zMisa zmisa;
1818
void model_init(void);
1919
void model_fini(void);
2020

21-
unit zinit_model(unit);
21+
unit zinit_model(const_sail_string);
2222
bool ztry_step(sail_int, bool);
2323
unit ztick_clock(unit);
2424

25+
bool zconfig_is_valid(unit);
2526
void zgenerate_dts(sail_string *out, unit);
2627

2728
unit zrvfi_set_instr_packet(mach_bits);

‎c_emulator/riscv_sim.cpp‎

Lines changed: 49 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
enum {
3535
OPT_TRACE_OUTPUT = 1000,
3636
OPT_PRINT_CONFIG,
37+
OPT_VALIDATE_CONFIG,
3738
OPT_SAILCOV,
3839
OPT_ENABLE_EXPERIMENTAL_EXTENSIONS,
3940
OPT_PRINT_DTS,
@@ -42,6 +43,8 @@ enum {
4243
static bool do_show_times = false;
4344
bool do_report_arch = false;
4445
bool do_print_dts = false;
46+
char *config_file = NULL;
47+
bool do_validate_config = false;
4548
char *term_log = NULL;
4649
static const char *trace_log_path = NULL;
4750
FILE *trace_log = NULL;
@@ -101,27 +104,28 @@ char *sailcov_file = NULL;
101104
#endif
102105

103106
static struct option options[] = {
104-
{"device-tree-blob", required_argument, 0, 'b' },
105-
{"terminal-log", required_argument, 0, 't' },
106-
{"show-times", required_argument, 0, 'p' },
107-
{"report-arch", no_argument, 0, 'a' },
108-
{"test-signature", required_argument, 0, 'T' },
109-
{"signature-granularity", required_argument, 0, 'g' },
110-
{"rvfi-dii", required_argument, 0, 'r' },
111-
{"help", no_argument, 0, 'h' },
112-
{"config", required_argument, 0, 'c' },
113-
{"print-default-config", no_argument, 0, OPT_PRINT_CONFIG},
114-
{"trace", optional_argument, 0, 'v' },
115-
{"no-trace", optional_argument, 0, 'V' },
116-
{"trace-output", required_argument, 0, OPT_TRACE_OUTPUT},
117-
{"inst-limit", required_argument, 0, 'l' },
107+
{"device-tree-blob", required_argument, 0, 'b' },
108+
{"terminal-log", required_argument, 0, 't' },
109+
{"show-times", required_argument, 0, 'p' },
110+
{"report-arch", no_argument, 0, 'a' },
111+
{"test-signature", required_argument, 0, 'T' },
112+
{"signature-granularity", required_argument, 0, 'g' },
113+
{"rvfi-dii", required_argument, 0, 'r' },
114+
{"help", no_argument, 0, 'h' },
115+
{"config", required_argument, 0, 'c' },
116+
{"print-default-config", no_argument, 0, OPT_PRINT_CONFIG },
117+
{"validate-config", no_argument, 0, OPT_VALIDATE_CONFIG},
118+
{"trace", optional_argument, 0, 'v' },
119+
{"no-trace", optional_argument, 0, 'V' },
120+
{"trace-output", required_argument, 0, OPT_TRACE_OUTPUT },
121+
{"inst-limit", required_argument, 0, 'l' },
118122
{"enable-experimental-extensions", no_argument, 0,
119-
OPT_ENABLE_EXPERIMENTAL_EXTENSIONS },
123+
OPT_ENABLE_EXPERIMENTAL_EXTENSIONS },
120124
#ifdef SAILCOV
121-
{"sailcov-file", required_argument, 0, OPT_SAILCOV },
125+
{"sailcov-file", required_argument, 0, OPT_SAILCOV },
122126
#endif
123-
{"print-device-tree", no_argument, 0, OPT_PRINT_DTS },
124-
{0, 0, 0, 0 }
127+
{"print-device-tree", no_argument, 0, OPT_PRINT_DTS },
128+
{0, 0, 0, 0 }
125129
};
126130

127131
static void print_usage(const char *argv0, int ec)
@@ -139,6 +143,17 @@ static void print_usage(const char *argv0, int ec)
139143
exit(ec);
140144
}
141145

146+
static void validate_config(const char *conf_file)
147+
{
148+
const char *s = zconfig_is_valid(UNIT) ? "valid" : "invalid";
149+
if (conf_file) {
150+
fprintf(stdout, "Configuration in %s is %s.\n", conf_file, s);
151+
} else {
152+
fprintf(stdout, "Default configuration is %s.\n", s);
153+
}
154+
exit(0);
155+
}
156+
142157
static void report_arch(void)
143158
{
144159
fprintf(stdout, "RV%" PRIu64 "\n", zxlen);
@@ -248,6 +263,7 @@ static int process_args(int argc, char **argv)
248263
case 'c': {
249264
if (access(optarg, R_OK) == 0) {
250265
sail_config_set_file(optarg);
266+
config_file = strdup(optarg);
251267
have_config = true;
252268
} else {
253269
fprintf(stderr, "configuration file '%s' does not exist.\n", optarg);
@@ -258,6 +274,9 @@ static int process_args(int argc, char **argv)
258274
case OPT_PRINT_CONFIG:
259275
printf("%s", DEFAULT_JSON);
260276
exit(0);
277+
case OPT_VALIDATE_CONFIG:
278+
do_validate_config = true;
279+
break;
261280
case OPT_PRINT_DTS:
262281
do_print_dts = true;
263282
break;
@@ -319,14 +338,15 @@ static int process_args(int argc, char **argv)
319338
std::filesystem::remove(path);
320339
}
321340

322-
if (optind > argc || (optind == argc && !rvfi && !do_print_dts)) {
341+
if (optind > argc
342+
|| (optind == argc && !rvfi && !do_print_dts && !do_validate_config)) {
323343
fprintf(stderr, "No elf file provided.\n");
324344
print_usage(argv[0], 0);
325345
}
326346
if (dtb_file)
327347
read_dtb(dtb_file);
328348

329-
if (!rvfi && !do_report_arch && !do_print_dts)
349+
if (!rvfi && !do_report_arch && !do_print_dts && !do_validate_config)
330350
fprintf(stdout, "Running file %s.\n", argv[optind]);
331351
return optind;
332352
}
@@ -430,9 +450,9 @@ void init_sail_reset_vector(uint64_t entry)
430450
zPC = rom_base;
431451
}
432452

433-
void init_sail(uint64_t elf_entry)
453+
void init_sail(uint64_t elf_entry, const char *config_file)
434454
{
435-
zinit_model(UNIT);
455+
zinit_model(config_file != nullptr ? config_file : "");
436456
if (rvfi) {
437457
/*
438458
rv_ram_base = UINT64_C(0x80000000);
@@ -449,11 +469,11 @@ void init_sail(uint64_t elf_entry)
449469
}
450470

451471
/* reinitialize to clear state and memory, typically across tests runs */
452-
void reinit_sail(uint64_t elf_entry)
472+
void reinit_sail(uint64_t elf_entry, const char *config_file)
453473
{
454474
model_fini();
455475
model_init();
456-
init_sail(elf_entry);
476+
init_sail(elf_entry, config_file);
457477
}
458478

459479
void write_signature(const char *file)
@@ -658,6 +678,9 @@ int main(int argc, char **argv)
658678
if (do_report_arch) {
659679
report_arch();
660680
}
681+
if (do_validate_config) {
682+
validate_config(config_file);
683+
}
661684
if (do_print_dts) {
662685
print_dts();
663686
}
@@ -684,7 +707,7 @@ int main(int argc, char **argv)
684707
(void)load_sail(argv[i], /*main_file=*/false);
685708
}
686709

687-
init_sail(entry);
710+
init_sail(entry, config_file);
688711

689712
if (gettimeofday(&init_end, NULL) < 0) {
690713
fprintf(stderr, "Cannot gettimeofday: %s\n", strerror(errno));
@@ -695,7 +718,7 @@ int main(int argc, char **argv)
695718
run_sail();
696719
if (rvfi) {
697720
/* Reset for next test */
698-
reinit_sail(entry);
721+
reinit_sail(entry, config_file);
699722
}
700723
} while (rvfi);
701724

‎model/CMakeLists.txt‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -203,15 +203,21 @@ foreach (xlen IN ITEMS 32 64)
203203
endif()
204204

205205
set(sail_cfg_srcs
206+
"riscv_validate_config.sail"
206207
"riscv_device_tree.sail"
207208
)
208209

210+
set(sail_model_srcs
211+
"riscv_model.sail"
212+
)
213+
209214
# Final file list.
210215
set(sail_srcs
211216
${sail_arch_srcs}
212217
${sail_seq_inst_srcs}
213218
${sail_step_srcs}
214219
${sail_cfg_srcs}
220+
${sail_model_srcs}
215221
"main.sail"
216222
)
217223

@@ -268,6 +274,7 @@ foreach (xlen IN ITEMS 32 64)
268274
--c-preserve try_step
269275
--c-preserve tick_clock
270276
--c-preserve generate_dts
277+
--c-preserve config_is_valid
271278
# Preserve RVFI functions.
272279
--c-preserve rvfi_set_instr_packet
273280
--c-preserve rvfi_get_cmd

‎model/main.sail‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ function main() : unit -> unit = {
2828
print_bits("PC = ", PC);
2929

3030
try {
31-
init_model();
31+
init_model("");
3232
sail_end_cycle();
3333
loop()
3434
} catch {

‎model/riscv_model.sail‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
/*=======================================================================================*/
2+
/* This Sail RISC-V architecture model, comprising all files and */
3+
/* directories except where otherwise noted is subject the BSD */
4+
/* two-clause license in the LICENSE file. */
5+
/* */
6+
/* SPDX-License-Identifier: BSD-2-Clause */
7+
/*=======================================================================================*/
8+
9+
// Chip reset. This only does the minimum resets required by the RISC-V spec.
10+
function reset() -> unit = {
11+
reset_sys();
12+
reset_vmem();
13+
14+
// To allow model extensions (code outside this repo) to perform additional reset.
15+
ext_reset();
16+
}
17+
18+
// Initialize model state. This is only called once; not for every chip reset.
19+
function init_model(config_filename : string) -> unit = {
20+
assert(config_is_valid(), (if config_filename == ""
21+
then "Default config"
22+
else "Config in " ^ config_filename)
23+
^ " is invalid.");
24+
hart_state = HART_ACTIVE();
25+
init_platform();
26+
reset();
27+
}

‎model/riscv_step.sail‎

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -274,19 +274,3 @@ function loop () : unit -> unit = {
274274
}
275275
}
276276
}
277-
278-
// Chip reset. This only does the minimum resets required by the RISC-V spec.
279-
function reset() -> unit = {
280-
reset_sys();
281-
reset_vmem();
282-
283-
// To allow model extensions (code outside this repo) to perform additional reset.
284-
ext_reset();
285-
}
286-
287-
// Initialize model state. This is only called once; not for every chip reset.
288-
function init_model() -> unit = {
289-
hart_state = HART_ACTIVE();
290-
init_platform();
291-
reset();
292-
}

‎model/riscv_validate_config.sail‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
/*=======================================================================================*/
2+
/* This Sail RISC-V architecture model, comprising all files and */
3+
/* directories except where otherwise noted is subject the BSD */
4+
/* two-clause license in the LICENSE file. */
5+
/* */
6+
/* SPDX-License-Identifier: BSD-2-Clause */
7+
/*=======================================================================================*/
8+
9+
function check_privs() -> bool = {
10+
if hartSupports(Ext_S) & not(hartSupports(Ext_U))
11+
then {
12+
print_endline("User mode (U) should be enabled if supervisor mode (S) is enabled.");
13+
return false;
14+
};
15+
true
16+
}
17+
18+
// This logic will need to change once MXL/SXL/UXL can differ.
19+
function check_mmu_config() -> bool = {
20+
var valid : bool = true;
21+
if xlen == 64 then {
22+
if not(hartSupports(Ext_S)) & (hartSupports(Ext_Sv57) | hartSupports(Ext_Sv48) | hartSupports(Ext_Sv39))
23+
then {
24+
valid = false;
25+
print_endline("Supervisor mode (S) disabled but one of (Sv57, Sv48, Sv39) is enabled: cannot support address translation without supervisor mode.");
26+
};
27+
if hartSupports(Ext_Sv57) & not(hartSupports(Ext_Sv48))
28+
then {
29+
valid = false;
30+
print_endline("Sv57 is enabled but Sv48 is disabled: supporting Sv57 requires supporting Sv48.");
31+
};
32+
if hartSupports(Ext_Sv48) & not(hartSupports(Ext_Sv39))
33+
then {
34+
valid = false;
35+
print_endline("Sv48 is enabled but Sv39 is disabled: supporting Sv48 requires supporting Sv39.");
36+
};
37+
if hartSupports(Ext_Sv32)
38+
then {
39+
valid = false;
40+
print_endline("Sv32 is enabled: Sv32 is not supported on RV64.");
41+
};
42+
} else {
43+
assert(xlen == 32);
44+
if not(hartSupports(Ext_S)) & hartSupports(Ext_Sv32)
45+
then {
46+
valid = false;
47+
print_endline("Supervisor mode (S) is disabled but Sv32 is enabled: cannot support address translation without supervisor mode.");
48+
};
49+
if hartSupports(Ext_Sv39) | hartSupports(Ext_Sv48) | hartSupports(Ext_Sv57)
50+
then {
51+
valid = false;
52+
print_endline("One or more of Sv39/Sv48/Sv57 is enabled: these are not supported on RV32.");
53+
};
54+
};
55+
valid
56+
}
57+
58+
function check_vlen_elen() -> bool = {
59+
// Should this be conditioned on a vector extension being enabled?
60+
if VLEN_pow < ELEN_pow
61+
then {
62+
print_endline("VLEN (set to 2^" ^ dec_str(VLEN_pow) ^ ") cannot be less than ELEN (set to 2^" ^ dec_str(ELEN_pow) ^ ").");
63+
return false;
64+
};
65+
true
66+
}
67+
68+
function has_overlap(a_lo : nat, a_hi : nat, b_lo : nat, b_hi : nat) -> bool = {
69+
not((a_lo < b_lo & a_hi < b_lo) | (b_lo < a_lo & b_hi < a_lo))
70+
}
71+
72+
// This will change when we have a more general memory layout.
73+
function check_mem_layout() -> bool = {
74+
var valid : bool = true;
75+
// Memory regions should not overlap. There are currently only three: ram, rom and clint.
76+
let ram_lo = unsigned(plat_ram_base);
77+
let ram_hi = unsigned(plat_ram_base) + unsigned(plat_ram_size);
78+
let rom_lo = unsigned(plat_rom_base);
79+
let rom_hi = unsigned(plat_rom_base) + unsigned(plat_rom_size);
80+
let clint_lo = unsigned(plat_clint_base);
81+
let clint_hi = unsigned(plat_clint_base) + unsigned(plat_clint_size);
82+
if has_overlap(rom_lo, rom_hi, ram_lo, ram_hi)
83+
then {
84+
valid = false;
85+
print_endline("The RAM and ROM regions overlap.");
86+
};
87+
if has_overlap(clint_lo, clint_hi, rom_lo, rom_hi)
88+
then {
89+
valid = false;
90+
print_endline("The Clint and ROM regions overlap.");
91+
};
92+
if has_overlap(clint_lo, clint_hi, ram_lo, ram_hi)
93+
then {
94+
valid = false;
95+
print_endline("The Clint and RAM regions overlap.");
96+
};
97+
98+
// Should memory regions also be 4K aligned?
99+
valid
100+
}
101+
102+
function config_is_valid() -> bool = {
103+
check_privs()
104+
& check_mmu_config()
105+
& check_mem_layout()
106+
& check_vlen_elen()
107+
}

0 commit comments

Comments
 (0)