[cfe-dev] [analyzer] Question about ProgramState::assumeInBound

[Balázs Benics via cfe-dev]

Oh, I see. Unfortunate :|
You probably remember our previous conversation ([analyzer] Constrain the
size of unknown memory
<http://lists.llvm.org/pipermail/cfe-dev/2020-March/064881.html>) where you
proposed to use assert with the `clang_analyzer_getExtent` to make
constraints on the size of the allocated memory region.

> ANALYZER_ASSERT(ANALYZER_EXTENT(buff) == size);
>
>

According to the Bugzilla tickets you linked, this is the limitation of our
constraint solver.
Even though the constraint solver has its limitations, we are not planning
to improve it, since that would be like a reimplementation of a SAT solver.
But we won't use Z3 as a constraint solver either, because that would be
really really slow. (AFAIK Z3 is only used for refutation if enabled)

It seems to be a dead-end to me, regarding that without Z3 like solver we
are not strong enough, and with it unbelievably slow.
If a general solution would be too complex, should we consider handling
only the easy cases as I mentioned?


Artem Dergachev <noqnoqneo at gmail.com> ezt írta (időpont: 2020. márc. 25.,
Sze, 16:25):

> Basically https://bugs.llvm.org/show_bug.cgi?id=40145.
>
> On 3/25/20 4:20 PM, Balázs Benics via cfe-dev wrote:
> > Why cannot prove analyzer that only the true case is feasible for the
> > following example?
> > ```
> > ProgramStateRef StInBound  = state->assumeInBound(Idx, Size, true);
> > ProgramStateRef StOutBound = state->assumeInBound(Idx, Size, false);
> > ```
> >
> > Given that we know:
> > SVals:
> >   Idx.dump():  (conj_$8{int, LC1, S2294, #1}) - 1U
> >   Size.dump(): extent_$5{SymRegion{reg_$4<char * dst>}}
> >
> > Range constraints according to the exploded graph nodes:
> > extent_$5{SymRegion{reg_$4<char * dst>}}  {[10,18446...]}
> >   conj_$8{int, LC1, S2294, #1}              {[1,9]}
> >
> > Does the `Idx < Size` hold for all possible values of `Idx` and `Size`?
> > IMO yes, since [0-8] < [10,18446...], but the analyzer returns
> > _non-null_ states for both of the `assumeInBound` calls, but why?
> >
> > Balazs
> >
> > _______________________________________________
> > cfe-dev mailing list
> > cfe-dev at lists.llvm.org
> > https://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/20200325/e11e2d34/attachment.html>