[analyzer] Do we have implicit assumptions on extents of memory regions?

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

[analyzer] Do we have implicit assumptions on extents of memory regions?

David Chisnall via cfe-dev
Is it reasonable to assume in the analyzer that a symbol representing the extent
of an analyzed memory region can not be greater then size_t_max/2?

If so, why does the constraint manager not know about this fact?
If not, why does the `ProgramState::assumeInBound` still heavily exploit this
fact in its implementation?

Without deciding this Z3 refutation will not be able to filter as many false
positives as it potentially could.

Regards,
Balazs

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

Re: [analyzer] Do we have implicit assumptions on extents of memory regions?

David Chisnall via cfe-dev


On 7/6/20 8:53 AM, Bal√°zs Benics via cfe-dev wrote:
Is it reasonable to assume in the analyzer that a symbol representing the extent
of an analyzed memory region can not be greater then size_t_max/2?

I think it's pretty reasonable. Otherwise ssize_t won't work. In fact, neither can it be equal to SIZE_MAX/2, for the same reason. The actual limits are probably smaller, e.g. Clang won't let you declare a fixed-length array larger than a certain size that's much smaller than SIZE_MAX/2 (even if you are willing to find a computer that has that much RAM).

If so, why does the constraint manager not know about this fact?

It's not up to the constraint manager to decide whether or not a specific symbol represents an extent. SymbolExtent obviously does represent an extent, so i guess it'll be reasonable to hardcode that. The opposite is not true though; say, the extent of heap-based symbolic region allocated by `malloc(x)` is the completely arbitrary symbol `$x` (it can even be a concrete value).

So instead of making the constraint manager make such guesses i'd much rather have the entities responsible for allocation (MallocChecker, ExprEngine for operator new/new[] and VLAs, etc.) *actively* tell the constraint manager that these symbols may only have limited range (it doesn't need to know that this is because of them being an extent of something, it only needs the raw facts) by explicitly adding the respective constraints via assume(). IteratorChecker already does that for iterator position / difference symbols and i think that's the right thing to do. Now it's entirely up to the constraint solver to take these hints into account.

If not, why does the `ProgramState::assumeInBound` still heavily exploit this
fact in its implementation?

Without deciding this Z3 refutation will not be able to filter as many false
positives as it potentially could.

Regards,
Balazs

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


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