From d2c5835fd69ddae36cce1de2714b466266d79b66 Mon Sep 17 00:00:00 2001
From: Daneshvar Amrollahi <amrollahi.daneshvar@gmail.com>
Date: Mon, 12 Sep 2022 16:19:45 +0000
Subject: [PATCH] Replaced string functions with summaries

---
 libc/string/memchr.c  | 42 +++++++++++++++++++------------
 libc/string/memcmp.c  | 57 ++++++++++++++++++++++++-------------------
 libc/string/memmem.c  | 49 ++++++++++++++++++++-----------------
 libc/string/memrchr.c | 42 +++++++++++++++++++------------
 libc/string/strchr.c  | 21 +++++++++++-----
 libc/string/strcmp.c  | 35 +++++++++++++++-----------
 libc/string/strlen.c  | 11 ++++++---
 libc/string/strncmp.c | 39 ++++++++++++++++-------------
 libc/string/strspn.c  | 24 +++++++++++-------
 9 files changed, 192 insertions(+), 128 deletions(-)

diff --git a/libc/string/memchr.c b/libc/string/memchr.c
index 413999722..5bd229d32 100644
--- a/libc/string/memchr.c
+++ b/libc/string/memchr.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef WANT_WIDE
 # define Wmemchr wmemchr
@@ -17,24 +18,33 @@ libc_hidden_proto(Wmemchr)
 
 Wvoid *Wmemchr(const Wvoid *s, Wint c, size_t n)
 {
-	register const Wuchar *r = (const Wuchar *) s;
-#ifdef __BCC__
-	/* bcc can optimize the counter if it thinks it is a pointer... */
-	register const char *np = (const char *) n;
-#else
-# define np n
-#endif
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "memchr_return_value");
+	klee_memchr(s, c, n, ret);
+	if (ret == n)
+		return NULL;
+	else
+		return (Wvoid *) (s + ret);
+
+// 	register const Wuchar *r = (const Wuchar *) s;
+// #ifdef __BCC__
+// 	/* bcc can optimize the counter if it thinks it is a pointer... */
+// 	register const char *np = (const char *) n;
+// #else
+// # define np n
+// #endif
 
-	while (np) {
-		if (*r == ((Wuchar)c)) {
-			return (Wvoid *) r;	/* silence the warning */
-		}
-		++r;
-		--np;
-	}
+// 	while (np) {
+// 		if (*r == ((Wuchar)c)) {
+// 			return (Wvoid *) r;	/* silence the warning */
+// 		}
+// 		++r;
+// 		--np;
+// 	}
 
-	return NULL;
+// 	return NULL;
+	
 }
-#undef np
+// #undef np
 
 libc_hidden_def(Wmemchr)
diff --git a/libc/string/memcmp.c b/libc/string/memcmp.c
index 377a8d692..4242b8baf 100644
--- a/libc/string/memcmp.c
+++ b/libc/string/memcmp.c
@@ -6,39 +6,46 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
-#ifdef WANT_WIDE
-# define Wmemcmp wmemcmp
-#else
-libc_hidden_proto(memcmp)
+// #ifdef WANT_WIDE
+// # define Wmemcmp wmemcmp
+// #else
+// libc_hidden_proto(memcmp)
 # define Wmemcmp memcmp
-#endif
+// #endif
 
 int Wmemcmp(const Wvoid *s1, const Wvoid *s2, size_t n)
 {
-	register const Wuchar *r1 = (const Wuchar *) s1;
-	register const Wuchar *r2 = (const Wuchar *) s2;
 
-#ifdef WANT_WIDE
-	while (n && (*r1 == *r2)) {
-		++r1;
-		++r2;
-		--n;
-	}
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "memcmp_return_value");
+	klee_memcmp(s1, s2, n, ret);
+	return ret;
 
