(cc:ing dev-static-analysis, original message at bottom) ----- Robert O'Callahan <[email protected]> wrote: > On Wed, Dec 30, 2009 at 5:53 AM, Brian William Hackett < > [email protected]> wrote: > > > Hi Rob, just an update and a few questions. I'm mostly done with a gcc > > plugin with support for in-source annotations (see below), and have > > integrated a different backend solver which is BSD-licensed (CVC3), which > > was the only licensing issue with the tool. Both of these need more work, > > but I'm guessing everything will be in good shape in ~2 weeks. > > > > Again, annotations here can be used to help the tool when it gets confused, > > or as compile time asserts for other properties (needs experimenting with). > > These all take COND values, which can use fields, functions, macros, etc., > > just no looping or recursion. > > > > This looks cool. Could we modify our NS_ASSERTION and NS_PRECONDITION macros > to include an __assert(COND)? What would happen if they call functions that > happen to loop or be recursive, can you just ignore the annotation in those > cases? What affect would this have on the analysis, given that we know many > of our assertions do fail in some testcases?
Hi, it's not a problem if the conditions have loops/recursion. It is probably best to add another attribute __assert_runtime that is equivalent to __assert but is used in NS_ASSERTION/NS_PRECONDITION. Overly complex conditions can be ignored for __assert_runtime and warned on for __assert/__precondition/etc. This would also be good for the UI so we could distinguish runtime assertions from annotations added by hand, e.g. bucket reports in the following way: 1. runtime assertions - __assert_runtime from NS_ASSERTION/NS_PRECONDITION. 2. static assertions - __assert, __precondition, etc. 3. write overflows 4. write underflows 5. ... These __assert_runtimes can affect the analysis, as when checking an assertion the tool will assume the truth of all previous assertions, e.g. in the following case the tool will prove the later assertion trivially without needing to know where x came from. __assert_runtime(x < 256); x *= 2; __assert(x < 512); It would be straightforward to turn off this behavior for __assert_runtime, so that the later assertion cannot be proved trivially. Not sure whether it's better to do this. Brian > > After finishing up the plugin/solver, things I want to get working are (in > > order): > > > > 1. Automated nightly runs on the latest source. > > 2. Diff run results against one another, e.g. the current source vs. one > > week or month ago. > > 3. Quickly apply small diffs (new annotations, proposed changes, ...) to > > see how they affect the results of a run. > > 4. Add annotations via a web interface. > > > > That sounds very good. > > > > Also, what's the best mailing list / cc: list for talking about this? > > > > mozilla.dev.static-analysis on news.mozilla.org. > > Thanks!!! > 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] Original message: Hi Rob, just an update and a few questions. I'm mostly done with a gcc plugin with support for in-source annotations (see below), and have integrated a different backend solver which is BSD-licensed (CVC3), which was the only licensing issue with the tool. Both of these need more work, but I'm guessing everything will be in good shape in ~2 weeks. Again, annotations here can be used to help the tool when it gets confused, or as compile time asserts for other properties (needs experimenting with). These all take COND values, which can use fields, functions, macros, etc., just no looping or recursion. // annotations on functions __precondition(COND) __precondition_assume(COND) __postcondition(COND) __postcondition_assume(COND) // annotations on globals, types, or fields __invariant(COND) __invariant_assume(COND) // annotations within a function __assert(COND) __assume(COND) These are attributes (names trivial to change): #define __precondition(COND) __attribute__((precondition(#COND))) #define __postcondition(COND) __attribute__((postcondition(#COND))) Example: __postcondition_assume(ubound(return) >= size) void* malloc(int size); After finishing up the plugin/solver, things I want to get working are (in order): 1. Automated nightly runs on the latest source. 2. Diff run results against one another, e.g. the current source vs. one week or month ago. 3. Quickly apply small diffs (new annotations, proposed changes, ...) to see how they affect the results of a run. 4. Add annotations via a web interface. Also, what's the best mailing list / cc: list for talking about this? Brian _______________________________________________ dev-static-analysis mailing list [email protected] https://lists.mozilla.org/listinfo/dev-static-analysis
