Skip to content

Commit

Permalink
revert modification for translation functions
Browse files Browse the repository at this point in the history 
simplify clean_inval to only do LOAD permission check
  • Loading branch information
Weiwei Li committed Jan 12, 2022
1 parent 7b39e3f commit 754e168
Show file tree
Hide file tree
Showing 9 changed files with 20 additions and 43 deletions.
2 changes: 1 addition & 1 deletion c_emulator/riscv_sim.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -342,7 +342,7 @@ char *process_args(int argc, char **argv)
#endif
case 'B':
block_size = atol(optarg);
if (((block_size & 7) == 0) && (block_size < 4096)) {
if (((block_size & (block_size - 1))) == 0 && (block_size < 4096)) {
fprintf(stderr, "setting cache-block-size to %" PRIu64 " B\n", block_size);
rv_cache_block_size = block_size;
} else {
Expand Down
24 changes: 7 additions & 17 deletions model/riscv_insts_zicbom.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,29 +25,19 @@ mapping clause assembly = RISCV_ZICBOM(cbop, rs1)

val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_clean_inval(vaddr, width, clean, inval) = {
match ext_data_get_addr(zeros(), vaddr, Cbo(Data), BYTE) {
match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let data: option(ExceptionType) = match translateAddr(vaddr, Cbo(Data)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Data), cur_privilege),
let data: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Read(Data), cur_privilege),
TR_Failure(e, _) => Some(e)
};
match data {
None() => RETIRE_SUCCESS,
Some(de) => {
let fetch: option(ExceptionType) = match translateAddr(vaddr, Cbo(Fetch)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Fetch), cur_privilege),
TR_Failure(e, _) => Some(e)
};
match fetch {
None() => RETIRE_SUCCESS,
Some(fe) =>
match (de, fe) {
(E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
(_, E_SAMO_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
(E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
(_, E_SAMO_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }
}
Some(e) => {
match (e) {
E_Load_Access_Fault() => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
E_Load_Page_Fault() => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,7 +118,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
}) : option((bits(8 * 'n), mem_meta));
match (t, result) {
(Execute(), None()) => MemException(E_Fetch_Access_Fault()),
(Read(_), None()) => MemException(E_Load_Access_Fault()),
(Read(Data), None()) => MemException(E_Load_Access_Fault()),
(_, None()) => MemException(E_SAMO_Access_Fault()),
(_, Some(v, m)) => { if get_config_print_mem()
then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v));
Expand All @@ -136,7 +136,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
Ext_PhysAddr_Error(e) => MemException(e)
} else match t {
Execute() => MemException(E_Fetch_Access_Fault()),
Read(_) => MemException(E_Load_Access_Fault()),
Read(Data) => MemException(E_Load_Access_Fault()),
_ => MemException(E_SAMO_Access_Fault())
}

Expand Down
6 changes: 3 additions & 3 deletions model/riscv_platform.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ function clint_load(t, addr, width) = {
then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
match t {
Execute() => MemException(E_Fetch_Access_Fault()),
Read(_) => MemException(E_Load_Access_Fault()),
Read(Data) => MemException(E_Load_Access_Fault()),
_ => MemException(E_SAMO_Access_Fault())
}
}
Expand Down Expand Up @@ -380,7 +380,7 @@ function htif_load(t, paddr, width) = {
then MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */
else match t {
Execute() => MemException(E_Fetch_Access_Fault()),
Read(_) => MemException(E_Load_Access_Fault()),
Read(Data) => MemException(E_Load_Access_Fault()),
_ => MemException(E_SAMO_Access_Fault())
}
}
Expand Down Expand Up @@ -473,7 +473,7 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc
then htif_load(t, paddr, width)
else match t {
Execute() => MemException(E_Fetch_Access_Fault()),
Read(_) => MemException(E_Load_Access_Fault()),
Read(Data) => MemException(E_Load_Access_Fault()),
_ => MemException(E_SAMO_Access_Fault())
}

Expand Down
7 changes: 2 additions & 5 deletions model/riscv_pmp_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,9 +100,7 @@ function pmpCheckRWX(ent, acc) = {
Read(_) => ent.R() == 0b1,
Write(_) => ent.W() == 0b1,
ReadWrite(_) => ent.R() == 0b1 & ent.W() == 0b1,
Execute() => ent.X() == 0b1,
Cbo(Data) => ent.R() == 0b1 | ent.W() == 0b1,
Cbo(Fetch) => ent.X() == 0b1
Execute() => ent.X() == 0b1
}
}

Expand Down Expand Up @@ -228,8 +226,7 @@ function pmpCheck_xlen (addr: xlenbits, width: xlenbits, acc: AccessType(ext_acc
Read(_) => Some(E_Load_Access_Fault()),
Write(_) => Some(E_SAMO_Access_Fault()),
ReadWrite(_) => Some(E_SAMO_Access_Fault()),
Execute() => Some(E_Fetch_Access_Fault()),
Cbo(_) => Some(E_SAMO_Access_Fault())
Execute() => Some(E_Fetch_Access_Fault())
}
}

Expand Down
7 changes: 1 addition & 6 deletions model/riscv_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,15 +125,11 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
(Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
(ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),
(Cbo(Data), User) => to_pte_check(p.U() == 0b1 & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))),
(Cbo(Fetch), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),

(Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1),
(ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),
(Cbo(Data), Supervisor) => to_pte_check((p.U() == 0b1 | do_sum) & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))),
(Cbo(Fetch), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),

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

Expand Down
4 changes: 1 addition & 3 deletions model/riscv_ptw.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,9 +111,7 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) ->
(Write(_), PTW_Access()) => E_SAMO_Access_Fault(),
(Write(_), _) => E_SAMO_Page_Fault(),
(Execute(), PTW_Access()) => E_Fetch_Access_Fault(),
(Execute(), _) => E_Fetch_Page_Fault(),
(Cbo(_), PTW_Access()) => E_SAMO_Access_Fault(),
(Cbo(_), _) => E_SAMO_Page_Fault()
(Execute(), _) => E_Fetch_Page_Fault()
} in {
/* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
e
Expand Down
5 changes: 2 additions & 3 deletions model/riscv_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,6 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
union AccessType ('a : Type) = {
Read : 'a,
Write : 'a,
Cbo : 'a,
ReadWrite : ('a, 'a),
Execute : unit
}
Expand Down Expand Up @@ -391,8 +390,8 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR,
AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */
enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */

enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* zicbom ops */
enum prop_zicbop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* zicbop ops */
enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* zicbom ops*/
enum prop_zicbop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* zicbop ops*/

enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD}

Expand Down
4 changes: 1 addition & 3 deletions model/riscv_vmem_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,6 @@
type ext_access_type = unit

let Data : ext_access_type = ()
let Fetch : ext_access_type = ()

let default_write_acc : ext_access_type = Data

Expand All @@ -81,8 +80,7 @@ function accessType_to_str (a) =
Read(_) => "R",
Write(_) => "W",
ReadWrite(_, _) => "RW",
Execute() => "X",
Cbo(_) => "RWX"
Execute() => "X"
}

overload to_str = {accessType_to_str}

0 comments on commit 754e168

Please sign in to comment.