[analyzer] Question about ProgramState::assumeInBound

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

Basically https://bugs.llvm.org/show_bug.cgi?id=40145.

Oh, I see. Unfortunate :expressionless:
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 <noqnoqneo@gmail.com> ezt írta (időpont: 2020. márc. 25., Sze, 16:25):