4 ms·

How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbad

How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.

pron 8y ago
It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well. So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
OnlyOneCannolo 8y ago
Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool. The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic. Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.

pron 8y ago

It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well. So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.

OnlyOneCannolo 8y ago

Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool. The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic. Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.