[cfe-dev] evaluating a LAnd expr in the static checker

[Artem Dergachev via cfe-dev]

Hello Devin,

I think your explanation is great, and that's what i thought when i 
first stepped on this constraint myself. But i also think that we could 
provide some useful features and improve user experience here.

I mean, it might be possible that the user (checker author) has a couple 
of SVal's and wants to conduct a "mathematical" logical-and/or on them, 
and doesn't care that in some programming languages (even if it's all 
the languages we support) there's a short-circuit rule. And we can 
support the user - constant-fold the resulting value if it 
constant-folds, perhaps construct a symbolic expression if it doesn't, 
wait until this expression gets alpha-renamed to something more sensible 
(when things start getting alpha-renamed). Probably, if the user 
constructs an LAnd (unlike LOr), and pass it into assume(), we could 
perform two sequential assumes under the hood. We just need to make sure 
we don't do that in ExprEngine.

We may change the name for the operation to make the distinction more 
clear and warn the user that what he's doing is different from his 
normal LAnd/LOr expression (in fact, we could provide a separate enum 
for operation kinds, instead of re-using the BO_*, and that'd 
demonstrate explicitly what operations we do support and how operations 
on symbols are different from AST expressions).

In fact, i've got a few more ideas about custom operations, eg. 
"bignum-arithmetic-less-than" (so that assumption "$x + 1 <= $x" 
resulted in a null state without overflows, but $x still mapped into a 
sensible integral type in the AST context) - sounds pretty questionable, 
but such things make vague sense when i try to imagine how summary-ipa 
might be automated with ghost-variable-based mutex-stacks from pthread 
lock checker (there's no problem to work around lack of such operations, 
but it might be a lines-of-code-saving feature).