[cfe-dev] Path constraints at function call in checker

[Devin Coughlin via cfe-dev]

> On Apr 11, 2016, at 4:23 PM, Jonathan Foote via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hello,
> 
> Is there a simple way to enumerate all of the constrained symbolic values (and constraints) required to reach a function call (where the call is outside the current translation unit) via symbolic execution in a Clang checker? For example, I'd like to get information about x, y and z at in this case:
> 
> ```
> int x = read();
> int y = read();
> int z = read();
> if (x > 1 && y > 2 && z > 3) {
>   foo(x);
> }
> ```
> 
> The desired information would be something roughly analogous to { (x,  [2, 2147483647]), (y,  [3, 2147483647]), (z, [4, 2147483647]) }. I've tried a few different methods to elicit this information in the PreCall and PostCall hooks, but it seems that the ConstraintManager only is tracking constraints on the arguments to `foo`. 

I think the issue here is that ‘y’ and ‘z’ are dead at the call to foo(). The analyzer is very aggressive about removing “dead” symbols that are no longer reachable. Because y and z are not read after the guard condition, the analyzer will remove both their bindings in the store and the constraints on the symbols they are bound to before the call to foo(). You should still be able to reconstruct the path condition by traversing the exploded node graph backward and looking for changes in constraints between a node and one if its immediate predecessors. There is code in BugReporterVisitors.cpp that already does something similar for the purpose of adding helpful path notes to diagnostics (TrackConstraintBRVisitor::VisitNode) — you may be able to adapt it for your needs.

Devin