Add counter of read/write bytes in files

runtime/POSIX/fd.c

@@ -401,6 +401,7 @@ ssize_t read(int fd, void *buf, size_t count) {
 
     memcpy(buf, f->dfile->contents + f->off, count);
     f->off += count;
+    f->dfile->read_bytes_real += count;
     if (fd == 0 && __exe_env.max_off < f->off) {
       __exe_env.max_off = f->off;
     }
@@ -473,6 +474,7 @@ ssize_t write(int fd, const void *buf, size_t count) {
       __exe_fs.stdout_writes += actual_count;
 
     f->off += count;
+    f->dfile->write_bytes_real += count;
     if (fd == 0 && __exe_env.max_off < f->off) {
       __exe_env.max_off = f->off;
     }

runtime/POSIX/fd.h

@@ -41,6 +41,12 @@ typedef struct {
   unsigned size;  /* in bytes */
   char* contents;
   struct stat64* stat;
+
+  unsigned read_bytes_symbolic; /* bytes that were read from file */
+  unsigned read_bytes_real;
+
+  unsigned write_bytes_symbolic; /* bytes that were written to file */
+  unsigned write_bytes_real;
 } exe_disk_file_t;
 
 typedef enum {

runtime/POSIX/fd_init.c

@@ -55,14 +55,33 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
 
   const char *sp;
   char sname[64];
-  for (sp=name; *sp; ++sp)
+  char read_bytes_name[64];
+  char write_bytes_name[64];
+  for (sp=name; *sp; ++sp){
     sname[sp-name] = *sp;
+    read_bytes_name[sp - name] = *sp;
+    write_bytes_name[sp - name] = *sp;
+  }
   memcpy(&sname[sp-name], "-stat", 6);
+  memcpy(&read_bytes_name[sp - name], "-read", 6);
+  memcpy(&write_bytes_name[sp - name], "-write", 7);
 
   assert(size);
 
   dfile->size = size;
   dfile->contents = malloc(dfile->size);
+
+  unsigned *ptr_read = malloc(sizeof(unsigned));
+  unsigned *ptr_write = malloc(sizeof(unsigned));
+  klee_make_symbolic(ptr_read, sizeof(unsigned), read_bytes_name);
+  klee_make_symbolic(ptr_write, sizeof(unsigned), write_bytes_name);
+  memcpy(&dfile->read_bytes_symbolic, ptr_read, sizeof(unsigned));
+  memcpy(&dfile->write_bytes_symbolic, ptr_write, sizeof(unsigned));
+  free(ptr_read);
+  free(ptr_write);
+  dfile->read_bytes_real = 0;
+  dfile->write_bytes_real = 0;
+
   if (!dfile->contents)
     klee_report_error(__FILE__, __LINE__, "out of memory in klee_init_env", "user.err");
   klee_make_symbolic(dfile->contents, dfile->size, name);

runtime/POSIX/klee_init_env.c

@@ -241,6 +241,12 @@ int __klee_posix_wrapped_main(int argc, char **argv, char **envp);
 
 void check_stdin_read() {
   klee_assume(__exe_env.stdin_off == __exe_env.max_off);
+  for (int i = 0; i < __exe_fs.n_sym_files; i++) {
+    klee_assume(__exe_fs.sym_files[i].read_bytes_real ==
+               __exe_fs.sym_files[i].read_bytes_symbolic);
+    klee_assume(__exe_fs.sym_files[i].write_bytes_real ==
+                __exe_fs.sym_files[i].write_bytes_symbolic);
+  }
 }
 
 /* This wrapper gets called instead of main if POSIX setup is used */