Add this suggestion to a batch that can be applied as a single commit.
  This suggestion is invalid because no changes were made to the code.
  Suggestions cannot be applied while the pull request is closed.
  Suggestions cannot be applied while viewing a subset of changes.
  Only one suggestion per line can be applied in a batch.
  Add this suggestion to a batch that can be applied as a single commit.
  Applying suggestions on deleted lines is not supported.
  You must change the existing code in this line in order to create a valid suggestion.
  Outdated suggestions cannot be applied.
  This suggestion has been applied or marked resolved.
  Suggestions cannot be applied from pending reviews.
  Suggestions cannot be applied on multi-line comments.
  Suggestions cannot be applied while the pull request is queued to merge.
  Suggestion cannot be applied right now. Please check back later.
  
    
  
    
Profiling showed that
codegen_span_stablewas a significant bottleneck for Kani, as it has to do all the queries torustc_publicand logic to construct aLocationfor a givenSpan. However, I tested and found that the function was typically being called multiple (~500) times on the exact sameSpanthroughout an execution.This PR introduces a new cache to store the result of those calculations for future use.
Since the key to this cache is a
rustc_public::Span, it's dependent on the type beingHash, something which will hopefully be implemented in rust-lang/rust#145018. For now, I've tested the change using a hacky transmute to implementHashmyself.Results
Caching span codegen led to a nice 9.4% reduction in the end to end compilation of the standard library (@ commit 177d0fd, assuming #4276 lands).
Like #4276, this is a caching change and will have an associated memory overhead. Based on the max capacity of the map during execution, I estimate its peak size to be ~4.4MB when run on the standard library, which is around 0.13%-0.17% of Kani's total memory usage on the same run. This seems acceptable for the measured performance benefit.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.