Skip to content

libs: new module for testing crucible-mir intrinsics #236

@samcowger

Description

@samcowger

Most intrinsics in crucible-mir's Mir.Intrinsics can (and do) have their behavior exercised by crux-mir test cases written in Rust, because it is usually feasible to write Rust that's known to invoke a particular intrinsic. However, for some intrinsics, there is no Rust function or code pattern that naturally leads to their execution - they're only used by/useful for clients of crucible-mir other than crux-mir. For example, there is no Rust translation path that leverages mirRef_indexAndLen* functionality. Its only use comes from saw-script's crucible-mir-comp, in Mir.Compositional.Builder.regToSetup. So, within crucible proper, mirRef_indexAndLen* is untested and untestable. (This lack of testing helped to obfuscate a bug I inadvertently introduced in its implementation - see GaloisInc/crucible#1704 (comment).)

We can address this by defining a new module in our crucible Rust crate whose purpose is to define stub functions that crux-mir test cases can override with internal intrinsics' behavior in order to test them, specifically for intrinsics with no other natural Rust equivalent. I might suggest something like crucible::intrinsics. For indexAndLen, then, we might expect to see a function there like:

pub fn index_and_len<T>(elem: *const T) -> (usize, usize) {
  unimplemented!()
}

Then, we could define an override in Mir.TransCustom that targets crucible::intrinsics::index_and_len and directs it to leverage mirRef_indexAndLen*, so that we could write test cases in crucible-mir like:

#[crux::test]
fn foo() {
  let xs = [0u8; 6];
  let x = xs[2];
  let (idx, len) = crucible::intrinsics::index_and_len(&raw const x);
  assert_eq!(idx, 2);
  assert_eq!(len, 6);
}

Metadata

Metadata

Assignees

Labels

enhancementstandard librariesIssues involving mir-json's modified versions of the Rust standard libraries

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions