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: https://github.com/angr/claripy/blob/728cc9d1bedc7c19aa1a6a318262e83e69be0a00/claripy/backends/backend_z3.py#L355 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 https://github.com/Z3Prover/z3/issues/6442 is resolved and c_uint(77) until then.

Environment

Claripy master: https://github.com/angr/claripy/commit/bd9b5975787398ee72022ab4cbdc1609ac0dea6d

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 https://github.com/angr/claripy/blob/728cc9d1bedc7c19aa1a6a318262e83e69be0a00/claripy/backends/backend_z3.py#L355

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?

angr / claripy