SVF icon indicating copy to clipboard operation
SVF copied to clipboard

Published 20 hours ago • verified publisher icon SVF-tools

Incorrect nander or ander

Open mbarbar opened this issue 4 years ago • 12 comments

For some programs (e.g. attached join.bc, uploaded with .txt extension so GitHub doesn't complain) there are points-to relations in nander not in ander.

To reproduce:

$ ./bin/wpa -nander -print-pts join.bc | grep 'NodeID' > n
$ ./bin/wpa -ander -print-pts join.bc | grep 'NodeID' > a
$ diff n a

Output is:

1568,1569c1568,1569
< NodeID 4495 		PointsTo: { 1 5729 15729 }
< NodeID 4504 		PointsTo: { 1 5729 15729 }
---
> NodeID 4495 		PointsTo: { 1 5729 }
> NodeID 4504 		PointsTo: { 1 5729 }
1572,1573c1572,1573
< NodeID 4516 		PointsTo: { 1 5729 15729 }
< NodeID 4517 		PointsTo: { 1 15729 }
---
> NodeID 4516 		PointsTo: { 1 5729 }
> NodeID 4517 		PointsTo: { 1 5729 }
1575c1575
< NodeID 4524 		PointsTo: { 1 5729 15729 }
---
> NodeID 4524 		PointsTo: { 1 5729 }
1585c1585
< NodeID 4628 		PointsTo: { 1 5729 15729 }
---
> NodeID 4628 		PointsTo: { 1 5729 }
1684,1686c1684,1686
< NodeID 5635 		PointsTo: { 1 5729 15729 }
< NodeID 5642 		PointsTo: { 1 5729 15729 }
< NodeID 5651 		PointsTo: { 1 5729 15729 }
---
> NodeID 5635 		PointsTo: { 1 5729 }
> NodeID 5642 		PointsTo: { 1 5729 }
> NodeID 5651 		PointsTo: { 1 5729 }
1689,1690c1689,1690
< NodeID 5663 		PointsTo: { 1 5729 15729 }
< NodeID 5664 		PointsTo: { 1 15729 }
---
> NodeID 5663 		PointsTo: { 1 5729 }
> NodeID 5664 		PointsTo: { 1 5729 }
2760c2760
< NodeID 8641 		PointsTo: { 1 8757 18757 }
---
> NodeID 8641 		PointsTo: { 1 8757 }
2762c2762
< NodeID 8648 		PointsTo: { 1 8757 18757 }
---
> NodeID 8648 		PointsTo: { 1 8757 }
2765,2766c2765,2766
< NodeID 8667 		PointsTo: { 1 8757 18757 }
< NodeID 8668 		PointsTo: { 1 18757 }
---
> NodeID 8667 		PointsTo: { 1 8757 }
> NodeID 8668 		PointsTo: { 1 8757 }

So some nander points-to sets are supersets of those in ander.

mbarbar avatar May 10 '20 14:05 mbarbar

It seems that the results are the same since the 5729 represents the base object and 15729 represents the first field of the base object.

yuleisui avatar May 11 '20 07:05 yuleisui

@kisslune can you look into this issue?

yuleisui avatar May 11 '20 07:05 yuleisui

Good point. expand.bc, also from Coreutils, is a better example which has the same issue (3542 vs. 13642) but also another issue where ander is missing 1 from some points-to sets (run with -fieldlimit=0 to only see the latter).

$ diff n a
471c471
< NodeID 1547 		PointsTo: { 1 }
---
> NodeID 1547 		PointsTo: {empty}
479c479
< NodeID 1568 		PointsTo: { 1 }
---
> NodeID 1568 		PointsTo: {empty}
483c483
< NodeID 1577 		PointsTo: { 1 }
---
> NodeID 1577 		PointsTo: {empty}
490c490
< NodeID 1596 		PointsTo: { 1 }
---
> NodeID 1596 		PointsTo: {empty}
495,496c495,496
< NodeID 1608 		PointsTo: { 1 }
< NodeID 1612 		PointsTo: { 1 }
---
> NodeID 1608 		PointsTo: {empty}
> NodeID 1612 		PointsTo: {empty}
499c499
< NodeID 1621 		PointsTo: { 1 }
---
> NodeID 1621 		PointsTo: {empty}
504c504
< NodeID 1632 		PointsTo: { 1 }
---
> NodeID 1632 		PointsTo: {empty}
509c509
< NodeID 1645 		PointsTo: { 1 }
---
> NodeID 1645 		PointsTo: {empty}
691c691
< NodeID 2227 		PointsTo: { 1 557 }
---
> NodeID 2227 		PointsTo: { 557 }
738,739c738,739
< NodeID 2402 		PointsTo: { 1 3642 13642 }
< NodeID 2411 		PointsTo: { 1 3642 13642 }
---
> NodeID 2402 		PointsTo: { 1 3642 }
> NodeID 2411 		PointsTo: { 1 3642 }
742,743c742,743
< NodeID 2423 		PointsTo: { 1 3642 13642 }
< NodeID 2424 		PointsTo: { 1 13642 }
---
> NodeID 2423 		PointsTo: { 1 3642 }
> NodeID 2424 		PointsTo: { 1 3642 }
745c745
< NodeID 2431 		PointsTo: { 1 3642 13642 }
---
> NodeID 2431 		PointsTo: { 1 3642 }
750,755c750,755
< NodeID 2480 		PointsTo: { 1 557 }
< NodeID 2482 		PointsTo: { 1 557 }
< NodeID 2523 		PointsTo: { 1 557 }
< NodeID 2532 		PointsTo: { 1 557 }
< NodeID 2534 		PointsTo: { 1 557 }
< NodeID 2535 		PointsTo: { 1 3642 13642 }
---
> NodeID 2480 		PointsTo: { 557 }
> NodeID 2482 		PointsTo: { 557 }
> NodeID 2523 		PointsTo: { 557 }
> NodeID 2532 		PointsTo: { 557 }
> NodeID 2534 		PointsTo: { 557 }
> NodeID 2535 		PointsTo: { 1 3642 }
757,758c757,758
< NodeID 2548 		PointsTo: { 1 557 }
< NodeID 2550 		PointsTo: { 1 557 }
---
> NodeID 2548 		PointsTo: { 557 }
> NodeID 2550 		PointsTo: { 557 }
767,770c767,770
< NodeID 2640 		PointsTo: { 1 557 }
< NodeID 2643 		PointsTo: { 1 557 }
< NodeID 2648 		PointsTo: { 1 557 }
< NodeID 2651 		PointsTo: { 1 557 }
---
> NodeID 2640 		PointsTo: { 557 }
> NodeID 2643 		PointsTo: { 557 }
> NodeID 2648 		PointsTo: { 557 }
> NodeID 2651 		PointsTo: { 557 }
775,780c775,780
< NodeID 2714 		PointsTo: { 1 557 }
< NodeID 2717 		PointsTo: { 1 557 }
< NodeID 2723 		PointsTo: { 1 557 }
< NodeID 2726 		PointsTo: { 1 557 }
< NodeID 2734 		PointsTo: { 1 557 }
< NodeID 2737 		PointsTo: { 1 557 }
---
> NodeID 2714 		PointsTo: { 557 }
> NodeID 2717 		PointsTo: { 557 }
> NodeID 2723 		PointsTo: { 557 }
> NodeID 2726 		PointsTo: { 557 }
> NodeID 2734 		PointsTo: { 557 }
> NodeID 2737 		PointsTo: { 557 }
789,790c789,790
< NodeID 2868 		PointsTo: { 1 557 }
< NodeID 2869 		PointsTo: { 1 557 }
---
> NodeID 2868 		PointsTo: { 557 }
> NodeID 2869 		PointsTo: { 557 }
802,804c802,804
< NodeID 2991 		PointsTo: { 1 557 }
< NodeID 2998 		PointsTo: { 1 557 }
< NodeID 3002 		PointsTo: { 1 557 }
---
> NodeID 2991 		PointsTo: { 557 }
> NodeID 2998 		PointsTo: { 557 }
> NodeID 3002 		PointsTo: { 557 }
806,809c806,809
< NodeID 3033 		PointsTo: { 1 557 }
< NodeID 3037 		PointsTo: { 1 557 }
< NodeID 3062 		PointsTo: { 1 557 }
< NodeID 3068 		PointsTo: { 1 557 }
---
> NodeID 3033 		PointsTo: { 557 }
> NodeID 3037 		PointsTo: { 557 }
> NodeID 3062 		PointsTo: { 557 }
> NodeID 3068 		PointsTo: { 557 }
832,833c832,833
< NodeID 3325 		PointsTo: { 1 557 }
< NodeID 3329 		PointsTo: { 1 557 }
---
> NodeID 3325 		PointsTo: { 557 }
> NodeID 3329 		PointsTo: { 557 }
852c852
< NodeID 3527 		PointsTo: { 1 557 }
---
> NodeID 3527 		PointsTo: { 557 }
856,858c856,858
< NodeID 3548 		PointsTo: { 1 3642 13642 }
< NodeID 3555 		PointsTo: { 1 3642 13642 }
< NodeID 3564 		PointsTo: { 1 3642 13642 }
---
> NodeID 3548 		PointsTo: { 1 3642 }
> NodeID 3555 		PointsTo: { 1 3642 }
> NodeID 3564 		PointsTo: { 1 3642 }
861,862c861,862
< NodeID 3576 		PointsTo: { 1 3642 13642 }
< NodeID 3577 		PointsTo: { 1 13642 }
---
> NodeID 3576 		PointsTo: { 1 3642 }
> NodeID 3577 		PointsTo: { 1 3642 }
866c866
< NodeID 3604 		PointsTo: { 1 557 }
---
> NodeID 3604 		PointsTo: { 557 }
995c995
< NodeID 3931 		PointsTo: { 1 557 }
---
> NodeID 3931 		PointsTo: { 557 }
1034c1034
< NodeID 4066 		PointsTo: { 1 557 }
---
> NodeID 4066 		PointsTo: { 557 }
1057c1057
< NodeID 4114 		PointsTo: { 1 557 }
---
> NodeID 4114 		PointsTo: { 557 }
1156c1156
< NodeID 4386 		PointsTo: { 1 }
---
> NodeID 4386 		PointsTo: {empty}
1164c1164
< NodeID 4411 		PointsTo: { 1 }
---
> NodeID 4411 		PointsTo: {empty}
1701c1701
< NodeID 5662 		PointsTo: { 1 557 }
---
> NodeID 5662 		PointsTo: { 557 }
1713c1713
< NodeID 5697 		PointsTo: { 1 557 }
---
> NodeID 5697 		PointsTo: { 557 }
1717c1717
< NodeID 5715 		PointsTo: { 1 557 }
---
> NodeID 5715 		PointsTo: { 557 }
1730c1730
< NodeID 5763 		PointsTo: { 1 5915 15915 }
---
> NodeID 5763 		PointsTo: { 1 5915 }
1732c1732
< NodeID 5770 		PointsTo: { 1 5915 15915 }
---
> NodeID 5770 		PointsTo: { 1 5915 }
1735,1736c1735,1736
< NodeID 5789 		PointsTo: { 1 5915 15915 }
< NodeID 5790 		PointsTo: { 1 15915 }
---
> NodeID 5789 		PointsTo: { 1 5915 }
> NodeID 5790 		PointsTo: { 1 5915 }

mbarbar avatar May 11 '20 08:05 mbarbar

Hello @mbarbar . The first problem is because -ander collapses PWCs while -nander does not do any cycle detection and elimination. The point-to sets of -ander differs from -nander with fewer field nodes because of the collapse of cycle. While the second problem is because of the incorrectness of the function addCopyEdge(). This is fixed in the last pull request.

kisslune avatar May 20 '20 04:05 kisslune

Fantastic, working for me for join.bc now. Thanks!

mbarbar avatar May 22 '20 14:05 mbarbar

Reopening regarding the issue of first fields being equivalent to the base object.

In this test case, the NOALIAS tests imply that the first field is not equivalent to the base object. If we are treating o and o.f_0 interchangeably, then the NOALIAS test should fail.

I think this needs to be considered, and a decision made as to whether first-field is equivalent to base, because the implications are not limited to the final points-to result, but also analyses which rely on these results. From a small ll,

ander

NodeID 36 		PointsTo: { 31 }
NodeID 37 		PointsTo: { 31 }

nander

NodeID 36 		PointsTo: { 31 1031 }
NodeID 37 		PointsTo: { 1031 }

fspta

NodeID 36 		PointsTo: { 31 1031 }
NodeID 37 		PointsTo: { 1031 }

Now, fspta is a subset of nander, but not ander, so there are relations that exist in the FS results that come about from something not encoded in the SVFG (because it was constructed using ander data).

You can see this commit for my personal suggestion that f_0 shouldn't exist: only o and o.f_n where n > 0

mbarbar avatar Jul 12 '20 16:07 mbarbar

Will this commit fix the issue? https://github.com/SVF-tools/SVF/commit/d6c8315395b048d7a8bca189dff55b66c1955714#diff-b28854c0c9113d7d62e1573a01d616d5

I remember that if we use lower bits to represent "base" and higher bits to represent "offset". The problem will be solved?

yuleisui avatar Jul 13 '20 01:07 yuleisui

Removing the + 1 would fix it I suspect, but introduce another issue. The other issue (which is why the change was made in the first place, if my memory is not failing me) is that the FIObjPN would become a GepObjPN.

mbarbar avatar Jul 13 '20 02:07 mbarbar

Also, whether the test I linked should pass or not needs to be considered regardless of what we do next.

mbarbar avatar Jul 13 '20 02:07 mbarbar

How about if we swap the higher and lower bits for representing fields and offsets? Would that work?

yuleisui avatar Jul 13 '20 02:07 yuleisui

If we keep the + 1, I think we would still have ander and nander producing different results. If we get rid of the + 1, the changing of the object's type I think still occurs. The only issue is with the 0 offset and whether it is equivalent to the base object, the rest are fine.

Edit: another solution would be to make o and o.f_0 distinct such that the following are different points-to sets : { o }, { o, o.f_0 }, { o.f_0 }. Under this solution though, I think making ander and nander results equivalent would be a bit more work.

mbarbar avatar Jul 13 '20 03:07 mbarbar

LOL, exactly. I have also met such kind of problem before.

Mohamad Barbar [email protected] 于2020年5月11日周一 下午4:01写道：

Good point. expand.bc https://github.com/SVF-tools/SVF/files/4608257/expand.txt, also from Coreutils, is a better example which has the same issue (3542 vs. 13642) but also another issue where ander is missing 1 from some points-to sets (run with -fieldlimit=0 to only see the latter).

$ diff n a 471c471 < NodeID 1547 PointsTo: { 1 }

NodeID 1547 PointsTo: {empty} 479c479 < NodeID 1568 PointsTo: { 1 }

NodeID 1568 PointsTo: {empty} 483c483 < NodeID 1577 PointsTo: { 1 }

NodeID 1577 PointsTo: {empty} 490c490 < NodeID 1596 PointsTo: { 1 }

NodeID 1596 PointsTo: {empty} 495,496c495,496 < NodeID 1608 PointsTo: { 1 } < NodeID 1612 PointsTo: { 1 }

NodeID 1608 PointsTo: {empty} NodeID 1612 PointsTo: {empty} 499c499 < NodeID 1621 PointsTo: { 1 }

NodeID 1621 PointsTo: {empty} 504c504 < NodeID 1632 PointsTo: { 1 }

NodeID 1632 PointsTo: {empty} 509c509 < NodeID 1645 PointsTo: { 1 }

NodeID 1645 PointsTo: {empty} 691c691 < NodeID 2227 PointsTo: { 1 557 }

NodeID 2227 PointsTo: { 557 } 738,739c738,739 < NodeID 2402 PointsTo: { 1 3642 13642 } < NodeID 2411 PointsTo: { 1 3642 13642 }

NodeID 2402 PointsTo: { 1 3642 } NodeID 2411 PointsTo: { 1 3642 } 742,743c742,743 < NodeID 2423 PointsTo: { 1 3642 13642 } < NodeID 2424 PointsTo: { 1 13642 }

NodeID 2423 PointsTo: { 1 3642 } NodeID 2424 PointsTo: { 1 3642 } 745c745 < NodeID 2431 PointsTo: { 1 3642 13642 }

NodeID 2431 PointsTo: { 1 3642 } 750,755c750,755 < NodeID 2480 PointsTo: { 1 557 } < NodeID 2482 PointsTo: { 1 557 } < NodeID 2523 PointsTo: { 1 557 } < NodeID 2532 PointsTo: { 1 557 } < NodeID 2534 PointsTo: { 1 557 } < NodeID 2535 PointsTo: { 1 3642 13642 }

NodeID 2480 PointsTo: { 557 } NodeID 2482 PointsTo: { 557 } NodeID 2523 PointsTo: { 557 } NodeID 2532 PointsTo: { 557 } NodeID 2534 PointsTo: { 557 } NodeID 2535 PointsTo: { 1 3642 } 757,758c757,758 < NodeID 2548 PointsTo: { 1 557 } < NodeID 2550 PointsTo: { 1 557 }

NodeID 2548 PointsTo: { 557 } NodeID 2550 PointsTo: { 557 } 767,770c767,770 < NodeID 2640 PointsTo: { 1 557 } < NodeID 2643 PointsTo: { 1 557 } < NodeID 2648 PointsTo: { 1 557 } < NodeID 2651 PointsTo: { 1 557 }

NodeID 2640 PointsTo: { 557 } NodeID 2643 PointsTo: { 557 } NodeID 2648 PointsTo: { 557 } NodeID 2651 PointsTo: { 557 } 775,780c775,780 < NodeID 2714 PointsTo: { 1 557 } < NodeID 2717 PointsTo: { 1 557 } < NodeID 2723 PointsTo: { 1 557 } < NodeID 2726 PointsTo: { 1 557 } < NodeID 2734 PointsTo: { 1 557 } < NodeID 2737 PointsTo: { 1 557 }

NodeID 2714 PointsTo: { 557 } NodeID 2717 PointsTo: { 557 } NodeID 2723 PointsTo: { 557 } NodeID 2726 PointsTo: { 557 } NodeID 2734 PointsTo: { 557 } NodeID 2737 PointsTo: { 557 } 789,790c789,790 < NodeID 2868 PointsTo: { 1 557 } < NodeID 2869 PointsTo: { 1 557 }

NodeID 2868 PointsTo: { 557 } NodeID 2869 PointsTo: { 557 } 802,804c802,804 < NodeID 2991 PointsTo: { 1 557 } < NodeID 2998 PointsTo: { 1 557 } < NodeID 3002 PointsTo: { 1 557 }

NodeID 2991 PointsTo: { 557 } NodeID 2998 PointsTo: { 557 } NodeID 3002 PointsTo: { 557 } 806,809c806,809 < NodeID 3033 PointsTo: { 1 557 } < NodeID 3037 PointsTo: { 1 557 } < NodeID 3062 PointsTo: { 1 557 } < NodeID 3068 PointsTo: { 1 557 }

NodeID 3033 PointsTo: { 557 } NodeID 3037 PointsTo: { 557 } NodeID 3062 PointsTo: { 557 } NodeID 3068 PointsTo: { 557 } 832,833c832,833 < NodeID 3325 PointsTo: { 1 557 } < NodeID 3329 PointsTo: { 1 557 }

NodeID 3325 PointsTo: { 557 } NodeID 3329 PointsTo: { 557 } 852c852 < NodeID 3527 PointsTo: { 1 557 }

NodeID 3527 PointsTo: { 557 } 856,858c856,858 < NodeID 3548 PointsTo: { 1 3642 13642 } < NodeID 3555 PointsTo: { 1 3642 13642 } < NodeID 3564 PointsTo: { 1 3642 13642 }

NodeID 3548 PointsTo: { 1 3642 } NodeID 3555 PointsTo: { 1 3642 } NodeID 3564 PointsTo: { 1 3642 } 861,862c861,862 < NodeID 3576 PointsTo: { 1 3642 13642 } < NodeID 3577 PointsTo: { 1 13642 }

NodeID 3576 PointsTo: { 1 3642 } NodeID 3577 PointsTo: { 1 3642 } 866c866 < NodeID 3604 PointsTo: { 1 557 }

NodeID 3604 PointsTo: { 557 } 995c995 < NodeID 3931 PointsTo: { 1 557 }

NodeID 3931 PointsTo: { 557 } 1034c1034 < NodeID 4066 PointsTo: { 1 557 }

NodeID 4066 PointsTo: { 557 } 1057c1057 < NodeID 4114 PointsTo: { 1 557 }

NodeID 4114 PointsTo: { 557 } 1156c1156 < NodeID 4386 PointsTo: { 1 }

NodeID 4386 PointsTo: {empty} 1164c1164 < NodeID 4411 PointsTo: { 1 }

NodeID 4411 PointsTo: {empty} 1701c1701 < NodeID 5662 PointsTo: { 1 557 }

NodeID 5662 PointsTo: { 557 } 1713c1713 < NodeID 5697 PointsTo: { 1 557 }

NodeID 5697 PointsTo: { 557 } 1717c1717 < NodeID 5715 PointsTo: { 1 557 }

NodeID 5715 PointsTo: { 557 } 1730c1730 < NodeID 5763 PointsTo: { 1 5915 15915 }

NodeID 5763 PointsTo: { 1 5915 } 1732c1732 < NodeID 5770 PointsTo: { 1 5915 15915 }

NodeID 5770 PointsTo: { 1 5915 } 1735,1736c1735,1736 < NodeID 5789 PointsTo: { 1 5915 15915 } < NodeID 5790 PointsTo: { 1 15915 }

NodeID 5789 PointsTo: { 1 5915 } NodeID 5790 PointsTo: { 1 5915 }

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/SVF-tools/SVF/issues/207#issuecomment-626540390, or unsubscribe https://github.com/notifications/unsubscribe-auth/AG2JXDUPWNQXV2PJN5G56YDRQ6WHNANCNFSM4M5IXPYQ .

kisslune avatar Jul 13 '20 07:07 kisslune