Saw-core evalGlobal performance problem

[brianhuffman]

Profiling shows that in the saw-core backends, the function evalGlobal'.global in module Verifier.SAW.Simulator is called way too many times. Each call requires a lookup in a map keyed by the Ident of the global. It should only be called at most once per global constant; the unique term ids should cache the result of each lookup after that. However, profiling shows that we are doing millions of map lookups, and the cost adds up.

[brianhuffman]

I think the problem is caused by the fact that definition bodies of constants defined in the saw-core prelude are not constructed as shared terms; they use the Unshared constructor instead. We could improve the performance either by doing hash consing and term sharing while importing the saw-core prelude, or by doing a name resolution pass over the ASTs.

[brianhuffman]

I believe that this problem no longer occurs; as of GaloisInc/saw-core#118 we are now producing shared terms from definitions in the saw-core prelude, which are now represented as Constant terms.