Null pointers (and then UB) when creating two Sorts with the same name

[shelvacu]

repro:

use z3::Sort;

fn main() {
    let cfg = z3::Config::new();
    let ctx = z3::Context::new(&cfg);

    let res1 = Sort::enumeration(
        &ctx,
        "SameNameSort".into(),
        &["A".into(), "B".into(),]
    );
    dbg!(&res1);
    let res2 = Sort::enumeration(
        &ctx,
        "SameNameSort".into(),
        &["C".into(), "D".into(),]
    );
    dbg!(&res2);
}

This manages to show the issue without triggering any UB, but doing anything interesting with res2 gives a nullptr exception

I'm not sure what exactly is supposed to happen, but at the very least this should panic!

[Pat-Lafon]

Just a little bit of lore for anyone who sees issues like this(and just want to ping @toolCHAINZ if they don't know about this to save them some pain in the future).

When something like this occurs, it's usually because the rust binding are missing a check for the error case. A super easy way to debug this is to run this example with

z3.rs/z3/src/context.rs

Line 14 in 674d7b1

Z3_set_error_handler(p, None);

commented out. This is what is otherwise suppressing the exception that Z3 raises in this case Error: enumeration sort name is already declared between res1 and res2. I think most(/all?) of the various z3 language bindings suppress this handler to give the bindings a chance to handle these kinds of errors in their native language as opposed to trying to catch the exception.

If you look at the implementation of enumeration, it looks like it needs a is_null check on the sort(I think before it gets wrapped but don't hold me to it) and either a panic or to make the function return a result/option(I think the library isn't currently consistent about the different cases... and I think both options are viable for different reasons).

[shelvacu]

You reminded me about this issue, I figure I should talk about what happened after I submitted this issue:

I took a deep dive into what went wrong here, at first thinking that I might submit a PR. I came to the same conclusion: A check for a null ptr return was missing. But why was it missing? Were there any others that were missing? So I dug some more, and realized that virtually every single function exposed by the z3 C API is a C++ try/catch block, with no easy way to determine which ones might have exceptions thrown. Thus I started rewriting in a major way to add a nullptr check to every call, and try to make it hard to make the same mistake in the future. I never ended up submitting a PR because it just kinda became a mess, but feel free to use my changes if you find them useful: master...shelvacu-forks:z3.rs:fix-ur-shit

In general, the change looks like:

• Change every opaque type (like Z3_context, Z3_ast) to use the struct recommended by the rustnomicon https://doc.rust-lang.org/nomicon/ffi.html#representing-opaque-structs
• Changing every z3-sys function to take in NonNull pointers (because z3 lib almost always requires non-null pointers) instead of pointers, and make every pointer-returning function return *mut something because every function might return a null pointer (if an exception is raised)
• On context, make new check_error* functions that will call Z3_get_error_code and wrap a value in a Result based on the error code
• Rewrite every single call to C-lib Z3_* functions to use the check_error functions
• Implementing Deref for every Z3 type with Target of pointer to the underlying C type
• A bunch of other stuff

It was a lot of very opinionated changes but they worked well for me; I made a fun project with the resulting fork.

Even if you don't use my changes (I couldn't blame you...) I would hope to see a more tight approach to avoiding UB in this library. Sometimes it turns out okay, but sometimes it's really really bad, and that's why rust works so hard to avoid it. For anything that probably won't ever return a nullptr, a panic!() is a perfectly fine solution.

[Pat-Lafon]

Cool, yeah I was wondering about NonNull at some point as well. Very interesting to see your attempt.

One question I have though, what do you think the tradeoff is between using NonNull like you've done at the Z3-sys layer as opposed to keeping that the same but wrapping all Z3 struct fields with NonNull?

Like

pub struct Bool<'ctx> {
    pub(crate) ctx: &'ctx Context,
    pub(crate) z3_ast: NonNull<Z3_ast>, // wrapped in Nonnull here
}

This would still keep the logic in z3-sys to a minimum(which I think could be a good thing since it means that most changes barely touch that crate). The null checks are then immediately addressable to the user in whatever way makes more sense at this higher level. I'm not fully sure if you ended up having additional layers of abstraction or not by adding more to the z3_sys crate.

Not sure how the opaque structs thing compares with what is currently done, could make sense. Your other suggestions are also interesting though I don't think I've desired to the same degree.

[shelvacu]

By adding NonNull at the z3-sys layer, I made sure that the type system would help me catch every single call; Passing the return value of Z3_foo to Z3_bar was no longer possible without checking for null. I'm not sure this is the "right" place to do that, but in practice it seemed to work well.

…

On July 17, 2025 10:39:11 PM PDT, Patrick LaFontaine ***@***.***> wrote: Pat-Lafon left a comment (prove-rs/z3.rs#313) Cool, yeah I was wondering about NonNull at some point as well. Very interesting to see your attempt. One question I have though, what do you think the tradeoff is between using NonNull like you've done at the Z3-sys layer as opposed to keeping that the same but wrapping all Z3 struct fields with NonNull? Like ```rust pub struct Bool<'ctx> { pub(crate) ctx: &'ctx Context, pub(crate) z3_ast: NonNull<Z3_ast>, // wrapped in Nonnull here } ``` This would still keep the logic in z3-sys to a minimum(which I think could be a good thing since it means that most changes barely touch that crate). The null checks are then immediately addressable to the user in whatever way makes more sense at this higher level. I'm not fully sure if you ended up having additional layers of abstraction or not by adding more to the z3_sys crate. Not sure how the opaque structs thing compares with what is currently done, could make sense. Your other suggestions are also interesting though I don't think I've desired to the same degree. -- Reply to this email directly or view it on GitHub: #313 (comment) You are receiving this because you authored the thread. Message ID: ***@***.***>

[toolCHAINZ]

I think we could probably just do this incrementally. Start with having NonNull in all the high level API structs, since we know we want that regardless, and then if we find there's places where null still sneaks through (I could see this happening in some of the "non standard" high APIs where lots of z3-sys calls happen within one high-level function), we can extend it to z3-sys too.

[toolCHAINZ]

My recent foray into proc macros in #417 makes me wonder if that's a good solution to doing this at the Z3-sys level with a proc macro.

We could decorate the giant extern C block with a proc attribute macro that rewrites every API endpoint so every argument with a type starting with Z3_<name> (which are all in actuality *mut _Z3_<name>) gets rewritten to be of type std::ptr::NonNull(_Z3_<name>). Output parameters (*mut Z3_<name>) can be rewritten std::ptr::NonNull(Z3_<name>). Return types are left as-is to signify that they are nullable.

This would allow @shelvacu's z3-sys-level change without introducing a bunch of churn/extra logic into the low-level bindings themselves.

We change all high-level structs to also hold NonNull ptrs, and then, as stated earlier in the thread, we just have to catch null pointers in the return values from the FFI and decide whether each function should just return Option or retrieve the error message from the ctx and return Result.

[toolCHAINZ]

Actually, even better:

Since https://doc.rust-lang.org/std/ptr/struct.NonNull.html#representation says that Option<NonNull<T>> has the same representation as NonNull<T>, I think we should be able to just change the definitions of all the Z3_* types to be NonNull<Inner> instead of *mut Inner.

We can then fix up all extern "C" return types to be Option<Z3_<whatever>>, since this will be an Option<NonNull<T>> and is guaranteed to have the same layout as the raw pointer. We could do that substitution manually or through a macro.

[toolCHAINZ]

I've made #450 which fixes the original case in this issue. That code now panics instead of exhibiting UB. Ideally, we'd have that API return a Result or Option but that can be later.