6 ms·
A gentle introduction to static analyzers for C
- Animats 3y agoThese are all just lints, not proof systems. The big problems in C are: * How big is it? * Who owns it? * Who locks it? Those are the problems which cause trouble after the program has first started to work at all. These lints don't help with those problems.
- steveklabnik 3y agoWhile they cannot solve all problems, it is worth not allowing the perfect to be the enemy of the good. You are correct that these are huge problems that are not currently solvable, but that doesn't mean that using these tools is a bad thing.
- flohofwoe 3y agoAt least gcc -fanalyze and clang-tidy are "proper" static analyzers. Don't get confused about the clang-tidy name, it might have started as a simple linter, but it also includes all the clang analyzer checks (e.g. search for clang-analyzer here: https://clang.llvm.org/extra/clang-tidy/checks/list.html https://clang.llvm.org/extra/clang-tidy/checks/list.html). And the clang static analyzer indeed does things like static ownership/lifetime tracking following the control flow as much as is possible at compile time. In code bases which haven't run through an analyzer yet it typically does need some handholding via asserts (for instance hinting that a pointer isn't expected to be null, otherwise you'll be swamped with false positives). Clang analyzer basically tells you things like "this statement here will cause a null pointer access if this seemingly unrelated function over there at the other end of the project is called with this specific argument, and here's how I arrived at that conclusion (...followed by dozens of "calling function x with y...", "entering loop with loop count z", "taking this if-branch because x is greater than y" etc... - in Xcode this is accompanied with a nice control flow visualization over the source code which makes it a bit easier to follow). Once a code base is static-analyzer-clean via "assert-hints", it will actually catch bugs at compile time which might be tricky to reproduce at runtime. Of course static analyzers are still only part of the solution (the "compile time part"), for runtime checks there are the various clang sanitizers.
- jvanderbot 3y agoI'd be suspicious of someone taking a stab at running ownership static verification before enabling basic sanity checks like those presented here. So. Maybe it qualifies as a "gentle introduction" since it's effectively step 1.
- bfrog 3y agoRight, people have created whole new languages to solve those
- pjmlp 3y agoYes, however many C and C++ developers to this day don't use any kind of lint checks, even though it was already invented in 1979 to deal with typical C flaws, by the group that created C in first place. Granted they could have made the language better, but I guess in the spirit of UNIX, they decided to have the separate pass be yet another tool. If someone is going with C, at very least they should already consider these, and eventually learn to adopt the real deal in terms of tooling for "safe" C.
- addaon 3y agoWhen you start thinking about how to write correct C code, there are a few steps along the way. Glorified linters are a great first step; in the best case, they prove useful safety properties of code (no access to uninitialized variables, etc). From there, static analyzers start proving more complex properties -- no stack overflow, for example. The final step along this journey is to proof assistants, proving arbitrary properties not just with regards to safety, but correctness. One often overlooked part is CompCert [1], a pretty-much-verified C compiler. All of the tools mentioned above prove properties on the semantics of the C code that is written. These properties are only conserved in practice if the translation of the C code to equivalent-semantic machine code is correct, and the execution of the machine code is correct with regards to its modeled semantics. The first part of this chain of trust is where CompCert slots in; for the second part, in practice, we are at the mercy of our silicon vendors. https://compcert.org/compcert-C.html https://compcert.org/compcert-C.html
- AlotOfReading 3y agoCompcert is a true tour de force in what can be done with formal methods, but my experience is that almost no one is actually in a position where semantic equivalence is major source of issues for them. I more commonly see it brought up internally as a way for people to avoid facing the larger issues traditionally plaguing high assurance C development that aren't as simple as "just" changing the compiler.
- addaon 3y ago> almost no one is actually in a position where semantic equivalence is major source of issues for them Well, they don't necessarily know if it is or not... When you're dealing with safety-critical software (DO-178, etc) where the cost of verification and validation can be easily 100x - 1000x the cost of writing the code, having traceability from C code to machine code be correct by proof instead of a manual process can be a lifesaver. Are a significant number of bugs actually excluded this way? That basically comes down to how much the defect rate has been reduced at the C code level by other activities, to determine significance. It's hard for me to imagine working on DAL B or DAL A code and not at least seriously considering use CompCert just to reduce the scope of necessary verification activities a bit.
- 38 3y ago> -Wall turns on a group of warnings that can catch common mistakes. I appreciate modern languages, which just catch this at compile time, without making people jump through hoops. for example I can just run "go build", and this wont even compile: package main func main() { println("Program run!") i := 10 // i declared and not used }
- flohofwoe 3y agoDeclaring '-Wall -Wextra -Werror' on the compiler command line isn't exactly "jumping through hoops" though. This should be the default of course, but this will just bring out the pitch forks because people have different opinions (for instance this innocent unused-variable-error in Go is currently by far the most controversial feature in Zig).
- spc476 3y agoAnd then you hit: warning: ISO C forbids assignment between function pointer and `void *' Which, while true, is allowed (and in fact, required by) POSIX. Of course, not passing "-pedantic" will suppress that warning, but you'll also suppress other, critical warnings. Okay, I'll put away my pitchfork now.
- pjmlp 3y agoSuch warnings might save some hours of pain when writing cross platform code.
- LoganDark 3y agoThis isn't really an innocent Go feature, either. I have a meme saved somewhere that's basically "no, fuck you, variable declared but not used".
- IshKebab 3y agoI agree, but that is not the most compelling example to be honest. I think a better one is my nemesis: int foo() {} This is not an error or even a warning by default! Worse, even if you have enabled warnings, it can cause stack corruption and crazy insane behaviour in a different file. I've lost hours to this because I was working on code without `-Werror`, I didn't see the warning, and incremental compilation meant the offending file was never recompiled (I was trying to fix the error in a different file). Of course modern languages don't have this insanity.
- jnwatson 3y agoThe open source tools listed are quite basic compared to commercially available tools.
- scscsc 3y agoHaving some experience in this field, I can say that all of the tools presented on the webpage are very lightweight static analyzers. They are all based on processing the syntax tree and they which will detect things like uninitialized variables, or do style checks. "Real" static analyzers, which are more useful, are based on symbolic execution and abstract interpretation and they will uncover more interesting classes of errors, like double frees, out of bounds array access, etc. Note that all analyzers will have FPs and FNs, because the underlying problem is uncomputable. The best open source "real" static analyzer overall for C++ is the Clang static analyzer. There are many commercial analyzers available, and most C++ shops will use one or more of these.
- chc4 3y agoclang-tidy is mentioned in the blog post, and what I personally use - it does do control flow and dataflow analysis to find double frees or missing frees from any possible program trace (though doesn't do any interprocedural analysis, for hopefully obvious reasons).
- flohofwoe 3y agoAFAIK clang-tidy is a superset of clang static analyzer nowadays. E.g. quote from the documentation page (https://clang.llvm.org/extra/clang-tidy/ https://clang.llvm.org/extra/clang-tidy/): clang-tidy has its own checks and can also run Clang Static Analyzer checks.
- bjourne 3y agoWhat I'm missing from static analyzers are English awareness: static void get_foobar() ... Get is a verb that means "to retrive" so "get_foobar" should return something. int n_bytes = ...; Why a signed type? A negative number of bytes is nonsense. In fact a whole language designed around assigning semantic meaning to names would be cool. f has to be a function, n has to be an integer >= 0, M has to be a square matrix of some type, has_xyz must be a boolean, and so on.
- cozzyd 3y agoget_foobar() could update some thread_local static value, for example.... or print something to screen. n_bytes could easily be negative if a byte offset, or as a sentinel. This is why we have a type system, to express these things :)
- bjourne 3y agoNah, those are type errors. Some languages use case so that FOO can never have the same type as foo. Nothing prevents a type system from similarly distinguishing between get_foo() and set_foo().
- neutrono 3y agoIn C23 you can use the attribute [[nodiscard]] on functions to mark that the result from function shouldn't be discarded. I think there is also a [[reproducible]] attribute for saying a function doesn't do side effects.
- flohofwoe 3y ago> A negative number of bytes is nonsense. That's true, but mixing signed and unsigned integers opens a much bigger can of worms (for instance it's not unusual to add a negative quantity to an unsigned integer). It's often better to just stick to signed integer types which are big enough to cover the required positive range (e.g. you only loose one bit, and 63 bits ought to be enough for anybody). ...also an optimizing compiler will usually turn something like: assert((index >= 0) && (index < size)); ...into a single comparison, since on the assembly level it's free to interpret that 'index' as unsigned.
- canucker2016 3y agoI've written a simple C/C++ linter/static analyzer long time ago that's analyzed large commercial and open source code bases. At that time, compilers didn't catch many of the errors my tool found. Couple of decades later, compiler warnings from the major compilers cover the majority of the bugs my tool looked for. Spewing out a list of potential bugs to stdout/stderr isn't enough. There needs to be a smooth workflow for the developer to quickly assess if a reported bug is an actual problem. Also the developer needs to be able to tell the tool to ignore the bug in the future, because getting a list of bugs that you know aren't problematic is annoying the next time around, but infuriating after the tenth time. Commenters have referred to some linters/analyzers as lightweight, etc. IMHO the simple tools will analyze code on a per-function basis. No/little data-flow analysis is done across function boundaries. The more thorough tools will go the extra mile and analyze resources allocated/values used in one function and passed to others. These tools will require a database and several minutes/hours depending on the size of the codebase. They're not meant as a precondition for committing code - they're doing work that computers are meant for - boring, repetitive, exhaustive, dreary code analysis. But most of the code where my tool found errors tended to reside in the uncommon code path, typically error handling code/uncommon cases. You don't want to create an Apple-level face-palm-like bug - https://dwheeler.com/essays/apple-goto-fail.html https://dwheeler.com/essays/apple-goto-fail.html So turn on the highest level of compiler warning you can and/or pass the appropriate analyze flag to your compiler.
- P_I_Staker 3y agoInterested in whether anyone has compared how these analyzers compare with expensive enterprise options? So much of this enterprise software is junk, but it seems like the options much more basic. In this case, perhaps the simple version is worse. I'm not as sure how these are designed either. Usually, this requires some fairly sophisticated management of the static test environment, and providing information to the tool. Perhaps it's just embedded systems, but you also have to manage a custom preprocessor. I'm not sure if these tool have any good rulesets, either default or stuff geared towards eg. CERT-C and MISRA-C. Anyway, I've played around with Unit test frameworks, too. I'm not sure if I found any that provide good coverage metrics. Also here, it seems in both cases you do get a basic suite of behavior static: rules you can enable for static checks, logs/reports, etc unit: framework, scripts, assert, test sequencing, etc Anybody use anything "heavier weight"? It doesn't have to be "free free", but not for $6-50k+... say less than $2k.
- canucker2016 3y agoPC-Lint/Flexelint is the grownup/commercial version of lint/compiler analyzers. Looks like they merged with a more corporate software company, but you can still find their webpages on archive.org. see https://web.archive.org/web/20061206130312/http://gimpel.com/html/lintchks.htm https://web.archive.org/web/20061206130312/http://gimpel.com... and https://web.archive.org/web/20061208002102/http://www.gimpel.com/html/pub80/msg.txt https://web.archive.org/web/20061208002102/http://www.gimpel.... And for fun, see https://web.archive.org/web/20070204002103/http://www.gimpel.com/html/bugs.htm https://web.archive.org/web/20070204002103/http://www.gimpel... Two commercial static analyzers I've heard of are Klocwork and Coverity. I know Coverity has a program to scan open source projects. So you can take a look at the output of their scans to see how they fare. For PC-lint, it was relatively easy to integrate into the build process. Just a few changes in each makefile - probably less if you use something like ninja/cmake to drive the build process. But adding static analysis to your build is similar to getting a home energy efficiency audit. The auditor comes in and analyzes your house and points out where you can improve the house's energy efficiency (go from single to double/triple pane windows, fill in cracks around doors, don't use oil/coal to heat the house, etc.) But once they're done and you've adjusted the house accordingly, further audits won't bring up any new issues unless something in the house has changed. Similar thing with static analyzer (and with turning on compiler warnings). First time you use that feature, you'll get a lot of issues - some of them you may modify, some you'll ignore. But further static analysis won't bring up many new issues, if at all, unless the code has changed. Which means it's important to run the analysis when code is committed. Besides being cheaper/faster to fix problems before the commit, issues won't build up until the next time you run the static analyzer. These tools don't eat, don't sleep, don't take vacation/sick days, won't get tired looking at the same code over and over again, and know much more about gotchas/footguns in the programming language than most programmers. When I talked with a programmer who had worked on an enterprise-level commercial static analyzer, we agreed that these types of tools would find about up to 10% of bugs in a project - closer to 10% for the lower quality projects.
- gdgghhhhh 3y agoThere is also smatch, it is used by the Linux Kernel community https://github.com/error27/smatch https://github.com/error27/smatch
- bfrog 3y agoI mean the best static analyzer is rustc bar none, but then you have to drop the ancient dialect known as C
- galangalalgol 3y agoI love rust, but "bar none" is perhaps overstating it. While formal methods aren't the same thing as static analyasis MISRA, SPARK, and normal Ada shouldn't be dismissed as things vastly less worthwhile.
- bfrog 3y agoMISRA is at best a glorified style guide and short for misra-ble. I have yet to actually see MISRA do much to prevent bugs. I haven't used SPARK and Ada to be frank, so perhaps they are even superior in their ability to catch bugs with static analysis, I have heard great things. It's something I've been meaning to try.
- galangalalgol 3y agoI've not used MISRA, so I'm really referring to the collection of tools for formal proofs that surround the style guide. Ada was worth trying for me just to contrast with rust and to add some humility to my rust evangelism. I don't like the verbosity or module system, and it is a bit dated as far as supporting anything but imperative styles. There is some confusion about how to deallocate stuff or if you should... Lastly, the thread safety mechanisms are kind of clunky to me.
- quincepie 3y agoNice article, I wasn't aware of the GCC -fanalyzer flag, I think that approach is much better than clang. The warnings also seem to be much nicer.