1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
// This file is part of SymCC.
//
// SymCC is free software: you can redistribute it and/or modify it under the
// terms of the GNU General Public License as published by the Free Software
// Foundation, either version 3 of the License, or (at your option) any later
// version.
//
// SymCC is distributed in the hope that it will be useful, but WITHOUT ANY
// WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
// A PARTICULAR PURPOSE. See the GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License along with
// SymCC. If not, see <https://www.gnu.org/licenses/>.
// RUN: /bin/echo -ne "\x00\x00\x00\x05aaaa" > %T/%basename_t.input
// RUN: %symcc -O2 %s -o %t
// RUN: env SYMCC_INPUT_FILE=%T/%basename_t.input %t %T/%basename_t.input 2>&1 | %filecheck %s
#include <stdio.h>
#include <arpa/inet.h>
#include <fcntl.h>
#include <sys/stat.h>
#include <unistd.h>
int main(int argc, char* argv[]) {
//
// Read from the input file using Unix primitives.
//
// ANY-NOT: Warning
int fd = open(argv[1], O_RDONLY);
if (fd < 0) {
perror("failed to open the input file");
return -1;
}
int input;
if (read(fd, &input, sizeof(input)) != 4) {
perror("failed to read from the input file");
return -1;
}
input = ntohl(input);
int four_as;
if (read(fd, &four_as, sizeof(four_as)) != 4) {
perror("failed to read from the input file");
return -1;
}
int eof = 42;
if (read(fd, &eof, sizeof(eof)) != 0) {
perror("this should be exactly the end of the file");
return -1;
}
// Make sure that we haven't created a symbolic expression
if (eof == 42)
fprintf(stderr, "All is good.\n");
else
fprintf(stderr, "Why was the variable overwritten?\n");
// SIMPLE-NOT: Trying to solve
// QSYM-NOT: SMT
// ANY: All is good.
// SIMPLE: Trying to solve
// SIMPLE: Found diverging input
// QSYM-COUNT-2: SMT
// QSYM: New testcase
// ANY: Not sure
if (input >= 42)
fprintf(stderr, "This may be the answer.\n");
else
fprintf(stderr, "Not sure this is correct...\n");
//
// Rewind and read again.
//
if (lseek(fd, 4, SEEK_SET) != 4) {
perror("failed to rewind the file");
return -1;
}
if (read(fd, &four_as, sizeof(four_as)) < 0) {
perror("failed to read from the input file");
return -1;
}
// SIMPLE: Trying to solve
// SIMPLE: Found diverging input
// QSYM-COUNT-2: SMT
// QSYM: New testcase
// ANY: No.
if (four_as != (int)0x61616161)
fprintf(stderr, "The matrix has changed.\n");
else
fprintf(stderr, "No.\n");
//
// Read with the C standard library.
//
// ANY: Warning
FILE *file = fopen(argv[1], "r");
if (file == NULL) {
perror("failed to open the input file");
return -1;
}
int same_input;
if (fread(&same_input, sizeof(same_input), 1, file) < 0) {
perror("failed to read from the input file");
return -1;
}
same_input = ntohl(same_input);
// SIMPLE: Trying to solve
// QSYM-COUNT-2: SMT
// ANY: Yep
if (same_input == 5)
fprintf(stderr, "Yep, it's the test input.\n");
else
fprintf(stderr, "Not the test input!\n");
//
// Rewind and read again.
//
// fseek doesn't return the current offset (unlike lseek) - it just returns 0
// on success!
if (fseek(file, 4, SEEK_SET) != 0) {
perror("failed to rewind the file");
return -1;
}
int same_four_as;
if (fread(&same_four_as, sizeof(same_four_as), 1, file) < 0) {
perror("failed to read from the input file");
return -1;
}
// SIMPLE: Trying to solve
// QSYM-COUNT-2: SMT
// ANY: Still
if (same_four_as == (int)0x61616161)
fprintf(stderr, "Still the test input.\n");
else
fprintf(stderr, "Not the test input!\n");
return 0;
}