fix issue #1306: compute vf guard for strong update in another branch #1309
Conversation
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## master #1309 +/- ##
==========================================
+ Coverage 64.55% 64.61% +0.05%
==========================================
Files 223 225 +2
Lines 23848 23892 +44
==========================================
+ Hits 15396 15438 +42
- Misses 8452 8454 +2
|
| @@ -276,6 +276,8 @@ void SaberSVFGBuilder::rmIncomingEdgeForSUStore(BVDataPTAImpl* pta) | |||
| } | |||
| for (SVFGEdge* edge: toRemove) | |||
| { | |||
| if (isa<StoreSVFGNode>(edge->getSrcNode())) | |||
There was a problem hiding this comment.
Do we need this condition? Not all edges in toRemove?
There was a problem hiding this comment.
Yes, the condition should be removed. But this case won't pass because of an IntraMSSAPhinode to strong update. I'm afraid there will be more false positives.
svf/lib/SABER/SrcSnkDDA.cpp
Outdated
| @@ -97,6 +97,7 @@ void SrcSnkDDA::analyze(SVFModule* module) | |||
| if(Options::DumpSlice()) | |||
| annotateSlice(_curSlice); | |||
|
|
|||
| memSSA.getRemovedSUVFEdges(); | |||
There was a problem hiding this comment.
why call this method here?
svf/include/SABER/SaberSVFGBuilder.h
Outdated
| @@ -97,6 +101,8 @@ class SaberSVFGBuilder : public SVFGBuilder | |||
| PointsTo globs; | |||
| /// Store all global SVFG nodes | |||
| SVFGNodeSet globSVFGNodes; | |||
| /// Removed strong update edge | |||
| Map<const SVFGNode*, SVFGNodeSet> removedSUVFEdges; | |||
There was a problem hiding this comment.
better to move this map to SaberCondAllocator
There was a problem hiding this comment.
I'm not sure. removedSUVFEdges is derived from saber svfg builder. The Sabercondallocator is not yet initialized at the moment.
svf/include/SABER/SaberSVFGBuilder.h
Outdated
| @@ -62,6 +62,10 @@ class SaberSVFGBuilder : public SVFGBuilder | |||
| svfg->addActualParmVFGNode(pagNode, cs); | |||
| } | |||
|
|
|||
| const Map<const SVFGNode*, SVFGNodeSet>& getRemovedSUVFEdges() const { | |||
There was a problem hiding this comment.
better to move this method under SaberCondAllocator
svf/include/SABER/ProgSlice.h
Outdated
| @@ -309,6 +312,7 @@ class ProgSlice | |||
| const SVFGNode* _curSVFGNode; ///< current svfg node during guard computation | |||
| Condition finalCond; ///< final condition | |||
| const SVFG* svfg; ///< SVFG | |||
| const Map<const SVFGNode*, SVFGNodeSet>& removedSUVFEdges; | |||
There was a problem hiding this comment.
better to move this map to SaberCondAllocator
svf/include/SABER/ProgSlice.h
Outdated
| @@ -59,9 +59,9 @@ class ProgSlice | |||
| typedef FIFOWorkList<const SVFBasicBlock*> CFWorkList; ///< worklist for control-flow guard computation | |||
|
|
|||
| /// Constructor | |||
| ProgSlice(const SVFGNode* src, SaberCondAllocator* pa, const SVFG* graph): | |||
| ProgSlice(const SVFGNode* src, SaberCondAllocator* pa, const SVFG* graph, const Map<const SVFGNode*, SVFGNodeSet>& edges): | |||
There was a problem hiding this comment.
keep the constructor unchanged and move the map to SaberCondAllocator
svf/include/SABER/SaberSVFGBuilder.h
Outdated
| @@ -33,6 +33,8 @@ | |||
| #include "MSSA/SVFGBuilder.h" | |||
| #include "SVFIR/SVFValue.h" | |||
| #include "Util/WorkList.h" | |||
| #include "SABER/SaberCondAllocator.h" | |||
There was a problem hiding this comment.
Put this include to cpp and use forward declaration instead.
|
CFL cases failed, looks to be assertion failures. |
Yes, CFL uses sabersvfgbuilder. |
https://github.com/SVF-tools/SVF/blob/master/svf/include/CFL/CFLVF.h#L62 |
I see, we will then need to set the condition allocator. |
fix issue #1306: we compute the vf guard of invalid branches stemming from removed strong-update value-flow, and conjunct the negation of that.