This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] added cache for SMT queries in the SMTConstraintManager
ClosedPublic

Authored by mikhail.ramalho on Aug 15 2018, 5:45 AM.

Details

Summary

This patch implements a new cache for the result of SMT queries; with this patch the regression tests are 25% faster.

It's implemented as a llvm::DenseMap where the key is the hash of the set of the constraints in a state.

There is still one method that does not use the cache, getSymVal, because it needs to get a symbol interpretation from the SMT, which is not cached yet.

Diff Detail

Event Timeline

Add comment to the cache member

This revision is now accepted and ready to land.Aug 21 2018, 10:49 AM
This revision was automatically updated to reflect the committed changes.