-	return (n == 0) ? 0 : ((*r1 < *r2) ? -1 : 1);
-#else
-	int r = 0;
+	// register const Wuchar *r1 = (const Wuchar *) s1;
+	// register const Wuchar *r2 = (const Wuchar *) s2;
 
-	while (n-- && ((r = ((int)(*r1++)) - *r2++) == 0));
+// #ifdef WANT_WIDE
+// 	while (n && (*r1 == *r2)) {
+// 		++r1;
+// 		++r2;
+// 		--n;
+// 	}
 
-	return r;
-#endif
+// 	return (n == 0) ? 0 : ((*r1 < *r2) ? -1 : 1);
+// #else
+// 	int r = 0;
+
+// 	while (n-- && ((r = ((int)(*r1++)) - *r2++) == 0));
+
+// 	return r;
+// #endif
 }
 
-#ifndef WANT_WIDE
-libc_hidden_def(memcmp)
-# ifdef __UCLIBC_SUSV3_LEGACY__
-strong_alias(memcmp,bcmp)
-# endif
-#endif
+// #ifndef WANT_WIDE
+// libc_hidden_def(memcmp)
+// # ifdef __UCLIBC_SUSV3_LEGACY__
+// strong_alias(memcmp,bcmp)
+// # endif
+// #endif
diff --git a/libc/string/memmem.c b/libc/string/memmem.c
index fd60f1e7b..ae6444360 100644
--- a/libc/string/memmem.c
+++ b/libc/string/memmem.c
@@ -6,37 +6,42 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef __USE_GNU
 libc_hidden_proto(memmem)
 void *memmem(const void *haystack, size_t haystacklen,
 		     const void *needle, size_t needlelen)
-{
-	register const char *ph;
-	register const char *pn;
-	const char *plast;
-	size_t n;
+{	
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "memmem_return_value");
+	klee_memmem(haystack, needle, haystacklen, needlelen, ret);
+	return (char *)(haystack + ret);
+	// register const char *ph;
+	// register const char *pn;
+	// const char *plast;
+	// size_t n;
 
-	if (needlelen == 0) {
-		return (void *) haystack;
-	}
+	// if (needlelen == 0) {
+	// 	return (void *) haystack;
+	// }
 
-	if (haystacklen >= needlelen) {
-		ph = (const char *) haystack;
-		pn = (const char *) needle;
-		plast = ph + (haystacklen - needlelen);
+	// if (haystacklen >= needlelen) {
+	// 	ph = (const char *) haystack;
+	// 	pn = (const char *) needle;
+	// 	plast = ph + (haystacklen - needlelen);
 
-		do {
-			n = 0;
-			while (ph[n] == pn[n]) {
-				if (++n == needlelen) {
-					return (void *) ph;
-				}
-			}
-		} while (++ph <= plast);
-	}
+	// 	do {
+	// 		n = 0;
+	// 		while (ph[n] == pn[n]) {
+	// 			if (++n == needlelen) {
+	// 				return (void *) ph;
+	// 			}
+	// 		}
+	// 	} while (++ph <= plast);
+	// }
 
-	return NULL;
+	// return NULL;
 }
 libc_hidden_def(memmem)
 #endif
diff --git a/libc/string/memrchr.c b/libc/string/memrchr.c
index 2959396b2..1bf9b97a3 100644
--- a/libc/string/memrchr.c
+++ b/libc/string/memrchr.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef __USE_GNU
 
@@ -13,26 +14,35 @@ libc_hidden_proto(memrchr)
 
 void *memrchr(const void *s, int c, size_t n)
 {
-	register const unsigned char *r;
-#ifdef __BCC__
-	/* bcc can optimize the counter if it thinks it is a pointer... */
-	register const char *np = (const char *) n;
-#else
-#define np n
-#endif
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "memrchr_return_value");
+	klee_memrchr(s, c, n, ret);
+	if (ret == n)
+		return NULL;
+	else
+		return s + ret;
+
+
+// 	register const unsigned char *r;
+// #ifdef __BCC__
+// 	/* bcc can optimize the counter if it thinks it is a pointer... */
+// 	register const char *np = (const char *) n;
+// #else
+// #define np n
+// #endif
 	
