[klee-commits] [1491] Added skeleton for network support.

cristic at stanford.edu cristic at stanford.edu
Wed Mar 11 17:15:55 PDT 2009


Revision: 1491
          http://keeda.stanford.edu/viewvc/viewvc.cgi?view=rev&revision=1491
Author:   cristic
Date:     2009-03-11 17:15:55 -0700 (Wed, 11 Mar 2009)
Log Message:
-----------
Added skeleton for network support.

Modified Paths:
--------------
    models/simple/fd.h
    models/simple/fd_init.c
    models/simple/klee_init_env.c

Modified: models/simple/fd.h
===================================================================
--- models/simple/fd.h	2009-03-06 23:10:47 UTC (rev 1490)
+++ models/simple/fd.h	2009-03-12 00:15:55 UTC (rev 1491)
@@ -36,8 +36,10 @@
   unsigned stdout_writes; /* how many chars were written to stdout */
   exe_disk_file_t *sym_files;
   /* --- */
+  unsigned n_sym_conns;
+  exe_disk_file_t *sym_conns;
   /* the maximum number of failures on one path; gets decremented after each failure */
-  unsigned max_failures; 
+  unsigned max_failures;
 
   /* Which read, write etc. call should fail */
   int *read_fail, *write_fail, *close_fail, *ftruncate_fail, *getcwd_fail;
@@ -64,6 +66,7 @@
 
 void klee_init_fds(unsigned n_files, unsigned file_length, 
 		   int sym_stdout_flag, int do_all_writes_flag, 
+		   unsigned n_conns, unsigned conn_len,
 		   unsigned max_failures);
 void klee_init_env(int *argcPtr, char ***argvPtr);
 

Modified: models/simple/fd_init.c
===================================================================
--- models/simple/fd_init.c	2009-03-06 23:10:47 UTC (rev 1490)
+++ models/simple/fd_init.c	2009-03-12 00:15:55 UTC (rev 1491)
@@ -100,6 +100,7 @@
    max_failures: maximum number of system call failures */
 void klee_init_fds(unsigned n_files, unsigned file_length, 
 		   int sym_stdout_flag, int save_all_writes_flag,
+		   unsigned n_conns, unsigned conn_len,
 		   unsigned max_failures) {
   unsigned k;
   char name[7] = "?-data";
@@ -149,4 +150,12 @@
   __exe_env.save_all_writes = save_all_writes_flag;
   __exe_env.version = __sym_uint32("model_version");
   klee_assume(__exe_env.version == 1);
+
+  /** Connections **/
+  __exe_fs.n_sym_conns = n_conns;
+  __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);
+  }
 }

Modified: models/simple/klee_init_env.c
===================================================================
--- models/simple/klee_init_env.c	2009-03-06 23:10:47 UTC (rev 1490)
+++ models/simple/klee_init_env.c	2009-03-12 00:15:55 UTC (rev 1491)
@@ -79,6 +79,7 @@
   char* new_argv[1024];
   unsigned max_len, min_argvs, max_argvs;
   unsigned sym_files = 0, sym_file_len = 0;
+  unsigned sym_conns = 0, sym_conn_len = 0;
   int sym_stdout_flag = 0;
   int save_all_writes_flag = 0;
   int fd_fail = 0;
@@ -151,6 +152,17 @@
 		
       fd_fail = __str_to_int(argv[k++], msg);
     }
+    else if (__streq(argv[k], "--sym-connections") || __streq(argv[k], "-sym-connections")) {
+      const char* msg = "--sym-connections expects two integer arguments <no-connections> <bytes-per-connection>";      
+
+      if (k+2 >= argc)
+	__emit_error(msg);
+      
+      k++;
+      sym_conns = __str_to_int(argv[k++], msg);
+      sym_conn_len = __str_to_int(argv[k++], msg);
+
+    }
     else {
       /* simply copy arguments */
       __add_arg(&new_argc, new_argv, argv[k++], 1024);
@@ -166,7 +178,8 @@
   *argvPtr = final_argv;
 
   klee_init_fds(sym_files, sym_file_len, 
-		sym_stdout_flag, save_all_writes_flag, 
+		sym_stdout_flag, save_all_writes_flag,
+		sym_conns, sym_conn_len,
 		fd_fail);
 }
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://keeda.Stanford.EDU/pipermail/klee-commits/attachments/20090311/1c871f38/attachment.html 


More information about the klee-commits mailing list