Get assumed value of function call in CSA

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

Get assumed value of function call in CSA

Hans Wennborg via cfe-dev
Hi!
I have a checker that stores the SymbolRef of a function call (return value). Later the checker makes assumption on this value. If the value was constrained by branch conditions these assumptions should fail in some cases (if the condition is the opposite of the assumption). The problem is if the return value is assigned to a variable the original symbol value is lost (garbage collected).

An example code:

void test() {
  int ret = (function() != 0);
  if (ret == 0) { }
}

It looks like that the analyzer decides about the value of 'function() != 0' at the time of the 'ret = (function() != 0);' statement. Then the value of the function call is lost from the state. The checker needs to test if it is possible for the 'function()' to be zero or nonzero (by making assumption on the function's return value) but the value is not in the state so any assume will succeed. Is it possible to prevent the value of 'function' from garbage collection? Or is there some way in the checker to find the assumed value of the function call? (The state graph shows a state where the needed value is available but I found that no checker callback is called in that phase.)

Balázs


_______________________________________________
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: Get assumed value of function call in CSA

Hans Wennborg via cfe-dev
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 <[hidden email]> 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
[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: Get assumed value of function call in CSA

Hans Wennborg 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
> <[hidden email] <mailto:[hidden email]>> 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
>     [hidden email] <mailto:[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