Merge pull request sosy-lab#428 from tautschnig/busybox-fixes4

BusyBox fixes to address sosy-lab#424

c/busybox-1.22.0/busybox_sv_comp-dirname.h

@@ -0,0 +1,9 @@
+char *dirname(char *path)
+{
+  static char dir[42]; // I believe PATH_MAX would be the correct length
+  for(int i=0; i<42; ++i)
+    dir[i] = __VERIFIER_nondet_char();
+  dir[41] = '\0';
+  return dir;
+}
+

c/busybox-1.22.0/busybox_sv_comp-getgrgid.h

@@ -0,0 +1,16 @@
+#define getgrgid bb_internal_getgrgid
+
+struct group *getgrgid(gid_t gid)
+{
+  (void)gid;
+
+  static struct group g;
+
+  g.gr_name = "";       /* group name */
+  g.gr_passwd = "";     /* group password */
+  g.gr_gid = __VERIFIER_nondet_uint();
+  g.gr_mem = NULL;      /* group members */
+
+  return &g;
+}
+

c/busybox-1.22.0/busybox_sv_comp-getpwnam.h

@@ -0,0 +1,28 @@
+#define getpwnam bb_internal_getpwnam
+
+struct passwd *getpwnam(const char *name)
+{
+  (void)name;
+
+  static struct passwd p;
+
+  p.pw_name = "";       /* username */
+  p.pw_passwd = "";     /* user password */
+  p.pw_uid = __VERIFIER_nondet_uint();
+  p.pw_gid = __VERIFIER_nondet_uint();
+  p.pw_gecos = "";      /* real name */
+  p.pw_dir = "";        /* home directory */
+  p.pw_shell = "";      /* shell program */
+
+  return &p;
+}
+
+#define getpwuid bb_internal_getpwuid
+
+struct passwd *getpwuid(uid_t uid)
+{
+  (void)uid;
+
+  return getpwnam(0);
+}
+

c/busybox-1.22.0/busybox_sv_comp-mmap.h

@@ -0,0 +1,36 @@
+void *mmap(void *addr, size_t length, int prot, int flags, int fd, off_t offset)
+{
+  if(__VERIFIER_nondet_int())
+    return MAP_FAILED;
+
+  (void)addr;
+  (void)prot;
+  (void)offset;
+
+  if(flags & MAP_ANONYMOUS)
+  {
+    if(fd != -1)
+      __VERIFIER_error();
+
+    void *res=calloc(length, 1);
+    if(res == NULL)
+      return MAP_FAILED;
+
+    return res;
+  }
+  else
+    return malloc(length);
+}
+
+int munmap(void *addr, size_t length)
+{
+  if(__VERIFIER_nondet_int())
+    return -1;
+
+  (void)length;
+
+  free(addr);
+
+  return 0;
+}
+

c/busybox-1.22.0/busybox_sv_comp-readlink.h

@@ -0,0 +1,16 @@
+ssize_t readlink(const char *path, char *buf, size_t bufsiz)
+{
+  (void)*path;
+
+  if(__VERIFIER_nondet_int() || bufsiz < 1)
+    return -1;
+
+  unsigned long len = __VERIFIER_nondet_ulong();
+  __VERIFIER_assume(len <= bufsiz);
+
+  for(size_t i=0; i<len; ++i)
+    buf[i] = __VERIFIER_nondet_char();
+
+  return len;
+}
+

c/busybox-1.22.0/busybox_sv_comp-realpath.h

@@ -0,0 +1,17 @@
+char *realpath(const char *path, char *resolved_path)
+{
+  if(__VERIFIER_nondet_int())
+    return NULL;
+
+  unsigned long offset=__VERIFIER_nondet_ulong();
+  __VERIFIER_assume(offset<PATH_MAX);
+
+  if(resolved_path == NULL)
+    resolved_path = malloc(offset+1);
+
+  /* terminating zero */
+  *(resolved_path + offset) = '\0';
+
+  return resolved_path;
+}
+

c/busybox-1.22.0/busybox_sv_comp-stpcpy.h

@@ -0,0 +1,6 @@
+char *stpcpy(char *dest, const char *src)
+{
+  while(*dest++ = *src++);
+  return dest;
+}
+

