Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

sixgill tool

65 views
Skip to first unread message

Brian William Hackett

unread,
Jan 20, 2010, 11:08:36 PM1/20/10
to rob...@ocallahan.org, tg...@mozilla.com, ai...@cs.stanford.edu, dev-stati...@lists.mozilla.org
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 */

Taras Glek

unread,
Jan 21, 2010, 5:40:07 PM1/21/10
to Brian William Hackett, ai...@cs.stanford.edu, rob...@ocallahan.org, dev-stati...@lists.mozilla.org
On 01/20/2010 08:08 PM, Brian William Hackett wrote:
> 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?
>
Awesome! Let continue this discussion in bugzilla, I filed
https://bugzilla.mozilla.org/show_bug.cgi?id=541220 for that.

I think Benjamin will want you to rename your macros to be NS_UPPERCASE.
The usual way of iterating discussions like this is by attaching your
changes as a diff in the bug and asking for review.

Cheers,
Taras

Taras Glek

unread,
Jan 21, 2010, 6:02:01 PM1/21/10
to Brian William Hackett, ai...@cs.stanford.edu, rob...@ocallahan.org, dev-stati...@lists.mozilla.org
On 01/20/2010 08:08 PM, Brian William Hackett wrote:
> 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?
>
The two errors I looked at, seem to be false positives

http://sixgill.org/firefox/write_overflow/ResolveSymlink_1244447419593944471.html

http://sixgill.org/firefox/write_overflow/EncodeString_3315072988729628109.html


Taras

Brian William Hackett

unread,
Jan 21, 2010, 6:48:55 PM1/21/10
to Taras Glek, ai...@cs.stanford.edu, rob...@ocallahan.org, dev-stati...@lists.mozilla.org

----- Taras Glek <tg...@mozilla.com> wrote:
> The two errors I looked at, seem to be false positives

Hi, yeah, the great majority of these reports are going to be false positives (I hope that was clear from the talk!). The trick here is that it should be clear from the report where the tool got confused, and it should be easy to add an annotation which the tool can use to check the assertion.

For both of these reports, the tool picked the wrong postcondition for a called function, and in both the right postcondition is easy to specify.

> http://sixgill.org/firefox/write_overflow/ResolveSymlink_1244447419593944471.html

The first step the tool took for this access was pick the postcondition (__return < 4097) for PR_Read:

PR_IMPLEMENT(PRInt32) PR_Read(PRFileDesc *fd, void *buf, PRInt32 amount);


>
> http://sixgill.org/firefox/write_overflow/EncodeString_3315072988729628109.html
>
>
> Taras

Brian William Hackett

unread,
Jan 21, 2010, 7:06:06 PM1/21/10
to Taras Glek, ai...@cs.stanford.edu, rob...@ocallahan.org, dev-stati...@lists.mozilla.org
Resending finished email (grr... at email client).

----- Taras Glek <tg...@mozilla.com> wrote:
> The two errors I looked at, seem to be false positives

Hi, yeah, the great majority of these reports are going to be false positives (I hope that was clear from the talk!). The trick here is that it should be clear from the report where the tool got confused, and it should be easy to add an annotation which the tool can use to check the assertion.

For both of these reports, the tool picked the wrong postcondition for a called function, and in both the right postcondition is easy to specify.

> http://sixgill.org/firefox/write_overflow/ResolveSymlink_1244447419593944471.html

The first step the tool took for this access was pick the (wrong) postcondition (__return < 4097) for PR_Read:

PR_IMPLEMENT(PRInt32) PR_Read(PRFileDesc *fd, void *buf, PRInt32 amount);

Adding __postcondition(return <= amount) will fix this report (the same postcondition would have to be added to pl_DefRead due to its potential recursion, this is an issue with the tool that needs to be fixed).

> http://sixgill.org/firefox/write_overflow/EncodeString_3315072988729628109.html

Again, the first step the tool took was picking a wrong postcondition for nsEncoderSupport::Convert.

