Non Deterministic floats in clang static analyzer.

classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
The analyzer tries to report use of uninitialized variables as soon as
he sees it, regardless of its type (float or int or string) or possible
consequences (whether it is possible to trigger various paths in the
program by producing particular sorts of garbage in the memory).

For example, your code produces a warning immediately:

   $ clang --analyze test.c
   test.c:4:13: warning: Undefined or garbage value returned to caller
             return x;
             ^~~~~~~~
   1 warning generated.

...because the analyzer believes that it makes no sense whatsoever to
make a function that returns an unitialized variable. Similarly, passing
an uninitialized value as an argument to any function (unless the
parameter is for writing) or performing arithmetic on an uninitialized
value makes little sense.

On the other hand, for user inputs the analyzer can (as a feature that's
currently experimental) conduct taint analysis: numeric symbols obtained
directly from the user are represented as tainted symbols that can
definitely take any possible value. For security applications, it'd
probably be better to treat undefined values as tainted symbols, however
for routine bug-finding the current behavior makes more sense to the
users and is easier to understand.

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 .

On 9/16/17 5:07 PM, Julian Löffler via cfe-dev 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
> [hidden email]
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
In reply to this post by Eric Fiselier via cfe-dev
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 <[hidden email]> 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
> [hidden email]
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
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.

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


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 <[hidden email]> 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
>> [hidden email]
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
In reply to this post by Eric Fiselier via cfe-dev
Hi Julian,

Sorry for interfering, if you need a brief description of how the clang static
analyzer performs a symbolic execution of the program, try this:
https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/README.txt

If you want to go into some details, there is an awesome clang static analyzer guide
written by Artem Dergachev: https://github.com/haoNoQ/clang-analyzer-guide

Best Regards,
Kirill

> Message: 4
> Date: Tue, 19 Sep 2017 12:43:33 +0200
> From: Julian Löffler via cfe-dev <[hidden email]>
> To: George Karpenkov <[hidden email]>
> Cc: [hidden email]
> Subject: Re: [cfe-dev] Non Deterministic floats in clang static
>         analyzer.
> Message-ID:
>         <[hidden email]>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> 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.
>
> 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^^
>
> 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 <[hidden email]> 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
>>>  [hidden email]
>>>  http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> cfe-dev mailing list
> [hidden email]
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
> ------------------------------
>
> End of cfe-dev Digest, Vol 123, Issue 61
> ****************************************
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
In reply to this post by Eric Fiselier via cfe-dev
Hi Julian,

> On Sep 19, 2017, at 3:43 AM, Julian Löffler <[hidden email]> 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 <[hidden email]> 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
>>> [hidden email]
>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier 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 .

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

George

On Sep 25, 2017, at 8:50 AM, Julian Löffler <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev




_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
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 <[hidden email]> 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

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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev





_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Non Deterministic floats in clang static analyzer.

Eric Fiselier via cfe-dev
In any case, the float modeling present in a patch seems quite incomplete.

On Oct 4, 2017, at 12:31 PM, George Karpenkov <[hidden email]> 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 <[hidden email]> 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

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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev






_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev