Next goals of lockbud

[BurtonQin]

• Migrate to rustc_smir for API stability between different versions of rust compilers.
• Support updated versions of Rust compilers.
• More complete documents on how lockbud works and how to develop it.
• Improve bug reports.
• More test cases.
• Improve accuracy of detectors and reduce false positives.
• Support more bug patterns.
• Accommodate detection algorithms from other Rust static checkers.
• Develop a vscode plugin to help visualize bugs.

[chenyan2002]

Interesting project! I was wondering have you tried to use the Rust analyzer for static analysis. Their libraries are all on crates-io, e.g., https://docs.rs/ra_ap_hir/latest/ra_ap_hir/, so no nightly rustc is required. The only problem I see is that the start up time can be long, because their state cannot be serialized unless we build the analyzer as a server similar to LSP.

[BurtonQin]

A precise points-to analysis lib is the key to the success of a static checker like lockbud. The current points-to analysis implementation of lockbud is mostly intraproc and mainly uses type and fn sig info for interproc handling. This imprecise and unsound design is limited by the Rust compiler's immature support for the rust analysis at the time of launching lockbud project. With the development of StableMIR and other efforts to improve the ability of MIR analysis, many brilliant tools emerged. kani and RAP are two great examples. They both implement their own points-to analysis.

https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs#L49-L49

kani: interprocedural, field-insensitive, MIR and StableMIR, intrinsics covered, sound, easy to understand.

https://github.com/Artisan-Lab/RAP/blob/main/rap/src/analysis/core/alias/mop.rs

RAP: interprocedural, field-sensitive, MIR, intrinsics not covered, a little convoluted.

I am learning from kani, StableMIR and RAP. I plan to start re-designing the current points-to analysis of lockbud before Sep. 15.

[BurtonQin]

Interesting project! I was wondering have you tried to use the Rust analyzer for static analysis. Their libraries are all on crates-io, e.g., https://docs.rs/ra_ap_hir/latest/ra_ap_hir/, so no nightly rustc is required. The only problem I see is that the start up time can be long, because their state cannot be serialized unless we build the analyzer as a server similar to LSP.

ra_ap_hir is one of the rust-analyzer's crates. To my knowledge, rust-analyzer only works on HIR and only rust compiler can generate MIR. Unfortunately, lockbud only works on MIR for now. I know Stable MIR is on the way. if it becomes mature, lockbud can work on stable rustc.

[BurtonQin]

A precise points-to analysis lib is the key to the success of a static checker like lockbud. The current points-to analysis implementation of lockbud is mostly intraproc and mainly uses type and fn sig info for interproc handling. This imprecise and unsound design is limited by the Rust compiler's immature support for the rust analysis at the time of launching lockbud project. With the development of StableMIR and other efforts to improve the ability of MIR analysis, many brilliant tools emerged. kani and RAP are two great examples. They both implement their own points-to analysis.

https://github.com/model-checking/kani/blob/main/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs#L49-L49

kani: interprocedural, field-insensitive, MIR and StableMIR, intrinsics covered, sound, easy to understand.

https://github.com/Artisan-Lab/RAP/blob/main/rap/src/analysis/core/alias/mop.rs

RAP: interprocedural, field-sensitive, MIR, intrinsics not covered, a little convoluted.

I am learning from kani, StableMIR and RAP. I plan to start re-designing the current points-to analysis of lockbud before Sep. 15.

I found a context-sensitive points-to analysis framework for Rust called RUPTA. Trying to replace the current pts of lockbud with RUPTA.
https://github.com/rustanlys/rupta

[BurtonQin]

https://arxiv.org/pdf/2401.01114
This paper nicely explains the design principle of the deadlock detector of lockbud.