Model Arrays.copyOf for non-functional arrays for soundness#191
Model Arrays.copyOf for non-functional arrays for soundness#191jjppp merged 8 commits intopascal-lab:masterfrom
Arrays.copyOf for non-functional arrays for soundness#191Conversation
|
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 |
|
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.
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.