SEGFAULT when joining bottom

[skius]

I stumbled upon a segmentation fault seemingly out of nowhere when joining elements of OptPk. After some in-depth investigation, it turned out that under certain conditions, mutably joining a bottom element leads to a double-free (I believe).

In particular, when mutably (destructive = true) joinining a bottom element that is the result of a mutable meet, one ends up aborting.

I came up with this (I believe minimal, but I didn't investigate much further) example:

#include "opt_pk.h"

int main() {
    elina_manager_t *pk = opt_pk_manager_alloc(0);

//  Swap what's commented out, and there won't be a segfault
//  elina_abstract0_t* bot = elina_abstract0_bottom(pk, 1, 0);
    elina_abstract0_t* bot = elina_abstract0_top(pk, 1, 0);

    elina_abstract0_t* top = elina_abstract0_top(pk, 1, 0);

    elina_tcons0_array_t arr = elina_tcons0_array_make(1);
    elina_tcons0_t unsat = elina_tcons0_make_unsat();
    arr.p[0] = unsat;

    elina_abstract0_t* top_meet_unsat = elina_abstract0_meet_tcons_array(pk, true, bot, &arr);
    elina_abstract0_t* top_meet_unsat_join = elina_abstract0_join(pk, true, top_meet_unsat, top);
    return 0;
}

$ clang  -lelinalinearize -lelinaux -loptpoly -lgmp -lmpfr examples/bug.c  
$ ./a.out
free(): invalid pointer
Aborted

I assume this is intended behavior, but I was wondering if other such edge cases are documented anywhere? One other example would be that explicitly freeing a bottom element leads again to a double-free.

Furthermore, is it a 'correct' workaround to always check prior to mutably joining whether the abstract0 is bottom, and if so, just copy the second operand into the first instead of joining?

[GgnDpSngh]

Hi there,

Thanks for finding this issue. This was a bug which we have fixed now. Please let us know if you encounter any further issues.

Cheers, Gagandeep Singh

[skius]

Thanks, that seems to have fixed the issues I was experiencing!

(Also, just mentioning this here in case it's of any interest: I discovered this while developing a Rust wrapper for ELINA over at skius/elina-rs)

Best

[GgnDpSngh]

Awesome, we could try to have the wrapper part of the ELINA repo if you like. Also, please let us know if you encounter any further issues.

Cheers, Gagandeep Singh

[skius]

we could try to have the wrapper part of the ELINA repo

Could you elaborate what you mean by that? If you mean adding it to the README, sure, please go ahead!

If you mean moving the source into the repo, I'm not sure how the Rust package ecosystem (crates.io) handles that, and in any case the wrapper is untested and missing some features still, so I'd need to finish that first. I lean towards keeping it separate in order to have more freedom and flexibility in adding perhaps exotic high-level features, however.