[Bug analyzer/106386] New: Reuse libstdc++ assertions in -fanalyzer

[redi at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=106386

            Bug ID: 106386
           Summary: Reuse libstdc++ assertions in -fanalyzer
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: enhancement
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: redi at gcc dot gnu.org
            Blocks: 97110
  Target Milestone: ---

Libstdc++ uses a large number of assertions for checking preconditions, defined
as the __glibcxx_assert macro. This means that when -D_GLIBCXX_ASSERTIONS is
defined there are runtime checks for precondition violations like accessing the
10th element in a std::vector with fewer than 10 elements.

I wonder if it would be possible for the analyzer to reuse these assertions to
infer preconditions, and then flag when those preconditions might not be met.

So for example, std::vector::operator() looks like this:

      reference
      operator[](size_type __n) noexcept
      {
        __glibcxx_requires_subscript(__n);
        return *(this->_M_impl._M_start + __n);
      }

where that macro expands to __glibcxx_assert(__n < this->size()).

The analyzer could infer that this function is undefined unless __n < size(),
and then flag possible accesses where that isn't true. Finding those cases at
compile-time is better than getting assertions at run-time.

This would be a very general solution, and would avoid the need for hardcoding
specific knowledge of std::vector preconditions, std::optional preconditions
(PR 106385), std::unique_ptr preconditions etc. It would immediately leverage
hundreds of existing precondition checks. Explicitly teaching the analyzer
about all those individual preconditions would be a huge undertaking, just to
gain parity with what is already checked with run-time assertions.

The macro is currently empty when _GLIBCXX_ASSERTIONS is not defined, but maybe
it could expand to some special attribute that is still visible to the
analyzer, without actually adding the run-time assertion (N.B. this seems to
have a lot of overlap with C++ Contracts proposals, which will use attributes
to state preconditions on functions).


Referenced Bugs:

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=97110
[Bug 97110] [meta-bug] tracker bug for supporting C++ in -fanalyzer