Skip to content

Commit 6f5ee62

Browse files
Saveliy Grigoryevsava-cska
authored andcommitted
Add support fopen
1 parent 9a117e9 commit 6f5ee62

8 files changed

Lines changed: 343 additions & 12 deletions

File tree

runtime/POSIX/fd.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ int __fd_open(const char *pathname, int flags, mode_t mode) {
156156
/* Should be the case if file was available, but just in case. */
157157
memset(f, 0, sizeof *f);
158158

159-
df = __get_sym_file(pathname);
159+
df = __get_sym_file(pathname);
160160
if (df) {
161161
/* XXX Should check access against mode / stat / possible
162162
deletion. */

runtime/POSIX/input_output.c

Lines changed: 113 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,82 @@
11
#include <stdio.h>
2+
#include <stdlib.h>
3+
#include <fcntl.h>
4+
#include <errno.h>
5+
6+
/*
7+
* Return the (stdio) flags for a given mode. Store the flags
8+
* to be passed to an open() syscall through *optr.
9+
* Return 0 on error.
10+
*/
11+
int convert_to_stdio_open_flags(const char *mode, int *optr) {
12+
int ret = 0, m = 0, o = 0;
13+
switch (*mode++) {
14+
case 'r': /* open for reading */
15+
ret = 1;
16+
m = O_RDONLY;
17+
o = 0;
18+
break;
19+
case 'w': /* open for writing */
20+
ret = 2;
21+
m = O_WRONLY;
22+
o = O_CREAT | O_TRUNC;
23+
break;
24+
case 'a': /* open for appending */
25+
ret = 2;
26+
m = O_WRONLY;
27+
o = O_CREAT | O_APPEND;
28+
break;
29+
default: /* illegal mode */
30+
errno = EINVAL;
31+
return 0;
32+
}
33+
/* [rwa]\+ or [rwa]b\+ means read and write */
34+
if (*mode == '+' || (*mode == 'b' && mode[1] == '+')) {
35+
ret = 3;
36+
m = O_RDWR;
37+
}
38+
*optr = m | o;
39+
return ret;
40+
}
41+
42+
FILE *fopen(const char *file, const char *mode) {
43+
FILE *fp;
44+
int f, oflags = 0;
45+
if (convert_to_stdio_open_flags(mode, &oflags) == 0)
46+
return NULL;
47+
if ((fp = malloc(sizeof(FILE))) == NULL)
48+
return NULL;
49+
if (oflags & O_CREAT) {
50+
if ((f = open(file, oflags, S_IRWXU)) < 0)
51+
return NULL;
52+
} else {
53+
if ((f = open(file, oflags)) < 0)
54+
return NULL;
55+
}
56+
fp->_fileno = f;
57+
fp->_mode = oflags;
58+
return fp;
59+
}
60+
61+
int get_file_descriptor(FILE *stream) {
62+
if (stream == stdin) {
63+
return 0;
64+
}
65+
if (stream == stdout) {
66+
return 1;
67+
}
68+
if (stream == stderr) {
69+
return 2;
70+
}
71+
return stream->_fileno;
72+
}
273

374
int fgetc(FILE *stream) {
4-
int fd = fileno(stream);
75+
if (stream == NULL) {
76+
return 0;
77+
}
78+
79+
int fd = get_file_descriptor(stream);
580
unsigned char buf;
681
ssize_t read_byte = read(fd, &buf, 1);
782
if (read_byte == 1) {
@@ -12,7 +87,11 @@ int fgetc(FILE *stream) {
1287
}
1388

1489
int getc(FILE *stream) {
15-
int fd = fileno(stream);
90+
if (stream == NULL) {
91+
return 0;
92+
}
93+
94+
int fd = get_file_descriptor(stream);
1695
unsigned char buf;
1796
ssize_t read_byte = read(fd, &buf, 1);
1897
if (read_byte == 1) {
@@ -23,18 +102,25 @@ int getc(FILE *stream) {
23102
}
24103

25104
size_t fread(void *buffer, size_t size, size_t count, FILE *stream) {
26-
int fd = fileno(stream);
105+
if (stream == NULL) {
106+
return 0;
107+
}
108+
109+
int fd = get_file_descriptor(stream);
27110
ssize_t read_byte = read(fd, buffer, size * count);
28111
if (read_byte == -1) {
29112
return 0;
30113
}
31114
return read_byte / size;
32115
}
33116

34-
char* fgets(char *s, int n, FILE *stream)
35-
{
117+
char* fgets(char *s, int n, FILE *stream) {
118+
if (stream == NULL) {
119+
return 0;
120+
}
121+
36122
char *p = s;
37-
if (s == NULL || n <= 0 || ferror(stream) || feof(stream)) {
123+
if (s == NULL || n <= 0) {
38124
return NULL;
39125
}
40126

@@ -44,7 +130,7 @@ char* fgets(char *s, int n, FILE *stream)
44130
break;
45131
}
46132
}
47-
if (ferror(stream) || (c == EOF && p == s)) {
133+
if (c == EOF && p == s) {
48134
return NULL;
49135
}
50136
*p = '\0';
@@ -77,7 +163,11 @@ char* gets(char *s)
77163
}
78164

79165
int fputc(int c, FILE *stream) {
80-
int fd = fileno(stream);
166+
if (stream == NULL) {
167+
return 0;
168+
}
169+
170+
int fd = get_file_descriptor(stream);
81171
unsigned char symb = c;
82172
int write_byte = write(fd, &symb, 1);
83173
if (write_byte == 1) {
@@ -88,7 +178,11 @@ int fputc(int c, FILE *stream) {
88178
}
89179

90180
int putc(int c, FILE *stream) {
91-
int fd = fileno(stream);
181+
if (stream == NULL) {
182+
return 0;
183+
}
184+
185+
int fd = get_file_descriptor(stream);
92186
unsigned char symb = c;
93187
int write_byte = write(fd, &symb, 1);
94188
if (write_byte == 1) {
@@ -99,16 +193,24 @@ int putc(int c, FILE *stream) {
99193
}
100194

101195
size_t fwrite(const void *buffer, size_t size, size_t count, FILE *stream) {
102-
int fd = fileno(stream);
196+
if (stream == NULL) {
197+
return 0;
198+
}
199+
200+
int fd = get_file_descriptor(stream);
103201
void *cop_buf = buffer;
104202
int write_byte = write(fd, cop_buf, size * count);
105-
if (write == -1) {
203+
if (write_byte == -1) {
106204
return 0;
107205
}
108206
return write_byte / size;
109207
}
110208

111209
int fputs(const char *str, FILE *stream) {
210+
if (stream == NULL) {
211+
return 0;
212+
}
213+
112214
if (str == NULL) {
113215
return EOF;
114216
}
Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
// REQUIRES: geq-llvm-10.0
2+
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
3+
// RUN: rm -rf %t.klee-out
4+
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64 --sym-files 3 64
5+
// RUN: test -f %t.klee-out/test000001.ktestjson
6+
// RUN: test -f %t.klee-out/test000002.ktestjson
7+
// RUN: test -f %t.klee-out/test000003.ktestjson
8+
// RUN: test -f %t.klee-out/test000004.ktestjson
9+
// RUN: test -f %t.klee-out/test000005.ktestjson
10+
// RUN: test -f %t.klee-out/test000006.ktestjson
11+
// RUN: test -f %t.klee-out/test000007.ktestjson
12+
// RUN: test -f %t.klee-out/test000008.ktestjson
13+
// RUN: test -f %t.klee-out/test000009.ktestjson
14+
// RUN: test -f %t.klee-out/test000010.ktestjson
15+
// RUN: test -f %t.klee-out/test000011.ktestjson
16+
// RUN: test -f %t.klee-out/test000012.ktestjson
17+
// RUN: test -f %t.klee-out/test000013.ktestjson
18+
// RUN: not test -f %t.klee-out/test000014.ktestjson
19+
20+
#include <stdio.h>
21+
22+
int main() {
23+
FILE *fA = fopen("A", "r");
24+
FILE *fB = fopen("B", "r");
25+
FILE *fC = fopen("C", "r");
26+
unsigned char x = fgetc(fA);
27+
if (x >= '0' && x <= '9') {
28+
unsigned char a = fgetc(fB);
29+
if (a >= 'a' && a <= 'z') {
30+
return 1;
31+
} else {
32+
return 2;
33+
}
34+
} else {
35+
unsigned char a = fgetc(fC);
36+
unsigned char b = fgetc(fA);
37+
if (a >= 'a' && a <= 'z') {
38+
if (b >= '0' && b <= '9') {
39+
return 3;
40+
} else {
41+
return 4;
42+
}
43+
} else {
44+
return 5;
45+
}
46+
}
47+
}
Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
// REQUIRES: geq-llvm-10.0
2+
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
3+
// RUN: rm -rf %t.klee-out
4+
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64 --sym-files 1 64
5+
// RUN: test -f %t.klee-out/test000001.ktestjson
6+
// RUN: test -f %t.klee-out/test000002.ktestjson
7+
// RUN: test -f %t.klee-out/test000003.ktestjson
8+
// RUN: test -f %t.klee-out/test000004.ktestjson
9+
// RUN: test -f %t.klee-out/test000005.ktestjson
10+
// RUN: test -f %t.klee-out/test000006.ktestjson
11+
// RUN: test -f %t.klee-out/test000007.ktestjson
12+
// RUN: test -f %t.klee-out/test000008.ktestjson
13+
// RUN: test -f %t.klee-out/test000009.ktestjson
14+
// RUN: test -f %t.klee-out/test000010.ktestjson
15+
// RUN: test -f %t.klee-out/test000011.ktestjson
16+
// RUN: test -f %t.klee-out/test000012.ktestjson
17+
// RUN: test -f %t.klee-out/test000013.ktestjson
18+
// RUN: test -f %t.klee-out/test000014.ktestjson
19+
// RUN: test -f %t.klee-out/test000015.ktestjson
20+
// RUN: test -f %t.klee-out/test000016.ktestjson
21+
// RUN: test -f %t.klee-out/test000017.ktestjson
22+
// RUN: test -f %t.klee-out/test000018.ktestjson
23+
// RUN: test -f %t.klee-out/test000019.ktestjson
24+
// RUN: test -f %t.klee-out/test000020.ktestjson
25+
// RUN: test -f %t.klee-out/test000021.ktestjson
26+
// RUN: not test -f %t.klee-out/test000022.ktestjson
27+
28+
#include <stdio.h>
29+
30+
int main() {
31+
FILE *fA = fopen("A", "r");
32+
char a[8];
33+
fgets(a, 6, fA);
34+
if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
35+
return 1;
36+
}
37+
return 0;
38+
}
Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64 --sym-files 1 64
4+
// RUN: test -f %t.klee-out/test000001.ktestjson
5+
// RUN: test -f %t.klee-out/test000002.ktestjson
6+
// RUN: test -f %t.klee-out/test000003.ktestjson
7+
// RUN: test -f %t.klee-out/test000004.ktestjson
8+
// RUN: test -f %t.klee-out/test000005.ktestjson
9+
// RUN: test -f %t.klee-out/test000006.ktestjson
10+
// RUN: not test -f %t.klee-out/test000007.ktestjson
11+
12+
#include "klee/klee.h"
13+
#include <stdio.h>
14+
15+
char simple_fputc(int x, int y) {
16+
FILE *fA = fopen("A", "w");
17+
if (x < y) {
18+
fputc('<', fA);
19+
return '<';
20+
} else if (x > y) {
21+
fputc('>', fA);
22+
return '>';
23+
} else {
24+
fputc('=', fA);
25+
return '=';
26+
}
27+
}
28+
29+
int main() {
30+
int x, y;
31+
klee_make_symbolic(&x, sizeof(int), "x");
32+
klee_make_symbolic(&y, sizeof(int), "y");
33+
char c = simple_fputc(x, y);
34+
return 0;
35+
}
Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64 --sym-files 1 64
4+
// RUN: test -f %t.klee-out/test000001.ktestjson
5+
// RUN: test -f %t.klee-out/test000002.ktestjson
6+
// RUN: test -f %t.klee-out/test000003.ktestjson
7+
// RUN: test -f %t.klee-out/test000004.ktestjson
8+
// RUN: test -f %t.klee-out/test000005.ktestjson
9+
// RUN: test -f %t.klee-out/test000006.ktestjson
10+
// RUN: test -f %t.klee-out/test000007.ktestjson
11+
// RUN: test -f %t.klee-out/test000008.ktestjson
12+
// RUN: test -f %t.klee-out/test000009.ktestjson
13+
// RUN: test -f %t.klee-out/test000010.ktestjson
14+
// RUN: test -f %t.klee-out/test000011.ktestjson
15+
// RUN: test -f %t.klee-out/test000012.ktestjson
16+
// RUN: not test -f %t.klee-out/test000013.ktestjson
17+
18+
#include "klee/klee.h"
19+
#include <stdio.h>
20+
21+
char simple_fputs(char c) {
22+
FILE *fA = fopen("A", "w");
23+
if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
24+
char a[] = "Vowel";
25+
fputs("Vowel", fA);
26+
return 'V';
27+
} else {
28+
char a[] = "Consonant";
29+
fputs("Consonant", fA);
30+
return 'C';
31+
}
32+
}
33+
34+
int main() {
35+
char c;
36+
klee_make_symbolic(&c, sizeof(char), "c");
37+
char d = simple_fputs(c);
38+
return 0;
39+
}
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// REQUIRES: geq-llvm-10.0
2+
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
3+
// RUN: rm -rf %t.klee-out
4+
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64 --sym-files 2 64
5+
// RUN: test -f %t.klee-out/test000001.ktestjson
6+
// RUN: test -f %t.klee-out/test000002.ktestjson
7+
// RUN: test -f %t.klee-out/test000003.ktestjson
8+
// RUN: not test -f %t.klee-out/test000004.ktestjson
9+
10+
#include <stdio.h>
11+
12+
int main() {
13+
FILE *fA = fopen("A", "r");
14+
FILE *fB = fopen("B", "r");
15+
16+
int arrA[4];
17+
int arrB[4];
18+
fread(arrA, sizeof(int), 4, fA);
19+
fread(arrB, sizeof(int), 4, fB);
20+
21+
int sumA = 0, sumB = 0;
22+
for (int i = 0; i < 4; i++) {
23+
sumA += arrA[i];
24+
sumB += arrB[i];
25+
}
26+
if (sumA == sumB) {
27+
return 0;
28+
} else if (sumA > sumB) {
29+
return 1;
30+
} else {
31+
return -1;
32+
}
33+
}

0 commit comments

Comments
 (0)