SVF
SVF copied to clipboard
Published
20 hours ago •
SVF-tools
SVF-tools
Unknown reason for a simple false positive and inconsistent flag behavior
Hi, there is a simple false positive.
example.c
#include <stdlib.h>
#include <stdio.h>
int main() {
int *ptr = (int *)malloc(sizeof(int));
for (int i=0; i < 2; i++) {
if(i==20000) {
free(ptr);
}
}
free(ptr);
return 0;
}
Compile
clang -c -g -emit-llvm example.c -o example.bc
Check 1
saber -dfree example.bc
Then, saber would report a double free. The complete output is:
*********General Stats***************
################ (program : loop_df.bc)###############
AddrsNum 13
BBWith2Succ 2
BBWith3Succ 0
CallsNum 0
ConstArrayObj 0
ConstStructObj 0
ConstantObj 0
CopysNum 1
FIObjNum 0
FSObjNum 9
FunctionObjs 4
GepsNum 0
GlobalObjs 0
HeapObjs 1
IndCallSites 0
LoadsNum 5
MaxStructSize 0
NonPtrObj 8
ReturnsNum 0
StackObjs 3
StoresNum 4
TotalCallSite 3
TotalFieldObjects 0
TotalObjects 10
TotalPTASVFStmts 12
TotalPointers 44
TotalSVFStmts 33
VarArrayObj 0
VarStructObj 0
----------------Time and memory stats--------------------
LLVMIRTime 0.006
SVFIRTime 0
SymbolTableTime 0
#######################################################
*********PTACallGraph Stats (Andersen analysis)***************
################ (program : loop_df.bc)###############
----------------Numbers stats----------------------------
CalRetPairInCycle 0
MaxNodeInCycle 0
NodeInCycle 0
TotalCycle 0
TotalEdge 3
TotalNode 4
#######################################################
*********Andersen Pointer Analysis Stats***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
AvgIn/OutAddrEdge 0.4
AvgIn/OutCopyEdge 0.2
AvgIn/OutEdge 0.75
AvgIn/OutLoadEdge 0.1
AvgIn/OutStoreEdge 0.05
AvgPtsSetSize 0.183333
AvgTopLvlPtsSize 0.909091
CollapseTime 0
CopyGepTime 0
LoadStoreTime 0
MemoryUsageVmrss 0
MemoryUsageVmsize 0
SCCDetectTime 0
SCCMergeTime 0
TotalTime 0
UpdateCGTime 0
----------------Numbers stats----------------------------
AddrProcessed 8
CopyProcessed 3
DummyFieldPtrs 0
FieldObjs 0
GepProcessed 0
IndCallSites 0
IndEdgeSolved 0
LoadProcessed 2
LocalVarInRecur 0
MaxInAddrEdge 1
MaxInCopyEdge 1
MaxInLoadEdge 1
MaxInStoreEdge 1
MaxNodesInSCC 0
MaxOutAddrEdge 1
MaxOutCopyEdge 2
MaxOutLoadEdge 2
MaxOutStoreEdge 1
MaxPtsSetSize 1
MemObjects 10
NodesInCycles 0
NullPointer 0
NumOfAddrs 8
NumOfCGEdge 7
NumOfCGNode 24
NumOfCopys 4
NumOfFieldExpand 0
NumOfGeps 0
NumOfLoads 2
NumOfSCCDetect 2
NumOfSFRs 0
NumOfStores 1
NumOfValidNode 20
NumOfValidObjNode 8
Pointers 44
PointsToBlkPtr 0
PointsToConstPtr 0
SolveIterations 2
StoreProcessed 1
TotalCycleNum 0
TotalObjects 10
TotalPWCCycleNum 0
TotalPointers 44
#######################################################
****Persistent Points-To Cache Statistics: Andersen's analysis bitvector****
################ (program : loop_df.bc)###############
UniquePointsToSets 9
TotalUnions 11
PropertyUnions 11
UniqueUnions 0
LookupUnions 0
PreemptiveUnions 0
TotalComplements 48
PropertyComplements 48
UniqueComplements 0
LookupComplements 0
PreemptiveComplements 0
TotalIntersections 3
PropertyIntersections 3
UniqueIntersections 0
LookupIntersections 0
PreemptiveIntersections 0
#######################################################
*********Memory SSA Statistics***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
AverageRegSize 1
GenMUCHITime 0
GenRegionTime 0
InsertPHITime 0
SSARenameTime 0
TotalMSSATime 0
----------------Numbers stats----------------------------
BBHasMSSAPhi 0
CSChiNode 1
CSHasChi 1
CSHasMu 1
CSMuNode 1
FunEntryChi 2
FunHasEntryChi 1
FunHasRetMu 1
FunRetMu 2
LoadHasMu 2
LoadMuNode 2
MSSAPhi 0
MaxRegSize 1
MemRegions 2
StoreChiNode 1
StoreHasChi 1
#######################################################
*********SVFG Statistics***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
ATNodeTime 0
AvgWeight 1
ConnDirEdgeTime 0
ConnIndEdgeTime 0
OptTime 0
TLNodeTime 0
TotalTime 0
----------------Numbers stats----------------------------
ActualIn 1
ActualOut 1
ActualParam 4
ActualRet 0
Addr 8
AvgInDegree 0
AvgIndInDeg 1
AvgIndOutDeg 1
AvgOutDegree 0
Copy 1
DirectCallEdge 0
DirectEdge 6
DirectRetEdge 0
FormalIn 2
FormalOut 2
FormalParam 0
FormalRet 0
Gep 0
IndCallEdge 0
IndRetEdge 0
IndirectEdge 5
IndirectEdgeLabels 5
Load 2
MSSAPhi 0
MaxInDegree 1
MaxIndInDeg 1
MaxIndOutDeg 3
MaxOutDegree 3
PHI 0
Store 1
TotalEdge 11
TotalNode 23
#######################################################
*********SVFG Statistics***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
ATNodeTime 0
AvgWeight 1
ConnDirEdgeTime 0
ConnIndEdgeTime 0
OptTime 0
TLNodeTime 0
TotalTime 0
----------------Numbers stats----------------------------
ActualIn 1
ActualOut 1
ActualParam 4
ActualRet 0
Addr 8
AvgInDegree 0
AvgIndInDeg 1
AvgIndOutDeg 1
AvgOutDegree 0
Copy 1
DirectCallEdge 0
DirectEdge 6
DirectRetEdge 0
FormalIn 2
FormalOut 2
FormalParam 0
FormalRet 0
Gep 0
IndCallEdge 0
IndRetEdge 0
IndirectEdge 5
IndirectEdgeLabels 5
Load 2
MSSAPhi 0
MaxInDegree 1
MaxIndInDeg 1
MaxIndOutDeg 3
MaxOutDegree 3
PHI 0
Store 1
TotalEdge 11
TotalNode 23
#######################################################
Double Free : memory allocation at : (CallICFGNode: { "ln": 5, "cl": 23, "fl": "loop_df.c" })
double free path:
--> ({ "ln": 6, "cl": 5, "fl": "loop_df.c" }|True)
--> ({ "ln": 7, "cl": 12, "fl": "loop_df.c" }|True)
Check 2
If we add one more flag to saber like this:
saber -dfree -leak example.bc
Then, the false positive would no longer appear.
*********General Stats***************
################ (program : loop_df.bc)###############
AddrsNum 13
BBWith2Succ 2
BBWith3Succ 0
CallsNum 0
ConstArrayObj 0
ConstStructObj 0
ConstantObj 0
CopysNum 1
FIObjNum 0
FSObjNum 9
FunctionObjs 4
GepsNum 0
GlobalObjs 0
HeapObjs 1
IndCallSites 0
LoadsNum 5
MaxStructSize 0
NonPtrObj 8
ReturnsNum 0
StackObjs 3
StoresNum 4
TotalCallSite 3
TotalFieldObjects 0
TotalObjects 10
TotalPTASVFStmts 12
TotalPointers 44
TotalSVFStmts 33
VarArrayObj 0
VarStructObj 0
----------------Time and memory stats--------------------
LLVMIRTime 0.006
SVFIRTime 0
SymbolTableTime 0
#######################################################
*********PTACallGraph Stats (Andersen analysis)***************
################ (program : loop_df.bc)###############
----------------Numbers stats----------------------------
CalRetPairInCycle 0
MaxNodeInCycle 0
NodeInCycle 0
TotalCycle 0
TotalEdge 3
TotalNode 4
#######################################################
*********Andersen Pointer Analysis Stats***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
AvgIn/OutAddrEdge 0.4
AvgIn/OutCopyEdge 0.2
AvgIn/OutEdge 0.75
AvgIn/OutLoadEdge 0.1
AvgIn/OutStoreEdge 0.05
AvgPtsSetSize 0.183333
AvgTopLvlPtsSize 0.909091
CollapseTime 0
CopyGepTime 0
LoadStoreTime 0
MemoryUsageVmrss 0
MemoryUsageVmsize 0
SCCDetectTime 0
SCCMergeTime 0
TotalTime 0
UpdateCGTime 0
----------------Numbers stats----------------------------
AddrProcessed 8
CopyProcessed 3
DummyFieldPtrs 0
FieldObjs 0
GepProcessed 0
IndCallSites 0
IndEdgeSolved 0
LoadProcessed 2
LocalVarInRecur 0
MaxInAddrEdge 1
MaxInCopyEdge 1
MaxInLoadEdge 1
MaxInStoreEdge 1
MaxNodesInSCC 0
MaxOutAddrEdge 1
MaxOutCopyEdge 2
MaxOutLoadEdge 2
MaxOutStoreEdge 1
MaxPtsSetSize 1
MemObjects 10
NodesInCycles 0
NullPointer 0
NumOfAddrs 8
NumOfCGEdge 7
NumOfCGNode 24
NumOfCopys 4
NumOfFieldExpand 0
NumOfGeps 0
NumOfLoads 2
NumOfSCCDetect 2
NumOfSFRs 0
NumOfStores 1
NumOfValidNode 20
NumOfValidObjNode 8
Pointers 44
PointsToBlkPtr 0
PointsToConstPtr 0
SolveIterations 2
StoreProcessed 1
TotalCycleNum 0
TotalObjects 10
TotalPWCCycleNum 0
TotalPointers 44
#######################################################
****Persistent Points-To Cache Statistics: Andersen's analysis bitvector****
################ (program : loop_df.bc)###############
UniquePointsToSets 9
TotalUnions 11
PropertyUnions 11
UniqueUnions 0
LookupUnions 0
PreemptiveUnions 0
TotalComplements 48
PropertyComplements 48
UniqueComplements 0
LookupComplements 0
PreemptiveComplements 0
TotalIntersections 3
PropertyIntersections 3
UniqueIntersections 0
LookupIntersections 0
PreemptiveIntersections 0
#######################################################
*********Memory SSA Statistics***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
AverageRegSize 1
GenMUCHITime 0
GenRegionTime 0
InsertPHITime 0
SSARenameTime 0
TotalMSSATime 0
----------------Numbers stats----------------------------
BBHasMSSAPhi 0
CSChiNode 1
CSHasChi 1
CSHasMu 1
CSMuNode 1
FunEntryChi 2
FunHasEntryChi 1
FunHasRetMu 1
FunRetMu 2
LoadHasMu 2
LoadMuNode 2
MSSAPhi 0
MaxRegSize 1
MemRegions 2
StoreChiNode 1
StoreHasChi 1
#######################################################
*********SVFG Statistics***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
ATNodeTime 0
AvgWeight 1
ConnDirEdgeTime 0
ConnIndEdgeTime 0
OptTime 0
TLNodeTime 0
TotalTime 0
----------------Numbers stats----------------------------
ActualIn 1
ActualOut 1
ActualParam 4
ActualRet 0
Addr 8
AvgInDegree 0
AvgIndInDeg 1
AvgIndOutDeg 1
AvgOutDegree 0
Copy 1
DirectCallEdge 0
DirectEdge 6
DirectRetEdge 0
FormalIn 2
FormalOut 2
FormalParam 0
FormalRet 0
Gep 0
IndCallEdge 0
IndRetEdge 0
IndirectEdge 5
IndirectEdgeLabels 5
Load 2
MSSAPhi 0
MaxInDegree 1
MaxIndInDeg 1
MaxIndOutDeg 3
MaxOutDegree 3
PHI 0
Store 1
TotalEdge 11
TotalNode 23
#######################################################
*********SVFG Statistics***************
################ (program : loop_df.bc)###############
----------------Time and memory stats--------------------
ATNodeTime 0
AvgWeight 1
ConnDirEdgeTime 0
ConnIndEdgeTime 0
OptTime 0
TLNodeTime 0
TotalTime 0
----------------Numbers stats----------------------------
ActualIn 1
ActualOut 1
ActualParam 4
ActualRet 0
Addr 8
AvgInDegree 0
AvgIndInDeg 1
AvgIndOutDeg 1
AvgOutDegree 0
Copy 1
DirectCallEdge 0
DirectEdge 6
DirectRetEdge 0
FormalIn 2
FormalOut 2
FormalParam 0
FormalRet 0
Gep 0
IndCallEdge 0
IndRetEdge 0
IndirectEdge 5
IndirectEdgeLabels 5
Load 2
MSSAPhi 0
MaxInDegree 1
MaxIndInDeg 1
MaxIndOutDeg 3
MaxOutDegree 3
PHI 0
Store 1
TotalEdge 11
TotalNode 23
#######################################################
I have two questions:
- For the first check, why would the false positive happen? How does SVF handle the loop? Use loop unrolling or other things?
- Why can adding one more flag hide the false positive?
How can I debug this kind of problem? Thanks.
