diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index dc703ce83edc..258691b9ade4 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -47,6 +47,7 @@ pub enum BuiltinFn { Memset, Nearbyint, Nearbyintf, + Posixmemalign, Pow, Powf, Powi, @@ -109,6 +110,7 @@ impl ToString for BuiltinFn { Memset => "memset", Nearbyint => "nearbyint", Nearbyintf => "nearbyintf", + Posixmemalign => "posix_memalign", Pow => "pow", Powf => "powf", Powi => "__builtin_powi", @@ -173,6 +175,7 @@ impl BuiltinFn { Memset => vec![Type::void_pointer(), Type::c_int(), Type::size_t()], Nearbyint => vec![Type::double()], Nearbyintf => vec![Type::float()], + Posixmemalign => vec![Type::void_pointer(), Type::size_t(), Type::size_t()], Powf => vec![Type::float(), Type::float()], Powi => vec![Type::double(), Type::c_int()], Powif => vec![Type::float(), Type::c_int()], @@ -234,6 +237,7 @@ impl BuiltinFn { Memset => Type::void_pointer(), Nearbyint => Type::double(), Nearbyintf => Type::float(), + Posixmemalign => Type::c_int(), Pow => Type::double(), Powf => Type::float(), Powi => Type::double(), @@ -296,6 +300,7 @@ impl BuiltinFn { Memset, Nearbyint, Nearbyintf, + Posixmemalign, Pow, Powf, Powi, diff --git a/tests/kani/LibC/posix_memalign.rs b/tests/kani/LibC/posix_memalign.rs new file mode 100644 index 000000000000..017e88036367 --- /dev/null +++ b/tests/kani/LibC/posix_memalign.rs @@ -0,0 +1,46 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Check support for `posix_memalign`. + +#![feature(rustc_private)] +#![feature(allocator_api)] +extern crate libc; + +use std::alloc::{Allocator, Layout, System}; +use std::ptr; + +#[repr(C, align(32))] +struct MyStruct { + data: [u128; 10], +} + +#[kani::proof] +fn alloc_zeroed() { + let layout = Layout::new::(); + let ptr = System.allocate_zeroed(layout).unwrap(); + assert_eq!(unsafe { ptr.as_ref()[0] }, 0); +} + +// Source rust/src/libstd/sys/unix/alloc.rs +unsafe fn aligned_malloc(layout: &Layout) -> *mut u8 { + let mut out = ptr::null_mut(); + let ret = libc::posix_memalign(&mut out, layout.align(), layout.size()); + if ret != 0 { ptr::null_mut() } else { out as *mut u8 } +} + +#[kani::proof] +fn aligned_malloc_main() { + let mut layout = Layout::from_size_align(0, 1); + let _mem = unsafe { aligned_malloc(&layout.unwrap()) }; +} + +#[kani::proof] +fn posix_memalign_incorrect_alignment() { + let mut out = ptr::null_mut(); + let small_page_size = 1; + let size = 4; + assert_eq!( unsafe { libc::posix_memalign(&mut out, small_page_size, size) }, libc::EINVAL); + let incorrect_page_size = 13; + assert_eq!( unsafe { libc::posix_memalign(&mut out, incorrect_page_size, size) }, libc::EINVAL); +}