Non Deterministic floats in clang static analyzer.

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

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 .

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

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

Hi Julian,

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

(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

Hi George,

How is the z3 mode enabled tho?
If I download the latest release binaries: 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

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).

In any case, the float modeling present in a patch seems quite incomplete.