Skip to content

Commit 9e883f5

Browse files
tautschnigtautschnig
authored
Merge pull request #8366 from tautschnig/fix-8357-va_list
C library: fix use of va_list for AARCH64
2 parents d87b506 + 40a3dbb commit 9e883f5

File tree

2 files changed

+93
-12
lines changed

2 files changed

+93
-12
lines changed

‎src/ansi-c/library/stdio.c

+89-11
Original file line numberDiff line numberDiff line change
@@ -1134,14 +1134,23 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
11341134
}
11351135

11361136
(void)*format;
1137-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1137+
# if defined(__aarch64__) || defined(_M_ARM64)
1138+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1139+
__CPROVER_OBJECT_SIZE(arg.__stack))
1140+
{
1141+
void *a = va_arg(arg, void *);
1142+
__CPROVER_havoc_object(a);
1143+
}
1144+
# else
1145+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
11381146
__CPROVER_OBJECT_SIZE(arg))
11391147
{
11401148
void *a = va_arg(arg, void *);
11411149
__CPROVER_havoc_object(a);
11421150
}
1151+
# endif
11431152

1144-
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1153+
# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
11451154
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
11461155
"vfscanf file must be open");
11471156
#endif
@@ -1183,12 +1192,21 @@ __CPROVER_HIDE:;
11831192
}
11841193

11851194
(void)*format;
1186-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1187-
__CPROVER_OBJECT_SIZE(*(void **)&arg))
1195+
#if defined(__aarch64__) || defined(_M_ARM64)
1196+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1197+
__CPROVER_OBJECT_SIZE(arg.__stack))
1198+
{
1199+
void *a = va_arg(arg, void *);
1200+
__CPROVER_havoc_object(a);
1201+
}
1202+
#else
1203+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
1204+
__CPROVER_OBJECT_SIZE(arg))
11881205
{
11891206
void *a = va_arg(arg, void *);
11901207
__CPROVER_havoc_object(a);
11911208
}
1209+
#endif
11921210

11931211
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
11941212
__CPROVER_assert(
@@ -1232,12 +1250,21 @@ int __stdio_common_vfscanf(
12321250
}
12331251

12341252
(void)*format;
1235-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
1253+
# if defined(__aarch64__) || defined(_M_ARM64)
1254+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
1255+
__CPROVER_OBJECT_SIZE(args.__stack))
1256+
{
1257+
void *a = va_arg(args, void *);
1258+
__CPROVER_havoc_object(a);
1259+
}
1260+
# else
1261+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
12361262
__CPROVER_OBJECT_SIZE(args))
12371263
{
12381264
void *a = va_arg(args, void *);
12391265
__CPROVER_havoc_object(a);
12401266
}
1267+
# endif
12411268

12421269
# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
12431270
__CPROVER_assert(
@@ -1311,12 +1338,21 @@ __CPROVER_HIDE:;
13111338
int result = __VERIFIER_nondet_int();
13121339
(void)*s;
13131340
(void)*format;
1314-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1341+
# if defined(__aarch64__) || defined(_M_ARM64)
1342+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1343+
__CPROVER_OBJECT_SIZE(arg.__stack))
1344+
{
1345+
void *a = va_arg(arg, void *);
1346+
__CPROVER_havoc_object(a);
1347+
}
1348+
# else
1349+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
13151350
__CPROVER_OBJECT_SIZE(arg))
13161351
{
13171352
void *a = va_arg(arg, void *);
13181353
__CPROVER_havoc_object(a);
13191354
}
1355+
# endif
13201356

13211357
return result;
13221358
}
@@ -1346,12 +1382,21 @@ __CPROVER_HIDE:;
13461382
int result = __VERIFIER_nondet_int();
13471383
(void)*s;
13481384
(void)*format;
1349-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
1350-
__CPROVER_OBJECT_SIZE(*(void **)&arg))
1385+
#if defined(__aarch64__) || defined(_M_ARM64)
1386+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
1387+
__CPROVER_OBJECT_SIZE(arg.__stack))
1388+
{
1389+
void *a = va_arg(arg, void *);
1390+
__CPROVER_havoc_object(a);
1391+
}
1392+
#else
1393+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
1394+
__CPROVER_OBJECT_SIZE(arg))
13511395
{
13521396
void *a = va_arg(arg, void *);
13531397
__CPROVER_havoc_object(a);
13541398
}
1399+
#endif
13551400

13561401
return result;
13571402
}
@@ -1387,12 +1432,21 @@ int __stdio_common_vsscanf(
13871432

13881433
(void)*s;
13891434
(void)*format;
1390-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
1435+
# if defined(__aarch64__) || defined(_M_ARM64)
1436+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
1437+
__CPROVER_OBJECT_SIZE(args.__stack))
1438+
{
1439+
void *a = va_arg(args, void *);
1440+
__CPROVER_havoc_object(a);
1441+
}
1442+
# else
1443+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
13911444
__CPROVER_OBJECT_SIZE(args))
13921445
{
13931446
void *a = va_arg(args, void *);
13941447
__CPROVER_havoc_object(a);
13951448
}
1449+
# endif
13961450

13971451
return result;
13981452
}
@@ -1773,7 +1827,18 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
17731827
{
17741828
(void)*fmt;
17751829

1776-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1830+
#if defined(__aarch64__) || defined(_M_ARM64)
1831+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
1832+
__CPROVER_OBJECT_SIZE(ap.__stack))
1833+
1834+
{
1835+
(void)va_arg(ap, int);
1836+
__CPROVER_precondition(
1837+
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
1838+
"vsnprintf object overlap");
1839+
}
1840+
#else
1841+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap) <
17771842
__CPROVER_OBJECT_SIZE(ap))
17781843

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

17861852
size_t i = 0;
17871853
for(; i < size; ++i)
@@ -1821,7 +1887,18 @@ int __builtin___vsnprintf_chk(
18211887
(void)bufsize;
18221888
(void)*fmt;
18231889

1824-
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1890+
#if defined(__aarch64__) || defined(_M_ARM64)
1891+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
1892+
__CPROVER_OBJECT_SIZE(ap.__stack))
1893+
1894+
{
1895+
(void)va_arg(ap, int);
1896+
__CPROVER_precondition(
1897+
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
1898+
"vsnprintf object overlap");
1899+
}
1900+
#else
1901+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap) <
18251902
__CPROVER_OBJECT_SIZE(ap))
18261903

18271904
{
@@ -1830,6 +1907,7 @@ int __builtin___vsnprintf_chk(
18301907
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
18311908
"vsnprintf object overlap");
18321909
}
1910+
#endif
18331911

18341912
size_t i = 0;
18351913
for(; i < size; ++i)

‎src/util/config.cpp

+4-1
Original file line numberDiff line numberDiff line change
@@ -308,7 +308,10 @@ void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch)
308308
break;
309309

310310
case flavourt::VISUAL_STUDIO:
311-
defines.push_back("_M_ARM");
311+
if(subarch == "arm64")
312+
defines.push_back("_M_ARM64");
313+
else
314+
defines.push_back("_M_ARM");
312315
break;
313316

314317
case flavourt::CODEWARRIOR:

0 commit comments

Comments
 (0)