Skip to content

Commit 754e168

Browse files
author
Weiwei Li
committed
revert modification for translation functions
simplify clean_inval to only do LOAD permission check
1 parent 7b39e3f commit 754e168

File tree

9 files changed

+20
-43
lines changed

9 files changed

+20
-43
lines changed

‎c_emulator/riscv_sim.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -342,7 +342,7 @@ char *process_args(int argc, char **argv)
342342
#endif
343343
case 'B':
344344
block_size = atol(optarg);
345-
if (((block_size & 7) == 0) && (block_size < 4096)) {
345+
if (((block_size & (block_size - 1))) == 0 && (block_size < 4096)) {
346346
fprintf(stderr, "setting cache-block-size to %" PRIu64 " B\n", block_size);
347347
rv_cache_block_size = block_size;
348348
} else {

‎model/riscv_insts_zicbom.sail‎

Lines changed: 7 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -25,29 +25,19 @@ mapping clause assembly = RISCV_ZICBOM(cbop, rs1)
2525

2626
val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
2727
function process_clean_inval(vaddr, width, clean, inval) = {
28-
match ext_data_get_addr(zeros(), vaddr, Cbo(Data), BYTE) {
28+
match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) {
2929
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
3030
Ext_DataAddr_OK(vaddr) => {
31-
let data: option(ExceptionType) = match translateAddr(vaddr, Cbo(Data)) {
32-
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Data), cur_privilege),
31+
let data: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
32+
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Read(Data), cur_privilege),
3333
TR_Failure(e, _) => Some(e)
3434
};
3535
match data {
3636
None() => RETIRE_SUCCESS,
37-
Some(de) => {
38-
let fetch: option(ExceptionType) = match translateAddr(vaddr, Cbo(Fetch)) {
39-
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Fetch), cur_privilege),
40-
TR_Failure(e, _) => Some(e)
41-
};
42-
match fetch {
43-
None() => RETIRE_SUCCESS,
44-
Some(fe) =>
45-
match (de, fe) {
46-
(E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
47-
(_, E_SAMO_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
48-
(E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
49-
(_, E_SAMO_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }
50-
}
37+
Some(e) => {
38+
match (e) {
39+
E_Load_Access_Fault() => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
40+
E_Load_Page_Fault() => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }
5141
}
5242
}
5343
}

‎model/riscv_mem.sail‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
118118
}) : option((bits(8 * 'n), mem_meta));
119119
match (t, result) {
120120
(Execute(), None()) => MemException(E_Fetch_Access_Fault()),
121-
(Read(_), None()) => MemException(E_Load_Access_Fault()),
121+
(Read(Data), None()) => MemException(E_Load_Access_Fault()),
122122
(_, None()) => MemException(E_SAMO_Access_Fault()),
123123
(_, Some(v, m)) => { if get_config_print_mem()
124124
then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v));
@@ -136,7 +136,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
136136
Ext_PhysAddr_Error(e) => MemException(e)
137137
} else match t {
138138
Execute() => MemException(E_Fetch_Access_Fault()),
139-
Read(_) => MemException(E_Load_Access_Fault()),
139+
Read(Data) => MemException(E_Load_Access_Fault()),
140140
_ => MemException(E_SAMO_Access_Fault())
141141
}
142142

‎model/riscv_platform.sail‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -266,7 +266,7 @@ function clint_load(t, addr, width) = {
266266
then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
267267
match t {
268268
Execute() => MemException(E_Fetch_Access_Fault()),
269-
Read(_) => MemException(E_Load_Access_Fault()),
269+
Read(Data) => MemException(E_Load_Access_Fault()),
270270
_ => MemException(E_SAMO_Access_Fault())
271271
}
272272
}
@@ -380,7 +380,7 @@ function htif_load(t, paddr, width) = {
380380
then MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */
381381
else match t {
382382
Execute() => MemException(E_Fetch_Access_Fault()),
383-
Read(_) => MemException(E_Load_Access_Fault()),
383+
Read(Data) => MemException(E_Load_Access_Fault()),
384384
_ => MemException(E_SAMO_Access_Fault())
385385
}
386386
}
@@ -473,7 +473,7 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc
473473
then htif_load(t, paddr, width)
474474
else match t {
475475
Execute() => MemException(E_Fetch_Access_Fault()),
476-
Read(_) => MemException(E_Load_Access_Fault()),
476+
Read(Data) => MemException(E_Load_Access_Fault()),
477477
_ => MemException(E_SAMO_Access_Fault())
478478
}
479479

‎model/riscv_pmp_control.sail‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -100,9 +100,7 @@ function pmpCheckRWX(ent, acc) = {
100100
Read(_) => ent.R() == 0b1,
101101
Write(_) => ent.W() == 0b1,
102102
ReadWrite(_) => ent.R() == 0b1 & ent.W() == 0b1,
103-
Execute() => ent.X() == 0b1,
104-
Cbo(Data) => ent.R() == 0b1 | ent.W() == 0b1,
105-
Cbo(Fetch) => ent.X() == 0b1
103+
Execute() => ent.X() == 0b1
106104
}
107105
}
108106

@@ -228,8 +226,7 @@ function pmpCheck_xlen (addr: xlenbits, width: xlenbits, acc: AccessType(ext_acc
228226
Read(_) => Some(E_Load_Access_Fault()),
229227
Write(_) => Some(E_SAMO_Access_Fault()),
230228
ReadWrite(_) => Some(E_SAMO_Access_Fault()),
231-
Execute() => Some(E_Fetch_Access_Fault()),
232-
Cbo(_) => Some(E_SAMO_Access_Fault())
229+
Execute() => Some(E_Fetch_Access_Fault())
233230
}
234231
}
235232

‎model/riscv_pte.sail‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -125,15 +125,11 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
125125
(Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
126126
(ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
127127
(Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),
128-
(Cbo(Data), User) => to_pte_check(p.U() == 0b1 & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))),
129-
(Cbo(Fetch), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),
130128

131129
(Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
132130
(Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1),
133131
(ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
134132
(Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),
135-
(Cbo(Data), Supervisor) => to_pte_check((p.U() == 0b1 | do_sum) & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))),
136-
(Cbo(Fetch), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),
137133

138134
(_, Machine) => internal_error("m-mode mem perm check")
139135
}
@@ -143,8 +139,7 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex
143139
let update_d = p.D() == 0b0 & (match a { // dirty-bit
144140
Execute() => false,
145141
Read() => false,
146-
Write(Data) => true,
147-
Cbo(_) => false,
142+
Write(_) => true,
148143
ReadWrite(_,_) => true
149144
});
150145

‎model/riscv_ptw.sail‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -111,9 +111,7 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) ->
111111
(Write(_), PTW_Access()) => E_SAMO_Access_Fault(),
112112
(Write(_), _) => E_SAMO_Page_Fault(),
113113
(Execute(), PTW_Access()) => E_Fetch_Access_Fault(),
114-
(Execute(), _) => E_Fetch_Page_Fault(),
115-
(Cbo(_), PTW_Access()) => E_SAMO_Access_Fault(),
116-
(Cbo(_), _) => E_SAMO_Page_Fault()
114+
(Execute(), _) => E_Fetch_Page_Fault()
117115
} in {
118116
/* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
119117
e

‎model/riscv_types.sail‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,6 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
168168
union AccessType ('a : Type) = {
169169
Read : 'a,
170170
Write : 'a,
171-
Cbo : 'a,
172171
ReadWrite : ('a, 'a),
173172
Execute : unit
174173
}
@@ -391,8 +390,8 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR,
391390
AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */
392391
enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */
393392

394-
enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* zicbom ops */
395-
enum prop_zicbop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* zicbop ops */
393+
enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* zicbom ops*/
394+
enum prop_zicbop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* zicbop ops*/
396395

397396
enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD}
398397

‎model/riscv_vmem_types.sail‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,6 @@
7171
type ext_access_type = unit
7272

7373
let Data : ext_access_type = ()
74-
let Fetch : ext_access_type = ()
7574

7675
let default_write_acc : ext_access_type = Data
7776

@@ -81,8 +80,7 @@ function accessType_to_str (a) =
8180
Read(_) => "R",
8281
Write(_) => "W",
8382
ReadWrite(_, _) => "RW",
84-
Execute() => "X",
85-
Cbo(_) => "RWX"
83+
Execute() => "X"
8684
}
8785

8886
overload to_str = {accessType_to_str}

0 commit comments

Comments
 (0)