c/busybox-1.22.0/busybox_sv_comp-ttyname.h

@@ -0,0 +1,12 @@
+int ttyname_r(int fd, char *buf, size_t buflen)
+{
+  if(__VERIFIER_nondet_int() || buflen < 1)
+    return -1; // should be proper error numbers
+
+  for(size_t i=0; i<buflen-1; ++i)
+    buf[i] = __VERIFIER_nondet_char();
+  buf[buflen-1] = '\0';
+
+  return 0;
+}
+

c/busybox-1.22.0/cat_true-no-overflow_true-valid-memsafety.c

@@ -1194,4 +1194,5 @@ static void * xzalloc(unsigned long int size)
   return ptr;
 }
 
+#include "busybox_sv_comp-mmap.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/cat_true-no-overflow_true-valid-memsafety.i

@@ -3191,6 +3191,33 @@ static void * xzalloc(unsigned long int size)
   memset(ptr, 0, size);
   return ptr;
 }
+void *mmap(void *addr, size_t length, int prot, int flags, int fd, off_t offset)
+{
+  if(__VERIFIER_nondet_int())
+    return ((void *) -1);
+  (void)addr;
+  (void)prot;
+  (void)offset;
+  if(flags & 0x20)
+  {
+    if(fd != -1)
+      __VERIFIER_error();
+    void *res=calloc(length, 1);
+    if(res == ((void *)0))
+      return ((void *) -1);
+    return res;
+  }
+  else
+    return malloc(length);
+}
+int munmap(void *addr, size_t length)
+{
+  if(__VERIFIER_nondet_int())
+    return -1;
+  (void)length;
+  free(addr);
+  return 0;
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.c

@@ -364,4 +364,5 @@ static void xfunc_die(void)
   exit((signed int)xfunc_error_retval);
 }
 
+#include "busybox_sv_comp-getpwnam.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i

@@ -2487,6 +2487,24 @@ static void xfunc_die(void)
   }
   exit((signed int)xfunc_error_retval);
 }
+struct passwd *bb_internal_getpwnam(const char *name)
+{
+  (void)name;
+  static struct passwd p;
+  p.pw_name = "";
+  p.pw_passwd = "";
+  p.pw_uid = __VERIFIER_nondet_uint();
+  p.pw_gid = __VERIFIER_nondet_uint();
+  p.pw_gecos = "";
+  p.pw_dir = "";
+  p.pw_shell = "";
+  return &p;
+}
+struct passwd *bb_internal_getpwuid(uid_t uid)
+{
+  (void)uid;
+  return bb_internal_getpwnam(0);
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/cp-incomplete_true-no-overflow_true-valid-memsafety.c

@@ -2141,4 +2141,7 @@ static void * xzalloc(unsigned long int size)
   return ptr;
 }
 
+#include "busybox_sv_comp-dirname.h"
+#include "busybox_sv_comp-mmap.h"
+#include "busybox_sv_comp-readlink.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/cp-incomplete_true-no-overflow_true-valid-memsafety.i

@@ -4240,6 +4240,52 @@ static void * xzalloc(unsigned long int size)
   memset(ptr, 0, size);
   return ptr;
 }
+char *dirname(char *path)
+{
+  static char dir[42];
+  for(int i=0; i<42; ++i)
+    dir[i] = __VERIFIER_nondet_char();
+  dir[41] = '\0';
+  return dir;
+}
+void *mmap(void *addr, size_t length, int prot, int flags, int fd, off_t offset)
+{
+  if(__VERIFIER_nondet_int())
+    return ((void *) -1);
+  (void)addr;
+  (void)prot;
+  (void)offset;
+  if(flags & 0x20)
+  {
+    if(fd != -1)
+      __VERIFIER_error();
+    void *res=calloc(length, 1);
+    if(res == ((void *)0))
+      return ((void *) -1);
+    return res;
+  }
+  else
+    return malloc(length);
+}
+int munmap(void *addr, size_t length)
+{
+  if(__VERIFIER_nondet_int())
+    return -1;
+  (void)length;
+  free(addr);
+  return 0;
+}
+ssize_t readlink(const char *path, char *buf, size_t bufsiz)
+{
+  (void)*path;
+  if(__VERIFIER_nondet_int() || bufsiz < 1)
+    return -1;
+  unsigned long len = __VERIFIER_nondet_ulong();
+  __VERIFIER_assume(len <= bufsiz);
+  for(size_t i=0; i<len; ++i)
+    buf[i] = __VERIFIER_nondet_char();
+  return len;
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.c

@@ -151,4 +151,5 @@ static char * single_argv(char **argv)
   return argv[(signed long int)1];
 }
 
