Use NonNull in Z3 safe bindings

[Pat-Lafon]

As observed in #226, some of the implementations of the safe Z3 function calls check whether the pointers they get from the unsafe bindings are null. I have proposed that the safe bindings could rely on NonNull to uniformly enforce this check.

To the best of my understanding, I'll use Model as an example:

The unsafe bindings for creating a Z3 Model return a raw pointer

#[doc(hidden)]
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct _Z3_model {
    _unused: [u8; 0],
}
/// Model for the constraints inserted into the logical context.
pub type Z3_model = *mut _Z3_model;

...

/// Retrieve the model for the last [`Z3_solver_check`]
///
/// The error handler is invoked if a model is not available because
/// the commands above were not invoked for the given solver, or if the result was `Z3_L_FALSE`.
pub fn Z3_solver_get_model(c: Z3_context, s: Z3_solver) -> Z3_model;

Model then gets exposed in the safe bindings as

/// Model for the constraints inserted into the logical context.
//
// Note for in-crate users: Never construct a `Model` directly; only use
// `Model::new()` which handles Z3 refcounting properly.
pub struct Model<'ctx> {
    ctx: &'ctx Context,
    z3_mdl: Z3_model,
}

unsafe fn wrap(ctx: &'ctx Context, z3_mdl: Z3_model) -> Model<'ctx> {
    Z3_model_inc_ref(ctx.z3_ctx, z3_mdl);
    Model { ctx, z3_mdl }
}

pub fn of_solver(slv: &Solver<'ctx>) -> Option<Model<'ctx>> {
    unsafe {
        let m = Z3_solver_get_model(slv.ctx.z3_ctx, slv.z3_slv);
        if m.is_null() {
            None
        } else {
            Some(Self::wrap(slv.ctx, m))
        }
    }
}

The observation made is that one has to remember to check and correctly handle the possibility of getting a null pointer from Z3_solver_get_model. Presumably there is an invariant that a Model struct only contains a valid pointer to a Z3 model. In some cases, the null check is more of a defensive programming mechanism since we might always expect that (a non-buggy usage of) Z3 will give a valid pointer, in other cases, null is a valid output of Z3 that should be handled.

Assuming that we want Model to always contain a non-null pointer, the compiler could help us if we wrap the pointer in NonNull. In this case, NonNull is parameterized over the underlying type of the Z3_model pointer which is _Z3_model.

pub struct Model<'ctx> {
    ctx: &'ctx Context,
    z3_mdl: NonNull<_Z3_model>,
}

The Model wrap function is then updated with the new argument type

impl<'ctx> Model<'ctx> {
    unsafe fn wrap(ctx: &'ctx Context, z3_mdl: NonNull<_Z3_model>) -> Model<'ctx> {
        Z3_model_inc_ref(ctx.z3_ctx.as_ptr(), z3_mdl.as_ptr());
        Model { ctx, z3_mdl }
    }

Now, every api that tries to create a model will need to wrap the underlying pointer in NonNull and either handle the null case or propagate this case up to the user via an option/error.

pub fn of_solver(slv: &Solver<'ctx>) -> Option<Model<'ctx>> {
    unsafe {
        let m = Z3_solver_get_model(slv.ctx.z3_ctx.as_ptr(), slv.z3_slv.as_ptr());
        NonNull::new(m).map(|m| Self::wrap(slv.ctx, m))
    }
}

Some methods do not currently handle the null case(presumably since the method is unlikely/not able to return null at this time). These cases can just call unwrap which turns the possibility of a null pointer into a runtime panic on the Rust side.

/// Translate model to context `dest`
pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Model<'dest_ctx> {
    unsafe {
        Model::wrap(
            dest,
            NonNull::new(Z3_model_translate(
                self.ctx.z3_ctx.as_ptr(),
                self.z3_mdl.as_ptr(),
                dest.z3_ctx.as_ptr(),
            ))
            .unwrap(),
        )
    }
}

Some downsides that come to mind:

• extra boilerplate to convert to/from the NonNull wrapper
• additional (probably unnecessary) null pointer checks
• that any wrapped pointers must conform to more strict requirements("Unlike *mut T, the pointer must always be non-null, even if the pointer is never dereferenced.", "Unlike *mut T, NonNull<T> was chosen to be covariant over T. This makes it possible to use NonNull<T> when building covariant types, but introduces the risk of unsoundness if used in a type that shouldn’t actually be covariant.")

The motivation for this change is very much like rust-lang/rust#49220 but one level up; explicit documentation with compiler inserted checks so that unexpected null pointers are handled(one could make this change at the level of the raw c bindings... however that seems like more sweeping change than adding additional checks to the implementation of the safe bindings).

The example diff can be found here: Pat-Lafon/z3.rs@748c90a...Pat-Lafon:7200e68

[Pat-Lafon]

One example of hitting this is if you create a function application that doesn't typecheck. For example:

let f = FuncDecl::new(&ctx, "f", &[&Sort::int(&ctx)], &Sort::int(&ctx));
let y = String::new_const(&ctx, "y");
let f_y = f.apply(&[&y]).as_int().unwrap();

Here we are a bit lucky that Dynamic::wrap contains an assertion:
thread 'main' panicked at 'assertion failed: !ast.is_null()', ~/.cargo/git/checkouts/z3.rs-5e2ffa4244686114/691ac97/z3/src/ast.rs:630:1 but it might be nice to return a more helpful error message here(though I guess this also speaks to the lack of coordination with Z3's error codes).