From 0510c5b8b1c56fd31c05da21ae52071f68977dff Mon Sep 17 00:00:00 2001 From: Sebastian Poeplau Date: Wed, 22 Feb 2023 11:37:22 +0000 Subject: [PATCH] Fix formatting of the new libc wrappers --- runtime/LibcWrappers.cpp | 453 +++++++++++++++++++-------------------- 1 file changed, 226 insertions(+), 227 deletions(-) diff --git a/runtime/LibcWrappers.cpp b/runtime/LibcWrappers.cpp index 99993a05..51e860f7 100644 --- a/runtime/LibcWrappers.cpp +++ b/runtime/LibcWrappers.cpp @@ -610,271 +610,270 @@ uint32_t SYM(ntohl)(uint32_t netlong) { } 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)); + 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)); - } + auto result = strcmp(a, b); + _sym_set_return_expression(nullptr); - _sym_push_path_constraint(allEqual, result == 0, - reinterpret_cast(SYM(strcmp))); + 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(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)); + 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)); - } + auto result = strncmp(a, b, n); + _sym_set_return_expression(nullptr); - _sym_push_path_constraint(allEqual, result == 0, - reinterpret_cast(SYM(strncmp))); + 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(SYM(strncmp))); + return result; } uint32_t SYM(strlen)(const char *s) { - tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen)); + 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); + // 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(SYM(strchr))); - ++shadowIt; - } + if (isConcrete(s, result != nullptr ? (result - s) : strlen(s))) + return (result - s); - // HACK! The last byte must be \x00! + // 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_equal( - (*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(0, 8), - cExpr), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); + _sym_build_not_equal( + (*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8), + cExpr), + /*taken*/ 1, reinterpret_cast(SYM(strchr))); + ++shadowIt; + } - return (result - s); + // 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(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(SYM(strchr))); - ++shadowIt; - } + 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); - // 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' + 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_not_equal(*shadowIt, tailExpr_0), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_1), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_2), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_3), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_4), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_5), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_6), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_7), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_8), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_9), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); + _sym_build_equal((*shadowIt != nullptr) ? *shadowIt + : _sym_build_integer(s[i], 8), + cExpr), + /*taken*/ 1, reinterpret_cast(SYM(strchr))); + ++shadowIt; + } - return result; + // 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(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_1), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_2), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_3), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_4), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_5), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_6), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_7), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_8), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_9), + /*taken*/ 1, + reinterpret_cast(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(SYM(strchr))); - ++shadowIt; - } + 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); - // 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' + 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_not_equal(*shadowIt, tailExpr_0), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_1), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_2), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_3), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_4), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_5), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_6), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_7), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_8), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); - _sym_push_path_constraint( - _sym_build_not_equal(*shadowIt, tailExpr_9), - /*taken*/ 1, reinterpret_cast(SYM(strchr))); + _sym_build_equal((*shadowIt != nullptr) ? *shadowIt + : _sym_build_integer(s[i], 8), + cExpr), + /*taken*/ 1, reinterpret_cast(SYM(strchr))); + ++shadowIt; + } - return result; + // 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(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_1), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_2), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_3), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_4), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_5), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_6), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_7), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_8), + /*taken*/ 1, + reinterpret_cast(SYM(strchr))); + _sym_push_path_constraint(_sym_build_not_equal(*shadowIt, tailExpr_9), + /*taken*/ 1, + reinterpret_cast(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)); + 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); + auto *result = strcpy(dest, src); + _sym_set_return_expression(nullptr); - size_t cpyLen = strlen(src); - if (isConcrete(src, cpyLen) && isConcrete(dest, cpyLen)) - return result; + size_t cpyLen = strlen(src); + if (isConcrete(src, cpyLen) && isConcrete(dest, cpyLen)) + return result; - auto srcShadow = ReadOnlyShadow(src, cpyLen); - auto destShadow = ReadWriteShadow(dest, cpyLen); + auto srcShadow = ReadOnlyShadow(src, cpyLen); + auto destShadow = ReadWriteShadow(dest, cpyLen); - std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin()); + std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin()); - return result; + return result; } }