GRExprEngine and complexe

I'm trying to do some static code analysis. Usually, my code uses tgmath.h to don't have to bother with all the maths fonctions variants.
The problem is that some tgmaths fonctions have complex number support, and even if I do not use complex numbers directly, some complex operator may appears in my code.

#include <tgmath.h>

int main(int argc, char **argv) {
   sin(M_PI_2 - .8);
   return 0;

expand to

int main(int argc, char **argv) {
   __builtin_choose_expr (__builtin_classify_type(1.57079632679489661923132169163975144 - .8) == 9, __builtin_choose_expr(__builtin_types_compatible_p(__typeof__(__real__(1.57079632679489661923132169163975144 - .8)), long double), csinl(1.57079632679489661923132169163975144 - .8), __builtin_choose_expr((__builtin_types_compatible_p(__typeof__(__real__(1.57079632679489661923132169163975144 - .8)), double) || __builtin_classify_type(__real__(1.57079632679489661923132169163975144 - .8)) == 1), (csin)(1.57079632679489661923132169163975144 - .8), csinf(1.57079632679489661923132169163975144 - .8))), __builtin_choose_expr(__builtin_types_compatible_p(__typeof__(1.57079632679489661923132169163975144 - .8), long double), sinl(1.57079632679489661923132169163975144 - .8), __builtin_choose_expr((__builtin_types_compatible_p(__typeof__(1.57079632679489661923132169163975144 - .8), double) || __builtin_classify_type(1.57079632679489661923132169163975144 - .8) == 1), (sin)(1.57079632679489661923132169163975144 - .8), sinf(1.57079632679489661923132169163975144 - .8))));
  return 0;

which contains some "__real__" operators.

The problem is in GRExprEngine::VisitUnaryOperator(). There is no case for UnaryOperator::Real and UnaryOperator::Imag. So when a Real operator is reached, the

assert (U->isIncrementDecrementOp()); is false.

What should be done to fix this ?

Hi Jean-Daniel,

I've added some initial support for __real__ and __imag__ in GRExprEngine:

This patch does two things:

1) The assertion you mentioned doesn't fire anymore.

2) We correctly reason about applying __real__ and __imag__ to non-complex types:

   __real__ x -> x
   __imag__x -> 0

3) For complex types, the expression evaluates to Unknown. The next step is to implement an RValue object that represents a Complex type, and then implement so more transfer function logic.

Aside from implementing more logic for complex types (which largely reduces to just reasoning about tuples of values), I think a larger issue is that we don't really do any reasoning about floats right now. This isn't an inherit limitation in the analyzer; it's just not been done.

We've focused purely on integers right now because they are so fundamental to reason about most branch conditions. Even the analyzer's reasoning about integers right now is very much in the early stages; all the analyzer reasons about is integer constants, and not integer ranges. We on implementing integer range tracking, and also plan on integrating more bit-level reason about integer values as well (e.g., the values of some bits are known and others are not).

For floating point (real numbers), different static analyses have taken different approaches. Some analyses like to reason about them as arbitrary real numbers, while others try to reason about their actual implementation on a machine (i.e., floats and doubles have finite precision). GRExprEngine is being designed to defer such choices to the plug-in transfer function object (i.e., the subclass of GRTransferFunc) that is used for clients to implement "analysis-specific" logic. This gives different clients to implement the level of precision that they need for a particular task. Many clients won't care about floating-point values, so it actual buys them scalability to not reason about them at all (i.e., simply treating floats as "Unknown").

Over the next couple of weeks I will be putting some significant effort into cleaning up some of the core pieces of the analyzer, but I honestly probably won't implement any specific support for reasoning about floating-point values any time soon since that would have little applicability for the problems I'm focusing on using static analysis. I will probably shore up some of the support for complex types, however, but only to the point that any specific reason about floats will get reduced to method calls to the GRTransferFunc object (where the default implementation will return "Unknown" for most complex operations).

If you are interested in implementing some support for floating-point values, the place to start would be to implement a subclass of GRTransferFuncs (or a subclass of GRSimpleVals) that implements transfer function logic for floats; e.g. implement support for add, subtract, etc. More of the "assumption" logic (which implements reasoning about ">", "==", etc.) will also get put into GRTransferFuncs, so basically all the symbolic reasoning you would want to do about floats could also be plug-in logic that doesn't have to go directly into GRExprEngine. The purpose of GRExprEngine is to reason about the details of the C syntax (as well as reason about memory), and reduce the myriad of ways you can do the same thing in C to a smaller set of operations that the plug-in transfer function logic can deal with.


Thank you for this answer (and for the quick fix). I will now be able to find some other memory leaks and other error in my code :wink: