@@ -436,4 +436,39 @@ int SYM(strncmp)(const char *a, const char *b, size_t n) {
436436 reinterpret_cast <uintptr_t >(SYM (strncmp)));
437437 return result;
438438}
439+
440+ uint32_t SYM (strlen)(const char *s) {
441+ tryAlternative (s, _sym_get_parameter_expression (0 ), SYM (strlen));
442+
443+ // HACK! we regard strlen as a special strchr(s, '\0')
444+ auto *result = strchr (s, 0 );
445+ _sym_set_return_expression (nullptr );
446+
447+ if (isConcrete (s, result != nullptr ? (result - s) : strlen (s)))
448+ return (result - s);
449+
450+ // We force set the value of c to \x00, it should be a concrete value
451+ auto *cExpr = _sym_build_integer (0 , 8 );
452+
453+ size_t length = result != nullptr ? (result - s) : strlen (s);
454+ auto shadow = ReadOnlyShadow (s, length);
455+ auto shadowIt = shadow.begin ();
456+ for (size_t i = 0 ; i < length; i++) {
457+ _sym_push_path_constraint (
458+ _sym_build_not_equal (
459+ (*shadowIt != nullptr ) ? *shadowIt : _sym_build_integer (s[i], 8 ),
460+ cExpr),
461+ /* taken*/ 1 , reinterpret_cast <uintptr_t >(SYM (strchr)));
462+ ++shadowIt;
463+ }
464+
465+ // HACK! The last byte must be \x00!
466+ _sym_push_path_constraint (
467+ _sym_build_equal (
468+ (*shadowIt != nullptr ) ? *shadowIt : _sym_build_integer (0 , 8 ),
469+ cExpr),
470+ /* taken*/ 1 , reinterpret_cast <uintptr_t >(SYM (strchr)));
471+
472+ return (result - s);
473+ }
439474}
0 commit comments