Converting StringV to Z3 looses trailing null bytes

Description

StringV's with implicit trailing zero values not stored explicitly in .args[0] do not have those trailing zeros passed to z3.

We do this conversion here:

claripy/claripy/backends/backend_z3.py

Line 355 in 728cc9d

return z3.StringVal(ast.args[0], ctx=self._context)

Note no where do we use ast.args[1].

While StringV's are mostly stored in .args[0], we store the true length of the string in .args[1]; the extra bytes are implicit null bytes at the end of .args[0].

For example:
claripy.StringV("a", 3") represents a\0\0.

This information is not passed to z3 in any capacity.

Steps to reproduce the bug

import claripy
import ctypes
import z3

# Our padded string
a = claripy.StringV("a", 10)
z3_a = claripy.backend_manager.backends.z3.convert(a)

# Check string length
length = ctypes.c_uint()
_ = z3.Z3_get_lstring(z3_a.ctx_ref(), z3_a.as_ast(), ctypes.byref(length))

print(length)

This yields: c_uint(1)

If z3 supports null bytes in strings this should yield c_uint(10) after Z3Prover/z3#6442 is resolved and c_uint(77) until then.

Environment

Claripy master: bd9b597

Additional context

If z3 strings allow null bytes within them, the fix would be to replace ast.args[0] with ast.args[0].ljust(ast.args[1], '\0') in

claripy/claripy/backends/backend_z3.py

Line 355 in 728cc9d

return z3.StringVal(ast.args[0], ctx=self._context)

If z3 does not allow null bytes within strings then perhaps we should disallow implicit trailing nulls in claripy, not use strings in z3, or find some hybrid String/BV approach?