nsresult nsEncoderSupport::Convert(const PRUnichar * aSrc,
PRInt32 * aSrcLength,
char * aDest,
PRInt32 * aDestLength)

This can be fixed with a precondition and postcondition describing this interface:

__precondition(ubound(aDest) >= *aDestLength)
__postcondition(ubound(aDest) >= *aDestLength)

(An alternative would be __postcondition(*aDestLength <= initial(*aDestLength)) where initial indicates the value at function entry for a term. This isn't supported yet though (would be easy to fix)).

Doing this is more work than using a bugfinder, a tool that guesses which accesses are likely to be bugs. Once the code is annotated though, you get strong guarantees (not airtight yet) that *all* the bugs have been found; with a bugfinder you don't get anything. Also, improvements to the tool's inference will reduce the need for annotations. In both the above cases it would not be too hard to work on the tool to infer these and similar postconditions.

Brian

Taras Glek

unread,
Jan 21, 2010, 8:39:46 PM1/21/10
to Brian William Hackett, ai...@cs.stanford.edu, rob...@ocallahan.org, dev-stati...@lists.mozilla.org
On 01/21/2010 04:06 PM, Brian William Hackett wrote:
> Resending finished email (grr... at email client).
>
> ----- Taras Glek<tg...@mozilla.com> wrote:
>
>> The two errors I looked at, seem to be false positives
>>
> Hi, yeah, the great majority of these reports are going to be false positives (I hope that was clear from the talk!). The trick here is that it should be clear from the report where the tool got confused, and it should be easy to add an annotation which the tool can use to check the assertion.
>
> For both of these reports, the tool picked the wrong postcondition for a called function, and in both the right postcondition is easy to specify.
>
Ok.

>
>> http://sixgill.org/firefox/write_overflow/ResolveSymlink_1244447419593944471.html
>>
> The first step the tool took for this access was pick the (wrong) postcondition (__return< 4097) for PR_Read:
>
> PR_IMPLEMENT(PRInt32) PR_Read(PRFileDesc *fd, void *buf, PRInt32 amount);
>
> Adding __postcondition(return<= amount) will fix this report (the same postcondition would have to be added to pl_DefRead due to its potential recursion, this is an issue with the tool that needs to be fixed).
>
>
>> http://sixgill.org/firefox/write_overflow/EncodeString_3315072988729628109.html
>>
> Again, the first step the tool took was picking a wrong postcondition for nsEncoderSupport::Convert.
>
> nsresult nsEncoderSupport::Convert(const PRUnichar * aSrc,
> PRInt32 * aSrcLength,
> char * aDest,
> PRInt32 * aDestLength)
>
> This can be fixed with a precondition and postcondition describing this interface:
>
> __precondition(ubound(aDest)>= *aDestLength)
> __postcondition(ubound(aDest)>= *aDestLength)
>
> (An alternative would be __postcondition(*aDestLength<= initial(*aDestLength)) where initial indicates the value at function entry for a term. This isn't supported yet though (would be easy to fix)).
>
Ok. Thanks for the examples. Can you assign the sixgill bug to yourself?

I think the way we will land this is by adding another build option to
Mozilla(similar to --with-static-checking flag).

Once we land this we will need to land annotations to fix the false
positives. These annotations would have to broken up into patches with
module-granularity. Generally that is done by filing individual bugs for
each component. Should set the bugs as depedent on 541220. Hopefully,
module-maintaines will help out.


> Doing this is more work than using a bugfinder, a tool that guesses which accesses are likely to be bugs. Once the code is annotated though, you get strong guarantees (not airtight yet) that *all* the bugs have been found; with a bugfinder you don't get anything. Also, improvements to the tool's inference will reduce the need for annotations. In both the above cases it would not be too hard to work on the tool to infer these and similar postconditions.
>

What would it take to be airtight? Is that even realistic?


Taras
Taras

Brian William Hackett

unread,
Jan 22, 2010, 12:46:35 AM1/22/10
to Taras Glek, ai...@cs.stanford.edu, rob...@ocallahan.org, dev-stati...@lists.mozilla.org

----- Taras Glek <tg...@mozilla.com> wrote:
> Ok. Thanks for the examples. Can you assign the sixgill bug to yourself?

Hi, I added an nsDebug.h patch to bug 541220. How do I assign the bug to myself?

> I think the way we will land this is by adding another build option to
> Mozilla(similar to --with-static-checking flag).

This might not be necessary. The process I've been using doesn't require any modifications to the mozilla build, but works by wrapping that build in a script which does two things:
1. Forks a manager process which collects and collates the plugin's results into some output databases.
2. Modifies PATH to intercept calls to gcc/g++/etc. and insert the appropriate xgill plugin arguments. The plugin communicates with the manager via a socket.

> Once we land this we will need to land annotations to fix the false
> positives. These annotations would have to broken up into patches with
> module-granularity. Generally that is done by filing individual bugs for
> each component. Should set the bugs as depedent on 541220. Hopefully,
> module-maintaines will help out.

Are these component-level bugs mainly for dependency tracking, i.e. would it be possible to commit a patch that adds just a few annotations? It would be great to have a low barrier to adding annotations to the source, since they don't change the behavior of the code at all. One thing that could help here is having a web interface for annotations so that they can be added without modifying the source. I had a prototype for this working last month and one of my TODO items is to get this working for real, so that any annotation you can add directly to the source can also be added over the web.

> What would it take to be airtight? Is that even realistic?

Yes, this is realistic, and is a main goal of this project. I want to be doing verification, but the analysis needs to be practical first and foremost (these have historically been mutually exclusive). There's some on this in the slides, and will be a lot more once the documentation is done. Basically though, there are two holes regarding integer overflow and clobbered null terminators that should be fixed by writing separate analyses (using the same framework), and several minor holes that need to be fixed directly (mainly for interprocedural aliasing and call modsets).

Brian

Jean-Marc Desperrier

unread,
Jan 22, 2010, 8:56:40 AM1/22/10
to
Brian William Hackett wrote:
> improvements to the tool's inference will reduce the need for annotations.
> In both the above cases it would not be too hard to work on the tool to infer these and similar postconditions.

I'm not sure autoinfering is always the good solution :-)

When you add the" __postcondition(return <= amount)" annotation to
PR_Read, you are actually changing an implicit, "must read some text"
part of the contract the PR_Read function has with the rest of the world
to something that's explicitly described. This is a very good thing.
It infering has the consequence you don't do it anymore, it's not
actually positive.

In fact, I don't know if it's not there already, the best would be to
take the __postcondition annotations as input and check that the
function really respect them.

I think inference would more useful as an help tool to let programmers
see what kind of __postcondition annotation could be put on the
function, but that it better be their choice to add them or not.

Of course, when the function is only used locally, inferring
automatically makes writing the code easier.

Brian William Hackett

unread,
Jan 22, 2010, 12:34:30 PM1/22/10
to Jean-Marc Desperrier, dev-stati...@lists.mozilla.org

----- Jean-Marc Desperrier <jmd...@alussinan.org> wrote:
> I'm not sure autoinfering is always the good solution :-)
>
> When you add the" __postcondition(return <= amount)" annotation to
> PR_Read, you are actually changing an implicit, "must read some text"
> part of the contract the PR_Read function has with the rest of the world
> to something that's explicitly described. This is a very good thing.
> It infering has the consequence you don't do it anymore, it's not
> actually positive.

Hi, I agree that making the contracts explicit is good. Mozilla has a lot of code though, and anything which reduces the annotation burden for that code I view as good. Your idea of having the inference export annotations which could be added to the code is a great meet-in-the-middle solution, definitely worth investigating.

> In fact, I don't know if it's not there already, the best would be to
> take the __postcondition annotations as input and check that the
> function really respect them.

Yes, each __postcondition will be checked and a report generated if it might not hold at exit from the function. There is an alternate __postcondition_assume which will *not* be checked; the tool just assumes it holds after each call.

Brian

Brad Hards

unread,
Jan 24, 2010, 3:53:13 AM1/24/10
to dev-stati...@lists.mozilla.org, tg...@mozilla.com, Brian William Hackett
On Thursday 21 January 2010 15:08:36 Brian William Hackett wrote:
> 2. I've put up a full source release and SVN access on the website.
I think I don't really understand this stuff, but it looks interesting for
doing checks in other C/C++ code.

It wasn't really easy to get to build, but eventually I managed it.
The basic recipe I used was to:
0. Check out sixgill from svn.
1. build gcc from svn trunk (to make sure it works)
2. Patch gcc with the PLUGIN_DECL_FINISH support (which I extracted from the
email on the gcc-patches list)
3. Installed CVC3 from source
4. Built a config.mk to turn on CVC3 solver and the GCC plugin.
5. make.

Overall, I think it might be easier if there was a script to check for CVC3
and a GCC with plugin support, and to set things up. Ideally I would be able
to use the CVC3 packages from my distro, and gcc header (when gcc 4.5 actually
gets released).

A patch to implement this is attached.

The only problem is that CVC3 doesn't actually use pkgconfig yet, and while I
have a patch to fix that, I'm not sure if it will get applied. The backup plan
is to do a search for the includes / libs, but pkgconfig would be nicer.

Thoughts, comments?

Brad

BTW: Now I have it built, can I have a hint on how to run this stuff?

Brian William Hackett

unread,
Jan 24, 2010, 2:42:18 PM1/24/10
to Brad Hards, tg...@mozilla.com, dev-stati...@lists.mozilla.org

----- Brad Hards <br...@frogmouth.net> wrote:
> Overall, I think it might be easier if there was a script to check for CVC3
> and a GCC with plugin support, and to set things up. Ideally I would be able
> to use the CVC3 packages from my distro, and gcc header (when gcc 4.5 actually
> gets released).
>
> A patch to implement this is attached.
>
> The only problem is that CVC3 doesn't actually use pkgconfig yet, and while I
> have a patch to fix that, I'm not sure if it will get applied. The backup plan
> is to do a search for the includes / libs, but pkgconfig would be nicer.
>
> Thoughts, comments?

Wow, thanks! A few comments:

1. It looks like there is a config.h.in missing from the patch.
2. Can this be made to work even if CVC3 does not use pkgconfig?
3. I'm not sure pkgconfig is really needed for CVC3; I'd thought of configuration for this project as being:

./configure [--with-cvc3=/path/to/cvc3] [--with-yices=/path/to/yices]

And auto-detect the GCC headers as your patch does. (I have zero experience building configure scripts though)

> BTW: Now I have it built, can I have a hint on how to run this stuff?

Yep, the tool runs in two phases; the frontend to build databases with CFGs and other source information, and the backend to do the actual analysis and assertion checking. If you want to use annotations, adapt the nsDebug.h patch for the program you're testing and you'll have the appropriate macros.

For the frontend, there are two different methods:

1. Building a toy/test program:

gcc -fplugin=/path/to/xgill.so test.c
gcc -E test.c | xsource

2. Building a real project:

Copy the bin/wrap_gcc directory somewhere, then modify basecc and build_xgill for the project you are building.
build_xgill from the appropriate project directory.

Both of these should make a directory with various .xdb databases, e.g. src_body.xdb for all function bodies. For the backend, run these from the .xdb directory:

xmemlocal # build memory model for each function
xinfer # get assertions to check, infer some loop invariants
xcheck -check-kind=kind # check assertions of the specified kind
make_index kind # make a directory 'kind' with HTML reports for the specified kind

The 'kind' used by xcheck can be 'write_overflow', 'read_overflow', 'annotation', or a few others.

This method of running doesn't use any timeouts or failure recovery and is best suited for analyzing small programs. For bigger programs, you can run with recovery and multiple cores:

xmonitor /path/to/poll_file 1
xmonitor /path/to/poll_file 2
... repeat for the number of processes you want to run. these can be on multiple machines, they just need to be able to read the same poll_file via NFS
xcomplete /path/to/poll_file /path/to/xdb_dir

Brian

Brad Hards

unread,
Jan 24, 2010, 6:13:44 PM1/24/10
to Brian William Hackett, tg...@mozilla.com, dev-stati...@lists.mozilla.org
On Monday 25 January 2010 06:42:18 Brian William Hackett wrote:
> A few comments:
>
> 1. It looks like there is a config.h.in missing from the patch.
This is generated by "autoheader" (which is run from the "autogen.sh" script)
from information in configure.ac. I can probably turn that off, since all it
does is provide some definitions along the lines of

/* Define to the address where bug reports for this package should be sent. */
#undef PACKAGE_BUGREPORT

which the configure script turns into something like:

/* Define to the address where bug reports for this package should be sent. */
#define PACKAGE_BUGREPORT "bhackett at stanford.edu"

(and equivalents for versions, short names and so on) although I thought that
might be useful when building more command line tools, since you only have the
information in one place.


> 2. Can this be made to work even if CVC3 does not use pkgconfig?

Yes.

> 3. I'm not sure pkgconfig is really needed for CVC3; I'd thought of
> configuration for this project as being:
>
> ./configure [--with-cvc3=/path/to/cvc3] [--with-yices=/path/to/yices]

I think we should be able to fall back to manually specifying the include and
library paths, but I'd prefer to be able to autodetect them if possible. So if
you have CVC3 headers and libraries in one of the standard places (e.g.
/usr/include or /usr/local/include for headers; and /usr/lib, /usr/lib64,
/usr/local/lib or /usr/local/lib64), then you shouldn't need to specify the
path, but you can manually specify them if necessary (e.g. it finds the wrong
version, or the path is completely non-standard).

I'm not so sure about yices (since I'm really only interested in the gcc front
end, and I haven't sorted out the combined licensing bits in my head, I
haven't actually agreed to the yices license yet), but manually specifying the
path could be a good option. We should be able to automatically detect yices
if it is unpacked into the sixgill source directory.

A couple of questions:
1. Do you know if a particular version of CVC3 is required (e.g. needs to be
2.1 or later) ?
2. If yices is unpacked into the sixgill source dir, what does the top level
directory structure look like. Is it something like:
sixgill/
sixgill/yices
sixgill/yices/include/
sixgill/yices/lib/

Let me have another go with the configure stuff, and I'll send you a revised
patch.

[I'll have a look at the usage instructions, give it a try, and follow-up on
that part separately]

Brad

Robert O'Callahan

unread,
Jan 24, 2010, 9:02:34 PM1/24/10
to Brian William Hackett, ai...@cs.stanford.edu, Taras Glek, dev-stati...@lists.mozilla.org
All this work sounds amazing, Brian!

On Fri, Jan 22, 2010 at 6:46 PM, Brian William Hackett <
bhac...@stanford.edu> wrote:

> Hi, I added an nsDebug.h patch to bug 541220. How do I assign the bug to
> myself?
>

I've done that, and I've given you Bugzilla permissions to do whatever you
need.

Are these component-level bugs mainly for dependency tracking, i.e. would it
> be possible to commit a patch that adds just a few annotations? It would be
> great to have a low barrier to adding annotations to the source, since they
> don't change the behavior of the code at all. One thing that could help
> here is having a web interface for annotations so that they can be added
> without modifying the source. I had a prototype for this working last month
> and one of my TODO items is to get this working for real, so that any
> annotation you can add directly to the source can also be added over the
> web.
>

Whatever annotation patches you come up with, I'm happy to rubber-stamp for
Taras (or anyone else with commit access) to land.

Rob
--
"He was pierced for our transgressions, he was crushed for our iniquities;
the punishment that brought us peace was upon him, and by his wounds we are
healed. We all, like sheep, have gone astray, each of us has turned to his
own way; and the LORD has laid on him the iniquity of us all." [Isaiah
53:5-6]

Brad Hards

unread,
Jan 25, 2010, 6:06:14 AM1/25/10
to dev-stati...@lists.mozilla.org, Brian William Hackett
On Monday 25 January 2010 10:13:44 Brad Hards wrote:
> Let me have another go with the configure stuff, and I'll send you a
> revised patch.
I've updated it to support using unmodified CVC3 (so it should work from distro
packages) and added a --with-yices option to the configure script. I also added
some installation instructions and some general cleanup stuff.

