From 58df33ec0c00209db906b59b03af4c81b142b104 Mon Sep 17 00:00:00 2001 From: fw Date: Fri, 3 Oct 2025 13:14:35 -0400 Subject: [PATCH 1/3] c2rust-refactor: tests: factor out `verify_double_cast` --- c2rust-refactor/src/transform/casts/tests.rs | 77 +++++++++++--------- 1 file changed, 41 insertions(+), 36 deletions(-) diff --git a/c2rust-refactor/src/transform/casts/tests.rs b/c2rust-refactor/src/transform/casts/tests.rs index b18e9fe077..6bb058bd03 100644 --- a/c2rust-refactor/src/transform/casts/tests.rs +++ b/c2rust-refactor/src/transform/casts/tests.rs @@ -63,48 +63,53 @@ fn cast_tys<'bv>(bv: BV<'bv>, tys: &[SimpleTy], pw: PointerWidth) -> BV<'bv> { thread_local!(static Z3_CONFIG: Config = Config::new()); thread_local!(static Z3_CONTEXT: Context = Z3_CONFIG.with(|cfg| Context::new(cfg))); -quickcheck! { - // Verify `check_double_cast` using QuickCheck and Z3 - fn verify_double_cast(pw: PointerWidth, tys: Vec) -> bool { - if tys.len() <= 1 { - return true; - } +// Verify `check_double_cast` using Z3 +fn verify_double_cast(pw: PointerWidth, tys: Vec) -> bool { + if tys.len() <= 1 { + return true; + } - Z3_CONTEXT.with(|ctx| { - // Build a minimized list of types with double casts removed - let mut min_tys = vec![tys[0].clone()]; - for ty in &tys[1..] { - assert!(!min_tys.is_empty()); - if *ty == min_tys[min_tys.len() - 1] { - // Cast to the same type, ignore it - continue; + Z3_CONTEXT.with(|ctx| { + // Build a minimized list of types with double casts removed + let mut min_tys = vec![tys[0].clone()]; + for ty in &tys[1..] { + assert!(!min_tys.is_empty()); + if *ty == min_tys[min_tys.len() - 1] { + // Cast to the same type, ignore it + continue; + } + if min_tys.len() < 2 { + min_tys.push(ty.clone()); + continue; + } + let last2 = &min_tys[min_tys.len() - 2..]; + match check_double_cast(last2[0], last2[1], *ty) { + DoubleCastAction::RemoveBoth => { + min_tys.pop(); } - if min_tys.len() < 2 { - min_tys.push(ty.clone()); - continue; + DoubleCastAction::RemoveInner => { + *min_tys.last_mut().unwrap() = ty.clone(); } - let last2 = &min_tys[min_tys.len() - 2..]; - match check_double_cast(last2[0], last2[1], *ty) { - DoubleCastAction::RemoveBoth => { - min_tys.pop(); - } - DoubleCastAction::RemoveInner => { - *min_tys.last_mut().unwrap() = ty.clone(); - } - DoubleCastAction::KeepBoth => { - min_tys.push(ty.clone()); - } + DoubleCastAction::KeepBoth => { + min_tys.push(ty.clone()); } } + } - let x = BV::new_const(&ctx, "x", ty_bit_width(tys[0], pw)); - let y = cast_tys(x.clone(), &tys[..], pw); - let z = cast_tys(x, &min_tys[..], pw); + let x = BV::new_const(&ctx, "x", ty_bit_width(tys[0], pw)); + let y = cast_tys(x.clone(), &tys[..], pw); + let z = cast_tys(x, &min_tys[..], pw); - // Check the full type list against the minimized one - let solver = Solver::new(&ctx); - solver.assert(&z._eq(&y).not()); - solver.check() == SatResult::Unsat - }) + // Check the full type list against the minimized one + let solver = Solver::new(&ctx); + solver.assert(&z._eq(&y).not()); + solver.check() == SatResult::Unsat + }) +} + +quickcheck! { + // Apply `verify_double_cast` to a sample of possible cast sequences using QuickCheck + fn quickcheck_double_cast(pw: PointerWidth, tys: Vec) -> bool { + verify_double_cast(pw, tys) } } From 93e12433d97bd28f27fe4e8522ac6bcddfa38ecb Mon Sep 17 00:00:00 2001 From: fw Date: Fri, 3 Oct 2025 12:54:44 -0400 Subject: [PATCH 2/3] c2rust-refactor: tests: print counterexample --- c2rust-refactor/src/transform/casts/tests.rs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/c2rust-refactor/src/transform/casts/tests.rs b/c2rust-refactor/src/transform/casts/tests.rs index 6bb058bd03..53879074de 100644 --- a/c2rust-refactor/src/transform/casts/tests.rs +++ b/c2rust-refactor/src/transform/casts/tests.rs @@ -60,7 +60,7 @@ fn cast_tys<'bv>(bv: BV<'bv>, tys: &[SimpleTy], pw: PointerWidth) -> BV<'bv> { tys.windows(2).fold(bv, |y, w| cast_bv(y, w[0], w[1], pw)) } -thread_local!(static Z3_CONFIG: Config = Config::new()); +thread_local!(static Z3_CONFIG: Config = { let mut c = Config::new(); c.set_model_generation(true); c }); thread_local!(static Z3_CONTEXT: Context = Z3_CONFIG.with(|cfg| Context::new(cfg))); // Verify `check_double_cast` using Z3 @@ -98,12 +98,23 @@ fn verify_double_cast(pw: PointerWidth, tys: Vec) -> bool { let x = BV::new_const(&ctx, "x", ty_bit_width(tys[0], pw)); let y = cast_tys(x.clone(), &tys[..], pw); - let z = cast_tys(x, &min_tys[..], pw); + let z = cast_tys(x.clone(), &min_tys[..], pw); // Check the full type list against the minimized one let solver = Solver::new(&ctx); solver.assert(&z._eq(&y).not()); - solver.check() == SatResult::Unsat + if solver.check() == SatResult::Unsat { + true + } else { + let model = solver.get_model().unwrap(); + panic!( + "{}b counterexample:\n{:?} =>\n {:?} via tys {tys:?} vs.\n {:?} via min_tys {min_tys:?}", + pw.0, + model.eval(&x, true).unwrap(), + model.eval(&y, true).unwrap(), + model.eval(&z, true).unwrap() + ) + } }) } From 882d68fd850a6c1588697e7f095030291de2e16e Mon Sep 17 00:00:00 2001 From: fw Date: Fri, 3 Oct 2025 13:14:56 -0400 Subject: [PATCH 3/3] c2rust-refactor: tests: add `test_cast_i32_u32_ssize` --- c2rust-refactor/src/transform/casts/tests.rs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/c2rust-refactor/src/transform/casts/tests.rs b/c2rust-refactor/src/transform/casts/tests.rs index 53879074de..a94656d928 100644 --- a/c2rust-refactor/src/transform/casts/tests.rs +++ b/c2rust-refactor/src/transform/casts/tests.rs @@ -63,6 +63,18 @@ fn cast_tys<'bv>(bv: BV<'bv>, tys: &[SimpleTy], pw: PointerWidth) -> BV<'bv> { thread_local!(static Z3_CONFIG: Config = { let mut c = Config::new(); c.set_model_generation(true); c }); thread_local!(static Z3_CONTEXT: Context = Z3_CONFIG.with(|cfg| Context::new(cfg))); +#[test] +fn test_cast_i32_u32_ssize() { + verify_double_cast( + PointerWidth(64), + vec![ + SimpleTy::Int(32, true), + SimpleTy::Int(32, false), + SimpleTy::Size(true), + ], + ); +} + // Verify `check_double_cast` using Z3 fn verify_double_cast(pw: PointerWidth, tys: Vec) -> bool { if tys.len() <= 1 {