[analyzer] Question about ProgramState::assumeInBound

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

[analyzer] Question about ProgramState::assumeInBound

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

Re: [analyzer] Question about ProgramState::assumeInBound

suyash singh via cfe-dev
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
> [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
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer] Question about ProgramState::assumeInBound

suyash singh via cfe-dev
Oh, I see. Unfortunate :|
You probably remember our previous conversation ([analyzer] Constrain the size of unknown memory) 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 <[hidden email]> 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
> [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