C library: implement {v,}snprintf

The model will non-deterministically alter the target string up to the
bound given as argument to {v,}snprintf.

Author: tautschnig

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

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  char result[10];
+  int bytes = snprintf(result, 10, "%d\n", 42);
+  assert(bytes <= 10);
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdarg.h>
+#include <stdio.h>
+
+int xsnprintf(char *ptr, size_t size, const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vsnprintf(ptr, size, format, list);
+  va_end(list);
+  return result;
+}
+
+int main()
+{
+  char result[10];
+  int bytes = xsnprintf(result, 10, "%d\n", 42);
+  assert(bytes <= 10);
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/stdio.c

@@ -1584,6 +1584,154 @@ int vasprintf(char **ptr, const char *fmt, va_list ap)
   return i;
 }
 
+/* FUNCTION: snprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+#undef snprintf
+
+int snprintf(char *str, size_t size, const char *fmt, ...)
+{
+  va_list list;
+  va_start(list, fmt);
+  int result = vsnprintf(str, size, fmt, list);
+  va_end(list);
+  return result;
+}
+
+/* FUNCTION: __builtin___snprintf_chk */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+int __builtin___vsnprintf_chk(
+  char *str,
+  size_t size,
+  int flag,
+  size_t bufsize,
+  const char *fmt,
+  va_list ap);
+
+int __builtin___snprintf_chk(
+  char *str,
+  size_t size,
+  int flag,
+  size_t bufsize,
+  const char *fmt,
+  ...)
+{
+  va_list list;
+  va_start(list, fmt);
+  int result = __builtin___vsnprintf_chk(str, size, flag, bufsize, fmt, list);
+  va_end(list);
+  return result;
+}
+
+/* FUNCTION: vsnprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+#undef vsnprintf
+
+char __VERIFIER_nondet_char(void);
+
+int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
+{
+  (void)*fmt;
+
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+        __CPROVER_OBJECT_SIZE(ap))
+
+  {
+    (void)va_arg(ap, int);
+    __CPROVER_precondition(
+      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+      "vsnprintf object overlap");
+  }
+
+  size_t i = 0;
+  for(; i < size; ++i)
+  {
+    char c = __VERIFIER_nondet_char();
+    str[i] = c;
+    if(c == '\0')
+      break;
+  }
+
+  return i;
+}
+
+/* FUNCTION: __builtin___vsnprintf_chk */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+char __VERIFIER_nondet_char(void);
+
+int __builtin___vsnprintf_chk(
+  char *str,
+  size_t size,
+  int flag,
+  size_t bufsize,
+  const char *fmt,
+  va_list ap)
+{
+  (void)flag;
+  (void)bufsize;
+  (void)*fmt;
+
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+        __CPROVER_OBJECT_SIZE(ap))
+
+  {
+    (void)va_arg(ap, int);
+    __CPROVER_precondition(
+      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+      "vsnprintf object overlap");
+  }
+
+  size_t i = 0;
+  for(; i < size; ++i)
+  {
+    char c = __VERIFIER_nondet_char();
+    str[i] = c;
+    if(c == '\0')
+      break;
+  }
+
+  return i;
+}
+
 /* FUNCTION: __acrt_iob_func */
 
 #ifdef _WIN32
@@ -1645,6 +1793,49 @@ int __stdio_common_vfprintf(
 
 #endif
 
+/* FUNCTION: __stdio_common_vsprintf */
+
+#ifdef _WIN32
+
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
+
+char __VERIFIER_nondet_char(void);
+
+int __stdio_common_vsprintf(
+  unsigned __int64 options,
+  char *str,
+  size_t size,
+  char const *fmt,
+  _locale_t locale,
+  va_list args)
+{
+  (void)options;
+  (void)*fmt;
+  (void)locale;
+  (void)args;
+
+  size_t i = 0;
+  for(; i < size; ++i)
+  {
+    char c = __VERIFIER_nondet_char();
+    str[i] = c;
+    if(c == '\0')
+      break;
+  }
+
+  return i;
+}
+
+#endif
+
 /* FUNCTION: __srget */
 
 #ifdef __FreeBSD__

src/ansi-c/library_check.sh

@@ -38,12 +38,15 @@ perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
 perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS
 perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS
 perl -p -i -e 's/^_time(32|64)\n//' __functions # time, Windows
+perl -p -i -e 's/^__builtin___snprintf_chk\n//' __functions # snprintf, macOS
+perl -p -i -e 's/^__builtin___vsnprintf_chk\n//' __functions # vsnprintf, macOS
 perl -p -i -e 's/^__inet_(addr|aton|ntoa|network)\n//' __functions # inet_*, FreeBSD
 perl -p -i -e 's/^__isoc99_v?fscanf\n//' __functions # fscanf, Linux
 perl -p -i -e 's/^__isoc99_v?scanf\n//' __functions # scanf, Linux
 perl -p -i -e 's/^__isoc99_v?sscanf\n//' __functions # sscanf, Linux
 perl -p -i -e 's/^__sigsetjmp\n//' __functions # sigsetjmp, Linux
 perl -p -i -e 's/^__stdio_common_vfscanf\n//' __functions # fscanf, Windows
+perl -p -i -e 's/^__stdio_common_vsprintf\n//' __functions # snprintf, Windows
 perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
 perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
 perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD