eth-sri / ELINA

ELINA: ETH LIbrary for Numerical Analysis
http://elina.ethz.ch/
Other
129 stars 53 forks source link

Combination of substitution and dimension removal can crash polyhedra domain #34

Open Cu3PO42 opened 6 years ago

Cu3PO42 commented 6 years ago

Hi Gagandeep,

I have encountered a case where the polyhedra domain crashes with an internal null pointer exception when doing the following:

You can reproduce it by using the following (minimal) example:

elina_manager_t *man = opt_pk_manager_alloc(false);
elina_abstract0_t *abs = elina_abstract0_top(man, 0, 3);

elina_dimchange_t removal;
elina_dimchange_init(&removal, 0, 2);
removal.dim[0] = 0;
removal.dim[1] = 1;

elina_linexpr0_t *sub1expr = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 3);
elina_coeff_set_scalar_double(sub1expr->p.coeff + 2, 1);

elina_linexpr0_t *sub2expr = elina_linexpr0_alloc(ELINA_LINEXPR_DENSE, 1);

elina_abstract0_substitute_linexpr(man, true, abs, 0, sub1expr, NULL);
elina_abstract0_remove_dimensions(man, true, abs, &removal);
elina_abstract0_substitute_linexpr(man, true, abs, 0, sub2expr, NULL);

Running this code leads a null pointer exception when executing the last line: In opt_pk_assign.c in line 244

nbcons +=  poly_a[k]->C->nbrows;

poly_a[k]->C is NULL.

I am currently on the most recent commit of the master branch.

Best regards,
Tobias

GgnDpSngh commented 6 years ago

Hi Tobias,

Thanks for spotting this. I have the bug now and there should be no crash due to remove.

Cheers, Gagan