@@ -659,4 +659,39 @@ int SYM(strncmp)(const char *a, const char *b, size_t n) {
659659 reinterpret_cast <uintptr_t >(SYM (strncmp)));
660660 return result;
661661}
662+
663+ uint32_t SYM (strlen)(const char *s) {
664+ tryAlternative (s, _sym_get_parameter_expression (0 ), SYM (strlen));
665+
666+ // HACK! we regard strlen as a special strchr(s, '\0')
667+ auto *result = strchr (s, 0 );
668+ _sym_set_return_expression (nullptr );
669+
670+ if (isConcrete (s, result != nullptr ? (result - s) : strlen (s)))
671+ return (result - s);
672+
673+ // We force set the value of c to \x00, it should be a concrete value
674+ auto *cExpr = _sym_build_integer (0 , 8 );
675+
676+ size_t length = result != nullptr ? (result - s) : strlen (s);
677+ auto shadow = ReadOnlyShadow (s, length);
678+ auto shadowIt = shadow.begin ();
679+ for (size_t i = 0 ; i < length; i++) {
680+ _sym_push_path_constraint (
681+ _sym_build_not_equal (
682+ (*shadowIt != nullptr ) ? *shadowIt : _sym_build_integer (s[i], 8 ),
683+ cExpr),
684+ /* taken*/ 1 , reinterpret_cast <uintptr_t >(SYM (strchr)));
685+ ++shadowIt;
686+ }
687+
688+ // HACK! The last byte must be \x00!
689+ _sym_push_path_constraint (
690+ _sym_build_equal (
691+ (*shadowIt != nullptr ) ? *shadowIt : _sym_build_integer (0 , 8 ),
692+ cExpr),
693+ /* taken*/ 1 , reinterpret_cast <uintptr_t >(SYM (strchr)));
694+
695+ return (result - s);
696+ }
662697}
0 commit comments