-	r = ((unsigned char *)s) + ((size_t) np);
+// 	r = ((unsigned char *)s) + ((size_t) np);
 
-	while (np) {
-		if (*--r == ((unsigned char)c)) {
-			return (void *) r;	/* silence the warning */
-		}
-		--np;
-	}
+// 	while (np) {
+// 		if (*--r == ((unsigned char)c)) {
+// 			return (void *) r;	/* silence the warning */
+// 		}
+// 		--np;
+// 	}
 
-	return NULL;
+// 	return NULL;
 }
-#undef np
+// #undef np
 
 libc_hidden_def(memrchr)
 #endif
diff --git a/libc/string/strchr.c b/libc/string/strchr.c
index 0ce552438..376313bec 100644
--- a/libc/string/strchr.c
+++ b/libc/string/strchr.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef WANT_WIDE
 # define Wstrchr wcschr
@@ -17,13 +18,21 @@ libc_hidden_proto(Wstrchr)
 
 Wchar *Wstrchr(register const Wchar *s, Wint c)
 {
-	do {
-		if (*s == ((Wchar)c)) {
-			return (Wchar *) s;	/* silence the warning */
-		}
-	} while (*s++);
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "strchr_return_value");
+	int n = strlen(s);
+	klee_strchr(s, c, n, ret);
+	if (ret == n)
+		return NULL;
+	else
+		return (Wchar *)(s + ret);
+	// do {
+	// 	if (*s == ((Wchar)c)) {
+	// 		return (Wchar *) s;	/* silence the warning */
+	// 	}
+	// } while (*s++);
 
-	return NULL;
+	// return NULL;
 }
 libc_hidden_def(Wstrchr)
 
diff --git a/libc/string/strcmp.c b/libc/string/strcmp.c
index 4a95ab882..e16fed843 100644
--- a/libc/string/strcmp.c
+++ b/libc/string/strcmp.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef WANT_WIDE
 # define Wstrcmp wcscmp
@@ -19,23 +20,29 @@ libc_hidden_proto(Wstrcmp)
 
 int Wstrcmp(register const Wchar *s1, register const Wchar *s2)
 {
-#ifdef WANT_WIDE
-	while (*((Wuchar *)s1) == *((Wuchar *)s2)) {
-		if (!*s1++) {
-			return 0;
-		}
-		++s2;
-	}
+	int s1_len = strlen(s1);
+	int s2_len = strlen(s2);
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "strcmp_return_value");
+	klee_strcmp(s1, s2, s1_len, s2_len, ret);
+	return (int)ret;
+// #ifdef WANT_WIDE
+// 	while (*((Wuchar *)s1) == *((Wuchar *)s2)) {
+// 		if (!*s1++) {
+// 			return 0;
+// 		}
+// 		++s2;
+// 	}
 
-	return (*((Wuchar *)s1) < *((Wuchar *)s2)) ? -1 : 1;
-#else
-	int r;
+// 	return (*((Wuchar *)s1) < *((Wuchar *)s2)) ? -1 : 1;
+// #else
+// 	int r;
 
-	while (((r = ((int)(*((Wuchar *)s1))) - *((Wuchar *)s2++))
-			== 0) && *s1++);
+// 	while (((r = ((int)(*((Wuchar *)s1))) - *((Wuchar *)s2++))
+// 			== 0) && *s1++);
 	
-	return r;
-#endif
+// 	return r;
+// #endif
 }
 libc_hidden_def(Wstrcmp)
 
diff --git a/libc/string/strlen.c b/libc/string/strlen.c
index bcb096b97..89289eaca 100644
--- a/libc/string/strlen.c
+++ b/libc/string/strlen.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef WANT_WIDE
 # define Wstrlen wcslen
