Skip to content

Commit 8848ad8

Browse files
tautschnigtautschnig
authored
Merge pull request #7369 from tautschnig/feature/scanf
C library: handle side effects of scanf
2 parents 9bb422d + a165746 commit 8848ad8

File tree

3 files changed

+274
-9
lines changed

3 files changed

+274
-9
lines changed

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

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,20 @@
33

44
int main()
55
{
6-
scanf();
7-
assert(0);
6+
scanf(""); // parse nothing, must not result in any out-of-bounds access
7+
int x = 0;
8+
scanf("%d", &x);
9+
_Bool nondet;
10+
if(nondet)
11+
__CPROVER_assert(x == 0, "need not remain zero");
12+
else
13+
__CPROVER_assert(x != 0, "may remain zero");
14+
long int lx = 0;
15+
long long int llx = 0;
16+
scanf("%d, %ld, %lld", &x, &lx, &llx);
17+
if(nondet)
18+
__CPROVER_assert(lx + llx == 0, "need not remain zero");
19+
else
20+
__CPROVER_assert(lx + llx != 0, "may remain zero");
821
return 0;
922
}

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

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
4-
^EXIT=0$
4+
\[main.assertion.1\] line 11 need not remain zero: FAILURE$
5+
\[main.assertion.2\] line 13 may remain zero: FAILURE$
6+
\[main.assertion.3\] line 18 need not remain zero: FAILURE$
7+
\[main.assertion.4\] line 20 may remain zero: FAILURE$
8+
^\*\* 4 of \d+ failed
9+
^VERIFICATION FAILED$
10+
^EXIT=10$
511
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
712
--
813
^warning: ignoring

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

Lines changed: 251 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -888,6 +888,28 @@ __CPROVER_HIDE:;
888888
return result;
889889
}
890890

891+
/* FUNCTION: __isoc99_scanf */
892+
893+
#ifndef __CPROVER_STDIO_H_INCLUDED
894+
# include <stdio.h>
895+
# define __CPROVER_STDIO_H_INCLUDED
896+
#endif
897+
898+
#ifndef __CPROVER_STDARG_H_INCLUDED
899+
# include <stdarg.h>
900+
# define __CPROVER_STDARG_H_INCLUDED
901+
#endif
902+
903+
int __isoc99_scanf(const char *restrict format, ...)
904+
{
905+
__CPROVER_HIDE:;
906+
va_list list;
907+
va_start(list, format);
908+
int result = vfscanf(stdin, format, list);
909+
va_end(list);
910+
return result;
911+
}
912+
891913
/* FUNCTION: sscanf */
892914

893915
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -910,6 +932,28 @@ __CPROVER_HIDE:;
910932
return result;
911933
}
912934

935+
/* FUNCTION: __isoc99_sscanf */
936+
937+
#ifndef __CPROVER_STDIO_H_INCLUDED
938+
# include <stdio.h>
939+
# define __CPROVER_STDIO_H_INCLUDED
940+
#endif
941+
942+
#ifndef __CPROVER_STDARG_H_INCLUDED
943+
# include <stdarg.h>
944+
# define __CPROVER_STDARG_H_INCLUDED
945+
#endif
946+
947+
int __isoc99_sscanf(const char *restrict s, const char *restrict format, ...)
948+
{
949+
__CPROVER_HIDE:;
950+
va_list list;
951+
va_start(list, format);
952+
int result = vsscanf(s, format, list);
953+
va_end(list);
954+
return result;
955+
}
956+
913957
/* FUNCTION: vfscanf */
914958

915959
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -939,7 +983,12 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
939983
}
940984

941985
(void)*format;
942-
(void)arg;
986+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
987+
__CPROVER_OBJECT_SIZE(arg))
988+
{
989+
void *a = va_arg(arg, void *);
990+
__CPROVER_havoc_object(a);
991+
}
943992

944993
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
945994
__CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -949,6 +998,104 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
949998
return result;
950999
}
9511000

1001+
/* FUNCTION: __isoc99_vfscanf */
1002+
1003+
#ifndef __CPROVER_STDIO_H_INCLUDED
1004+
# include <stdio.h>
1005+
# define __CPROVER_STDIO_H_INCLUDED
1006+
#endif
1007+
1008+
#ifndef __CPROVER_STDARG_H_INCLUDED
1009+
# include <stdarg.h>
1010+
# define __CPROVER_STDARG_H_INCLUDED
1011+
#endif
1012+
1013+
int __VERIFIER_nondet_int();
1014+
1015+
int __isoc99_vfscanf(
1016+
FILE *restrict stream,
1017+
const char *restrict format,
1018+
va_list arg)
1019+
{
1020+
__CPROVER_HIDE:;
1021+
int result = __VERIFIER_nondet_int();
1022+
1023+
if(stream != stdin)
1024+
{
1025+
#if !defined(__linux__) || defined(__GLIBC__)
1026+
(void)*stream;
1027+
#else
1028+
(void)*(char *)stream;
1029+
#endif
1030+
}
1031+
1032+
(void)*format;
1033+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
1034+
__CPROVER_OBJECT_SIZE(arg))
1035+
{
1036+
void *a = va_arg(arg, void *);
1037+
__CPROVER_havoc_object(a);
1038+
}
1039+
1040+
#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1041+
__CPROVER_assert(
1042+
__CPROVER_get_must(stream, "open"), "vfscanf file must be open");
1043+
#endif
1044+
1045+
return result;
1046+
}
1047+
1048+
/* FUNCTION: __stdio_common_vfscanf */
1049+
1050+
#ifdef _WIN32
1051+
1052+
# ifndef __CPROVER_STDIO_H_INCLUDED
1053+
# include <stdio.h>
1054+
# define __CPROVER_STDIO_H_INCLUDED
1055+
# endif
1056+
1057+
# ifndef __CPROVER_STDARG_H_INCLUDED
1058+
# include <stdarg.h>
1059+
# define __CPROVER_STDARG_H_INCLUDED
1060+
# endif
1061+
1062+
int __VERIFIER_nondet_int();
1063+
1064+
int __stdio_common_vfscanf(
1065+
unsigned __int64 options,
1066+
FILE *stream,
1067+
char const *format,
1068+
_locale_t locale,
1069+
va_list args)
1070+
{
1071+
(void)options;
1072+
(void)locale;
1073+
1074+
int result = __VERIFIER_nondet_int();
1075+
1076+
if(stream != stdin)
1077+
{
1078+
(void)*(char *)stream;
1079+
}
1080+
1081+
(void)*format;
1082+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
1083+
__CPROVER_OBJECT_SIZE(args))
1084+
{
1085+
void *a = va_arg(args, void *);
1086+
__CPROVER_havoc_object(a);
1087+
}
1088+
1089+
# ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
1090+
__CPROVER_assert(
1091+
__CPROVER_get_must(stream, "open"), "vfscanf file must be open");
1092+
# endif
1093+
1094+
return result;
1095+
}
1096+
1097+
#endif
1098+
9521099
/* FUNCTION: vscanf */
9531100

