elina_zonotope bugfix

[ljlin]

Hi Gagan.

When we used elina_zonotope, we found that the output is abnormal. Through debugging, we think there is a bug in the following code snippet.

ELINA/elina_zonotope/zonotope_internal.h

Lines 1399 to 1402 in e824898

	elina_scalar_sub(c0,dmax,dmin, ELINA_SCALAR_DOUBLE);
	elina_scalar_div_2(c0, c0);
	res->c_inf = c0->val.dbl;
	res->c_sup = c0->val.dbl;

When we changed the 1401st line as follows, the precision is improved a lot.

res->c_inf = -c0->val.dbl;

And when we convert an abstract element into a lincons array, the elina abstract0 API generates MPQ scalars, which is then read as a double when we use this lincons array to intersect with a zonotope in the following code snippet.

ELINA/elina_zonotope/elina_box_meetjoin.c

Lines 385 to 392 in 3be0c7e

	if(cst->discr==ELINA_COEFF_SCALAR){
	*itv_inf = -cst->val.scalar->val.dbl;
	*itv_sup = cst->val.scalar->val.dbl;
	}
	else{
	*itv_inf = -cst->val.interval->inf->val.dbl;
	*itv_sup = cst->val.interval->sup->val.dbl;
	}

Thanks,
Jianlin

[GgnDpSngh]

Hi Jianlin,

Thanks for spotting it, note that ELINA no longer supports Join for the Zonotope domain based on [1] as it turns out to be imprecise for analysis, e.g., for approximating the ReLU activation in the neural networks (Instead, we compute a more precise ReLU transformer based on [2] via the "zonoml" domain which builds on top of "elina_zonotope"). A version of ELINA that has the Zonotope join implemented could be found here:
ELINA with Zonotope Join.

From our experience, the Join above gives more precise results than Apron.

References:

1. A logical product approach to zonotope intersection, CAV 2009.
2. Fast and Effective Robustness Certification, NeurIPS 2018.

Cheers,
Gagandeep Singh

[ljlin]

Hi Gagan.
Thank you very much for the information you provided, but I found that both cfdbc46 and 7a2def1 have memory leaks when I use them. I found that after aef18a8, there is no such problem.

Although there is no best join transformer in the Zonotope domain, I need one. Is it feasible to add the join operation (with minor modification) in

ELINA/elina_zonotope/zonotope_meetjoin.c

Line 178 in cfdbc46

zonotope_t* zonotope_join(elina_manager_t* man, bool destructive, zonotope_t* z1, zonotope_t* z2)

to the latest version?

[GgnDpSngh]

Hi Jianlin,

I have added support for the Zonotope join in the latest version of ELINA and tested it on many examples. It seems to be correct, let me know if you have any further problems/questions regarding ELINA.

Cheers,
Gagandeep Singh