Skip to content
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.

Sign up for GitHub

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

Jump to bottom

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

Open
grandnew opened this issue Oct 30, 2024 · 0 comments
Open

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

grandnew opened this issue Oct 30, 2024 · 0 comments

Comments

@grandnew
Copy link

grandnew commented Oct 30, 2024 •
edited
Loading

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@grandnew