[cfe-dev] Non Deterministic floats in clang static analyzer.
George Karpenkov via cfe-dev
cfe-dev at lists.llvm.org
Wed Oct 4 12:32:22 PDT 2017
In any case, the float modeling present in a patch seems quite incomplete.
> On Oct 4, 2017, at 12:31 PM, George Karpenkov <ekarpenkov at apple.com> wrote:
>
> 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 <mailto: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/6a2e438a/attachment.html>
More information about the cfe-dev
mailing list