Get assumed value of function call in CSA

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

Hi!

Adding Artem as he already did some heroic work hunting down liveness bugs.

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

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.