hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
195 stars 20 forks source link

Check performance of `RewriteControlFlow` #1033

Open maximebuyse opened 2 weeks ago

maximebuyse commented 2 weeks ago

The RewriteControlFlow phase visits expressions only if they contain control flow (return, break, continue). But that means visiting twice the expressions when they contain control flow which is bad in terms of complexity in the worst cases. We should check if this has an impact. A solution could be to memoize which subexpressions contain control flow.

maximebuyse commented 1 day ago

I am trying to extract crate protobuf and I have a very large memory use starting at this phase. I counted the number of nodes in the expressions of the AST before and after this phase and it is multiplied by more than 1000 so clearly something is wrong there.