[klee-commits] [1515] Changes to the way we represent connections.
cristic at stanford.edu
cristic at stanford.edu
Wed Mar 18 17:33:39 PDT 2009
Revision: 1515
http://keeda.stanford.edu/viewvc/viewvc.cgi?view=rev&revision=1515
Author: cristic
Date: 2009-03-18 17:33:39 -0700 (Wed, 18 Mar 2009)
Log Message:
-----------
Changes to the way we represent connections.
Moved exe_conn_t structure inside exe_disk_file_t structure.
Making peer address symbolic.
Other smaller changes.
Modified Paths:
--------------
models/simple/fd.h
models/simple/fd_init.c
models/simple/sockets.c
Modified: models/simple/fd.h
===================================================================
--- models/simple/fd.h 2009-03-19 00:04:59 UTC (rev 1514)
+++ models/simple/fd.h 2009-03-19 00:33:39 UTC (rev 1515)
@@ -9,19 +9,19 @@
#include <dirent.h>
#include <netinet/in.h>
+typedef struct {
+ struct sockaddr_storage *localaddr, *remoteaddr;
+ socklen_t localaddrlen, remoteaddrlen;
+} exe_conn_t;
+
typedef struct {
- unsigned size; /* in bytes */
+ unsigned size; /* in bytes */
char* contents;
struct stat64* stat;
+ exe_conn_t *conn; /* ptr to a connection, if a symbolic connected
+ socket. */
} exe_disk_file_t;
-typedef struct {
- struct sockaddr_storage localaddr;
- struct sockaddr_storage remoteaddr;
- socklen_t localaddrlen;
- socklen_t remoteaddrlen;
-} exe_conn_t;
-
typedef enum {
eOpen = (1 << 0),
eCloseOnExec = (1 << 1),
@@ -37,9 +37,6 @@
has eOpen. */
off64_t off; /* offset */
exe_disk_file_t* dfile; /* ptr to file on disk, if symbolic */
- exe_conn_t *conn; /* ptr to a connection, if a symbolic
- connected socket. If non-null, dfile
- is non-null either */
} exe_file_t;
typedef struct {
Modified: models/simple/fd_init.c
===================================================================
--- models/simple/fd_init.c 2009-03-19 00:04:59 UTC (rev 1514)
+++ models/simple/fd_init.c 2009-03-19 00:33:39 UTC (rev 1515)
@@ -26,28 +26,30 @@
exe_sym_env_t __exe_env = {
- {{ 0, eOpen | eReadable, 0, 0, 0},
- { 1, eOpen | eWriteable, 0, 0, 0},
- { 2, eOpen | eWriteable, 0, 0, 0}},
+ {{ 0, eOpen | eReadable, 0, 0},
+ { 1, eOpen | eWriteable, 0, 0},
+ { 2, eOpen | eWriteable, 0, 0}},
022,
0,
0
};
static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
- const char *name, struct stat64 *defaults) {
+ const char *name, struct stat64 *defaults,
+ int is_conn) {
struct stat64 *s = malloc(sizeof(*s));
const char *sp;
- char sname[64];
+ char stat_name[64], conn_name[64];
+
for (sp=name; *sp; ++sp)
- sname[sp-name] = *sp;
- memcpy(&sname[sp-name], "-stat", 6);
+ stat_name[sp-name] = *sp;
+ memcpy(&stat_name[sp-name], "-stat", 6);
dfile->size = size;
dfile->contents = malloc(dfile->size);
klee_make_symbolic_name(dfile->contents, dfile->size, name);
- klee_make_symbolic_name(s, sizeof(*s), sname);
+ klee_make_symbolic_name(s, sizeof(*s), stat_name);
/* For broken tests */
if (!klee_is_symbolic(s->st_ino) &&
@@ -81,6 +83,20 @@
s->st_size = dfile->size;
s->st_blocks = 8;
dfile->stat = s;
+
+ dfile->conn = NULL;
+ if (is_conn) {
+ klee_assume((dfile->stat->st_mode & S_IFMT) == S_IFSOCK);
+
+ for (sp=name; *sp; ++sp)
+ conn_name[sp-name] = *sp;
+ memcpy(&conn_name[sp-name], "-conn", 6);
+
+ dfile->conn = calloc(1, sizeof(*(dfile->conn)));
+ dfile->conn->localaddr = calloc(1, sizeof(*(dfile->conn->localaddr)));
+ dfile->conn->remoteaddr = malloc(sizeof(*(dfile->conn->localaddr)));
+ klee_make_symbolic_name(dfile->conn, sizeof(*dfile->conn), conn_name);
+ }
}
static unsigned __sym_uint32(const char *name) {
@@ -110,13 +126,13 @@
__exe_fs.sym_files = malloc(sizeof(*__exe_fs.sym_files) * n_files);
for (k=0; k < n_files; k++) {
name[0] = 'A' + k;
- __create_new_dfile(&__exe_fs.sym_files[k], file_length, name, &s);
+ __create_new_dfile(&__exe_fs.sym_files[k], file_length, name, &s, 0);
}
/* setting symbolic stdin */
if (file_length) {
__exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin));
- __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s);
+ __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s, 0);
__exe_env.fds[0].dfile = __exe_fs.sym_stdin;
}
else __exe_fs.sym_stdin = NULL;
@@ -139,7 +155,7 @@
/* setting symbolic stdout */
if (sym_stdout_flag) {
__exe_fs.sym_stdout = malloc(sizeof(*__exe_fs.sym_stdout));
- __create_new_dfile(__exe_fs.sym_stdout, 1024, "stdout", &s);
+ __create_new_dfile(__exe_fs.sym_stdout, 1024, "stdout", &s, 0);
__exe_env.fds[1].dfile = __exe_fs.sym_stdout;
__exe_fs.stdout_writes = 0;
}
@@ -154,8 +170,7 @@
__exe_fs.sym_conns = malloc(sizeof(*__exe_fs.sym_conns) * n_conns);
for (k=0; k < n_conns; k++) {
name[0] = 'a' + k;
- __create_new_dfile(&__exe_fs.sym_conns[k], conn_len, name, &s);
- klee_assume((__exe_fs.sym_conns[k].stat->st_mode & S_IFMT) == S_IFSOCK);
+ __create_new_dfile(&__exe_fs.sym_conns[k], conn_len, name, &s, 1);
}
__exe_fs.n_sym_conns_used = 0;
}
Modified: models/simple/sockets.c
===================================================================
--- models/simple/sockets.c 2009-03-19 00:04:59 UTC (rev 1514)
+++ models/simple/sockets.c 2009-03-19 00:33:39 UTC (rev 1515)
@@ -168,7 +168,6 @@
int __fd_accept(int sockfd, struct sockaddr *addr, socklen_t *addrlen) {
int connfd;
exe_file_t *connf;
- exe_disk_file_t *conndf;
exe_file_t *f = __get_file(sockfd);
unsigned long args[3];
@@ -221,36 +220,25 @@
if (connfd < 0) return connfd;
connf = &__exe_env.fds[connfd];
-
connf->flags |= eReadable | eWriteable;
- connf->conn = calloc(1, sizeof(*connf->conn));
-#if 0
- connf->conn->domain = f->conn->domain;
- connf->conn->type = f->conn->type;
- connf->conn->protocol = f->conn->protocol;
-#endif
- connf->conn->localaddrlen = sizeof(connf->conn->localaddr);
- args[0] = f->fd;
- args[1] = (unsigned long)&connf->conn->localaddr;
- args[2] = (unsigned long)&connf->conn->localaddrlen;
- if (syscall(__NR_socketcall, SYS_GETSOCKNAME, args) < 0) {
- errno = klee_get_errno();
+ connf->dfile = __get_sym_conn();
+ if (!connf->dfile) {
+ errno = EMFILE;
return -1;
}
- /* TODO: fill in the remote addresses */
-
- conndf = __get_sym_conn();
- if (!conndf) {
- errno = EMFILE;
+ /* XXX Should check access against mode / stat / possible deletion. */
+
+ connf->dfile->conn->localaddrlen = sizeof(connf->dfile->conn->localaddr);
+ args[0] = f->fd;
+ args[1] = (unsigned long) &connf->dfile->conn->localaddr;
+ args[2] = (unsigned long) &connf->dfile->conn->localaddrlen;
+ if (syscall(__NR_socketcall, SYS_GETSOCKNAME, args) < 0) {
+ errno = klee_get_errno();
return -1;
}
- /* XXX Should check access against mode / stat / possible
- deletion. */
- connf->dfile = conndf;
-
return connfd;
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://keeda.Stanford.EDU/pipermail/klee-commits/attachments/20090318/f0eb9d03/attachment.html
More information about the klee-commits
mailing list