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

[Julian Löffler via cfe-dev]

Hi George,


How is the z3 mode enabled tho?
If I download the latest release binaries: 
http://releases.llvm.org/download.html#5.0.0

and run e.g :
clang-5.0 -cc1 -w -analyze -DANALYZER_CM_Z3 -analyzer-constraints=z3 
-analyzer-checker=core,debug.ExprInspection

I'll get an error:
fatal error: error in backend: Clang was not compiled with Z3 support!


Kind regards,
Julian



On 03/10/2017 00:21, George Karpenkov wrote:
> (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 .
>
> 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 
>> <mailto: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 
>>>> <mailto: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 <mailto: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 <mailto: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/20171004/155c3295/attachment.html>