>Dear Linus and Kernel hackers,
>
>torvalds@transmeta.com (Linus Torvalds) writes:
>> Well, if we had a static analysis tool we'd obviously be able to track a
>> lot of things that we can't currently track. You could build a tree of all
>> calling sequences, and statically verify quite a few rules. You might not
>> prove correctness, but you could find a lot of things like this.
>>
>> Dreaming? Yes.
>
>One valuable tool might be Tom Lord's ctool, a tool for
>"Application Specific Static Code Checking for C Programs",
>written in systas Scheme (a near cousin of GUILE).
>It is available from ftp://ftp2.lanminds.com/lord/twaddle.tar.gz
>as well perhaps as from ftp://emf.net/users/lord/
>It has been used to verify the behavior of the C implementation
>of systas itself with respect to a few GC invariants,
>which can be viewed as whole-program (inter-file) mutual exclusion analysis
>thru generation of critical-section-aware, longjmp-aware, global call graph.
>So this technology (be it ctool or a similar tool) could probably be used
>to verify mutual exclusion for the Linux kernel.
>
>One major problem I see is that ctool (and all non-trivial C analysis tools
>I know) can only handle code that is already preprocessed, because of
>difficulty of #conditional analysis, of the horrid general-case
>macro-replacement analysis, and the abominable combination of them
>(since depending on conditional macro definition, the parse tree may
>be significantly different, though I believe this should not be the
>case in cleanly-written code like Linux should be).
>This means that unless we write a better tool that's CPP-aware
>(which is not trivial), we can only analyze preprocessed source trees
>that are valid in a particular configuration.
I've done some work on a system, based on CPP output. It certainly
makes parsing easier with respect to conditional macros and includes.
One use was creating an exact dependency file when the compiler in use
didn't support that output.
For generating a call graph, one tough parts involves function calls via
indirect lookup and use of tables of function addresses.
john alvord
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.altern.org/andrebalsa/doc/lkml-faq.html