Compositional Dynamic Test Generation
- DART
- M: mapping from memory address to words
- Identify symbolic variables by their addresses
- Execute the program P for each possible input vector I, Execs(P) forms an execution tree, and explore all paths in the tree
- SMART (assumes no recursions or unbounded loops)
- Summaries: disjunction of conjunctions of input and output constraints
- Top-down search algorithm
- Execute the program until reaches the first function f, whose execution terminates on a “halt”
- Back track inside f, computing summary
- Resume to where f is called, treating f as a blackbox
- Summary for f includes the summaries of lower-level functions called by f
Demand-Driven CSE
- Check whether a combination of currently-known fully-explored intraprocedual paths are sufficient to generate a new test input covering the target node
- Algorithm
- Start with empty set of intraprocedual execution trees
- Execute the program, new nodes and edges with constraint labels are added to the trees, place holders for dangling nodes
- Choose a dangling node as the next target to be covered
- Interprocedual path constraints: disjunction of path constraints of all interprocedual paths to target n, by joining all intraprocedual paths
Compositional Symbolic Execution Using Fine-Grained Summaries
- Records the precondition and post condition of the path, and on subsequent calls that satisfy that precondition, the corresponding post condition can be returned instead of executing the function again
- Fine-grained: blocks within functions are summarized
- Goal: eliminate redundant constraint solving
- Storing the summaries of each PATH during the actual execution
Details:
- Each forward step contains two operations: version number updating and concatenation
- Uses backward reasoning (we can possibly do it with forward reasoning)
3 strategies of choosing good summarization targets: