1 //===-- fd_init.c ---------------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9
10 #define _LARGEFILE64_SOURCE
11 #define _FILE_OFFSET_BITS 64
12 #include "fd.h"
13
14 #include "klee/klee.h"
15
16 #include <assert.h>
17 #include <stdio.h>
18 #include <stdlib.h>
19 #include <string.h>
20 #include <sys/stat.h>
21 #include <sys/syscall.h>
22 #include <unistd.h>
23
24 exe_file_system_t __exe_fs;
25
26 /* NOTE: It is important that these are statically initialized
27 correctly, since things that run before main may hit them given the
28 current way things are linked. */
29
30 /* XXX Technically these flags are initialized w.o.r. to the
31 environment we are actually running in. We could patch them in
32 klee_init_fds, but we still have the problem that uclibc calls
33 prior to main will get the wrong data. Not such a big deal since we
34 mostly care about sym case anyway. */
35
36
37 exe_sym_env_t __exe_env = {
38 {{ 0, eOpen | eReadable, 0, 0},
39 { 1, eOpen | eWriteable, 0, 0},
40 { 2, eOpen | eWriteable, 0, 0}},
41 022,
42 0,
43 0
44 };
45
__create_new_dfile(exe_disk_file_t * dfile,unsigned size,const char * name,struct stat64 * defaults)46 static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
47 const char *name, struct stat64 *defaults) {
48 struct stat64 *s = malloc(sizeof(*s));
49 const char *sp;
50 char sname[64];
51 for (sp=name; *sp; ++sp)
52 sname[sp-name] = *sp;
53 memcpy(&sname[sp-name], "-stat", 6);
54
55 assert(size);
56
57 dfile->size = size;
58 dfile->contents = malloc(dfile->size);
59 klee_make_symbolic(dfile->contents, dfile->size, name);
60
61 klee_make_symbolic(s, sizeof(*s), sname);
62
63 /* For broken tests */
64 if (!klee_is_symbolic(s->st_ino) &&
65 (s->st_ino & 0x7FFFFFFF) == 0)
66 s->st_ino = defaults->st_ino;
67
68 /* Important since we copy this out through getdents, and readdir
69 will otherwise skip this entry. For same reason need to make sure
70 it fits in low bits. */
71 klee_assume((s->st_ino & 0x7FFFFFFF) != 0);
72
73 /* uclibc opendir uses this as its buffer size, try to keep
74 reasonable. */
75 klee_assume((s->st_blksize & ~0xFFFF) == 0);
76
77 klee_prefer_cex(s, !(s->st_mode & ~(S_IFMT | 0777)));
78 klee_prefer_cex(s, s->st_dev == defaults->st_dev);
79 klee_prefer_cex(s, s->st_rdev == defaults->st_rdev);
80 klee_prefer_cex(s, (s->st_mode&0700) == 0600);
81 klee_prefer_cex(s, (s->st_mode&0070) == 0040);
82 klee_prefer_cex(s, (s->st_mode&0007) == 0004);
83 klee_prefer_cex(s, (s->st_mode&S_IFMT) == S_IFREG);
84 klee_prefer_cex(s, s->st_nlink == 1);
85 klee_prefer_cex(s, s->st_uid == defaults->st_uid);
86 klee_prefer_cex(s, s->st_gid == defaults->st_gid);
87 klee_prefer_cex(s, s->st_blksize == 4096);
88 klee_prefer_cex(s, s->st_atime == defaults->st_atime);
89 klee_prefer_cex(s, s->st_mtime == defaults->st_mtime);
90 klee_prefer_cex(s, s->st_ctime == defaults->st_ctime);
91
92 s->st_size = dfile->size;
93 s->st_blocks = 8;
94 dfile->stat = s;
95 }
96
__sym_uint32(const char * name)97 static unsigned __sym_uint32(const char *name) {
98 unsigned x;
99 klee_make_symbolic(&x, sizeof x, name);
100 return x;
101 }
102
103 /* n_files: number of symbolic input files, excluding stdin
104 file_length: size in bytes of each symbolic file, including stdin
105 sym_stdout_flag: 1 if stdout should be symbolic, 0 otherwise
106 save_all_writes_flag: 1 if all writes are executed as expected, 0 if
107 writes past the initial file size are discarded
108 (file offset is always incremented)
109 max_failures: maximum number of system call failures */
klee_init_fds(unsigned n_files,unsigned file_length,unsigned stdin_length,int sym_stdout_flag,int save_all_writes_flag,unsigned max_failures)110 void klee_init_fds(unsigned n_files, unsigned file_length,
111 unsigned stdin_length, int sym_stdout_flag,
112 int save_all_writes_flag, unsigned max_failures) {
113 unsigned k;
114 char name[7] = "?-data";
115 struct stat64 s;
116
117 stat64(".", &s);
118
119 __exe_fs.n_sym_files = n_files;
120 __exe_fs.sym_files = malloc(sizeof(*__exe_fs.sym_files) * n_files);
121 for (k=0; k < n_files; k++) {
122 name[0] = 'A' + k;
123 __create_new_dfile(&__exe_fs.sym_files[k], file_length, name, &s);
124 }
125
126 /* setting symbolic stdin */
127 if (stdin_length) {
128 __exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin));
129 __create_new_dfile(__exe_fs.sym_stdin, stdin_length, "stdin", &s);
130 __exe_env.fds[0].dfile = __exe_fs.sym_stdin;
131 }
132 else __exe_fs.sym_stdin = NULL;
133
134 __exe_fs.max_failures = max_failures;
135 if (__exe_fs.max_failures) {
136 __exe_fs.read_fail = malloc(sizeof(*__exe_fs.read_fail));
137 __exe_fs.write_fail = malloc(sizeof(*__exe_fs.write_fail));
138 __exe_fs.close_fail = malloc(sizeof(*__exe_fs.close_fail));
139 __exe_fs.ftruncate_fail = malloc(sizeof(*__exe_fs.ftruncate_fail));
140 __exe_fs.getcwd_fail = malloc(sizeof(*__exe_fs.getcwd_fail));
141
142 klee_make_symbolic(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
143 klee_make_symbolic(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
144 klee_make_symbolic(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
145 klee_make_symbolic(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
146 klee_make_symbolic(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
147 }
148
149 /* setting symbolic stdout */
150 if (sym_stdout_flag) {
151 __exe_fs.sym_stdout = malloc(sizeof(*__exe_fs.sym_stdout));
152 __create_new_dfile(__exe_fs.sym_stdout, 1024, "stdout", &s);
153 __exe_env.fds[1].dfile = __exe_fs.sym_stdout;
154 __exe_fs.stdout_writes = 0;
155 }
156 else __exe_fs.sym_stdout = NULL;
157
158 __exe_env.save_all_writes = save_all_writes_flag;
159 __exe_env.version = __sym_uint32("model_version");
160 klee_assume(__exe_env.version == 1);
161 }
162