Temporarily at:
http://userweb.kernel.org/~chrisl/sparse-0.2-cl2
Will appear later at:
http://ftp.kernel.org//pub/linux/kernel/people/chrisl/patches/sparse/sparse-0.2-cl2/
I have been play with sparse to add more Stanford checker style
of checking. The paper is "Checking System Rules Using System-
Specific, Programmer-Written Compiler Extensions" by Dawson Engler
etc.
Unlike the Stanford checker and smatch, this checker is working on
the linearization level instead of AST level. Linearization code
can be very convenient (when it works) to trace the data flow because
pseudo is in SSA form. There is define/user chain to avoid scan
every instruction.
I take the malloc checking for example to explain how the checker
works. The checking usually happen in three step:
The first step is scanning the linearize instruction. It look for
relevant operations. For malloc checker, the task is find out
the malloc/free function call and usage of malloced pointer.
The second step is converting the relevant operations into checker
instruction. The checker instruction is a simplification of the whole
program, only contain the operation relevant to checker.
The third step is executing the checker instruction. It try to execute
every possible execution flow in the function. The execution engine
will let the checker instruction perform state changes.
Thanks to step two, the size and complexity of the of program has been
greatly reduced.
The new checking has been very fast, it add a few seconds to the make C=1
run.
Again, comment and feed back are always welcome.
Chris
Change log in sparse-0.2-cl2:
- adding pointer signedness fix
- adding spinlock checking
Change log in sparse-0.2-cl1:
The most interesting part is the inline function annotation.
The new checker can find out inlined function usage. The interrupt
checker does not depend on x86 asm instruction any more.
origin.patch
006eff06c7adcfb0d06c6fadf6e9b64f0488b2bf URL: git://git.kernel.org/pub/scm/linux/kernel/git/josh/sparse.git
incompatible-ptr-signess
Bug fix in pointer modifiers inherent at function degeneration.
sizeof-incomplete
Fix double semicolon in struct declare
anon-symbol
Fix core dump on anonymous symbol.
instruction-buffer-size
Fix core dump on huge switch
debug-checker
Adding debug option for showing the linearized instruction.
no-dead-instruction
Disable liveness "dead" instruction by default.
ptr-allocator
Make the ptrlist using the sparse allocator.
annotate-inline-2
Add annotation for inline function call.
malloc-checker
Adding the malloc NULL pointer checker.
interrupt-checker
Adding the interrupt checker
spinlock-checker
Adding spinlock checker
Total 12 patches
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to [email protected]
More majordomo info at http://vger.kernel.org/majordomo-info.html
Please read the FAQ at http://www.tux.org/lkml/
[Index of Archives]
[Kernel Newbies]
[Netfilter]
[Bugtraq]
[Photo]
[Stuff]
[Gimp]
[Yosemite News]
[MIPS Linux]
[ARM Linux]
[Linux Security]
[Linux RAID]
[Video 4 Linux]
[Linux for the blind]
[Linux Resources]
