public static function getString(&$str)
    {
        $p = mb_orig_strpos($str, "\x00");
        if ($p === false) {
            return '';
        }
        $r = mb_orig_substr($str, 0, $p);
        $str = mb_orig_substr($str, $p + 1);
        return $r;
    }