Using Boogie as a "Super" FxCop...

Feb 28, 2010 at 6:06 PM

Ever since I saw Spec# and how it could verify all kinds of stuff, I thought it would be a great tool to do things that are very difficult in FxCop. For example:

protected override void Dispose(bool disposing)
{
    this.disposableObject.Dispose();
    this.disposableObject = null;

    base.Dispose(disposing);
}

The above code runs fine if you only call Dispose once. The second time you call it, the disposableObject field will be null. This will cause an exception. The correct code would check the disposableObject field for null before calling dispose on it.

The problem with FxCop is that the Abstract Syntax Tree (AST) it builds is very low level. Just trying to figure out if the call to Dispose above is inside an if statement is difficult. Besides that, the AST's are very different for Debug or Release compiled code.

In any case, that's just one of many things that I think it would be trivial to do if I could run Boogie.exe against a compiled C# (or whatever) assembly. Your PDF documents seem to say that this is trivial, but I haven't been able to figure out how to do this. I downloaded and compiled the BytecodeTranslator but it blows up on any assembly I give it. Specifically I tried it against a C# assembly with the only real line of code being: Console.WriteLine("Done!");

It's very possible that I just didn't compile the BytecodeTranslator correctly. It was a little confusing getting the different source code from the different CodePlex projects. I would have been nice to have the BytecodeTranslator.dll downloadable, but I couldn't find it.

In any case, I feel I'm missing something obvious. Any help would be great!

Coordinator
Mar 1, 2010 at 4:03 PM

Yes, we are aware of the problems with the existing bytecode translator. It was written to take IL generated by the Spec# compiler. (Although I have successfully fed it binaries compiled by C#, so please let me know what problems you saw there.)

We have started a new version of the bytecode translator (as part of this Codeplex site) called BCT. It is meant to be a bytecode translator that a) will work against C#, b) understand contracts written using the Code Contracts for .NET library (http://www.research.microsoft.com/contracts), and c) be pluggable with respect to the methodology that you want enforced. Currently the bytecode translator imposes the Spec# methodology (often called the Boogie methodology in our papers) that may be too strict for the kinds of analyses that you want to do.

As a side note, the above problem you outline would be caught by a non-null type analysis. But a deeper property that you might want to enforce is that most methods on a disposable object have an (implicit) precondition that the object has not already been disposed. So a type-state property is that once Dispose has been called, some set of methods may no longer be called.

Mar 2, 2010 at 12:20 AM

I was using the BCT from the CodePlex site. As I said, I couldn't get it to work with a C# DLL with the only real line of code being: Console.WriteLine("Done!"); Here's the top bit of the stack trace:

The byte-code translator failed with uncaught exception: Stack empty.
Stack trace:    at System.ThrowHelper.ThrowInvalidOperationException(ExceptionResource resource)
   at System.Collections.Generic.Stack`1.Pop()
   at BytecodeTranslator.ExpressionTraverser.Visit(IMethodCall methodCall) in C:\CodePlex\Boogie\BCT\BytecodeTranslator\ExpressionTraverser.cs:line 336
   at Microsoft.Cci.MutableCodeModel.MethodCall.Dispatch(ICodeVisitor visitor) in C:\CodePlex\CCICodePlex\Ast\Sources\MutableCodeModel\Expressions.cs:line 1892
   at Microsoft.Cci.BaseCodeTraverser.Visit(IExpression expression) in C:\CodePlex\CCICodePlex\Ast\Sources\CodeModel\Visitors.cs:line 994

I tried this with both a debug and release build. Here's what happened when I tried it against the Spec# compiled AbsInt.dll:

Non-Class StructuralTypes.Function_optional(NonNullType) CallSite_optional(NonNullType) Element was found
The byte-code translator failed with uncaught exception: Non-Class Type StructuralTypes.Function_optional(NonNullType) CallSite_optional(NonNullType) Element is not yet supported.
Stack trace:    at BytecodeTranslator.ToplevelTraverser.Visit(ITypeDefinition typeDefinition) in C:\CodePlex\Boogie\BCT\BytecodeTranslator\ToplevelTraverser.cs:line 67
   at Microsoft.Cci.BaseMetadataTraverser.Visit(INamespaceMember namespaceMember) in C:\CodePlex\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\Visitors.cs:line 877

As I said, I assume I've just compiled BCT incorrectly. As far as I can tell, I have all the latest code and it seems to compile fine.

From your respose, it sounds like Boogie, or at least what is on the CodePlex site, is not what is being used by Code Contracts in VS 2010/.Net 4.0. The reason I was considering Boogie was that it was solid enough for VS 2010/.Net 4.0. I'm still very interested in using it, but more hesitant to put large amounts of my personal time into it.

I would love to see something like FxCop but with a very powerful static analysis language like Boogie. Since I hadn't seen anybody else talk about this, I was going to give it a try myself. I'm thinking something like the Code "SQL" in NDepend. I want to get much deeper than NDepend does since it is very similar to what FxCop can do since they both work with IL pretty much directly.

What I'm thinking is that the BCT can translate my assembly into whatever *.bpl files. I can then add in a *.bpl for each "rule" I'm trying to check and execute it. Does that sound like something that is possible?

Coordinator
Mar 2, 2010 at 5:06 PM

Oh, I see. I misunderstood. I thought you meant you were using the old bytecode translator. I'm not surprised at all that BCT crashes: we just had gotten that project started and haven't had time to work on it. (But we're hoping to very soon.)

Yes, Boogie is not the static analysis engine for Code Contracts. Getting the BCT project to work is one step on the way to allowing Boogie to be used for that.

In theory it sounds as if what you would like to do would work. Unfortunately there is a large amount of engineering that has to happen first...

Mar 3, 2010 at 1:06 AM

I really just wanted to know if I'm crazy to start on a project like I'm thinking. I've already done some work in FxCop to analyze flow through a method. See the CodePlex project http://jslfxcop.codeplex.com/. That will let me get close to a bunch of the "rules" I want to write.

I'm also thinking about looking at the CCI AST project. I think that will let me handle the difference between Debug and Release compiling. I see the FxCop (Static Analysis) in VS 2010 uses the Microsoft Phoenix project to do some of the flow analysis. I've been trying to work with it but is just SOOOOO needlessly complex.

I still think a set of libraries like Boogie that would work against IL would be a very cool addition to the .Net framework. Think what a product like NDepend could do if they could throw this under their current product!

Anyway, thank you very much for the information. :-)