prove-rs / z3.rs

Rust bindings for the Z3 solver.
338 stars 105 forks source link

Symbol::as_z3_symbol can return Null Pointer #235

Open Pat-Lafon opened 1 year ago

Pat-Lafon commented 1 year ago

It seem like the integer conversion for Symbol does not check that the integer is within the valid bounds that Z3_mk_int_symbol expects(0 <= 2^30 -1). If you try to create a symbol with u32::MAX for example then any of the functions that use a symbol via as_z3_symbol will be using a null pointer.

I'm not sure what bad things can happen because of this, I think some of the usual cases do get caught or just have other operations return null as well.

#[test]
fn test() {
    let cfg = crate::Config::new();
    let ctx = Context::new(&cfg);
    println!("{}", crate::ast::Bool::new_const(&ctx, u32::MAX).to_string());
}
Pat-Lafon commented 1 year ago

In doing some more digging, I see that Z3 tries to warn the user about this but in #92 we disabled the error handler and don't otherwise try to detect this situation.