[cfe-dev] Get assumed value of function call in CSA

[Artem Dergachev via cfe-dev]

Most likely you're looking at an example of an "eagerly assume" 
behavior: the state split for the condition is performed immediately 
after operator `!=` in order to simplify further computations. The eager 
state split is well-justified because otherwise there's no reason to 
write the operator; it doesn't do anything except producing a comparison 
result, so the comparison result cannot be always the same.

Once the state split is performed, the value in the variable `ret` is 
either a concrete 1 or a concrete 0 (depending on the branch taken) and 
therefore the original symbol is no longer mentioned anywhere in the 
state and therefore it can be cleaned up.

You can catch the moment of cleanup in the checkDeadSymbols callback as 
usual. At this moment you still have constraints over the original 
return value symbol, and moreover, these constraints are *final*: the 
symbol will never be constrained any further, as it's getting cleaned up 
and will never appear again in the state. So at this point you can 
already make a decision about whether the return value was ever tested 
for errors, by looking at the current constraints for your symbol.

On 1/22/20 7:32 PM, Gábor Horváth wrote:
> Hi!
>
> Adding Artem as he already did some heroic work hunting down liveness 
> bugs.
>
> On Wed, Jan 22, 2020 at 6:38 AM Balázs Kéri via cfe-dev 
> <cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>> wrote:
>
>     void test() {
>       int ret = (function() != 0);
>       if (ret == 0) { }
>     }
>
>
>
> There are actually two possible scenarios that can happen for a code 
> like that.
>
> 1. We conjure a symbol for function, and build a symbolic expression 
> from the initialization expression and bind this symbolic expression 
> to ret. In this case the symbol returned by the function is still in 
> use, it will not be garbage collected.
> 2. We conjure a symbol for the function but for some reason we cannot 
> build a symbolic expression from the initialization expression (either 
> something is not representable using the current implementation, or we 
> explicitly chose not to represent the expression due to solver 
> limitations or performance tradeoffs). In this case we will conjure a 
> new symbol for ret and since we never ever mention the symbol returned 
> by the function anywhere it can be garbage collected.
>
> While this behavior might be annoying, given the current limitations 
> of the constraint solver, you might not be able to leverage the 
> information even if the symbol wasn't garbage collected in the first 
> place.  But in case you want to experiment a bit, you can always 
> subscribe to checkLiveSymbols callback and keep the symbols alive 
> artificially to see if you can get something useful out of them. For 
> the cases where you can we might want to change the behavior.
>
> Cheers,
> Gabor
>
>
>     _______________________________________________
>     cfe-dev mailing list
>     cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>
>     https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>