ELINA
ELINA copied to clipboard
Combination of substitution and dimension removal can crash polyhedra domain
Hi Gagandeep,
I have encountered a case where the polyhedra domain crashes with an internal null pointer exception when doing the following:
- Create a top value with 3 dimensions.
- Substitute the first dimension by the third by using a linear expression.
- Remove the first two dimensions.
- Substitute the remaining dimension by a zero vector.
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
Hi Tobias,
Thanks for spotting this. I have the bug now and there should be no crash due to remove.
Cheers, Gagan