[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:

RangeConstraintManager: 8.24s
Z3ConstraintManager: 247.29s

RangeConstraintManager: 10.23s
Z3ConstraintManager: 250.35s

And for memory usage (max RSS):

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

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


More information about the cfe-commits mailing list