Hi guys, some updates:
1. The tool I've been working on now has a name, sixgill, and a skeletal
website, sixgill.org
2. I've put up a full source release and SVN access on the website.
3. This site also has reports for write overflows and NS_ASSERTION violations
in a current version of Firefox. These were generated with the gcc plugin
frontend and CVC3 solver (BSD-licensed); 83% of the write accesses were checked
(consistent with the old stuff) and 51% of the NS_ASSERTIONs (needs some more
work).
4. Nightly builds should be working soon (hopefully in a few days). There are
no obstacles for the tool here, just getting hardware and scripts set up.
5. My priority right now is to put together lots of (much needed)
documentation, then handle the remaining items from my email a few weeks ago
(none of those should take too long).
Also, to use this tool the annotation macros need to be defined somewhere in
the Firefox source. Below is the code I added to my local copy of
xpcom/glue/nsDebug.h. This needs to go after the block defining
NS_ASSERTION/etc. as it redefines those (only when the plugin is running), and
depends on a macro XGILL_PLUGIN being set when the plugin is running (done by
the tool's build scripts). Does this look OK?
Brian
/* macros for static assertions, used by the sixgill tool.
* when the tool is not running these macros are no-ops. */
#ifdef XGILL_PLUGIN
#define __precondition(COND) __attribute__((precondition(#COND)))
#define __precondition_assume(COND) __attribute__((precondition_assume(#COND)))
#define __postcondition(COND) __attribute__((postcondition(#COND)))
#define __postcondition_assume(COND)
__attribute__((postcondition_assume(#COND)))
#define __invariant(COND) __attribute__((invariant(#COND)))
#define __invariant_assume(COND) __attribute__((invariant_assume(#COND)))
#define __paste2(X,Y) X ## Y
#define __paste1(X,Y) __paste2(X,Y)
#define __assert_static(COND) \
PR_BEGIN_MACRO \
__attribute__((assert(#COND), unused)) int __paste1(__annotation,
__COUNTER__); \
PR_END_MACRO
#define __assume_static(COND) \
PR_BEGIN_MACRO \
__attribute__((assume(#COND), unused)) int __paste1(__annotation,
__COUNTER__); \
PR_END_MACRO
#define __assert_runtime(COND) \
PR_BEGIN_MACRO \
__attribute__((assert_runtime(#COND), unused)) int __paste1(__annotation,
__COUNTER__); \
PR_END_MACRO
/* redefine runtime assertion macros to perform static assertions.
* don't include the original runtime assertions; this ensures the tool will
* consider cases where assertions fail. */
#ifdef DEBUG
#undef NS_PRECONDITION
#undef NS_ASSERTION
#undef NS_POSTCONDITION
#define NS_PRECONDITION(expr, str) __assert_runtime(expr)
#define NS_ASSERTION(expr, str) __assert_runtime(expr)
#define NS_POSTCONDITION(expr, str) __assert_runtime(expr)
#endif /* DEBUG */
#else /* XGILL_PLUGIN */
#define __precondition(COND) /* nothing */
#define __precondition_assume(COND) /* nothing */
#define __postcondition(COND) /* nothing */
#define __postcondition_assume(COND) /* nothing */
#define __invariant(COND) /* nothing */
#define __invariant_assume(COND) /* nothing */
#define __assert_static(COND) PR_BEGIN_MACRO /* nothing */ PR_END_MACRO
#define __assume_static(COND) PR_BEGIN_MACRO /* nothing */ PR_END_MACRO
#define __assert_runtime(COND) PR_BEGIN_MACRO /* nothing */ PR_END_MACRO
#endif /* XGILL_PLUGIN */
_______________________________________________
dev-static-analysis mailing list
[email protected]
https://lists.mozilla.org/listinfo/dev-static-analysis
