[PATCH] D28953: [analyzer] Eliminate analyzer limitations on symbolic constraint generation

Dominic Chen via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Wed May 10 15:26:29 PDT 2017


ddcc added a comment.

It's been a while since I looked at the code, but I don't believe that all of the new constraints are necessarily unsupported by the current range constraint manager. Rather, they were just not being generated by the SimpleSValBuilder. The changes pass the testsuite for both the Range and Z3 constraint managers, without any special testcase handling that is Z3 specific.

Here are some runtime performance numbers on the testsuite:

Pre-Commit
RangeConstraintManager: 8.24s
Z3ConstraintManager: 247.29s

Post-Commit
RangeConstraintManager: 10.23s
Z3ConstraintManager: 250.35s

And for memory usage (max RSS):

Pre-Commit
edges-new.mm (RangeConstraintManager): 42688k
edges-new.mm (Z3ConstraintManager): 52916k
malloc-plist.c (RangeConstraintManager): 39812k
malloc-plist.c (Z3ConstraintManager): 50544k

Post-Commit
edges-new.mm (RangeConstraintManager): 43032k
edges-new.mm (Z3ConstraintManager): 52956k
malloc-plist.c (RangeConstraintManager): 40204k
malloc-plist.c (Z3ConstraintManager): 50364k


https://reviews.llvm.org/D28953





More information about the cfe-commits mailing list