[cfe-dev] How to generate constraints on input to reach a specific program statement/location in execution?

[James Huang via cfe-dev]

Hi,

I'd like to generate the constraints on input to a program that can
cause the execution of the program to reach a certain
statement/location. For this purpose, I'm interested in developing a
checker using the symbolic execution provided by clang's static
analyzer. Looking through the static analyzer's documentation, my
initial thought was to retrieve the constraints for each conditional
branch statement (e.g. if, for, while, switch) along the execution
path. However, there are a few challenges.

1) Does the static analyzer keep track of constraints for each
variables? If so, how to retrieve the constraints for a specific
variable? The documentation mentions a generic data map associated
with a program state, but it seems that it is the responsibility of
the developer of a checker to maintain it.

2) How to retrieve information on the source location of a statement
without generating a bug report? We need to know how a statement is
control dependent on a conditional branch statement. For example,
whether a statement belongs to the then block or else block of a if
statement. We find that the IfStmt class has information on the range
of source locations of its then block and else block, which can be
used to answer this question. But the source locations seems to be
available only through a SourceManager class that can be used only
when generating a bug report?

3) How to get information on a conditional branch statement before its
execution? The static analyzer doesn't allow pre-processing call back
to any control flow transfer statement, but provides a
checkConditionalBranch call back for conditional branch statement.
However, it only provides the condition used in the branch statement
instead of the branch statement itself.

Thanks.