secure-software-engineering / phasar

A LLVM-based static analysis framework.
Other
919 stars 140 forks source link

Fix InitialSeeds for IFDS #632

Closed fabianbs96 closed 1 year ago

fabianbs96 commented 1 year ago

The default edge value of the InitialSeeds for IFDS analyses is TOP (the bottom value of the binary lattice) indicating "no information". This is incorrect as holding IFDS dataflow facts semantically have to be annotated with the top value of the binary lattice, which is called BOTTOM in phasar. This issue prevents the IDESolver from computing IFDS results at certain call sites.

This PR solves that problem by correctly assigning the BOTTOM edge value to the initial seeds of IFDS analyses.

Should fix #629.

Luweicai commented 1 year ago

Hi, @fabianbs96. This patch fix the problem that preventing the IDESolver from computing IFDS results at certain call sites.

But it seems casue a new problem: the new generated fact will have the value of TOP at no called position.

%1 = add nsw i32 %0, 1;
%2 = add nsw i32 %1, 1;
call void @tt(i32 %3);
%5 = add nsw i32 %4, 1;

The result is:


N: %1 = add nsw i32 %0, 1;
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: BOTTOM

N: %2 = add nsw i32 %1, 1;
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: TOP
%1 = add nsw i32 %0, 1; | V: TOP

N: call void @tt(i32 %3);
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: BOTTOM
%1 = add nsw i32 %0, 1; | V: BOTTOM

N: %5 = add nsw i32 %4, 1;
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: TOP
D: %1 = add nsw i32 %0, 1; | V: TOP
D: %2 = add nsw i32 %1, 1; | V: TOP