@@ -17,10 +18,14 @@ libc_hidden_proto(Wstrlen)
 
 size_t Wstrlen(const Wchar *s)
 {
-	register const Wchar *p;
+	int len_s;
+	klee_make_symbolic(&len_s, sizeof(len_s), "strlen_return_value");
+	klee_strlen(s, len_s);   
+	return len_s;
+	// register const Wchar *p;
 
-	for (p=s ; *p ; p++);
+	// for (p=s ; *p ; p++);
 
-	return p - s;
+	// return p - s;
 }
 libc_hidden_def(Wstrlen)
diff --git a/libc/string/strncmp.c b/libc/string/strncmp.c
index 8cebaacac..58c8ae5b3 100644
--- a/libc/string/strncmp.c
+++ b/libc/string/strncmp.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef WANT_WIDE
 # define Wstrncmp wcsncmp
@@ -16,26 +17,30 @@ libc_hidden_proto(strncmp)
 
 int Wstrncmp(register const Wchar *s1, register const Wchar *s2, size_t n)
 {
-#ifdef WANT_WIDE
-	while (n && (*((Wuchar *)s1) == *((Wuchar *)s2))) {
-		if (!*s1++) {
-			return 0;
-		}
-		++s2;
-		--n;
-	}
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "strncmp_return_value");
+	klee_strncmp(s1, s2, n, ret);
+	return ret;
+// #ifdef WANT_WIDE
+// 	while (n && (*((Wuchar *)s1) == *((Wuchar *)s2))) {
+// 		if (!*s1++) {
+// 			return 0;
+// 		}
+// 		++s2;
+// 		--n;
+// 	}
 
-	return (n == 0) ? 0 : ((*((Wuchar *)s1) < *((Wuchar *)s2)) ? -1 : 1);
-#else
-	int r = 0;
+// 	return (n == 0) ? 0 : ((*((Wuchar *)s1) < *((Wuchar *)s2)) ? -1 : 1);
+// #else
+// 	int r = 0;
 
-	while (n--
-		   && ((r = ((int)(*((unsigned char *)s1))) - *((unsigned char *)s2++))
-			== 0)
-		   && *s1++);
+// 	while (n--
+// 		   && ((r = ((int)(*((unsigned char *)s1))) - *((unsigned char *)s2++))
+// 			== 0)
+// 		   && *s1++);
 
-	return r;
-#endif
+// 	return r;
+// #endif
 }
 #ifndef WANT_WIDE
 libc_hidden_weak(strncmp)
diff --git a/libc/string/strspn.c b/libc/string/strspn.c
index ca83ef900..ccc2be979 100644
--- a/libc/string/strspn.c
+++ b/libc/string/strspn.c
@@ -6,6 +6,7 @@
  */
 
 #include "_string.h"
+#include "../klee/include/klee/klee.h"
 
 #ifdef WANT_WIDE
 # define Wstrspn wcsspn
@@ -17,15 +18,20 @@ libc_hidden_proto(Wstrspn)
 
 size_t Wstrspn(const Wchar *s1, const Wchar *s2)
 {
-	register const Wchar *s = s1;
-	register const Wchar *p = s2;
+	uint32_t ret;
+	klee_make_symbolic(&ret, sizeof(ret), "strspn_return_value");
+	int s1_len = strlen(s1), s2_len = strlen(s2);
+	klee_strspn(s1, s2, s1_len, s2_len, ret);
+	return (size_t)ret;
+	// register const Wchar *s = s1;
+	// register const Wchar *p = s2;
 
-	while (*p) {
-		if (*p++ == *s) {
-			++s;
-			p = s2;
-		}
-	}
-	return s - s1;
+	// while (*p) {
+	// 	if (*p++ == *s) {
+	// 		++s;
+	// 		p = s2;
+	// 	}
+	// }
+	// return s - s1;
 }
 libc_hidden_def(Wstrspn)