diff --git a/runtime/LibcWrappers.cpp b/runtime/LibcWrappers.cpp
index cfe55525..51e860f7 100644
--- a/runtime/LibcWrappers.cpp
+++ b/runtime/LibcWrappers.cpp
@@ -608,4 +608,272 @@ uint32_t SYM(ntohl)(uint32_t netlong) {
 
   return result;
 }
+
+int SYM(strcmp)(const char *a, const char *b) {
+  tryAlternative(a, _sym_get_parameter_expression(0), SYM(strcmp));
+  tryAlternative(b, _sym_get_parameter_expression(1), SYM(strcmp));
+
+  auto result = strcmp(a, b);
+  _sym_set_return_expression(nullptr);
+
+  if (isConcrete(a, strlen(a)) && isConcrete(b, strlen(b)))
+    return result;
+
+  auto aShadowIt = ReadOnlyShadow(a, strlen(a)).begin_non_null();
+  auto bShadowIt = ReadOnlyShadow(b, strlen(b)).begin_non_null();
+  auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt);
+  for (size_t i = 1; i < strlen(a); i++) {
+    ++aShadowIt;
+    ++bShadowIt;
+    allEqual =
+        _sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt));
+  }
+
+  _sym_push_path_constraint(allEqual, result == 0,
+                            reinterpret_cast<uintptr_t>(SYM(strcmp)));
+  return result;
+}
+
+int SYM(strncmp)(const char *a, const char *b, size_t n) {
+  tryAlternative(a, _sym_get_parameter_expression(0), SYM(strncmp));
+  tryAlternative(b, _sym_get_parameter_expression(1), SYM(strncmp));
+  tryAlternative(n, _sym_get_parameter_expression(2), SYM(strncmp));
+
+  auto result = strncmp(a, b, n);
+  _sym_set_return_expression(nullptr);
+
+  if (isConcrete(a, n) && isConcrete(b, n))
+    return result;
+
+  auto aShadowIt = ReadOnlyShadow(a, n).begin_non_null();
+  auto bShadowIt = ReadOnlyShadow(b, n).begin_non_null();
+  auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt);
+  for (size_t i = 1; i < n; i++) {
+    ++aShadowIt;
+    ++bShadowIt;
+    allEqual =
+        _sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt));
+  }
+
+  _sym_push_path_constraint(allEqual, result == 0,
+                            reinterpret_cast<uintptr_t>(SYM(strncmp)));
+  return result;
+}
+
+uint32_t SYM(strlen)(const char *s) {
+  tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));
+
+  // HACK! we regard strlen as a special strchr(s, '\0')
+  auto *result = strchr(s, 0);
+  _sym_set_return_expression(nullptr);
+
+  if (isConcrete(s, result != nullptr ? (result - s) : strlen(s)))
+    return (result - s);
+
+  // We force set the value of c to \x00, it should be a concrete value
+  auto *cExpr = _sym_build_integer(0, 8);
+
+  size_t length = result != nullptr ? (result - s) : strlen(s);
+  auto shadow = ReadOnlyShadow(s, length);
+  auto shadowIt = shadow.begin();
+  for (size_t i = 0; i < length; i++) {
+    _sym_push_path_constraint(
+        _sym_build_not_equal(
+            (*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8),
+            cExpr),
+        /*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
+    ++shadowIt;
+  }
+
+  // HACK! The last byte must be \x00!
+  _sym_push_path_constraint(
+      _sym_build_equal(
+          (*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(0, 8), cExpr),
+      /*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
+
+  return (result - s);
+}
+
+int SYM(atoi)(const char *s) {
+  tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));
+
+  // HACK! we mimic the libc function summary in klee
+  /* int atoi(const char *str) {
+   *     return (int)strtol(str, (char **)NULL, 10);
+   *   }
+   * */
+  auto result = strtol(s, (char **)NULL, 10);
+  _sym_set_return_expression(nullptr);
+
+  if (isConcrete(s, strlen(s)))
+    return result;
+
+  size_t length = strlen(s);
+  size_t num_len = 0;
+  for (size_t i = 0; i < length; i++) {
+    if ('0' <= (char)s[i] && (char)s[i] <= '9') {
+      num_len++;
+    } else {
+      break;
+    }
+  }
+  auto shadow = ReadOnlyShadow(s, length);
+  auto shadowIt = shadow.begin();
+  for (size_t i = 0; i < num_len; i++) {
+    int res = (char)s[i];
+    auto *cExpr = _sym_build_integer(res, 8);
+    _sym_push_path_constraint(
+        _sym_build_equal((*shadowIt != nullptr) ? *shadowIt
+                                                : _sym_build_integer(s[i], 8),
+                         cExpr),
+        /*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
+    ++shadowIt;
+  }
+
+  // The value of tail must be non-num
+  auto *tailExpr_0 = _sym_build_integer(48, 8); // '0'
+  auto *tailExpr_1 = _sym_build_integer(49, 8); // '1'
+  auto *tailExpr_2 = _sym_build_integer(50, 8); // '2'
+  auto *tailExpr_3 = _sym_build_integer(51, 8); // '3'
+  auto *tailExpr_4 = _sym_build_integer(52, 8); // '4'
+  auto *tailExpr_5 = _sym_build_integer(53, 8); // '5'
+  auto *tailExpr_6 = _sym_build_integer(54, 8); // '6'
+  auto *tailExpr_7 = _sym_build_integer(55, 8); // '7'
+  auto *tailExpr_8 = _sym_build_integer(56, 8); // '8'
+  auto *tailExpr_9 = _sym_build_integer(57, 8); // '9'
+
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_0),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_1),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_2),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_3),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_4),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_5),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_6),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_7),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_8),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_9),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+
+  return result;
+}
+
+long int SYM(atol)(const char *s) {
+  tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));
+
+  // HACK! we mimic the libc function summary in klee
+  /* int atoi(const char *str) {
+   *     return (int)strtol(str, (char **)NULL, 10);
+   *   }
+   * */
+  auto result = strtol(s, (char **)NULL, 10);
+  _sym_set_return_expression(nullptr);
+
+  if (isConcrete(s, strlen(s)))
+    return result;
+
+  size_t length = strlen(s);
+  size_t num_len = 0;
+  for (size_t i = 0; i < length; i++) {
+    if ('0' <= (char)s[i] && (char)s[i] <= '9') {
+      num_len++;
+    } else {
+      break;
+    }
+  }
+  auto shadow = ReadOnlyShadow(s, length);
+  auto shadowIt = shadow.begin();
+  for (size_t i = 0; i < num_len; i++) {
+    int res = (char)s[i];
+    auto *cExpr = _sym_build_integer(res, 8);
+    _sym_push_path_constraint(
+        _sym_build_equal((*shadowIt != nullptr) ? *shadowIt
+                                                : _sym_build_integer(s[i], 8),
+                         cExpr),
+        /*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
+    ++shadowIt;
+  }
+
+  // The value of tail must be non-num
+  auto *tailExpr_0 = _sym_build_integer(48, 8); // '0'
+  auto *tailExpr_1 = _sym_build_integer(49, 8); // '1'
+  auto *tailExpr_2 = _sym_build_integer(50, 8); // '2'
+  auto *tailExpr_3 = _sym_build_integer(51, 8); // '3'
+  auto *tailExpr_4 = _sym_build_integer(52, 8); // '4'
+  auto *tailExpr_5 = _sym_build_integer(53, 8); // '5'
+  auto *tailExpr_6 = _sym_build_integer(54, 8); // '6'
+  auto *tailExpr_7 = _sym_build_integer(55, 8); // '7'
+  auto *tailExpr_8 = _sym_build_integer(56, 8); // '8'
+  auto *tailExpr_9 = _sym_build_integer(57, 8); // '9'
+
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_0),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_1),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_2),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_3),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_4),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_5),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_6),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_7),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_8),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+  _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_9),
+                            /*taken*/ 1,
+                            reinterpret_cast<uintptr_t>(SYM(strchr)));
+
+  return result;
+}
+
+char *SYM(strcpy)(char *dest, const char *src) {
+  tryAlternative(dest, _sym_get_parameter_expression(0), SYM(strcpy));
+  tryAlternative(src, _sym_get_parameter_expression(1), SYM(strcpy));
+
+  auto *result = strcpy(dest, src);
+  _sym_set_return_expression(nullptr);
+
+  size_t cpyLen = strlen(src);
+  if (isConcrete(src, cpyLen) && isConcrete(dest, cpyLen))
+    return result;
+
+  auto srcShadow = ReadOnlyShadow(src, cpyLen);
+  auto destShadow = ReadWriteShadow(dest, cpyLen);
+
+  std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin());
+
+  return result;
+}
 }
diff --git a/test/atoi.c b/test/atoi.c
new file mode 100644
index 00000000..86bb7589
--- /dev/null
+++ b/test/atoi.c
@@ -0,0 +1,33 @@
+#include <stdarg.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+int main(int argc, char *argv[]) {
+
+  char buf[1024];
+  ssize_t i;
+  if ((i = read(0, buf, sizeof(buf) - 1)) < 24)
+    return 0;
+  buf[i] = 0;
+  if (buf[0] != 'A')
+    return 0;
+  if (buf[1] != 'B')
+    return 0;
+  if (buf[2] != 'C')
+    return 0;
+  if (buf[3] != 'D')
+    return 0;
+  if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4))
+    return 0;
+  if (atoi(buf + 12) == 678) {
+    printf("The result of atoi(buf+12) is: %lu\n", atoi(buf + 12));
+    printf("HIT!\n");
+  } else {
+    printf("The result of atoi(buf+12) is: %lu\n", atoi(buf + 12));
+    printf("NOT HIT!\n");
+  }
+
+  return 0;
+}
diff --git a/test/atol.c b/test/atol.c
new file mode 100644
index 00000000..4498e797
--- /dev/null
+++ b/test/atol.c
@@ -0,0 +1,33 @@
+#include <stdarg.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+int main(int argc, char *argv[]) {
+
+  char buf[1024];
+  ssize_t i;
+  if ((i = read(0, buf, sizeof(buf) - 1)) < 24)
+    return 0;
+  buf[i] = 0;
+  if (buf[0] != 'A')
+    return 0;
+  if (buf[1] != 'B')
+    return 0;
+  if (buf[2] != 'C')
+    return 0;
+  if (buf[3] != 'D')
+    return 0;
+  if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4))
+    return 0;
+  if (atol(buf + 12) == 99999999) {
+    printf("The result of atoi(buf+12) is: %lu\n", atol(buf + 12));
+    printf("HIT!\n");
+  } else {
+    printf("The result of atoi(buf+12) is: %lu\n", atol(buf + 12));
+    printf("NOT HIT!\n");
+  }
+
+  return 0;
+}
diff --git a/test/strcmp.c b/test/strcmp.c
new file mode 100644
index 00000000..6786f57b
--- /dev/null
+++ b/test/strcmp.c
@@ -0,0 +1,31 @@
+#include <stdarg.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+int main(int argc, char *argv[]) {
+
+  char buf[1024];
+  ssize_t i;
+  if ((i = read(0, buf, sizeof(buf) - 1)) < 24)
+    return 0;
+  buf[i] = 0;
+  if (buf[0] != 'A')
+    return 0;
+  if (buf[1] != 'B')
+    return 0;
+  if (buf[2] != 'C')
+    return 0;
+  if (buf[3] != 'D')
+    return 0;
+  if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4))
+    return 0;
+  if (strcmp(buf + 12, "AAAA") == 0) {
+    printf("HIT!\n");
+  } else {
+    printf("NOT HIT!\n");
+  }
+
+  return 0;
+}
diff --git a/test/strcpy.c b/test/strcpy.c
new file mode 100644
index 00000000..f60851d3
--- /dev/null
+++ b/test/strcpy.c
@@ -0,0 +1,35 @@
+#include <stdarg.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+int main(int argc, char *argv[]) {
+
+  char buf[1024];
+  ssize_t i;
+  if ((i = read(0, buf, sizeof(buf) - 1)) < 24)
+    return 0;
+  buf[i] = 0;
+  if (buf[0] != 'A')
+    return 0;
+  if (buf[1] != 'B')
+    return 0;
+  if (buf[2] != 'C')
+    return 0;
+  if (buf[3] != 'D')
+    return 0;
+  if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4))
+    return 0;
+
+  char buf_2[4];
+  strcpy(buf_2, buf + 12);
+  if (memcmp(buf_2, "NICE", 4)) {
+    printf("NOT HIT!\n");
+    return 0;
+  } else {
+    printf("HIT!\n");
+  }
+
+  return 0;
+}
diff --git a/test/strlen.c b/test/strlen.c
new file mode 100644
index 00000000..4a512536
--- /dev/null
+++ b/test/strlen.c
@@ -0,0 +1,34 @@
+#include <stdarg.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+int main(int argc, char *argv[]) {
+
+  char buf[1024];
+  ssize_t i;
+  if ((i = read(0, buf, sizeof(buf) - 1)) < 24)
+    return 0;
+  buf[i] = 0;
+  if (buf[0] != 'A')
+    return 0;
+  if (buf[1] != 'B')
+    return 0;
+  if (buf[2] != 'C')
+    return 0;
+  if (buf[3] != 'D')
+    return 0;
+  if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4))
+    return 0;
+  if (strlen(buf + 12) == 5) {
+    printf("The string length after buf + 12 is: %lu\n", strlen(buf + 12));
+    printf("HIT!\n");
+  } else {
+    printf("The string length after buf + 12 is: %lu\n", strlen(buf + 12));
+    printf("strchr(buf+12) is: %s\n", strchr(buf + 12, '\0'));
+    printf("NOT HIT!\n");
+  }
+
+  return 0;
+}
diff --git a/test/strncmp.c b/test/strncmp.c
new file mode 100644
index 00000000..500c83e5
--- /dev/null
+++ b/test/strncmp.c
@@ -0,0 +1,31 @@
+#include <stdarg.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+int main(int argc, char *argv[]) {
+
+  char buf[1024];
+  ssize_t i;
+  if ((i = read(0, buf, sizeof(buf) - 1)) < 24)
+    return 0;
+  buf[i] = 0;
+  if (buf[0] != 'A')
+    return 0;
+  if (buf[1] != 'B')
+    return 0;
+  if (buf[2] != 'C')
+    return 0;
+  if (buf[3] != 'D')
+    return 0;
+  if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4))
+    return 0;
+  if (strncmp(buf + 12, "AAAA", 4) == 0) {
+    printf("HIT!\n");
+  } else {
+    printf("NOT HIT!\n");
+  }
+
+  return 0;
+}