After spending hours trying to get my code to verify properly on a Vector2 struct, I have finally given up the goat. Not only was I running into some subtle issues that I couldn't get to the bottom of, but a coworker convinced me that having a mutable vector object was a good idea. So in the end, it just made sense to scrap the idea and switch it over.
That done, everything is verifying beautifully. The only things that aren't verified are things that CC would have problems with anyway, and that I could probably only truly verify with Spec#.
Now that I'm over those hurdles, I can explain the other reason why I made the switch. After a lunchtime discussion that threatened to devolve into napkin sketches, I finally grasped the concept Derek was trying to explain. It goes something like this:
In any given second of the application, the physics engine will be called something like 100 times. Which means lots of vectors will be needed for the application. Say there's even only 100 vectors being created by each step. That's 10,000 vectors per second being created and destroyed. In C#, structs are value types, meaning they pass by value and not by reference. Every method that needed a vector would cause the object to be copied and, though it isn't big, this isn't necessary. Instead, the program should pool vectors, pulling old, unused vector objects from a collection, mutating the x and y values to suit the needs of the calculation and then putting them back in the collection when they are no longer being used. Theoretically, instead of creating 10,000 objects (or more) a second, this should allow me to instantiate no more than 100 vector objects, no matter how many times per second my physic engine is doing work. Even though structures are optimized for performance in C#, pooling them should prevent an insane amount of work from being performed under the hood.
Another (tiny) optimization I made is to lazily perform the length computation. Since it involves a square root operation, I want to only calculate it on demand. For collision detection reasons, I'm instead storing the length squared value. Another coworker (John) turned me on to this idea. For most things, I won't even need to get the actual length and storing the "c squared" value of the Pythagorean theorem will allow me to skip a costly operation when I need to.
Well, that's all for now. If anyone has any other suggestions, or and clues to how I can get structures to work for me with Code Contracts, leave a comment. I'd love to see what other people are doing with it.
Saturday, August 10, 2013
Friday, August 2, 2013
My First Code Contracts Bug?
Over the past few weeks (really, since I've finished all this cool set up type stuff), I've been using Code Contracts to verify my physics engine. Until yesterday, everything was going smoothly.
And then I managed to find a bug.
And, like all bugs, it took me a frustratingly long time to get to the bottom of it.
The idea of Code Contracts, in case you don't know, is that you can write code that will be checked for correctness at compile time (sometimes) and at run time (during those other times). You also get to determine what is correct for a given method or class. It's like writing unit tests for every possible valid input value for a method and having all the tests pass.
For instance, lets say you have a method addOne that takes an integer and returns that value incremented by one:
public int addOne(int input)
{
return input + 1;
}
Easy enough, right? Now, lets say you want to restrict the input values to 0 or greater. Code Contracts lets you specify that like so:
public int addOne(int input)
{
Contract.Requires<ArgumentException>(input >=0, "Input must be greater than 0!");
return input + 1;
}
This contract will generate an ArgumentException at run time with the given message if the input doesn't meet the precondition for the method (input >= 0).
This is fine, even a bit cool (sure beats writing if-then-throw blocks!) but what else can we do? Well, lets say we want to guarantee that the return value will be the input value + 1. We can write the following:
public int addOne(int input)
{
Contract.Requires<ArgumentException>(input >=0, "Input must be greater than 0!");
Contract.Ensures(Contract.Result<int>() == input + 1);
return input + 1;
}
During the build process, the verifier will go through the code and see that, yes, the method will indeed meet the stated condition. If you were to say, have the method return input - 1 while leaving the postcondition the same, the verifier would warn you that something was wrong. Cool, huh?
I think so. Like all software, however, this has some bugs. One of the important parts of verification is that it needs to be easy and it needs to be able to verify methods that are inherited from super types as well as those derived from other types with other methods that are verified.
I've been trying like crazy to get a simple == operator to work between two structs. The first is my Vector2 struct, the second is Edge. Vector2 has an X, a Y and a Length (which is derived from X and Y) while Edge is simply two Vector2s, V1 and V2.
My Vector2 == operator simply compares the X's and the Y's and returns whether they are both equal to each other. This compiled fine with no warnings. My Edge struct, trying to compare the Vector2s using the same principle, consistently generated a "Ensures unproven" warning, no matter how I tried to resolve it.
I finally broke down and wrote two classes that represented what I was doing with the structs. By trial and error I determined the following really annoying thing about Code Contracts. Composition works from within class objects but not other structures.
Could this be the first bug I've found in Code Contracts? I'm sure it's possible. If this were some sort of design feature, I would think it would have been documented somewhere. Unless I'm doing something so incomprehensibly stupid that it's just a rule of thumb (please, point this out to me if this is the case). I'll probably be posting to the Microsoft Dev forum about this at some point, just to get a definitive answer. At least I know how to work around it, which means I should be pushing a new update sometime soon.
And then I managed to find a bug.
And, like all bugs, it took me a frustratingly long time to get to the bottom of it.
The idea of Code Contracts, in case you don't know, is that you can write code that will be checked for correctness at compile time (sometimes) and at run time (during those other times). You also get to determine what is correct for a given method or class. It's like writing unit tests for every possible valid input value for a method and having all the tests pass.
For instance, lets say you have a method addOne that takes an integer and returns that value incremented by one:
public int addOne(int input)
{
return input + 1;
}
Easy enough, right? Now, lets say you want to restrict the input values to 0 or greater. Code Contracts lets you specify that like so:
public int addOne(int input)
{
Contract.Requires<ArgumentException>(input >=0, "Input must be greater than 0!");
return input + 1;
}
This contract will generate an ArgumentException at run time with the given message if the input doesn't meet the precondition for the method (input >= 0).
This is fine, even a bit cool (sure beats writing if-then-throw blocks!) but what else can we do? Well, lets say we want to guarantee that the return value will be the input value + 1. We can write the following:
public int addOne(int input)
{
Contract.Requires<ArgumentException>(input >=0, "Input must be greater than 0!");
Contract.Ensures(Contract.Result<int>() == input + 1);
return input + 1;
}
During the build process, the verifier will go through the code and see that, yes, the method will indeed meet the stated condition. If you were to say, have the method return input - 1 while leaving the postcondition the same, the verifier would warn you that something was wrong. Cool, huh?
I think so. Like all software, however, this has some bugs. One of the important parts of verification is that it needs to be easy and it needs to be able to verify methods that are inherited from super types as well as those derived from other types with other methods that are verified.
I've been trying like crazy to get a simple == operator to work between two structs. The first is my Vector2 struct, the second is Edge. Vector2 has an X, a Y and a Length (which is derived from X and Y) while Edge is simply two Vector2s, V1 and V2.
My Vector2 == operator simply compares the X's and the Y's and returns whether they are both equal to each other. This compiled fine with no warnings. My Edge struct, trying to compare the Vector2s using the same principle, consistently generated a "Ensures unproven" warning, no matter how I tried to resolve it.
I finally broke down and wrote two classes that represented what I was doing with the structs. By trial and error I determined the following really annoying thing about Code Contracts. Composition works from within class objects but not other structures.
 |
| TestComposite Class: No Errors |
 |
| TestComposite Struct: Errors |
Keep an eye out for a new article on setting up Jenkins to automatically deploy build artifacts to CodePlex. I think I'm going to take a bit of a break from CC before I try to dive deep again.
Happy hacking!
Happy hacking!
Subscribe to:
Posts (Atom)