+#include "busybox_sv_comp-dirname.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i

@@ -1213,6 +1213,14 @@ static char * single_argv(char **argv)
     bb_show_usage();
   return argv[(signed long int)1];
 }
+char *dirname(char *path)
+{
+  static char dir[42];
+  for(int i=0; i<42; ++i)
+    dir[i] = __VERIFIER_nondet_char();
+  dir[41] = '\0';
+  return dir;
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/dos2unix_true-no-overflow_true-valid-memsafety.c

@@ -1388,4 +1388,5 @@ static void * xzalloc(unsigned long int size)
   return ptr;
 }
 
+#include "busybox_sv_comp-readlink.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/dos2unix_true-no-overflow_true-valid-memsafety.i

@@ -3439,6 +3439,17 @@ static void * xzalloc(unsigned long int size)
   memset(ptr, 0, size);
   return ptr;
 }
+ssize_t readlink(const char *path, char *buf, size_t bufsiz)
+{
+  (void)*path;
+  if(__VERIFIER_nondet_int() || bufsiz < 1)
+    return -1;
+  unsigned long len = __VERIFIER_nondet_ulong();
+  __VERIFIER_assume(len <= bufsiz);
+  for(size_t i=0; i<len; ++i)
+    buf[i] = __VERIFIER_nondet_char();
+  return len;
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.c

@@ -506,4 +506,5 @@ static void * xmalloc(unsigned long int size)
   return ptr;
 }
 
+#include "busybox_sv_comp-stpcpy.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i

@@ -2575,6 +2575,11 @@ static void * xmalloc(unsigned long int size)
   }
   return ptr;
 }
+char *stpcpy(char *dest, const char *src)
+{
+  while(*dest++ = *src++);
+  return dest;
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/id-incomplete_true-no-overflow_true-valid-memsafety.c

@@ -1355,4 +1355,6 @@ static void * xzalloc(unsigned long int size)
   return ptr;
 }
 
+#include "busybox_sv_comp-getgrgid.h"
+#include "busybox_sv_comp-getpwnam.h"
 #include "busybox_sv_comp_impl.h"

c/busybox-1.22.0/id-incomplete_true-no-overflow_true-valid-memsafety.i

@@ -3251,6 +3251,34 @@ static void * xzalloc(unsigned long int size)
   memset(ptr, 0, size);
   return ptr;
 }
+struct group *bb_internal_getgrgid(gid_t gid)
+{
+  (void)gid;
+  static struct group g;
+  g.gr_name = "";
+  g.gr_passwd = "";
+  g.gr_gid = __VERIFIER_nondet_uint();
+  g.gr_mem = ((void *)0);
+  return &g;
+}
+struct passwd *bb_internal_getpwnam(const char *name)
+{
+  (void)name;
+  static struct passwd p;
+  p.pw_name = "";
+  p.pw_passwd = "";
+  p.pw_uid = __VERIFIER_nondet_uint();
+  p.pw_gid = __VERIFIER_nondet_uint();
+  p.pw_gecos = "";
+  p.pw_dir = "";
+  p.pw_shell = "";
+  return &p;
+}
+struct passwd *bb_internal_getpwuid(uid_t uid)
+{
+  (void)uid;
+  return bb_internal_getpwnam(0);
+}
 static struct utmp dummy_utmp;
 struct utmp *getutent(void) {
   if (__VERIFIER_nondet_int())

c/busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.c

@@ -3508,4 +3508,7 @@ static void * xzalloc(unsigned long int size)
   return ptr;
 }
 
+#include "busybox_sv_comp-getgrgid.h"
+#include "busybox_sv_comp-getpwnam.h"
+#include "busybox_sv_comp-readlink.h"
 #include "busybox_sv_comp_impl.h"