HomePhabricator

[analyzer] added cache for SMT queries in the SMTConstraintManager

Authored by mikhail.ramalho on Aug 23 2018, 6:21 AM.

Description

[analyzer] added cache for SMT queries in the SMTConstraintManager

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.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin, Szelethus

Differential Revision: https://reviews.llvm.org/D50773

llvm-svn: 340535