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

[Alexey Sidorin via cfe-dev]

Hello James,

1. Analyzer deals with constraint with using some constraint manager. 
The only current implementation of ConstraintManager - 
RangeConstraintManager class - keeps the constraints in a special trait 
in GDM named ConstraintRange. You can take a look at 
RangeConstraintManager.cpp file for more details. These constraints are 
represented as a set of integer ranges that value can have on some 
execution branch. Not all constraints can be resolved with this manager 
because it is simple enough. You should note that analyzer does not 
constraint the variable itself (which is just a piece of memory - 
MemRegion); it constraints its value if it is represented as a symbol. 
To retrieve the constraint on some symbol, you possibly should add a 
corresponding function to constraint manager. You may try this approach.

Also note that analyzer remembers all options on the path it follows. 
You may also use this to generate constraints with walking through the 
generated ExplodedGraph.

2. For each statement you can retrieve its location with 
getLocStart/getLocEnd/getSourceRange methods.


19.10.2016 23:58, 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.
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev