Skip to content

Commit

Permalink
Fix build errors with kani
Browse files Browse the repository at this point in the history
Signed-off-by: Sangwan Kwon <[email protected]>
  • Loading branch information
bitboom committed Nov 21, 2024
1 parent 2248bf9 commit 66fa71a
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 2 deletions.
11 changes: 9 additions & 2 deletions rmm/src/monitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,10 @@ pub struct Monitor {
#[cfg(kani)]
// `rsi` and `page_table` are removed in model checking harnesses
// to reduce overall state space
pub struct Monitor {}
pub struct Monitor {
pub rmi: RmiHandle,
mainloop: Mainloop,
}

impl Monitor {
#[cfg(not(kani))]
Expand All @@ -31,7 +34,10 @@ impl Monitor {

#[cfg(kani)]
pub fn new() -> Self {
Self {}
Self {
rmi: RmiHandle::new(),
mainloop: Mainloop::new(),
}
}

#[cfg(not(kani))]
Expand Down Expand Up @@ -132,6 +138,7 @@ impl Monitor {
}

pub fn handle_rsi(&self, ctx: &mut Context, rec: &mut Rec<'_>, run: &mut Run) -> usize {
#[cfg(not(kani))]
match self.rsi.on_event.get(&ctx.cmd) {
Some(handler) => {
ctx.do_rsi(|arg, ret| handler(arg, ret, self, rec, run));
Expand Down
3 changes: 3 additions & 0 deletions rmm/src/rmi/rtt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ pub fn set_event_handler(rmi: &mut RmiHandle) {

// The below is added to avoid a fault regarding the RTT entry
// during the `create_pgtbl_at()` in `rtt::create()`.
#[cfg(not(kani))]
rmm.page_table.map(rtt_addr, true);
rtt::create(&rd, rtt_addr, ipa, level)?;
set_granule(&mut rtt_granule, GranuleState::RTT)?;
Expand Down Expand Up @@ -197,8 +198,10 @@ pub fn set_event_handler(rmi: &mut RmiHandle) {
rmm.page_table.map(target_pa, true);

// copy src to target
#[cfg(not(kani))]
rmm.page_table.map(src_pa, false);
host::copy_to_obj::<DataPage>(src_pa, &mut target_page).ok_or(Error::RmiErrorInput)?;
#[cfg(not(kani))]
rmm.page_table.unmap(src_pa);

// map ipa to taget_pa in S2 table
Expand Down

0 comments on commit 66fa71a

Please sign in to comment.