shrbadihi / eqbench Goto Github PK

Is there a simple way to find out which functions for each project should an equivalence checking tool check for equality? (Specifically talking about the C versions of the programs.)

So far I found out that:

• for the CLEVER benchmark the function that should be checked is probably included in the field program name (after a dot) in Desc.json file of each program,
• for programs that do not contain *.json file I think mostly all functions located in the file can be evaluated, but there are exceptions e.g. constructor function in Neq version of the program hashCode in ej_hash benchmark, ...
• for programs that do contain *.json file should probably be checked the function that is:
  • often called snippet (e.g. in benchmarks/caldat/badluk/Neq) or
  • has the same name as the name of the program (e.g. benchmarks/airy/beschb/Neq) or
  • the name of the function 'contains' the name of the program (e.g. benchmarks/raytrace/sphere/Neq)
  • ...

I guess that the Eq versions of programs are not a big deal because there should be all functions in the file evaluated as equal,
but the problem is in Neq versions because it often contains some equal functions and usually one not equal.

The benchmark ell/ellpi/Eq is marked as semantically equal, however, it clearly isn't. The gist of the change is simplification of an arithmetic expression using mathematical laws -- simplifying (A + B) * (A - B) to A^2 - B^2, however it's changed to A^2 + B^2 instead. Try adding the following main to the programs:

int main(void) {
    printf("%f\n", snippet(30.0, 1, 2.0));
    return 0;
}

The old version produces:

invalid arguments in rf
invalid arguments in rj
-nan

The new version produces:

-0.729108

which clearly showcases inequality. I believe that the change in newV.c should be to q=1.0-((s*ak)*(s*ak)) instead of q=1.0+((s*ak)*(s*ak)). One thing that I am not completely sure about is whether this makes it really semantically equal. Due to the change of order of operations, it is possible that there the floating points are rounded differently (floating point arithmetic is not distributive). On the other hand, there are checks for invalid arguments which exclude large and small numbers so perhaps this prevents rounding differences from occurring but I am not sure how to effectively verify this. I am going to open a PR with the change for now but feel free to suggest a different fix and/or continue the discussion regarding rounding of floating points.

I have a question about the number of programs in the benchmarks, I am not sure if I am overlooking something or if there is a different number of programs than is adduced in the EqBench paper.
Specifically talking about the REVE and CLEVER benchmarks, I have counted:

• 22 Eq and 8 Neq programs for REVE (in the paper is 23 Eq and 9 Neq),
• 27 Eq and 20 Neq programs for CLEVER benchmark (in the paper is 29 Eq and 21 Neq).

Please let me know if I am missing something or if there is in fact different number of programs.