[analyzer] constructing svals

I’m having some trouble understanding exactly under what circumstances I can construct a “known” sval for various expressions.

Here’s a concrete example that I ran into and was surprised about:

int f(float x){
return (int)x;
}

int main(int argc, char** argv){
int x = -1;
f(x);
return 0;
}

I then created a checker that registered for the PreCall check. When checkPreCall was invoked, Call.getArgSVal(0) is unknown, which makes sense to me because the system doesn’t reason about floating-point, however, I was surprised that this also results in an unknown value (regardless of it’s overall sensibility):

C.getState()->getSVal(dyn_cast(Call.getArgExpr(0)->getSubExpr()))

Indeed, if I change the definition of f so that it becomes:

int f(int x){
return x;
}

Then Call.getArgSVal(0) is known and insofar as I can tell should be equivalent to the above in the earlier context. I’d be interested to understand why that’s not the case and in general what expressions can be converted to usable svals during the check calls.

Thanks!

-Mike

Hi, Michael. The analyzer tracks the values of expressions in a map from Expr* (actually Stmt*) to SVal called the Environment, which is part of the ProgramState. In order to keep the Environment small, expressions that have already been evaluated are cleared out of the current state at certain points in the program. That means you can’t rely on being able to get the value of anything other than your immediate subexpressions.

The next logical step is to try to move backwards through the ExplodedGraph until you find a node that still references the expression you want to look at. However, that’s not guaranteed to be present, either: ExplodedNodes are trimmed out of the graph unless they are “interesting” in some way (for example, they have been generated by a checker and may be referenced in a bug report later). So you can’t rely on any node still referencing the value of a particular expression several steps down the line—only immediate subexpressions.

Is there anything in particular you’re trying to do here, or was it just experimentation that didn’t pan out?

Jordan

Jordan,

Thanks, I really appreciate the reply. Based on the above example it definitely appeared as though only immediate subexpressions were available, but obviously that wasn’t what I had expected and so it’s nice to have confirmation that it’s generally the case.

This was more or less experimentation that didn’t pan out. I’m still familiarizing myself with the engine and its capabilities and so when I ran into this I wasn’t sure if I was doing something wrong or that’s how it was meant to be. Originally, I had assumed that when more or less in the same context, I would be able to successfully evaluate the same set of expressions.

-Mike