[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