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

Improve performance. Add brunch stats. #41

Closed kuhar closed 5 years ago

kuhar commented 5 years ago

@agurfinkel I committed performance and correctness fixes and left the stats and timers on this branch.

kuhar commented 5 years ago

No sure why it didn't pick up my updated commit message, though... I know -- because I pushed the wrong commit

kuhar commented 5 years ago

@agurfinkel

I dont see how this takes care of goobals that are passed but not through arguments. They would be the bigger issue

The current version is also unsound... I'm working on a better way to handle that.

But I don't see how this optimisation would apply to global not passed by arguments. Thinking about it, it should be possible to do something very similar for return values during bottom-up.

kuhar commented 5 years ago

OK, I think that transitive allocation site pruning can be done in the Cloner if we can build a call-site-specific local memory graph for the cloned actuals. I don't know if this can be easily done now with a simple local reasoning (e.g., BasicAA). @agurfinkel what's your idea for that?