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

[Anna Zaks via cfe-dev]

> On Oct 19, 2016, at 1:58 PM, James Huang via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> 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.

The constrains are being kept, but as others have mentioned, they are mainly used to rule out unreachable paths and querying if certain conditions hold. We only keep constrains that can be expressed as integer values over a single symbol. Furthermore, we aggressively prune the nodes as well as constrains and you would need to experiment with turning off that optimization.

> 
> 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?

Each node should have a ProgramPoint, which could be wrapping a statement or an expression, which in turn have the location information. You can look at the code that generates the bug reports given error nodes.

> 
> 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.

One way of approaching this would be to reach the node for which you’d like to generate the information and walk the path of the ExploadedGraph up, collecting the constraints along the way.

> 
> Thanks.
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev