search

SVF-tools / SVF

Static Value-Flow Analysis Framework for Source Code
http://svf-tools.github.io/SVF/
Other
1.43k stars 436 forks source link

Unknown reason for a simple false positive and inconsistent flag behavior #1584

Open grandnew opened 2 weeks ago

grandnew commented 2 weeks ago

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:

  1. For the first check, why would the false positive happen? How does SVF handle the loop? Use loop unrolling or other things?
  2. Why can adding one more flag hide the false positive?

How can I debug this kind of problem? Thanks.