search

seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Tea-dsa or sea-dsa? #158

Closed shijy16 closed 1 year ago

shijy16 commented 1 year ago

Hi, thanks for the great work.

I am using this project to analyze function pointers and generate precise call graphs for c/c++ projects. But I am confused on using tea-dsa or sea-dsa.

According to your paper, tea-dsa is much faster and more precise than sea-dsa. But it seems sea-dsa is updated to newer llvm constantly while tea-dsa is not. Dose this mean sea-dsa is a better choice for my purpose?

shijy16 commented 1 year ago

I figured that all changes in tea-dsa had already been merged into the main branch. So does the main branch implement the newest tea-dsa algorithm?

agurfinkel commented 1 year ago

https://github.com/seahorn/sea-dsa is the main branch. Main dev branch is https://github.com/seahorn/sea-dsa/tree/dev14

All performance improvements from tea-dsa have been incorporated into the main branches. The separate tea-dsa branch is only preserved for historical reasons.

The option --sea-dsa-type-aware (https://github.com/seahorn/sea-dsa/blob/8fc33bd29b878c8975e958da594e67ba02bb42f4/lib/seadsa/Graph.cc#L33) turns type awareness of tea-dsa on. It is off by default in sea-dsa, but we almost always turn it on in our clients (i.e., seahorn). It relies on some type strictness that is not always followed even by C code, so sometimes it has to be disabled for soundness.

shijy16 commented 1 year ago

Thank you! This helps a lot. Closing this issue as resolved.