In the topic of code analysis or program analysis (Wikipedia article), there is static code analysis (Wikipedia article) and dynamic program analysis (Wikipedia article). This topic overlaps with performance analysis, formal verification, as well as general debugging.
Bounty
There is a FOSS Factory bounty (p276) on some of these tasks.
Static
GCC's warnings. Yes, really.
GCC plugins can be used for additional semantic analysis. For example, http://lwn.net/Articles/457543/, and search for kernel context in the comments.
Have GCC make use of RPC/MIG in/out specifiers, and have it emit useful warnings in case these are pointing to uninitialized data (for in only).
Engineering zero-defect software, Eric S. Raymond, 2012-05-13
-
For example, Debian's hurd_20110319-2 package (Samuel Thibault, 2011-08-05: I had a look at those, some are spurious; the realloc issues are for real).
Coccinelle
Has already been used for finding and fixing double mutex unlocking issues.
-
<teythoon> btw, I've been looking at http://frama-c.com/ lately <teythoon> it's a theorem prover for c/c++ <braunr> oh nice <teythoon> I think it's most impressive, it works on the hurd (aptitude install frama-c o_O) <teythoon> *and it works <braunr> "Simple things should be simple, <braunr> complex things should be possible." <braunr> :) <braunr> looks great <teythoon> even the gui is awesome, allows one to browse source code in a very impressive way <braunr> clear separation between value changes, dependencies, side effects <braunr> we could have plugins for stuff like ports <braunr> handles concurrency oO <nalaginrut> so you want to use Frame-C to analyze the whole Hurd code base? <teythoon> nalaginrut: well, frama-c looks "able" to assist in analyzing the Hurd, yes <teythoon> nalaginrut: but theorem proving is a manual process, one needs to guide the prover <teythoon> nalaginrut: b/c some stuff is not decideable <nalaginrut> I ask this because I can imagine how to analyze Linux since all the code is in a directory. But Hurd's codes are distributed to many other projects <braunr> that's not a problem <braunr> each server can be analyzed separately <teythoon> braunr: also, each "entry point" <nalaginrut> alright, but sounds a big work <teythoon> it is <braunr> otherwise, formal verification would be widespread :) <teythoon> that, and most tools are horrible to use, frama-c is really an exception in this regard
Coverity (nonfree)
https://scan.coverity.com/projects/1307 If you want access, speak up in #hurd or on the mailing list.
IRC, OFTC, #debian-hurd, 2014-02-03
<pere> btw, did you consider adding hurd and mach to <URL: https://scan.coverity.com/ > to detect bugs automatically? <pere> I found lots of bugs in gnash, ipmitool and sysvinit when I started scanning those projects. :) <teythoon> i did some static analysis work, i haven't used coverty but free tools for that <teythoon> i think thomas wanted to look into coverty though <pere> quite easy to set up, but you need to download and run a non-free tarball on the build host. <teythoon> does that tar ball contains binary code ? <teythoon> that'd be a show stopper for the hurd of course <pere> did not investigate. I just put it in a contained virtual machine. <pere> did not want it on my laptop. :) <pere> prefer free software here. :) <pere> but I did not have to "accept license", at least. :)
IRC, OFTC, #debian-hurd, 2014-02-05
<pere> ah, cool. <URL: https://scan.coverity.com/projects/1307 > is now in place. :)
clean up the code, Code_Analysis, Coverity.
-
IRC, freenode, #hurd, 2011-12-04
<mcsim> has anyone used splint on hurd? <mcsim> this is tool for statically checking C programs <mcsim> seems I made it work
Hurd-specific Applications
Port Sequence Numbers. If these are used, care must be taken to update them reliably,
id:"1123688017.3905.22.camel@buko.sinrega.org"
. This could be checked by a static analysis tool.
Dynamic
glibc's
libmcheck
Used by GDB, for example.
Is not thread-safe, sourceware [BZ #6547], sourceware [BZ #9939], sourceware [BZ #12751], Stack Overflow question 314931.
MALLOC_CHECK_
/MALLOC_PERTURB_
IRC, freenode, #glibc, 2011-09-28
<vsrinivas> two things you can do -- there is an environment variable (DEBUG_MALLOC_ iirc?) that can be set to 2 to make ptmalloc (glibc's allocator) more forceful and verbose wrt error checking <vsrinivas> another is to grab a copy of Tor's source tree and copy out OpenBSD's allocator (its a clearly-identifyable file in the tree); LD_PRELOAD it or link it into your app, it is even more aggressive about detecting memory misuse. <vsrinivas> third, Red hat has a gdb python plugin that can instrument glibc's heap structure. its kinda handy, might help? <vsrinivas> MALLOC_CHECK_ was the envvar you want, sorry.
http://git.fedorahosted.org/cgit/initscripts.git/diff/?id=deb0df0124fbe9b645755a0a44c7cb8044f24719
In context of
id:"1341350006-2499-1-git-send-email-rbraun@sceen.net"
/thealloca
issue mentioned in gnumach page cache policy:IRC, freenode, #hurd, 2012-07-08:
<youpi> braunr: there's actually already an ifdef REDZONE in libthreads
It's
RED_ZONE
.<youpi> except it seems clumsy :) <youpi> ah, no, the libthreads code properly sets the guard, just for grow-up stacks
GCC, LLVM/clang: Address Sanitizer (asan), Memory Sanitizer (msan), Thread Sanitizer (tasn), Undefined Behavor Sanitizer (ubsan), ...
-
-
CTraps is a gcc plugin and runtime library that inserts calls to runtime library functions just before shared memory accesses in parallel/concurrent code.
The purpose of this plugin is to expose information about when and how threads communicate with one another to programmers for the purpose of debugging and performance tuning. The overhead of the instrumentation and runtime code is very low -- often low enough for always-on use in production code. In a series of initial experiments the overhead was 0-10% in many important cases.
-
Input fuzzing
Not a new topic; has been used (and papers published?) for early UNIX tools. What about some RPC fuzzing?
Jones: system call abuse, Dave Jones, 2010.
- [Trinity: A Linux system call fuzzer]http://codemonkey.org.uk/projects/trinity/(). Trinity: A Linux kernel fuzz tester (and then some), Dave Jones, The Eleventh Annual Southern California Linux Expo, 2013.
American fuzzy lop, a practical, instrumentation-driven fuzzer for binary formats.
Melkor - An ELF File Format Fuzzer, Alejandro Hernández.
- Can use this to find bugs in our exec server,
for example? See also the discussion in
id:"5452389B.502@samsung.com"
.
- Can use this to find bugs in our exec server,
for example? See also the discussion in
Mayhem, an automatic bug finding system
IRC, freenode, #hurd, 2013-06-29:
<teythoon> started reading the mayhem paper referenced here http://lists.debian.org/debian-devel/2013/06/msg00720.html <teythoon> that's nice work, they are doing symbolic execution of x86 binary code, that's effectively model checking with some specialized formulas <teythoon> (too bad the mayhem code isn't available, damn those academic people keeping the good stuff to themselvs...) <teythoon> (and I really think that's bad practice, how should anyone reproduce their results? that's not how science works imho...)