-
Notifications
You must be signed in to change notification settings - Fork 190
Model Arrays.copyOf for non-functional arrays for soundness
#191
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Model Arrays.copyOf for non-functional arrays for soundness
#191
Conversation
|
All contributors have signed the CLA ✍️ ✅ |
|
I have read the CLA Document and I hereby sign the CLA |
|
recheck |
src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java
Outdated
Show resolved
Hide resolved
src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java
Outdated
Show resolved
Hide resolved
src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java
Outdated
Show resolved
Hide resolved
src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java
Outdated
Show resolved
Hide resolved
src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java
Outdated
Show resolved
Hide resolved
src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java
Outdated
Show resolved
Hide resolved
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #191 +/- ##
=============================================
+ Coverage 0 75.82% +75.82%
- Complexity 0 4658 +4658
=============================================
Files 0 481 +481
Lines 0 16070 +16070
Branches 0 2199 +2199
=============================================
+ Hits 0 12185 +12185
- Misses 0 3018 +3018
- Partials 0 867 +867
🚀 New features to boost your workflow:
|
src/test/resources/pta/taint/ZeroLengthArrayWithArraysCopyOf-pta-expected.txt
Outdated
Show resolved
Hide resolved
|
This PR appears to introduce a precision regression (compared with the version that reverts the ZeroLengthArray optimization). The data on dacapo-2006/eclipse is as follows: revert f4f1c5d This PR(86ef02d) This PR revert ZeroLengthArray optimization |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Merge after the precision regression is addressed
|
another regression experiment (ci PTA): before patch + revert ZLA optimazation patch patch + revert ZLA optimazation |
| CSObj csNewArray = csManager.getCSObj(context, newArray); | ||
| solver.addVarPointsTo(context, result, csNewArray); | ||
| } else { | ||
| solver.addVarPointsTo(context, result, csObj); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The regression is caused by missing handlers.keySet().forEach(solver::addIgnoredMethod) in onStart()
Arrays.copyOf for non-functional arrays to obtain sound results for taint analysis
Arrays.copyOf for non-functional arrays to obtain sound results for taint analysisArrays.copyOf for non-functional arrays for soundness
While investigating issue #168 , I found that Tai-e’s current handling of Arrays.copyOf is insufficient, which prevents correct analysis of the following code pattern:
Specifically, in the first new statement, Tai-e generates a mock object ZeroLengthArray( PR #140 ) and stores it in the points-to set of original. In the subsequent call to Arrays.copyOf, Tai-e propagates all objects from original’s points-to set to copy's. As a result, copy contains only the non-functional mock object ZeroLengthArray, which cannot hold array indexes. Consequently, copy[copy.length - 1] yields null, making correct array store/load analysis impossible.
To address this, I optimized the handling of Arrays.copyOf and added a corresponding testcase, which resolve the above issue.