How to tune the clam options to reproduce ELINA paper results

[dengyuhui14]

Hi,

I want to reproduce the results in the paper Fast Polyhdra Abstract Domain. However clam(crab-llvm) has many options that can be tuned and I don't know how to tune them. Could you please tell me the options you ran?

Thank you for all the help!

[GgnDpSngh]

Hi there,

The easiest option would be to try the artifact for the POPL'17 paper available here https://www.sri.inf.ethz.ch/optpoly. Please let me know if you have any further questions.

Cheers, Gagandeep Singh

[dengyuhui14]

Hi,

I tried to download the artifact from https://www.sri.inf.ethz.ch/optpoly/POPL2017.zip but it says page not found.

Thank you for all the help!

[GgnDpSngh]

Hi,

I will check why it is not available. In the meantime, the same settings were also used in the POPL'18 whose artifact can be found here https://www.sri.inf.ethz.ch/popl18-paper251, I checked the VM downloads. Please let me know if it works.

Cheers, Gagandeep Singh

[dengyuhui14]

Hi,

The VM downloads from https://www.sri.inf.ethz.ch/popl18-paper251 works!

Thank you so much!

[dengyuhui14]

Hi Gagandeep,

The latest version of elina_poly in github is the implementation of POPL'17 paper? Or it is the implementation of POPL'18 paper?

Thanks a lot!

[dengyuhui14]

Hi Gagandeep,

What operating system should the virtual box use to open the VDI file?

Thanks!

[GgnDpSngh]

Hi there,

Both implementations are available. The one from POPL'17 is in the "ELINA/elina_poly" folder. We tested the VM to work on Ubuntu and Windows using 64-bit VirtualBox.

Cheers, Gagandeep Singh

[dengyuhui14]

Thanks a lot!

[dengyuhui14]

Hi Gagandeep,

The VM works very well! Thank you so much!

I want to add more timers in this file so that I can get the results like this:

Top: 912574
Bottom: 194799
Free: 6.98225e+08
Copy: 5.18543e+08
Is_Lequal: 930267
Meet_Abstract: 1.48898e+06
Join: 8.29443e+09
Widening: 0
Add_dimension: 1.89152e+08
remove: 3.69083e+08
Permute_dimension: 3.26793e+08
Meet_Lincons_Array: 4.89948e+09
Forget_Array 1.1978e+09
Poly_to_Box: 2.94505e+09
Is_Top: 2.53098e+08
Is_Bottom: 3.89681e+06
Expand: 0
Fold: 0
Sat_Lincons: 0
Assign Linexpr: 6.16999e+09
Substitute Linexpr: 0
Bound Dimension: 0
Conversion time: 0
Poly is unconstrained time: 1.79199e+06
join count: 714
ELINA Polyhedra Analysis: 2.58709e+10 cycles

But I don't know which files and which function prints these results. Could you please tell me what file should I modify to print my new timer?

Thanks!

[GgnDpSngh]

Hi there,

The function to print the timing is here: https://github.com/eth-sri/ELINA/blob/eaefbbd9b42e0e80c0701b5c20b7906e88fbb954/elina_oct/opt_oct_representation.c#L302, you can put the timing in the function like this: https://github.com/eth-sri/ELINA/blob/eaefbbd9b42e0e80c0701b5c20b7906e88fbb954/elina_oct/opt_oct_hmat.c#L290.

Please let me know if it works.

Cheers, Gagandeep Singh

[dengyuhui14]

It works! Thank you so much!

[dengyuhui14]

Hi Gagandeep,

I found that elina_poly refactors the polyhedra in many function like

https://github.com/eth-sri/ELINA/blob/eaefbbd9b42e0e80c0701b5c20b7906e88fbb954/elina_poly/opt_pk_meetjoin.c#L326

and

https://github.com/eth-sri/ELINA/blob/eaefbbd9b42e0e80c0701b5c20b7906e88fbb954/elina_poly/opt_pk_meetjoin.c#L875

Is it possible that I write a refactor function so that the meet, join and other operators that need refactor can use this unique refactor function? Is it the case that different operators need different refactoring steps?

Thanks!

[GgnDpSngh]

Yeah, the refactoring is different for different abstract transformers. We made specific functions with custom optimizations but it may be possible to have a more generic function for refactoring at the cost of some speed.

Cheers, Gagandeep Singh

[dengyuhui14]

Got it! Thanks a lot!