Skip to content

Commit

Permalink
C library: fix use of va_list for AARCH64
Browse files Browse the repository at this point in the history 
This is a fixup to "C model library: Support ARM64 va_list types" that
1) only changed only a subset of the code locations that required change
   and
2) did so with a crude workaround.

Really, we need to abide by ARM's procedure call standard for ARM64,
which mandates that `va_list` be a particular struct. See

https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#definition-of-va-list
and
https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#the-va-arg-macro

While at it, also add the necessary define for Visual Studio's support
of ARM64.

Fixes: #8357
  • Loading branch information
@tautschnig
tautschnig committed Sep 18, 2024
1 parent d87b506 commit 40a3dbb
Show file tree
Hide file tree
Showing 2 changed files with 93 additions and 12 deletions.
100 changes: 89 additions & 11 deletions src/ansi-c/library/stdio.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1134,14 +1134,23 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
}

(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
# if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
# else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
__CPROVER_OBJECT_SIZE(arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
# endif

#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
"vfscanf file must be open");
#endif
Expand Down Expand Up @@ -1183,12 +1192,21 @@ __CPROVER_HIDE:;
}

(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
__CPROVER_OBJECT_SIZE(*(void **)&arg))
#if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
#else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
__CPROVER_OBJECT_SIZE(arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
#endif

#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
__CPROVER_assert(
Expand Down Expand Up @@ -1232,12 +1250,21 @@ int __stdio_common_vfscanf(
}

(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
# if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
__CPROVER_OBJECT_SIZE(args.__stack))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
}
# else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
__CPROVER_OBJECT_SIZE(args))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
}
# endif

# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
__CPROVER_assert(
Expand Down Expand Up @@ -1311,12 +1338,21 @@ __CPROVER_HIDE:;
int result = __VERIFIER_nondet_int();
(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
# if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
# else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
__CPROVER_OBJECT_SIZE(arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
# endif

return result;
}
Expand Down Expand Up @@ -1346,12 +1382,21 @@ __CPROVER_HIDE:;
int result = __VERIFIER_nondet_int();
(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
__CPROVER_OBJECT_SIZE(*(void **)&arg))
#if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
__CPROVER_OBJECT_SIZE(arg.__stack))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
#else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
__CPROVER_OBJECT_SIZE(arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
}
#endif

return result;
}
Expand Down Expand Up @@ -1387,12 +1432,21 @@ int __stdio_common_vsscanf(

(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
# if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
__CPROVER_OBJECT_SIZE(args.__stack))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
}
# else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
__CPROVER_OBJECT_SIZE(args))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
}
# endif

return result;
}
Expand Down Expand Up @@ -1773,7 +1827,18 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
{
(void)*fmt;

while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
#if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
__CPROVER_OBJECT_SIZE(ap.__stack))

{
(void)va_arg(ap, int);
__CPROVER_precondition(
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
"vsnprintf object overlap");
}
#else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap) <
__CPROVER_OBJECT_SIZE(ap))

{
Expand All @@ -1782,6 +1847,7 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
"vsnprintf object overlap");
}
#endif

size_t i = 0;
for(; i < size; ++i)
Expand Down Expand Up @@ -1821,7 +1887,18 @@ int __builtin___vsnprintf_chk(
(void)bufsize;
(void)*fmt;

while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
#if defined(__aarch64__) || defined(_M_ARM64)
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
__CPROVER_OBJECT_SIZE(ap.__stack))

{
(void)va_arg(ap, int);
__CPROVER_precondition(
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
"vsnprintf object overlap");
}
#else
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap) <
__CPROVER_OBJECT_SIZE(ap))

{
Expand All @@ -1830,6 +1907,7 @@ int __builtin___vsnprintf_chk(
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
"vsnprintf object overlap");
}
#endif

size_t i = 0;
for(; i < size; ++i)
Expand Down
5 changes: 4 additions & 1 deletion src/util/config.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -308,7 +308,10 @@ void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch)
break;

case flavourt::VISUAL_STUDIO:
defines.push_back("_M_ARM");
if(subarch == "arm64")
defines.push_back("_M_ARM64");
else
defines.push_back("_M_ARM");
break;

case flavourt::CODEWARRIOR:
Expand Down

0 comments on commit 40a3dbb

Please sign in to comment.