eth-sri / ELINA

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

Segfault when creating a polyhedra using a tcons_array #56

Closed mzehendner closed 4 years ago

mzehendner commented 4 years ago

The Segfault occurs when using a tree constraint, that includes a coefficient of type double. Here is a minimal example to recreate the segfault:

int main() {
  elina_tcons0_array_t arr = elina_tcons0_array_make(1);
  elina_coeff_t *cst = elina_coeff_alloc(ELINA_COEFF_SCALAR);
  elina_coeff_set_scalar_double(cst, 1.0);
  elina_texpr0_t *expr = elina_texpr0_cst(cst);
  arr.p[0] = elina_tcons0_make(ELINA_CONS_EQ, expr, NULL);
  elina_manager_t *man = opt_pk_manager_alloc(false);
  elina_abstract0_t *abs = elina_abstract0_of_tcons_array(man, 0, 0, &arr);
  return 0;
}

The problem seems to be in elina_scalar_trunc. The type of the scalar is expected to be the type of the parameter discr, which is passed through from opt_pk_meet_tcons_array with the value ELINA_SCALAR_MPQ.

at 0x493C0A1: __gmpz_tdiv_q (in /usr/lib/libgmp.so.10.4.0)
by 0x4C0BFE4: elina_scalar_trunc_mpq (elina_scalar_arith.c:536)
by 0x4C0BFE4: elina_scalar_trunc (elina_scalar_arith.c:559)
by 0x4C0D350: elina_interval_is_int (elina_interval_arith.c:353)
by 0x4C11F4A: elina_interval_intlinearize_texpr0_rec (elina_linearize_texpr.c:906)
by 0x4C13B1F: elina_intlinearize_elina_tcons0_array (elina_linearize_texpr.c:1597)
by 0x4C13D8F: elina_intlinearize_tcons0_array (elina_linearize_texpr.c:1680)
by 0x4C0A4CE: elina_generic_meet_intlinearize_tcons_array (elina_generic.c:222)
by 0x48A4B3E: opt_pk_meet_tcons_array (opt_pk_meetjoin.c:763)
by 0x48C8678: elina_abstract0_meet_tcons_array (elina_abstract0.c:1003)
by 0x10B4B9: main (test.c:190)
GgnDpSngh commented 4 years ago

Hi there,

Thank you very much for reporting this bug, I have fixed it now. Please pull, let me know if you have any other issues with ELINA.

Cheers, Gagandeep Singh