C library: handle side effects of scanf

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

@@ -3,7 +3,20 @@
 
 int main()
 {
-  scanf();
-  assert(0);
+  scanf(""); // parse nothing, must not result in any out-of-bounds access
+  int x = 0;
+  scanf("%d", &x);
+  _Bool nondet;
+  if(nondet)
+    __CPROVER_assert(x == 0, "need not remain zero");
+  else
+    __CPROVER_assert(x != 0, "may remain zero");
+  long int lx = 0;
+  long long int llx = 0;
+  scanf("%d, %ld, %lld", &x, &lx, &llx);
+  if(nondet)
+    __CPROVER_assert(lx + llx == 0, "need not remain zero");
+  else
+    __CPROVER_assert(lx + llx != 0, "may remain zero");
   return 0;
 }

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

@@ -1,8 +1,13 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+\[main.assertion.1\] line 11 need not remain zero: FAILURE$
+\[main.assertion.2\] line 13 may remain zero: FAILURE$
+\[main.assertion.3\] line 18 need not remain zero: FAILURE$
+\[main.assertion.4\] line 20 may remain zero: FAILURE$
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

src/ansi-c/library/stdio.c

@@ -888,6 +888,28 @@ __CPROVER_HIDE:;
   return result;
 }
 
+/* FUNCTION: __isoc99_scanf */
+
+#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 __isoc99_scanf(const char *restrict format, ...)
+{
+__CPROVER_HIDE:;
+  va_list list;
+  va_start(list, format);
+  int result = vfscanf(stdin, format, list);
+  va_end(list);
+  return result;
+}
+
 /* FUNCTION: sscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -910,6 +932,28 @@ __CPROVER_HIDE:;
   return result;
 }
 
+/* FUNCTION: __isoc99_sscanf */
+
+#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 __isoc99_sscanf(const char *restrict s, const char *restrict format, ...)
+{
+__CPROVER_HIDE:;
+  va_list list;
+  va_start(list, format);
+  int result = vsscanf(s, format, list);
+  va_end(list);
+  return result;
+}
+
 /* FUNCTION: vfscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -939,7 +983,12 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
   }
 
   (void)*format;
-  (void)arg;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -949,6 +998,104 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
   return result;
 }
 
+/* FUNCTION: __isoc99_vfscanf */
+
+#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 __VERIFIER_nondet_int();
+
+int __isoc99_vfscanf(
+  FILE *restrict stream,
+  const char *restrict format,
+  va_list arg)
+{
+__CPROVER_HIDE:;
+  int result = __VERIFIER_nondet_int();
+
+  if(stream != stdin)
+  {
+#if !defined(__linux__) || defined(__GLIBC__)
+    (void)*stream;
+#else
+    (void)*(char *)stream;
+#endif
+  }
+
+  (void)*format;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+  __CPROVER_assert(
+    __CPROVER_get_must(stream, "open"), "vfscanf file must be open");
+#endif
+
+  return result;
+}
+
+/* FUNCTION: __stdio_common_vfscanf */
+
+#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
+
+int __VERIFIER_nondet_int();
+
+int __stdio_common_vfscanf(
+  unsigned __int64 options,
+  FILE *stream,
+  char const *format,
+  _locale_t locale,
+  va_list args)
+{
+  (void)options;
+  (void)locale;
+
+  int result = __VERIFIER_nondet_int();
+
+  if(stream != stdin)
+  {
+    (void)*(char *)stream;
+  }
+
+  (void)*format;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
+        __CPROVER_OBJECT_SIZE(args))
+  {
+    void *a = va_arg(args, void *);
+    __CPROVER_havoc_object(a);
+  }
+
+#  ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+  __CPROVER_assert(
+    __CPROVER_get_must(stream, "open"), "vfscanf file must be open");
+#  endif
+
+  return result;
+}
+
+#endif
+
 /* FUNCTION: vscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -967,6 +1114,24 @@ int vscanf(const char *restrict format, va_list arg)
   return vfscanf(stdin, format, arg);
 }
 
+/* FUNCTION: __isoc99_vscanf */
+
+#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 __isoc99_vscanf(const char *restrict format, va_list arg)
+{
+__CPROVER_HIDE:;
+  return vfscanf(stdin, format, arg);
+}
+
 /* FUNCTION: vsscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -983,14 +1148,96 @@ int __VERIFIER_nondet_int();
 
 int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
 {
-  __CPROVER_HIDE:;
-  int result=__VERIFIER_nondet_int();
+__CPROVER_HIDE:;
+  int result = __VERIFIER_nondet_int();
   (void)*s;
   (void)*format;
-  (void)arg;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+
+  return result;
+}
+
+/* FUNCTION: __isoc99_vsscanf */
+
+#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 __VERIFIER_nondet_int();
+
+int __isoc99_vsscanf(
+  const char *restrict s,
+  const char *restrict format,
+  va_list arg)
+{
+__CPROVER_HIDE:;
+  int result = __VERIFIER_nondet_int();
+  (void)*s;
+  (void)*format;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+
   return result;
 }
 
+/* FUNCTION: __stdio_common_vsscanf */
+
+#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
+
+int __VERIFIER_nondet_int();
+
+int __stdio_common_vsscanf(
+  unsigned __int64 options,
+  char const *s,
+  size_t buffer_count,
+  char const *format,
+  _locale_t locale,
+  va_list args)
+{
+  (void)options;
+  (void)locale;
+
+  int result = __VERIFIER_nondet_int();
+
+  (void)*s;
+  (void)*format;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
+        __CPROVER_OBJECT_SIZE(args))
+  {
+    void *a = va_arg(args, void *);
+    __CPROVER_havoc_object(a);
+  }
+
+  return result;
+}
+
+#endif
+
 /* FUNCTION: printf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED