[cfe-dev] GRExprEngine and complexe

[Ted Kremenek]

On Jun 19, 2008, at 7:44 AM, Jean-Daniel Dupas wrote:

> 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:

   http://lists.cs.uiuc.edu/pipermail/cfe-commits/Week-of-Mon-20080616/006179.html

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.

Ted