]> granicus.if.org Git - clang/commit
[analyzer] added cache for SMT queries in the SMTConstraintManager
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 23 Aug 2018 13:21:35 +0000 (13:21 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 23 Aug 2018 13:21:35 +0000 (13:21 +0000)
commite29bf811025bd91d59ab1c920442abdf9afa9b8d
tree7abbf4229d1f89b054c482b93359e7d20d1003bc
parent60783c86231dcc00106c9b25d708921eb6796e37
[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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@340535 91177308-0d34-0410-b5e6-96231b3b80d8
include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h