Skip to content

Commit cd7459e

Browse files
tautschnigtautschnig
committed
C library: implement {v,}snprintf
The model will non-deterministically alter the target string up to the bound given as argument to {v,}snprintf.
1 parent 1fd7011 commit cd7459e

File tree

6 files changed

+240
-0
lines changed

6 files changed

+240
-0
lines changed

‎regression/cbmc-library/snprintf-01/main.c

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
#include <stdio.h>
3+
4+
int main()
5+
{
6+
char result[10];
7+
int bytes = snprintf(result, 10, "%d\n", 42);
8+
assert(bytes <= 10);
9+
return 0;
10+
}

‎regression/cbmc-library/snprintf-01/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-library/vsnprintf-01/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
#include <stdarg.h>
3+
#include <stdio.h>
4+
5+
int xsnprintf(char *ptr, size_t size, const char *format, ...)
6+
{
7+
va_list list;
8+
va_start(list, format);
9+
int result = vsnprintf(ptr, size, format, list);
10+
va_end(list);
11+
return result;
12+
}
13+
14+
int main()
15+
{
16+
char result[10];
17+
int bytes = xsnprintf(result, 10, "%d\n", 42);
18+
assert(bytes <= 10);
19+
return 0;
20+
}

‎regression/cbmc-library/vsnprintf-01/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

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

+191
Original file line numberDiff line numberDiff line change
@@ -1584,6 +1584,154 @@ int vasprintf(char **ptr, const char *fmt, va_list ap)
15841584
return i;
15851585
}
15861586

1587+
/* FUNCTION: snprintf */
1588+
1589+
#ifndef __CPROVER_STDIO_H_INCLUDED
1590+
# include <stdio.h>
1591+
# define __CPROVER_STDIO_H_INCLUDED
1592+
#endif
1593+
1594+
#ifndef __CPROVER_STDARG_H_INCLUDED
1595+
# include <stdarg.h>
1596+
# define __CPROVER_STDARG_H_INCLUDED
1597+
#endif
1598+
1599+
#undef snprintf
1600+
1601+
int snprintf(char *str, size_t size, const char *fmt, ...)
1602+
{
1603+
va_list list;
1604+
va_start(list, fmt);
1605+
int result = vsnprintf(str, size, fmt, list);
1606+
va_end(list);
1607+
return result;
1608+
}
1609+
1610+
/* FUNCTION: __builtin___snprintf_chk */
1611+
1612+
#ifndef __CPROVER_STDIO_H_INCLUDED
1613+
# include <stdio.h>
1614+
# define __CPROVER_STDIO_H_INCLUDED
1615+
#endif
1616+
1617+
#ifndef __CPROVER_STDARG_H_INCLUDED
1618+
# include <stdarg.h>
1619+
# define __CPROVER_STDARG_H_INCLUDED
1620+
#endif
1621+
1622+
int __builtin___vsnprintf_chk(
1623+
char *str,
1624+
size_t size,
1625+
int flag,
1626+
size_t bufsize,
1627+
const char *fmt,
1628+
va_list ap);
1629+
1630+
int __builtin___snprintf_chk(
1631+
char *str,
1632+
size_t size,
1633+
int flag,
1634+
size_t bufsize,
1635+
const char *fmt,
1636+
...)
1637+
{
1638+
va_list list;
1639+
va_start(list, fmt);
1640+
int result = __builtin___vsnprintf_chk(str, size, flag, bufsize, fmt, list);
1641+
va_end(list);
1642+
return result;
1643+
}
1644+
1645+
/* FUNCTION: vsnprintf */
1646+
1647+
#ifndef __CPROVER_STDIO_H_INCLUDED
1648+
# include <stdio.h>
1649+
# define __CPROVER_STDIO_H_INCLUDED
1650+
#endif
1651+
1652+
#ifndef __CPROVER_STDARG_H_INCLUDED
1653+
# include <stdarg.h>
1654+
# define __CPROVER_STDARG_H_INCLUDED
1655+
#endif
1656+
1657+
#undef vsnprintf
1658+
1659+
char __VERIFIER_nondet_char(void);
1660+
1661+
int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
1662+
{
1663+
(void)*fmt;
1664+
1665+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1666+
__CPROVER_OBJECT_SIZE(ap))
1667+
1668+
{
1669+
(void)va_arg(ap, int);
1670+
__CPROVER_precondition(
1671+
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
1672+
"vsnprintf object overlap");
1673+
}
1674+
1675+
size_t i = 0;
1676+
for(; i < size; ++i)
1677+
{
1678+
char c = __VERIFIER_nondet_char();
1679+
str[i] = c;
1680+
if(c == '\0')
1681+
break;
1682+
}
1683+
1684+
return i;
1685+
}
1686+
1687+
/* FUNCTION: __builtin___vsnprintf_chk */
1688+
1689+
#ifndef __CPROVER_STDIO_H_INCLUDED
1690+
# include <stdio.h>
1691+
# define __CPROVER_STDIO_H_INCLUDED
1692+
#endif
1693+
1694+
#ifndef __CPROVER_STDARG_H_INCLUDED
1695+
# include <stdarg.h>
1696+
# define __CPROVER_STDARG_H_INCLUDED
1697+
#endif
1698+
1699+
char __VERIFIER_nondet_char(void);
1700+
1701+
int __builtin___vsnprintf_chk(
1702+
char *str,
1703+
size_t size,
1704+
int flag,
1705+
size_t bufsize,
1706+
const char *fmt,
1707+
va_list ap)
1708+
{
1709+
(void)flag;
1710+
(void)bufsize;
1711+
(void)*fmt;
1712+
1713+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
1714+
__CPROVER_OBJECT_SIZE(ap))
1715+
1716+
{
1717+
(void)va_arg(ap, int);
1718+
__CPROVER_precondition(
1719+
__CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
1720+
"vsnprintf object overlap");
1721+
}
1722+
1723+
size_t i = 0;
1724+
for(; i < size; ++i)
1725+
{
1726+
char c = __VERIFIER_nondet_char();
1727+
str[i] = c;
1728+
if(c == '\0')
1729+
break;
1730+
}
1731+
1732+
return i;
1733+
}
1734+
15871735
/* FUNCTION: __acrt_iob_func */
15881736

