use crate::{
abstr::{self, Abstr, BitvectorDomain, PanicBitvector, PanicResult},
bitvector::abstr::three_valued::CThreeValuedBitvector,
concr::{self, CConcreteBitvector},
misc::{CBound, Join},
traits::misc::MetaEq,
};
macro_rules! uni_op_test {
($op:tt) => {
seq_macro::seq!(L in 0..=8 {
#[test]
pub fn $op~L() {
use $crate::abstr::three_valued::CThreeValuedBitvector;
use $crate::concr::CConcreteBitvector;
let abstr_func = |a: CThreeValuedBitvector<L>| a.$op();
let concr_func = |a: CConcreteBitvector<L>| a.$op();
$crate::bitvector::abstr::three_valued::tests::op::exec_uni_check(abstr_func, concr_func);
}
});
};
}
macro_rules! ext_op_test {
($op:tt) => {
seq_macro::seq!(L in 0..=6 {
seq_macro::seq!(X in 0..=6 {
#[test]
pub fn $op~L~X() {
use $crate::abstr::three_valued::CThreeValuedBitvector;
use $crate::concr::CConcreteBitvector;
let abstr_func =
|a: CThreeValuedBitvector<L>| -> CThreeValuedBitvector<X> { $crate::forward::BExt::$op(a, CBound) };
let concr_func = |a: CConcreteBitvector<L>| -> CConcreteBitvector<X> { $crate::forward::BExt::$op(a, CBound) };
$crate::bitvector::abstr::three_valued::tests::op::exec_uni_check(abstr_func, concr_func);
}
});
});
};
}
macro_rules! bi_op_test {
($op:tt,$exact:tt) => {
seq_macro::seq!(L in 0..=6 {
#[test]
pub fn $op~L() {
use $crate::abstr::three_valued::CThreeValuedBitvector;
use $crate::concr::CConcreteBitvector;
let abstr_func = |a: CThreeValuedBitvector<L>, b: CThreeValuedBitvector<L>| a.$op(b);
let concr_func = |a: CConcreteBitvector<L>, b: CConcreteBitvector<L>| a.$op(b);
$crate::bitvector::abstr::three_valued::tests::op::exec_bi_check(abstr_func, concr_func, $exact);
}
});
};
}
macro_rules! cmp_op_test {
($op:tt,$exact:tt) => {
seq_macro::seq!(L in 0..=6 {
#[test]
pub fn $op~L() {
use $crate::abstr::three_valued::CThreeValuedBitvector;
use $crate::concr::CConcreteBitvector;
let abstr_func = |a: CThreeValuedBitvector<L>, b: CThreeValuedBitvector<L>| a.$op(b);
let concr_func = |a: CConcreteBitvector<L>, b: CConcreteBitvector<L>| a.$op(b);
$crate::bitvector::abstr::three_valued::tests::op::exec_comparison_check(abstr_func, concr_func, $exact);
}
});
};
}
macro_rules! divrem_op_test {
($op:tt,$exact:tt) => {
seq_macro::seq!(L in 0..=6 {
#[test]
pub fn $op~L() {
use $crate::abstr::three_valued::CThreeValuedBitvector;
use $crate::concr::CConcreteBitvector;
let abstr_func = |a: CThreeValuedBitvector<L>, b: CThreeValuedBitvector<L>| a.$op(b).into();
let concr_func = |a: CConcreteBitvector<L>, b: CConcreteBitvector<L>| a.$op(b).into();
$crate::bitvector::abstr::three_valued::tests::op::exec_divrem_check(abstr_func, concr_func);
}
});
};
}
pub(super) fn exec_uni_check<const W: u32, const X: u32>(
abstr_func: fn(CThreeValuedBitvector<W>) -> CThreeValuedBitvector<X>,
concr_func: fn(CConcreteBitvector<W>) -> CConcreteBitvector<X>,
) {
for a in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
let abstr_result = abstr_func(a);
let equiv_result = join_concr_iter(
CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| a.contains_concrete(c))
.map(concr_func),
);
if !abstr_result.meta_eq(&equiv_result) {
panic!(
"Wrong result with parameter {}, expected {}, got {}",
a, equiv_result, abstr_result
);
}
}
}
pub(super) fn exec_bi_check<const W: u32, const X: u32>(
abstr_func: fn(CThreeValuedBitvector<W>, CThreeValuedBitvector<W>) -> CThreeValuedBitvector<X>,
concr_func: fn(CConcreteBitvector<W>, CConcreteBitvector<W>) -> CConcreteBitvector<X>,
exact: bool,
) {
for a in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
for b in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
let abstr_result = abstr_func(a, b);
let a_concr_iter = CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| a.contains_concrete(c));
let equiv_result = join_concr_iter(a_concr_iter.flat_map(|a_concr| {
CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| b.contains_concrete(c))
.map(move |b_concr| concr_func(a_concr, b_concr))
}));
if exact {
if !abstr_result.meta_eq(&equiv_result) {
panic!(
"Non-exact result with parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
} else if !abstr_result.contains(&equiv_result) {
panic!(
"Unsound result with parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
if a.concrete_value().is_some()
&& b.concrete_value().is_some()
&& abstr_result.concrete_value().is_none()
{
panic!(
"Non-concrete-value result with concrete-value parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
}
}
}
pub(super) fn exec_comparison_check<const W: u32>(
abstr_func: fn(CThreeValuedBitvector<W>, CThreeValuedBitvector<W>) -> crate::abstr::Boolean,
concr_func: fn(CConcreteBitvector<W>, CConcreteBitvector<W>) -> crate::concr::Boolean,
exact: bool,
) {
for a in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
for b in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
let abstr_result = abstr_func(a, b);
let a_concr_iter = CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| a.contains_concrete(c));
let equiv_result = join_boolean_iter(a_concr_iter.flat_map(|a_concr| {
CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| b.contains_concrete(c))
.map(move |b_concr| concr_func(a_concr, b_concr))
}));
if exact {
if !abstr_result.meta_eq(&equiv_result) {
panic!(
"Non-exact result with parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
} else if !abstr_result.can_contain(&equiv_result) {
panic!(
"Unsound result with parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
if a.concrete_value().is_some()
&& b.concrete_value().is_some()
&& abstr_result.is_unknown()
{
panic!(
"Non-concrete-value result with concrete-value parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
}
}
}
pub(super) fn exec_divrem_check<const W: u32, const X: u32>(
abstr_func: fn(
CThreeValuedBitvector<W>,
CThreeValuedBitvector<W>,
) -> PanicResult<CThreeValuedBitvector<X>>,
concr_func: fn(
CConcreteBitvector<W>,
CConcreteBitvector<W>,
) -> concr::PanicResult<CConcreteBitvector<X>>,
) {
for a in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
for b in CThreeValuedBitvector::<W>::all_with_bound_iter(CBound) {
let abstr_panic_result = abstr_func(a, b);
let abstr_result = abstr_panic_result.result;
let abstr_panic = abstr_panic_result.panic;
let a_concr_iter = CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| a.contains_concrete(c));
let equiv_result = join_concr_iter(a_concr_iter.flat_map(|a_concr| {
CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| b.contains_concrete(c))
.map(move |b_concr| concr_func(a_concr, b_concr).result)
}));
let a_concr_iter = CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| a.contains_concrete(c));
let equiv_panic = join_panic_concr_iter(a_concr_iter.flat_map(|a_concr| {
CConcreteBitvector::<W>::all_with_bound_iter(CBound)
.filter(|c| b.contains_concrete(c))
.map(move |b_concr| concr_func(a_concr, b_concr).panic)
}));
if !abstr_result.contains(&equiv_result) {
panic!(
"Unsound result with parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
if !abstr_panic.meta_eq(&equiv_panic) {
panic!(
"Non-exact panic with parameters {}, {}, expected {:?}, got {:?}",
a, b, equiv_panic, abstr_panic
);
}
if a.concrete_value().is_some()
&& b.concrete_value().is_some()
&& abstr_result.concrete_value().is_none()
{
panic!(
"Non-concrete-value result with concrete-value parameters {}, {}, expected {}, got {}",
a, b, equiv_result, abstr_result
);
}
}
}
}
pub(super) fn join_boolean_iter(mut iter: impl Iterator<Item = concr::Boolean>) -> abstr::Boolean {
let first_concrete = iter
.next()
.expect("Expected at least one concrete bitvector in iterator");
let mut result = abstr::Boolean::from_concrete(first_concrete);
for c in iter {
let abstr = abstr::Boolean::from_concrete(c);
result = result.join(&abstr);
}
result
}
pub(super) fn join_concr_iter<const W: u32>(
mut iter: impl Iterator<Item = CConcreteBitvector<W>>,
) -> CThreeValuedBitvector<W> {
if W == 0 {
return CThreeValuedBitvector::new_unknown(CBound);
}
let first_concrete = iter
.next()
.expect("Expected at least one concrete bitvector in iterator");
let mut result = CThreeValuedBitvector::from_concrete_value(first_concrete);
for c in iter {
let abstr = CThreeValuedBitvector::from_concrete_value(c);
result = result.join(&abstr);
}
result
}
pub(super) fn join_panic_concr_iter(
mut iter: impl Iterator<Item = CConcreteBitvector<32>>,
) -> PanicBitvector {
let first_concrete = iter
.next()
.expect("Expected at least one concrete bitvector in iterator");
let mut result = PanicBitvector::from_concrete(first_concrete);
for c in iter {
result = result.join(&PanicBitvector::from_concrete(c))
}
result
}