Monday, August 27, 2012 10:14 PM
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?
Tuesday, August 28, 2012 3:38 PM
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.