Skip to content

[SV-COMP'18 4/19] Constrain the malloc/alloca size to fit our object:offset encoding #1993

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

[SV-COMP'18 4/19] Constrain the malloc/alloca size to fit our object:offset encoding #1993

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions src/ansi-c/library/new.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,12 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
// This just does memory allocation.
__CPROVER_HIDE:;
void *res;
// ensure that all bytes in the allocated memory can be addressed
// using our object:offset encoding as specified in
// flattening/pointer_logic.h; also avoid sign-extension issues
// for 32-bit systems that yields a maximum allocation of 2^23-1,
// i.e., just under 8MB
__CPROVER_assume(malloc_size < (1UL << ((sizeof(char *) - 1) * 8 - 1)));
res = __CPROVER_allocate(malloc_size, 0);

// ensure it's not recorded as deallocated
Expand Down Expand Up @@ -35,6 +41,12 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
// The constructor call is done by the front-end.
// This just does memory allocation.
__CPROVER_HIDE:;
// ensure that all bytes in the allocated memory can be addressed
// using our object:offset encoding as specified in
// flattening/pointer_logic.h; also avoid sign-extension issues
// for 32-bit systems that yields a maximum allocation of 2^23-1,
// i.e., just under 8MB
__CPROVER_assume(size * count < (1UL << ((sizeof(char *) - 1) * 8 - 1)));
void *res;
res = __CPROVER_allocate(size*count, 0);

Expand Down
12 changes: 12 additions & 0 deletions src/ansi-c/library/stdlib.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,12 @@ inline void *malloc(__CPROVER_size_t malloc_size)
// realistically, malloc may return NULL,
// and __CPROVER_allocate doesn't, but no one cares
__CPROVER_HIDE:;
// ensure that all bytes in the allocated memory can be addressed
// using our object:offset encoding as specified in
// flattening/pointer_logic.h; also avoid sign-extension issues
// for 32-bit systems that yields a maximum allocation of 2^23-1,
// i.e., just under 8MB
__CPROVER_assume(malloc_size < (1UL << ((sizeof(char *) - 1) * 8 - 1)));
void *malloc_res;
malloc_res = __CPROVER_allocate(malloc_size, 0);

Expand All @@ -132,6 +138,12 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
{
__CPROVER_HIDE:;
// ensure that all bytes in the allocated memory can be addressed
// using our object:offset encoding as specified in
// flattening/pointer_logic.h; also avoid sign-extension issues
// for 32-bit systems that yields a maximum allocation of 2^23-1,
// i.e., just under 8MB
__CPROVER_assume(alloca_size < (1UL << ((sizeof(char *) - 1) * 8 - 1)));
void *res;
res = __CPROVER_allocate(alloca_size, 0);

Expand Down