Comments (6)
ARDiff is a method-level equivalence-checking tool. So if you are checking the equivalence of the method snippet, ARDiff assumes the method lib is not changed and thus they are equivalent.
Is it what you were trying to check?
from ardiff.
Thank you very much for your reply. I want to check the equivalence of snippet functions affected by changes to lib functions. Can I understand that ARDiff can only check the equivalence under changes to the first function itself?
from ardiff.
Yes, that is correct.
from ardiff.
To follow-up on your example, you can run ARDiff on lib functions to check the equivalence of this function.
from ardiff.
To follow-up on your example, you can run ARDiff on lib functions to check the equivalence of this function.
Thank you very much for your reply. I have tested the fib function separately and used the default parameter, but the result is still not given after 300 seconds timeout. I also built other test cases, some of which correctly judged equivalence, but some of which gave incorrect results. Take the following test
public class oldV {
public static double snippet(int x, int y) {
if (x > 30 || y > 30) {
return 0;
}
else if (x == 2) {
for (int i = 2; i < 10; i++) {
if (y % i == 0) {
return i;
}
}
return y;
}
else {
return 0;
}
}
}
public class newV {
public static double snippet(int x, int y) {
if (x > 30 || y > 30) {
return 0;
}
else if (x == 2) {
for (int i = 2; i < 10; i++) {
if (y % i == 0) {
return i + 1;
}
}
return y;
}
else {
return 0;
}
}
}
This pair of programs is not equivalent, but ARDiff decides it is. Could you explain why this is the case? thank you.
from ardiff.
Regarding the fib function, as there is a recursion in one and the loop in the other, creating the symbolic execution and then solving the symbolic summaries take so much time. Solving NEQ cases is also generally harder than EQ. I tried your example with ARDiff and IMP-S (the other symbolic-execution-based technique) both ran out of time.
Regarding the other example, the problem is with SMT solver to reason about %. Since it is non-linear arithmetic it is so complex for SMT solvers to handle (related post: https://stackoverflow.com/questions/66781172/modular-arithmetic-using-z3). When I changed "if(y % i == 0)" to "if(y / i == 0)", ARDiff output Not-Equivalent. The issue is that the JPF cannot explore this path and consequently cannot create the summary of the path. So based on the the explored paths, the two versions are equivalent. ARDiff, similar to other symbolic-execution-based techniques, rely on the fact that the underlying symbolic execution engine can theroritically explore all paths.
Hope that helps!
from ardiff.
Related Issues (3)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from ardiff.