9541101
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -967,6 +1114,24 @@ int vscanf(const char *restrict format, va_list arg)
9671114
return vfscanf(stdin, format, arg);
9681115
}
9691116

1117+
/* FUNCTION: __isoc99_vscanf */
1118+
1119+
#ifndef __CPROVER_STDIO_H_INCLUDED
1120+
# include <stdio.h>
1121+
# define __CPROVER_STDIO_H_INCLUDED
1122+
#endif
1123+
1124+
#ifndef __CPROVER_STDARG_H_INCLUDED
1125+
# include <stdarg.h>
1126+
# define __CPROVER_STDARG_H_INCLUDED
1127+
#endif
1128+
1129+
int __isoc99_vscanf(const char *restrict format, va_list arg)
1130+
{
1131+
__CPROVER_HIDE:;
1132+
return vfscanf(stdin, format, arg);
1133+
}
1134+
9701135
/* FUNCTION: vsscanf */
9711136

9721137
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -983,14 +1148,96 @@ int __VERIFIER_nondet_int();
9831148

9841149
int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
9851150
{
986-
__CPROVER_HIDE:;
987-
int result=__VERIFIER_nondet_int();
1151+
__CPROVER_HIDE:;
1152+
int result = __VERIFIER_nondet_int();
9881153
(void)*s;
9891154
(void)*format;
990-
(void)arg;
1155+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
1156+
__CPROVER_OBJECT_SIZE(arg))
1157+
{
1158+
void *a = va_arg(arg, void *);
1159+
__CPROVER_havoc_object(a);
1160+
}
1161+
1162+
return result;
1163+
}
1164+
1165+
/* FUNCTION: __isoc99_vsscanf */
1166+
1167+
#ifndef __CPROVER_STDIO_H_INCLUDED
1168+
# include <stdio.h>
1169+
# define __CPROVER_STDIO_H_INCLUDED
1170+
#endif
1171+
1172+
#ifndef __CPROVER_STDARG_H_INCLUDED
1173+
# include <stdarg.h>
1174+
# define __CPROVER_STDARG_H_INCLUDED
1175+
#endif
1176+
1177+
int __VERIFIER_nondet_int();
1178+
1179+
int __isoc99_vsscanf(
1180+
const char *restrict s,
1181+
const char *restrict format,
1182+
va_list arg)
1183+
{
1184+
__CPROVER_HIDE:;
1185+
int result = __VERIFIER_nondet_int();
1186+
(void)*s;
1187+
(void)*format;
1188+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
1189+
__CPROVER_OBJECT_SIZE(arg))
1190+
{
1191+
void *a = va_arg(arg, void *);
1192+
__CPROVER_havoc_object(a);
1193+
}
1194+
9911195
return result;
9921196
}
9931197

1198+
/* FUNCTION: __stdio_common_vsscanf */
1199+
1200+
#ifdef _WIN32
1201+
1202+
# ifndef __CPROVER_STDIO_H_INCLUDED
1203+
# include <stdio.h>
1204+
# define __CPROVER_STDIO_H_INCLUDED
1205+
# endif
1206+
1207+
# ifndef __CPROVER_STDARG_H_INCLUDED
1208+
# include <stdarg.h>
1209+
# define __CPROVER_STDARG_H_INCLUDED
1210+
# endif
1211+
1212+
int __VERIFIER_nondet_int();
1213+
1214+
int __stdio_common_vsscanf(
1215+
unsigned __int64 options,
1216+
char const *s,
1217+
size_t buffer_count,
1218+
char const *format,
1219+
_locale_t locale,
1220+
va_list args)
1221+
{
1222+
(void)options;
1223+
(void)locale;
1224+
1225+
int result = __VERIFIER_nondet_int();
1226+
1227+
(void)*s;
1228+
(void)*format;
1229+
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
1230+
__CPROVER_OBJECT_SIZE(args))
1231+
{
1232+
void *a = va_arg(args, void *);
1233+
__CPROVER_havoc_object(a);
1234+
}
1235+
1236+
return result;
1237+
}
1238+
1239+
#endif
1240+
9941241
/* FUNCTION: printf */
9951242

9961243
#ifndef __CPROVER_STDIO_H_INCLUDED

0 commit comments

Comments
 (0)