1.4.50813.1 - Performance Issues

Question

We have a smallish C# library that usually runs the cccheck in over 6 minutes (running on Win8 RTM/VS2012 RTM).  And the memory usage of cccheck.exe balloons to 1.5 GB.  Here's the cc output:

1>  CodeContracts: foo: Validated: 88.5%

1>  CodeContracts: foo: Contract density: 1.81

1>  CodeContracts: foo: Total methods analyzed 695

1> CodeContracts: foo: Methods with 0 warnings 616

1>  CodeContracts: foo: Total method analysis read from the cache 291

1>  CodeContracts: foo: Total time 6:41min. 578ms/method

1>  CodeContracts: foo: Total thrown timeouts 2 (method analysis time outs: 0)

1>  CodeContracts: foo: Detected 5 assume to suggest

1>  CodeContracts: foo: Methods with necessary preconditions: 2

1>  CodeContracts: foo: Discovered 13 new candidate preconditions in 00:00:03.1463464

1>  CodeContracts: foo: Retained 4 preconditions after filtering

1>  CodeContracts: foo: Inferred 0 object invariants

1>  CodeContracts: foo: Retained 0 object invariants after filtering

1>  CodeContracts: foo: Discovered 161 postconditions to suggest

1>  CodeContracts: foo: Retained 148 postconditions after filtering

1>  CodeContracts: foo: Detected 0 code fixes

1>  CodeContracts: foo: Proof obligations with a code fix: 0

Does any of this point to a problem (perhaps the two timeouts)?  Or perhaps a problem on our side?  Are there some tweaks to our code that can improve the performance?

Answer 1

I've run into similar issues with the static checker where I had a tiny assembly (2 classes) take 45 minutes to check and use up to 7 GB of memory.  I tracked down that particular issue to a single class that cccheck was timing out on.  It had a private constructor and lots of public/static/readonly members (essentially a polymorphic/typed enum).  The solution was to explicitly specify post-conditions in the constructor and invariants on the class rather than allowing them to be inferred from the constructor preconditions and the fact that I was using readonly fields.  That brought the cccheck time and memory usage *way* down, and got rid of the timeouts.  Now as a matter of course I always use explicit pre- and post-conditions in constructors to supplement invariants.  Contract inference is nice, but it seems like it comes at a cost.

Another technique I use quite a bit is use value objects to encapsulate related sets of preconditions so they don't have to be re-verified all over the place.  For example, a DomainName type that wraps a string value and enforces non-nullity and validity of the domain name using regular expressions in the constructor, or a Percentage type that wraps a decimal and ensures that the value is always >=0 and <= 100.  This seems to cut down on obvious suggestions and warnings coming out of cccheck and seems to reduce the time and memory required.