diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4e965b4105ef..2f97fcb5ec53 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1991,30 +1991,42 @@ impl<'tcx> GotocCtx<'tcx> { let x = fargs.remove(0); let y = fargs.remove(0); - // if(same_object(x, y)) { - // assert(x + 1 <= y || y + 1 <= x); - // assume(x + 1 <= y || y + 1 <= x); - // } - let one = Expr::int_constant(1, Type::c_int()); - let non_overlapping = - x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone())); - let non_overlapping_check = self.codegen_assert_assume( - non_overlapping, - PropertyClass::SafetyCheck, - "memory regions pointed to by `x` and `y` must not overlap", - loc, - ); - let non_overlapping_stmt = - Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc); - - // T t = *y; *y = *x; *x = t; let deref_y = y.clone().dereference(); - let (temp_var, assign_to_t) = - self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); - let assign_to_y = y.dereference().assign(x.clone().dereference(), loc); - let assign_to_x = x.dereference().assign(temp_var, loc); + if deref_y.typ().sizeof(&self.symbol_table) == 0 { + // do not attempt to dereference (and assign) a ZST + Stmt::skip(loc) + } else { + // if(same_object(x, y)) { + // assert(x + 1 <= y || y + 1 <= x); + // assume(x + 1 <= y || y + 1 <= x); + // } + let one = Expr::int_constant(1, Type::c_int()); + let non_overlapping = x + .clone() + .plus(one.clone()) + .le(y.clone()) + .or(y.clone().plus(one.clone()).le(x.clone())); + let non_overlapping_check = self.codegen_assert_assume( + non_overlapping, + PropertyClass::SafetyCheck, + "memory regions pointed to by `x` and `y` must not overlap", + loc, + ); + let non_overlapping_stmt = Stmt::if_then_else( + x.clone().same_object(y.clone()), + non_overlapping_check, + None, + loc, + ); + + // T t = *y; *y = *x; *x = t; + let (temp_var, assign_to_t) = + self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); + let assign_to_y = y.dereference().assign(x.clone().dereference(), loc); + let assign_to_x = x.dereference().assign(temp_var, loc); - Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) + Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) + } } } diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap.rs index 4279bb713ece..996784b5181d 100644 --- a/tests/kani/Intrinsics/typed_swap.rs +++ b/tests/kani/Intrinsics/typed_swap.rs @@ -19,3 +19,10 @@ fn test_typed_swap_u32() { assert!(b == a_before); assert!(a == b_before); } + +#[kani::proof] +pub fn check_swap_unit() { + let mut x: () = kani::any(); + let mut y: () = kani::any(); + std::mem::swap(&mut x, &mut y) +} diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs index 5ca439a18e1c..4f41d176a73a 100644 --- a/tests/std-checks/core/src/mem.rs +++ b/tests/std-checks/core/src/mem.rs @@ -45,8 +45,6 @@ mod verify { /// FIX-ME: Modifies clause fail with pointer to ZST. /// - /// FIX-ME: `typed_swap` intrisic fails for ZST. - /// #[kani::proof_for_contract(contracts::swap)] pub fn check_swap_unit() { let mut x: () = kani::any();