Slow pretty-printer and consistency checks

[fpoli]

By profiling for 165 seconds a Carbon run with VisualVM I found that:

• The time spent in the JVM is 53s, which is 32% of the wall-clock time.
• Pretty-printing a boogie.Program takes 11s, which is 20% of the CPU time used by the JVM.
• The consistency checks of a silver.ast.Program take 14s, which is 26% of the CPU time used by the JVM.

Ignoring the first point, which might be due to Carbon's implementation, pretty-printing and consistency checks take a nontrivial fraction of the time and are mostly implemented using Silver functions. There is probably room for improvement there, because it might be e.g. that a lot of the time is spent allocating the many closures used by the functional-style implementation of the pretty-printer.

A screenshot of the profiling, where the second column is the CPU time of the JVM ond the third is the overall execution time:

The measurements are done on just one set of 11 Viper programs, but the profiling shows that pretty-printing and consistency checks can be bottlenecks. Some stats about the concatenation of those Viper programs:

• 636'489 lines of code (including empty lines and comments)
• 2'486 domains, containing in total
  • 26'437 domain functions
  • 39'609 axioms
• 135 top-level functions
• 55 methods
• 0 fields
• 0 predicates