[cfe-dev] GRExprEngine and complexe

[Jean-Daniel Dupas]

Le 19 juin 08 à 20:24, Ted Kremenek a écrit :

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

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 ;-)



-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2427 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20080620/ddcdc0a2/attachment.bin>