Portability issue with the `funptr` array

[corwin-of-amber]

Hi,

I compiled ELINA on an M1 Mac (aarch64). I had to disable timing since that has an obvious dependency on x86 assembly, but that does not seem to cause any issues. What does is that some calls to man->funptr (from elina_manager_t) use variadic types like this one: https://github.com/eth-sri/ELINA/blob/20019fe24f26f29ba964ffc186e51a52fa986853/elina_auxiliary/elina_abstract0.h#L529

This is incompatible with ARM calling conventions, because on ARM arguments are passed via registers, and a variadic function call uses different registers from a regular call. (I know that because I have recently tried to do the very same thing myself and was bitten by it.)

Currently, this make ELINA crash in e.g. elina_abstract0_of_lincons_array.

[GgnDpSngh]

Dear Shachar,

Thanks for pointing out the compatibility issues due to the use of variadic functions. We will try to resolve it in the next few days and let you know.

Cheers, Gagandeep Singh

[corwin-of-amber]

I am happy to help with testing. I can also help with fixing it. I assume the calls to funptr are relatively easy to hunt.

[GgnDpSngh]

Thanks for your help, if you have test cases, that would help us. The calls are mostly in "elina_abstract0.c/h", "elina_generic.c", and three in octagon and zones implementations. I believe that the calls are made with the same arguments so variability is not needed, but will need to confirm that.

Cheers, Gagandeep Singh

[corwin-of-amber]

Yes, that is also my impression. I searched for usages using CLion and there seem to be about 80. Most of them are very similar. Almost all of them access the funptr vector with a constant index, and almost all of them have the call immediately after the cast so it's easy to figure out the correct signature.

[corwin-of-amber]

BTW I also make use of clang's compile-time warning and I came across this line: https://github.com/eth-sri/ELINA/blob/20019fe24f26f29ba964ffc186e51a52fa986853/elina_linearize/elina_linearize_texpr.c#L570

clang says the condition is always false which seems to be a correct observation...

[GgnDpSngh]

Yes, I have a deadline + international travel this week, but can fix the variable arguments to function call by Friday next week.

Thanks for spotting the false condition, there should be "or" statements there. I have fixed the code.

Cheers, Gagandeep Singh

[corwin-of-amber]

I will submit a PR with at least some of the fixes and you can review it whenever you have time.