prove-rs / z3.rs

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

Varops crash with empty slice #84

Open st3ll1s opened 4 years ago

st3ll1s commented 4 years ago

I appreciate the changes by @bumblepie in #83. However, there seems to be a crash (not a panic!) with an empty slice as the argument to varops:

#[test]
fn test_zero_args() {
    let _ = env_logger::try_init();
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let _ = ast::Int::add(&ctx, &[]);
}

Results in

Error: no arguments supplied to arithmetical operator

Most Z3 C API functions require the list of operands to be nonempty.

A slight improvement might be to add an assert! in the right places to guard against an empty slice so the panic can be caught.

fitzgen commented 4 years ago

Thanks for the bug report @st3ll1s.

I think where it makes sense, we should return a default value, eg or([]) == false and and([]) == true (and document this behavior). For any operations where there isn't a default value, then we should panic (and document this behavior).

@bumblepie, would you care to implement this fix?

bumblepie commented 4 years ago

Yeah, I can pick this up - I'm hesitant to give a default value for or([]) etc - in those cases I'm not sure it's intuitive to expect either true or false, even if it is documented. We could always return a Result - I think it's the most "rusty" way of doing things, although it is a bit less ergonomic. Otherwise, the assert! idea makes sense if we want to keep the signature the same. Another option would be to create some NonEmptySlice type that implements tryfrom<slice> and use that rather than a slice in the signature