Skip to content

Commit

Permalink
Remove Ecall and Ebreak from Instr
Browse files Browse the repository at this point in the history
The ECALL and EBREAK instructions have distinct mcause values and are
not considered illegal instructions. Since they trigger different types
of traps, they do not require decoding in our decoder for illegal
instructions. As a result, we can safely remove them from the
instruction decoder.
  • Loading branch information
francois141 authored and CharlyCst committed Jan 27, 2025
1 parent 382b5e7 commit 4a49aef
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 16 deletions.
6 changes: 0 additions & 6 deletions model_checking/sail_decoder/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,12 +101,6 @@ pub fn encdec_backwards(sail_ctx: &mut SailVirtCtx, arg_hashtag_: BitVector<32>)
v__7 if { (v__7 == BitVector::<32>::new(0b00010000010100000000000001110011)) } => {
ast::WFI(())
}
v__13 if { (v__13 == BitVector::<32>::new(0b00000000000000000000000001110011)) } => {
ast::ECALL(())
}
v__19 if { (v__19 == BitVector::<32>::new(0b00000000000100000000000001110011)) } => {
ast::EBREAK(())
}
v__25
if {
((v__25.subrange::<25, 32, 7>() == BitVector::<7>::new(0b0001001))
Expand Down
4 changes: 2 additions & 2 deletions model_checking/src/adapters.rs
Original file line number Diff line number Diff line change
Expand Up @@ -447,8 +447,8 @@ pub fn ast_to_miralis_instr(ast_entry: ast) -> Instr {
match ast_entry {
ast::MRET(()) => Instr::Mret,
ast::WFI(()) => Instr::Wfi,
ast::ECALL(()) => Instr::Ecall,
ast::EBREAK(()) => Instr::Ebreak,
ast::ECALL(()) => panic!("Miralis does not need to decode ecalls"),
ast::EBREAK(()) => panic!("Miralis does not need to decode ebreaks"),
ast::SFENCE_VMA((rs1, rs2)) => Instr::Sfencevma {
rs1: Register::from(rs1.bits as usize),
rs2: Register::from(rs2.bits as usize),
Expand Down
8 changes: 0 additions & 8 deletions src/decoder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@ use crate::logger;
/// A RISC-V instruction.
#[derive(Debug, PartialEq, Eq, Clone)]
pub enum Instr {
Ecall,
Ebreak,
Wfi,
/// CSR Read/Write
Csrrw {
Expand Down Expand Up @@ -110,8 +108,6 @@ impl MiralisContext {
let func7 = (raw >> 25) & 0b1111111;
if func3 == 0b000 {
return match imm {
0b000000000000 => Instr::Ecall,
0b000000000001 => Instr::Ebreak,
0b000100000101 => Instr::Wfi,
0b001100000010 => Instr::Mret,
0b000100000010 => Instr::Sret,
Expand Down Expand Up @@ -872,10 +868,6 @@ mod tests {
#[test]
fn system_instructions() {
let mctx = MiralisContext::new(unsafe { Arch::detect_hardware() }, 0x100000, 0x2000);
// ECALL: Environment call.
assert_eq!(mctx.decode_illegal_instruction(0x00000073), Instr::Ecall);
// EBREAK: Environment break.
assert_eq!(mctx.decode_illegal_instruction(0x00100073), Instr::Ebreak);
// MRET: Return from machine mode.
assert_eq!(mctx.decode_illegal_instruction(0x30200073), Instr::Mret);
// SRET: Return from supervisor mode.
Expand Down

0 comments on commit 4a49aef

Please sign in to comment.