[cfe-dev] Non Deterministic floats in clang static analyzer.

[George Karpenkov via cfe-dev]

(re-adding cfe-dev)

Hi Julian,

Artem’s reply above in this thread indicates that currently float modeling is not performed:

> Finally, the analyzer isn't conducting symbolic floating-point arithmetic at all yet, only integers. A step in the direction of improving it can be found in https://reviews.llvm.org/D28954 <https://reviews.llvm.org/D28954> .

You might have more luck using Z3-mode and the mentioned patch.

George

> On Sep 25, 2017, at 8:50 AM, Julian Löffler <loefflju at informatik.uni-freiburg.de> wrote:
> 
> Hey there,
> 
> What is strange to me, that Clang/scanbuild does not recognize the following:
> 
> Program:
> 
> #include <math.h>
> 
> extern void clang_analyzer_warnIfReached();
> 
> int main(){
>   float x = NAN;
>   // NAN == NAN --> False.
>   if(x == x){
>      clang_analyzer_warnIfReached();
>   }
> }
> 
> The clang_analyzer_warnIfReached() should not be reachable, but is reachable.
> 
> 
> On 19/09/2017 19:03, George Karpenkov wrote:
>> Hi Julian,
>> 
>>> On Sep 19, 2017, at 3:43 AM, Julian Löffler <loefflju at informatik.uni-freiburg.de> wrote:
>>> 
>>> Hey George,
>>> 
>>> Thanks a lot for the additional information.
>>> 
>>> Using prototypes works as expected I think.
>>> 
>>> However, do you think clang is a good tool to analyze reachability of certain program-points?
>>> 
>>> Currently we model requirements of a math-lib in the form of small programs for each function, where we analyze if we can reach error-states. (i.e. states where the requirement can be injured). The question is if we should rather use Clang  on the source code.
>> Clang static analyzer is neither sound, nor complete, so you will not be able to verify
>> that a certain program point is definitely not reachable.
>> There are many sources of imprecision: functions are inlined only if they are smaller than a certain size,
>> program is analyzed one translation unit at a time, and many others.
>> 
>> However, unlike more academic tools clang static analyzer
>> gives you a push-button technology: you can just run it on an *arbitrary* codebase, and in a very timely manner
>> get a list of found bugs.
>> As far as I am aware that would be very difficult to achieve with e.g. Ultimate Atomizer and similar tools.
>> 
>>> Usually we do that using trace abstraction and abstract interpretation, anyway I did not find a hint what clang static analyzer is doing exactly.
>>> So if you have a clue which analysis-methods Clang static analyzer uses, I'd be glad to hear it^^
>> I believe it would be closest to symbolic execution.
>> 
>> George
>> 
>>> 
>>> Thanks a lot and kind regards,
>>> 
>>> Julian
>>> 
>>> 
>>> On 19.09.2017 03:02, George Karpenkov wrote:
>>>> Hi Julian,
>>>> 
>>>> Artem has mentioned a few good points, to that I would like to add that:
>>>> 
>>>> a) Using uninitialized values as non-det inputs from the user like CBMC
>>>> does is usually not a good thing to do, as uninitialized values are not simply
>>>> non-deterministic, and can cause undefined behavior.
>>>> 
>>>> b) In order to get Clang static analyzer to model non-deterministic input from user
>>>> it is enough to define a function prototype without implementation which would return
>>>> desired type.
>>>> 
>>>> Regards,
>>>> George
>>>> 
>>>>> On Sep 16, 2017, at 7:07 AM, Julian Löffler via cfe-dev <cfe-dev at lists.llvm.org> wrote:
>>>>> 
>>>>> Greetings,
>>>>> 
>>>>> I wonder how one can obtain that Clang Static Analyzer recognizes non-deterministic-floats.
>>>>> 
>>>>> Usually you can simulate them in c as follows:
>>>>> 
>>>>> float nondet_float(){
>>>>>     float x;
>>>>>     return x;
>>>>> }
>>>>> 
>>>>> float myFloat = nondet_float();
>>>>> 
>>>>> Such that tools like CBMC will handle such variables as non-det floats, which are assumed to be every possible value.
>>>>> 
>>>>> Is that behavior somehow possible in Clang Static Analyzer?
>>>>> Or is it generally impossible for Static code analyzers to do such things?
>>>>> 
>>>>> Regards,
>>>>> Julian
>>>>> _______________________________________________
>>>>> cfe-dev mailing list
>>>>> cfe-dev at lists.llvm.org
>>>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20171002/de9beb4f/attachment.html>