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

Wed Oct 4 12:31:20 PDT 2017

Hi Julian,

I think you would need to recompile Clang+LLVM yourself to do that (it’s not very difficult, the documentation is pretty good).
Then you would need to make sure that CMake during the configuration pass can find Z3, there’s a corresponding variable you need to
set (I don’t remember which one though, but I think it would be trivial to find).

> On Oct 4, 2017, at 7:29 AM, Julian Löffler <loefflju at informatik.uni-freiburg.de> wrote:
> 
> 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 <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 <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 <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/d3e63e27/attachment.html>