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: