transmutability: Refactor tests for simplicity
This commit is contained in:
parent
78f2104e33
commit
b7fbf20fe1
1 changed files with 74 additions and 66 deletions
|
@ -1,93 +1,115 @@
|
||||||
use itertools::Itertools;
|
use itertools::Itertools;
|
||||||
|
|
||||||
use super::query_context::test::{Def, UltraMinimal};
|
use super::query_context::test::{Def, UltraMinimal};
|
||||||
use crate::maybe_transmutable::MaybeTransmutableQuery;
|
use crate::{Answer, Assume, Reason, layout};
|
||||||
use crate::{Reason, layout};
|
|
||||||
|
type Tree = layout::Tree<Def, !>;
|
||||||
|
type Dfa = layout::Dfa<!>;
|
||||||
|
|
||||||
|
trait Representation {
|
||||||
|
fn is_transmutable(src: Self, dst: Self, assume: Assume) -> Answer<!>;
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Representation for Tree {
|
||||||
|
fn is_transmutable(src: Self, dst: Self, assume: Assume) -> Answer<!> {
|
||||||
|
crate::maybe_transmutable::MaybeTransmutableQuery::new(src, dst, assume, UltraMinimal)
|
||||||
|
.answer()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Representation for Dfa {
|
||||||
|
fn is_transmutable(src: Self, dst: Self, assume: Assume) -> Answer<!> {
|
||||||
|
crate::maybe_transmutable::MaybeTransmutableQuery::new(src, dst, assume, UltraMinimal)
|
||||||
|
.answer()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn is_transmutable<R: Representation + Clone>(
|
||||||
|
src: &R,
|
||||||
|
dst: &R,
|
||||||
|
assume: Assume,
|
||||||
|
) -> crate::Answer<!> {
|
||||||
|
let src = src.clone();
|
||||||
|
let dst = dst.clone();
|
||||||
|
// The only dimension of the transmutability analysis we want to test
|
||||||
|
// here is the safety analysis. To ensure this, we disable all other
|
||||||
|
// toggleable aspects of the transmutability analysis.
|
||||||
|
R::is_transmutable(src, dst, assume)
|
||||||
|
}
|
||||||
|
|
||||||
mod safety {
|
mod safety {
|
||||||
use super::*;
|
use super::*;
|
||||||
use crate::Answer;
|
use crate::Answer;
|
||||||
|
|
||||||
type Tree = layout::Tree<Def, !>;
|
|
||||||
|
|
||||||
const DST_HAS_SAFETY_INVARIANTS: Answer<!> =
|
const DST_HAS_SAFETY_INVARIANTS: Answer<!> =
|
||||||
Answer::No(crate::Reason::DstMayHaveSafetyInvariants);
|
Answer::No(crate::Reason::DstMayHaveSafetyInvariants);
|
||||||
|
|
||||||
fn is_transmutable(src: &Tree, dst: &Tree, assume_safety: bool) -> crate::Answer<!> {
|
|
||||||
let src = src.clone();
|
|
||||||
let dst = dst.clone();
|
|
||||||
// The only dimension of the transmutability analysis we want to test
|
|
||||||
// here is the safety analysis. To ensure this, we disable all other
|
|
||||||
// toggleable aspects of the transmutability analysis.
|
|
||||||
let assume = crate::Assume {
|
|
||||||
alignment: true,
|
|
||||||
lifetimes: true,
|
|
||||||
validity: true,
|
|
||||||
safety: assume_safety,
|
|
||||||
};
|
|
||||||
crate::maybe_transmutable::MaybeTransmutableQuery::new(src, dst, assume, UltraMinimal)
|
|
||||||
.answer()
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn src_safe_dst_safe() {
|
fn src_safe_dst_safe() {
|
||||||
let src = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
let src = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
||||||
let dst = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
let dst = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
||||||
assert_eq!(is_transmutable(&src, &dst, false), Answer::Yes);
|
assert_eq!(is_transmutable(&src, &dst, Assume::default()), Answer::Yes);
|
||||||
assert_eq!(is_transmutable(&src, &dst, true), Answer::Yes);
|
assert_eq!(
|
||||||
|
is_transmutable(&src, &dst, Assume { safety: true, ..Assume::default() }),
|
||||||
|
Answer::Yes
|
||||||
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn src_safe_dst_unsafe() {
|
fn src_safe_dst_unsafe() {
|
||||||
let src = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
let src = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
||||||
let dst = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
let dst = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
||||||
assert_eq!(is_transmutable(&src, &dst, false), DST_HAS_SAFETY_INVARIANTS);
|
assert_eq!(is_transmutable(&src, &dst, Assume::default()), DST_HAS_SAFETY_INVARIANTS);
|
||||||
assert_eq!(is_transmutable(&src, &dst, true), Answer::Yes);
|
assert_eq!(
|
||||||
|
is_transmutable(&src, &dst, Assume { safety: true, ..Assume::default() }),
|
||||||
|
Answer::Yes
|
||||||
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn src_unsafe_dst_safe() {
|
fn src_unsafe_dst_safe() {
|
||||||
let src = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
let src = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
||||||
let dst = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
let dst = Tree::Def(Def::NoSafetyInvariants).then(Tree::u8());
|
||||||
assert_eq!(is_transmutable(&src, &dst, false), Answer::Yes);
|
assert_eq!(is_transmutable(&src, &dst, Assume::default()), Answer::Yes);
|
||||||
assert_eq!(is_transmutable(&src, &dst, true), Answer::Yes);
|
assert_eq!(
|
||||||
|
is_transmutable(&src, &dst, Assume { safety: true, ..Assume::default() }),
|
||||||
|
Answer::Yes
|
||||||
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn src_unsafe_dst_unsafe() {
|
fn src_unsafe_dst_unsafe() {
|
||||||
let src = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
let src = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
||||||
let dst = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
let dst = Tree::Def(Def::HasSafetyInvariants).then(Tree::u8());
|
||||||
assert_eq!(is_transmutable(&src, &dst, false), DST_HAS_SAFETY_INVARIANTS);
|
assert_eq!(is_transmutable(&src, &dst, Assume::default()), DST_HAS_SAFETY_INVARIANTS);
|
||||||
assert_eq!(is_transmutable(&src, &dst, true), Answer::Yes);
|
assert_eq!(
|
||||||
|
is_transmutable(&src, &dst, Assume { safety: true, ..Assume::default() }),
|
||||||
|
Answer::Yes
|
||||||
|
);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
mod bool {
|
mod bool {
|
||||||
use super::*;
|
use super::*;
|
||||||
use crate::Answer;
|
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn should_permit_identity_transmutation_tree() {
|
fn should_permit_identity_transmutation_tree() {
|
||||||
let answer = crate::maybe_transmutable::MaybeTransmutableQuery::new(
|
let src = Tree::bool();
|
||||||
layout::Tree::<Def, !>::bool(),
|
assert_eq!(is_transmutable(&src, &src, Assume::default()), Answer::Yes);
|
||||||
layout::Tree::<Def, !>::bool(),
|
assert_eq!(
|
||||||
crate::Assume { alignment: false, lifetimes: false, validity: true, safety: false },
|
is_transmutable(&src, &src, Assume { validity: true, ..Assume::default() }),
|
||||||
UltraMinimal,
|
Answer::Yes
|
||||||
)
|
);
|
||||||
.answer();
|
|
||||||
assert_eq!(answer, Answer::Yes);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn should_permit_identity_transmutation_dfa() {
|
fn should_permit_identity_transmutation_dfa() {
|
||||||
let answer = crate::maybe_transmutable::MaybeTransmutableQuery::new(
|
let src = Dfa::bool();
|
||||||
layout::Dfa::<!>::bool(),
|
assert_eq!(is_transmutable(&src, &src, Assume::default()), Answer::Yes);
|
||||||
layout::Dfa::<!>::bool(),
|
assert_eq!(
|
||||||
crate::Assume { alignment: false, lifetimes: false, validity: true, safety: false },
|
is_transmutable(&src, &src, Assume { validity: true, ..Assume::default() }),
|
||||||
UltraMinimal,
|
Answer::Yes
|
||||||
)
|
);
|
||||||
.answer();
|
|
||||||
assert_eq!(answer, Answer::Yes);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
|
@ -122,13 +144,7 @@ mod bool {
|
||||||
if src_set.is_subset(&dst_set) {
|
if src_set.is_subset(&dst_set) {
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
Answer::Yes,
|
Answer::Yes,
|
||||||
MaybeTransmutableQuery::new(
|
is_transmutable(&src_layout, &dst_layout, Assume::default()),
|
||||||
src_layout.clone(),
|
|
||||||
dst_layout.clone(),
|
|
||||||
crate::Assume { validity: false, ..crate::Assume::default() },
|
|
||||||
UltraMinimal,
|
|
||||||
)
|
|
||||||
.answer(),
|
|
||||||
"{:?} SHOULD be transmutable into {:?}",
|
"{:?} SHOULD be transmutable into {:?}",
|
||||||
src_layout,
|
src_layout,
|
||||||
dst_layout
|
dst_layout
|
||||||
|
@ -136,13 +152,11 @@ mod bool {
|
||||||
} else if !src_set.is_disjoint(&dst_set) {
|
} else if !src_set.is_disjoint(&dst_set) {
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
Answer::Yes,
|
Answer::Yes,
|
||||||
MaybeTransmutableQuery::new(
|
is_transmutable(
|
||||||
src_layout.clone(),
|
&src_layout,
|
||||||
dst_layout.clone(),
|
&dst_layout,
|
||||||
crate::Assume { validity: true, ..crate::Assume::default() },
|
Assume { validity: true, ..Assume::default() }
|
||||||
UltraMinimal,
|
),
|
||||||
)
|
|
||||||
.answer(),
|
|
||||||
"{:?} SHOULD be transmutable (assuming validity) into {:?}",
|
"{:?} SHOULD be transmutable (assuming validity) into {:?}",
|
||||||
src_layout,
|
src_layout,
|
||||||
dst_layout
|
dst_layout
|
||||||
|
@ -150,13 +164,7 @@ mod bool {
|
||||||
} else {
|
} else {
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
Answer::No(Reason::DstIsBitIncompatible),
|
Answer::No(Reason::DstIsBitIncompatible),
|
||||||
MaybeTransmutableQuery::new(
|
is_transmutable(&src_layout, &dst_layout, Assume::default()),
|
||||||
src_layout.clone(),
|
|
||||||
dst_layout.clone(),
|
|
||||||
crate::Assume { validity: false, ..crate::Assume::default() },
|
|
||||||
UltraMinimal,
|
|
||||||
)
|
|
||||||
.answer(),
|
|
||||||
"{:?} should NOT be transmutable into {:?}",
|
"{:?} should NOT be transmutable into {:?}",
|
||||||
src_layout,
|
src_layout,
|
||||||
dst_layout
|
dst_layout
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue