diff --git a/model_checking/sail_decoder/lib.rs b/model_checking/sail_decoder/lib.rs index 7e27d8ca..374578de 100644 --- a/model_checking/sail_decoder/lib.rs +++ b/model_checking/sail_decoder/lib.rs @@ -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)) diff --git a/model_checking/src/adapters.rs b/model_checking/src/adapters.rs index 2812d999..cf43ca26 100644 --- a/model_checking/src/adapters.rs +++ b/model_checking/src/adapters.rs @@ -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), diff --git a/src/decoder.rs b/src/decoder.rs index 15502f8d..4f93ba3b 100644 --- a/src/decoder.rs +++ b/src/decoder.rs @@ -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 { @@ -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, @@ -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.