15891737
#ifdef _WIN32
@@ -1645,6 +1793,49 @@ int __stdio_common_vfprintf(
16451793

16461794
#endif
16471795

1796+
/* FUNCTION: __stdio_common_vsprintf */
1797+
1798+
#ifdef _WIN32
1799+
1800+
# ifndef __CPROVER_STDIO_H_INCLUDED
1801+
# include <stdio.h>
1802+
# define __CPROVER_STDIO_H_INCLUDED
1803+
# endif
1804+
1805+
# ifndef __CPROVER_STDARG_H_INCLUDED
1806+
# include <stdarg.h>
1807+
# define __CPROVER_STDARG_H_INCLUDED
1808+
# endif
1809+
1810+
char __VERIFIER_nondet_char(void);
1811+
1812+
int __stdio_common_vsprintf(
1813+
unsigned __int64 options,
1814+
char *str,
1815+
size_t size,
1816+
char const *fmt,
1817+
_locale_t locale,
1818+
va_list args)
1819+
{
1820+
(void)options;
1821+
(void)*fmt;
1822+
(void)locale;
1823+
(void)args;
1824+
1825+
size_t i = 0;
1826+
for(; i < size; ++i)
1827+
{
1828+
char c = __VERIFIER_nondet_char();
1829+
str[i] = c;
1830+
if(c == '\0')
1831+
break;
1832+
}
1833+
1834+
return i;
1835+
}
1836+
1837+
#endif
1838+
16481839
/* FUNCTION: __srget */
16491840

16501841
#ifdef __FreeBSD__

‎src/ansi-c/library_check.sh

+3
Original file line numberDiff line numberDiff line change
@@ -38,12 +38,15 @@ perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
3838
perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS
3939
perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS
4040
perl -p -i -e 's/^_time(32|64)\n//' __functions # time, Windows
41+
perl -p -i -e 's/^__builtin___snprintf_chk\n//' __functions # snprintf, macOS
42+
perl -p -i -e 's/^__builtin___vsnprintf_chk\n//' __functions # vsnprintf, macOS
4143
perl -p -i -e 's/^__inet_(addr|aton|ntoa|network)\n//' __functions # inet_*, FreeBSD
4244
perl -p -i -e 's/^__isoc99_v?fscanf\n//' __functions # fscanf, Linux
4345
perl -p -i -e 's/^__isoc99_v?scanf\n//' __functions # scanf, Linux
4446
perl -p -i -e 's/^__isoc99_v?sscanf\n//' __functions # sscanf, Linux
4547
perl -p -i -e 's/^__sigsetjmp\n//' __functions # sigsetjmp, Linux
4648
perl -p -i -e 's/^__stdio_common_vfscanf\n//' __functions # fscanf, Windows
49+
perl -p -i -e 's/^__stdio_common_vsprintf\n//' __functions # snprintf, Windows
4750
perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
4851
perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
4952
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD

0 commit comments

Comments
 (0)