viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Relaxing Ordering of Dependencies #51

Closed ArquintL closed 2 years ago

ArquintL commented 2 years ago

As reported by @jogasser, a slightly differently ordered AST can result in a cache miss despite containing identical members. The reason is that all dependencies of a member are hashed into a single string that is then used to decide whether a member needs to be reverified or not. Thus, the ordering of dependencies has an influence on cache lookups despite not mattering at all. This PR orders the hashes of dependencies before calculating the overall hash.