Patch attached.

Brad

Jean-Marc Desperrier

unread,
Jan 25, 2010, 1:54:29 PM1/25/10
to
Brad Hards wrote:
> Patch attached.

Attachments are not allowed on news://mozilla.dev.static-analysis

Can you publish your patch somewhere ? I think it would be OK to put it
in a page on https://developer.mozilla.org , it can be on your personal
page ( https://developer.mozilla.org/User:<login> ) if you hesitate to
modify the public ones.

Benjamin Smedberg

unread,
Jan 25, 2010, 2:22:51 PM1/25/10
to

The best place to send patches is a bug on bugzilla.mozilla.org.

--BDS

Brad Hards

unread,
Jan 25, 2010, 6:38:03 PM1/25/10
to dev-stati...@lists.mozilla.org
On Tuesday 26 January 2010 05:54:29 Jean-Marc Desperrier wrote:
> Brad Hards wrote:
> > Patch attached.
>
> Attachments are not allowed on news://mozilla.dev.static-analysis
Urgh, sorry. I view it as a mailing list, which I thought would allow patches.


> Can you publish your patch somewhere ? I think it would be OK to put it
> in a page on https://developer.mozilla.org , it can be on your personal
> page ( https://developer.mozilla.org/User:<login> ) if you hesitate to
> modify the public ones.
Brian has merged it, so just svn up for patch goodness.

I wasn't sure whether it was even appropriate to "hijack" the mozilla static
analysis list for sixgill discussions. Obviously not so bad when we're working
on analyses for mozilla, but what about when it is more general (e.g. sixgill
internals or a new analysis technique) or when it has nothing to do with
mozilla (e.g. applying sixgill to $random_project).

Yet another list? Just private email? Thoughts?

Brad

Brian William Hackett

unread,
Jan 25, 2010, 8:17:42 PM1/25/10
to Brad Hards, dev-stati...@lists.mozilla.org
----- Brad Hards <br...@frogmouth.net> wrote:
> I wasn't sure whether it was even appropriate to "hijack" the mozilla static
> analysis list for sixgill discussions. Obviously not so bad when we're working
> on analyses for mozilla, but what about when it is more general (e.g. sixgill
> internals or a new analysis technique) or when it has nothing to do with
> mozilla (e.g. applying sixgill to $random_project).
>
> Yet another list? Just private email? Thoughts?

I'll set up a couple mailing lists @sixgill.org, and email here when those are ready.

Brian

Brad Hards

unread,
Jan 25, 2010, 9:46:50 PM1/25/10
to dev-stati...@lists.mozilla.org, Brian William Hackett
On Monday 25 January 2010 06:42:18 Brian William Hackett wrote:
> ----- Brad Hards <br...@frogmouth.net> wrote:
> > Overall, I think it might be easier if there was a script to check for
> > CVC3 and a GCC with plugin support, and to set things up. Ideally I would
> > be able to use the CVC3 packages from my distro, and gcc header (when gcc
> > 4.5 actually gets released).
> >
> > A patch to implement this is attached.
> >
> > The only problem is that CVC3 doesn't actually use pkgconfig yet, and
> > while I have a patch to fix that, I'm not sure if it will get applied.
> > The backup plan is to do a search for the includes / libs, but pkgconfig
> > would be nicer.
> >
> > Thoughts, comments?
>
> Wow, thanks! A few comments:

>
> 1. It looks like there is a config.h.in missing from the patch.
> 2. Can this be made to work even if CVC3 does not use pkgconfig?
> 3. I'm not sure pkgconfig is really needed for CVC3; I'd thought of
> configuration for this project as being:
>
> ./configure [--with-cvc3=/path/to/cvc3] [--with-yices=/path/to/yices]
>
> And auto-detect the GCC headers as your patch does. (I have zero experience
> building configure scripts though)
>
> > BTW: Now I have it built, can I have a hint on how to run this stuff?
>
> Yep, the tool runs in two phases; the frontend to build databases with CFGs
> and other source information, and the backend to do the actual analysis
> and assertion checking. If you want to use annotations, adapt the
> nsDebug.h patch for the program you're testing and you'll have the
> appropriate macros.
>
> For the frontend, there are two different methods:
>
> 1. Building a toy/test program:
>
> gcc -fplugin=/path/to/xgill.so test.c
> gcc -E test.c | xsource
>
> 2. Building a real project:
>
> Copy the bin/wrap_gcc directory somewhere, then modify basecc and
> build_xgill for the project you are building. build_xgill from the
> appropriate project directory.
>
> Both of these should make a directory with various .xdb databases, e.g.
> src_body.xdb for all function bodies. For the backend, run these from the
> .xdb directory:
>
> xmemlocal # build memory model for each function
> xinfer # get assertions to check, infer some loop
> invariants xcheck -check-kind=kind # check assertions of the specified kind
> make_index kind # make a directory 'kind' with HTML reports
> for the specified kind

I tried this using the "buffer.c" test file, as shown below.

I think it is working up until the report generation ("make index") step. I'm
getting a report that doesn't appear to have any content. Am I doing something
wrong?

On the actual analysis, I can see that the output of xcheck has a line like:
Point 3: (i* < ubound(buf*,int32))
I'm assuming that this is telling me that there is a case where
the pointer i can overrun the valid range of buf. In this particular case
the valid range is buf[0]...buf[99], but we are trying to assign from
buf[0] to buf[100] in bad_access().

Brad

Steps follow:

[bradh-dev@repens sixgill-test]$ g++ -fplugin=../sixgill/gcc/xgill.so -c buffer.c -o buffer.o
[bradh-dev@repens sixgill-test]$ g++ -E buffer.c | ../sixgill/bin/xsource
[bradh-dev@repens sixgill-test]$ ls -al
total 124
drwxrwxr-x. 2 bradh-dev bradh-dev 4096 2010-01-26 13:33 .
drwx------. 73 bradh-dev bradh-dev 4096 2010-01-26 13:30 ..
-rw-rw-r--. 1 bradh-dev bradh-dev 12611 2010-01-26 13:32 body_callee.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12612 2010-01-26 13:32 body_caller.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 635 2010-01-26 13:30 buffer.c
-rw-rw-r--. 1 bradh-dev bradh-dev 1664 2010-01-26 13:32 buffer.o
-rw-rw-r--. 1 bradh-dev bradh-dev 12812 2010-01-26 13:32 escape_access.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12689 2010-01-26 13:32 escape_edge_backward.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12685 2010-01-26 13:32 escape_edge_forward.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12564 2010-01-26 13:33 file_preprocess.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12630 2010-01-26 13:33 file_source.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 53 2010-01-26 13:32 src_body_topo.sort
-rw-rw-r--. 1 bradh-dev bradh-dev 13459 2010-01-26 13:32 src_body.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12380 2010-01-26 13:32 src_comp.xdb
-rw-rw-r--. 1 bradh-dev bradh-dev 12380 2010-01-26 13:32 src_init.xdb
[bradh-dev@repens sixgill-test]$ ../sixgill/bin/xmemlocal
Generating memory for 'void bad_access(int*, int)'
Computed modset:
modset: void bad_access(int*, int):loop:3:4
mod buf* [zterm(int32)]
mod i

Computed modset:
modset: void bad_access(int*, int)
mod buf* [zterm(int32)]


Generating memory for 'void foo(int*)'
Computed modset:
modset: void foo(int*)
mod buf* [zterm(int32)]


Generating memory for 'void bar()'
Computed modset:
modset: void bar()


[bradh-dev@repens sixgill-test]$ ../sixgill/bin/xinfer
Generating summaries for 'void bad_access(int*, int)'
Solver: CVC3: 0:00.00 / 0:00.01
Solver: CVC3: 0:00.00 / 0:00.00
Computed summary:
summary: void bad_access(int*, int):loop:3:4
assert write_overflow check: 3: (i* < ubound(buf*,int32))
assert write_underflow check: 3: (lbound(buf*,int32) <= i*)
assert read_overflow check: 2: (i* < ubound(buf*,int32))
assert read_underflow check: 2: (lbound(buf*,int32) <= i*)
assume: (0 <= i*)

Computed summary:
summary: void bad_access(int*, int)
assert read_overflow redundant: 4: (i* < ubound(buf*,int32))
assert read_underflow redundant: 4: (lbound(buf*,int32) <= i*)

Elapsed: 0:00.02

Generating summaries for 'void foo(int*)'
Solver: CVC3: 0:00.00 / 0:00.00
Computed summary:
summary: void foo(int*)

Elapsed: 0:00.00

Generating summaries for 'void bar()'
Solver: CVC3: 0:00.00 / 0:00.00
Computed summary:
summary: void bar()

Elapsed: 0:00.00

[bradh-dev@repens sixgill-test]$ ../sixgill/bin/xcheck -check-kind=write_overflow

Checking: 'void bad_access(int*, int)'

ASSERTION 'write_overflow$buffer.c$void bad_access(int*, int)$loop:3:4$1'
Point 3: (i* < ubound(buf*,int32))
Solver: CVC3: 0:00.01 / 0:00.02
REPORT Finished 'write_overflow$buffer.c$void bad_access(int*, int)$loop:3:4$1'
TRAIT: Block 'void bad_access(int*, int)'
TRAIT: Block 'void foo(int*)'
TRAIT: Block 'void bar()'
TRAIT: BlockCount 3
TRAIT: BoundType int32

Finished: 'void bad_access(int*, int)' FILE buffer.c REDUNDANT 0 ASSERTION 1 SUCCESS 0 REPORT 1
Elapsed: 0:00.02


Checking: 'void foo(int*)'

Finished: 'void foo(int*)' FILE buffer.c REDUNDANT 0 ASSERTION 0 SUCCESS 0 REPORT 0
Elapsed: 0:00.00


Checking: 'void bar()'

Finished: 'void bar()' FILE buffer.c REDUNDANT 0 ASSERTION 0 SUCCESS 0 REPORT 0
Elapsed: 0:00.00


[bradh-dev@repens sixgill-test]$ ../sixgill/bin/make_index write_overflow
Wrote write_overflow/index.html
[bradh-dev@repens sixgill-test]$ ls write_overflow/
index.html
[bradh-dev@repens sixgill-test]$ cat write_overflow/index.html

<html>
<head>

<style type="text/css">

a.dir {
white-space: pre;
font-family: monospace;
text-decoration: none;
color: black;
}

a.report {
white-space: pre;
font-weight: bold;
text-decoration: none;
color: blue;
}

span.errors {
white-space: pre;
font-family: monospace;
color: red;
}

</style>

<script type="text/javascript">

function toggleDir(name)
{
var dirItem = document.getElementById(name);

if (dirItem.style.display == "none") {
dirItem.style.display = "";
}
else {
dirItem.style.display = "none";
}

return false;
}

</script>

</head>
<body>

<h2>Reports</h2>
</body>
</html>

Robert O'Callahan

unread,
Feb 18, 2010, 11:09:30 PM2/18/10
to
On 26/01/10 12:38 PM, Brad Hards wrote:
> I wasn't sure whether it was even appropriate to "hijack" the mozilla static
> analysis list for sixgill discussions. Obviously not so bad when we're working
> on analyses for mozilla, but what about when it is more general (e.g. sixgill
> internals or a new analysis technique) or when it has nothing to do with
> mozilla (e.g. applying sixgill to $random_project).
>
> Yet another list? Just private email? Thoughts?

I think it's fine to keep using the newsgroup for now. If sixgill takes
over the world, it can have its own list :-).

Rob

0 new messages