553759 - Make assertions provided by AvmAssert() available to MSVC++ static analysis

Status: RESOLVED WONTFIX

(Tamarin Graveyard :: Virtual Machine, enhancement, P3)

Description

[William Maddox]

User-Agent:       Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; en-US; rv:1.9.1.8) Gecko/20100202 Firefox/3.5.8
Build Identifier: 

The static analysis tool in Visual Studio 2008 is frequently unable to infer, for example, that a pointer is non-NULL.  It appears to be doing a procedure-at-a-time analysis at the level of sophistication characteristic of an optimizing compiler rather than that of the heavier-duty analysis tools on the market that are impractical to run routinely during the edit-compile-debug cycle. There is a complex annotation language for APIs that mitigates this deficiency and is arguably a useful form of documentation and expression of programmer intent.  It is, however, specific to the Microsoft tools and not integrated into our style of development and large existing codebase.  Instead, we use traditional executable assertions, via AvmAssert(), to express non-obvious assumptions that should be documented and verified.

This patch makes these assertions available to the MS VC++ static analyzer, which will assume them to be true for static analysis purposes.  It appears that in many cases we have already included an assertion in places where the static analyzer is unable to infer the needed property.

The downside of this approach is that assertions are blindly trusted by the static analyzer, which means we have only testing of debug builds to provide confidence that the assertions are true.  Ideally, assertions are things we would like the static analyzer to verify where possible, and to trust only when the deductive power of the analyzer is exceeded.

I've filed this bug as an enhancement request, but in fact it can be viewed as a fix for a large portion of the static analysis failures reported elsewhere, e.g., bug 551695.


Reproducible: Always

Comment 1

[William Maddox]

Attachment: Make assertions via AvmAssert() available to MSVC++ static analysis

Comment 2

[William Maddox]

Attachment: Make assertions via GCAssert() available to MSVC++ static analysis

MMgc has its own assertion mechanism, which essentially duplicates AvmAssert.

Comment 3

[Lars T Hansen]

Gosh, I'm not enthusiastic about having two double sets of debugging macros here - and when would I use the ...DebugOnly set and when would I use the other set?

Comment 4

[Lars T Hansen]

(F- for reasons of macro duplication and missing comments as to the purpose of the two different but eerily similar sets, though in principle I love the idea of the assertion macros interacting with the static analysis in some way.)

Comment 5

[William Maddox]

I'm not all that fond of the AvmAssertDebugOnly myself.  The obvious alternative is to require that these cases be enclosed in #ifdef _DEBUG ... #endif.  I really don't like to proliferate preprocessor directives, however.

The issue is that the _assume builtin requires a valid expression as its argument. There are many cases where the code captures additional state in auxilliary variables or defines auxilliary predicates solely for use in assertions.  Since the presumption has been that assertions are not evaluated except in debug builds, this additional scaffolding is conditionalized on _DEBUG, and the declarations are not available in non-debug builds.  As a result, calls to AvmAssert, etc. expand to invalid invocations of _assume.  The new scheme that I propose requires that all instances of AvmAssert, etc. be well-formed in all configurations, i.e, the programmer must write the assertions as if the asserted condition will be evaluated in all cases. AvmAssertDebugOnly and the other xxxDebugOnly forms are to be used when the old behavior is required.

Should I simply drop the xxxDebugOnly shorthand, or do you have something else in mind?  I agree that documentation would be helpful, and I'm open to the suggestion that writing out the #ifdef _DEBUG ... #endif around the assertions as well as the supporting auxilliary declarations is more stylistically consistent, if more verbose.

Comment 6

[Edwin Smith]

If I were propose adding a new api (and i'm not, mind you), I might widen the scope for them to be release-asserts.  Maybe call it AvmAssume, or something more clear.  possible use cases

- directing static analyzers
- directing the optimizer (if such a thing is possible)
- runtime diagnostics (think crash logging)

The essential feature is that they're *not* compiled out in release mode, and therefore must be fast and not use any debugger capabilities.

another option is to make these use cases be new goals for AvmAssert, and slowly fix things over time.

Comment 7

[William Maddox]

The underlying _assume builtin does direct the optimizer as well as well as the static analyzer, which is why I generate it only during analysis (#ifdef _PREFAST_).  One can occasionaly find code that will limp along or even recover following a failed assertion, so that allowing the optimizer to depend on the assertion without checking it in a release build leaves the code even more broken than before.  It may be appropriate to add an AvmAssume with this property, but it would have been a bad idea to give the existing AvmAssert this behavior. I think that you have raised an important point, however, in that there are indeed assertions that we may want to actually check in release builds.

My intention was more in line with your last option, in that I am proposing to alter the semantics of of AvmAssert such that the checks might in principle be enabled in release builds, and requiring that clients be agnostic in this respect.  This gives us the freedom to implement more complete checking as a future policy choice in the assertion infrastructure, as well as avoiding breakage due to bad arugments to _assume.  I was expecting that expensive assertions suitable for debug builds only would be the less commmon case, so I introduced new macros with new names for this purpose.

Comment 8

[William Maddox]

In eval/eval.h, a DEBUG_ONLY() macro is defined that expands to its argument in debug builds, and to nothing otherwise.  Perhaps it should be moved to AvmDebug.h and made more generally available.

Comment 9

[Edwin Smith]

Comment on attachment 433681 [details] [diff] [review]
Make assertions via AvmAssert() available to MSVC++ static analysis

Same rationale as Lars

Comment 10

[Sylvestre Ledru [:Sylvestre]]

No assignee, updating the status.

Comment 11

[Sylvestre Ledru [:Sylvestre]]

No assignee, updating the status.

Comment 12

[Sylvestre Ledru [:Sylvestre]]

No assignee, updating the status.