shrbadihi / eqbench Goto Github PK
View Code? Open in Web Editor NEWLicense: MIT License
License: MIT License
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:
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,*.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, ...*.json
file should probably be checked the function that is:
snippet
(e.g. in benchmarks/caldat/badluk/Neq
) orbenchmarks/airy/beschb/Neq
) orbenchmarks/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:
REVE
(in the paper is 23 Eq and 9 Neq),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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.