On Monday 25 January 2010 06:42:18 Brian William Hackett wrote:
> ----- Brad Hards <[email protected]> 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-...@repens sixgill-test]$ g++ -fplugin=../sixgill/gcc/xgill.so -c
buffer.c -o buffer.o
[bradh-...@repens sixgill-test]$ g++ -E buffer.c | ../sixgill/bin/xsource
[bradh-...@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-...@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-...@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-...@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-...@repens sixgill-test]$ ../sixgill/bin/make_index write_overflow
Wrote write_overflow/index.html
[bradh-...@repens sixgill-test]$ ls write_overflow/
index.html
[bradh-...@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>
_______________________________________________
dev-static-analysis mailing list
[email protected]
https://lists.mozilla.org/listinfo/dev-static-analysis
