Combination of substitution and dimension removal can crash polyhedra domain

[Cu3PO42]

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

[GgnDpSngh]

Hi Tobias,

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

Cheers,
Gagan