point to set is empty

[yuffon]

Hi, I am using SVF 2.7 to do point to analysis on the following code.

#include <malloc.h>

struct info{
    int* value;
};

void mycheck1(void *buf){}
void mycheck2(void *buf){}
void mycheck3(void *buf){}

int main(){
    int *pool = malloc(128);   //don't use void *, otherwise we won't see the empty pt set
    struct info *ptr = (struct info *)pool; // a type case here
    ptr->value = malloc(4); //a malloc

    mycheck1(pool);
    mycheck2(ptr);
    mycheck3(ptr->value);  // the point to set of ptr->value is empty
    return 1;
}

I insert mycheck functions to help me to retrive point-to analysis results. The results are:

mycheck1: argument point to set:41 
mycheck2: argument point to set:73 
mycheck3: argument point to set:

How to fix this?

Thanks.

[yuleisui]

@jumormt could you take a look at this case in our latest SVF

[yuleisui]

I just run "wpa -ander -print-pts". It shows the points-to set of NodeID 53 (the argument buf of mycheck3) is not empty.

#include <stdlib.h>

extern void MAYALIAS(void*, void*); struct info{ int* value; };

void mycheck1(void *buf){} void mycheck2(void *buf){} void mycheck3(void *buf){ MAYALIAS(buf,buf); }

int main(){ int *pool = malloc(128); //don't use void *, otherwise we won't see the empty pt set struct info *ptr = (struct info *)pool; // a type case here ptr->value = malloc(4); //a malloc

mycheck1(pool);
mycheck2(ptr);
mycheck3(ptr->value);  // the point to set of ptr->value is empty
return 1;

}

---

NodeID 0 PointsTo: {empty}

NodeID 4 PointsTo: { 3 }

NodeID 6 PointsTo: { 3 }

NodeID 8 PointsTo: { 3 }

NodeID 9 PointsTo: { 12 }

NodeID 10 PointsTo: { 13 }

NodeID 14 PointsTo: {empty}

NodeID 16 PointsTo: { 17 }

NodeID 21 PointsTo: { 22 }

NodeID 24 PointsTo: { 75 }

NodeID 25 PointsTo: { 26 }

NodeID 30 PointsTo: { 31 }

NodeID 36 PointsTo: { 37 }

NodeID 39 PointsTo: { 75 }

NodeID 40 PointsTo: { 41 }

NodeID 45 PointsTo: { 46 }

NodeID 48 PointsTo: { 84 }

NodeID 49 PointsTo: { 50 }

NodeID 53 PointsTo: { 84 }

NodeID 54 PointsTo: { 84 }

NodeID 56 PointsTo: { 57 }

NodeID 62 PointsTo: { 63 }

NodeID 65 PointsTo: { 66 }

NodeID 67 PointsTo: { 68 }

NodeID 69 PointsTo: { 70 }

NodeID 74 PointsTo: { 75 }

NodeID 77 PointsTo: { 78 }

NodeID 81 PointsTo: { 75 }

NodeID 83 PointsTo: { 84 }

NodeID 86 PointsTo: { 75 }

NodeID 87 PointsTo: { 110 }

NodeID 89 PointsTo: { 75 }

NodeID 91 PointsTo: { 75 }

NodeID 93 PointsTo: { 75 }

NodeID 94 PointsTo: { 110 }

NodeID 95 PointsTo: { 84 }

NodeID 100 PointsTo: { 105 }

NodeID 101 PointsTo: { 106 }

NodeID 102 PointsTo: { 107 }

NodeID 103 PointsTo: { 108 }

NodeID 104 PointsTo: { 109 }

[yuffon]

On my computer, with SVF 2.7:

If using int *pool = malloc(128);, the result of wpa -fspta -print-pts ./pool-int-mem2reg.ll is

NodeID 0                PointsTo: {empty}


NodeID 4                PointsTo: { 3 }


NodeID 7                PointsTo: { 8 }


NodeID 10               PointsTo: { 44 }


NodeID 11               PointsTo: { 12 }


NodeID 16               PointsTo: { 17 }


NodeID 19               PointsTo: { 44 }


NodeID 20               PointsTo: { 21 }


NodeID 24               PointsTo: { 25 }


NodeID 27               PointsTo: {empty}


NodeID 28               PointsTo: { 29 }


NodeID 32               PointsTo: { 33 }


NodeID 35               PointsTo: { 36 }


NodeID 37               PointsTo: { 38 }


NodeID 39               PointsTo: { 40 }


NodeID 43               PointsTo: { 44 }


NodeID 46               PointsTo: { 47 }


NodeID 48               PointsTo: { 44 }


NodeID 50               PointsTo: { 44 }


NodeID 51               PointsTo: { 44 }


NodeID 53               PointsTo: { 54 }


NodeID 56               PointsTo: { 54 }


NodeID 57               PointsTo: { 44 }


NodeID 58               PointsTo: { 81 }


NodeID 60               PointsTo: { 44 }


NodeID 61               PointsTo: { 44 }


NodeID 63               PointsTo: { 44 }


NodeID 64               PointsTo: { 44 }


NodeID 66               PointsTo: { 44 }


NodeID 67               PointsTo: { 81 }


NodeID 68               PointsTo: {empty}


NodeID 69               PointsTo: {empty}


NodeID 71               PointsTo: { 3 }


NodeID 73               PointsTo: { 74 }

But if using void *pool = malloc(128);, the result is

NodeID 0                PointsTo: {empty}


NodeID 4                PointsTo: { 3 }


NodeID 7                PointsTo: { 8 }


NodeID 10               PointsTo: { 44 }


NodeID 11               PointsTo: { 12 }


NodeID 16               PointsTo: { 17 }


NodeID 19               PointsTo: { 44 }


NodeID 20               PointsTo: { 21 }


NodeID 24               PointsTo: { 25 }


NodeID 27               PointsTo: { 53 }


NodeID 28               PointsTo: { 29 }


NodeID 32               PointsTo: { 33 }


NodeID 35               PointsTo: { 36 }


NodeID 37               PointsTo: { 38 }


NodeID 39               PointsTo: { 40 }


NodeID 43               PointsTo: { 44 }


NodeID 46               PointsTo: { 47 }


NodeID 49               PointsTo: { 44 }


NodeID 50               PointsTo: { 44 }


NodeID 52               PointsTo: { 53 }


NodeID 55               PointsTo: { 53 }


NodeID 56               PointsTo: { 44 }


NodeID 57               PointsTo: { 79 }


NodeID 59               PointsTo: { 44 }


NodeID 61               PointsTo: { 44 }


NodeID 62               PointsTo: { 44 }


NodeID 64               PointsTo: { 44 }


NodeID 65               PointsTo: { 79 }


NodeID 66               PointsTo: { 53 }


NodeID 67               PointsTo: { 53 }


NodeID 69               PointsTo: { 3 }


NodeID 71               PointsTo: { 72 }

Using wpa -ander also give two different results for the two versions of programs.

I will try the latest version of SVF.

[yuffon]

Hi @yuleisui, SVF 2.9 is OK. It seems like a fixed bug somewhere in the old version. Thanks.

[yuleisui]

I didn't see the bc code. it might be because "int pool = malloc(128)" will make SVF treat the underlying object as an int object in 2.7. A standard way is to cast the void to int*, "int pool = (int)malloc(128)", you can have a try to change this statement by adding a cast to see whether 2.7 will work correctly.

2.9 will fix the issue as the type inference will infer the object type rather than looking at the allocation site's typed pointer.