Pex - Automated Whitebox Testing for .NET : Input Generation

Input Generation By Dynamic Symbolic Execution

Pex generates inputs for parameterized unit tests by analyzing the branch conditions in the program. Test inputs are chosen based on whether they can trigger new branching behaviors of the program. The analysis is an incremental process. It refines a predicate q: I -> {true, false} over the formal test input parameters I. q represents the set of behaviors which Pex has already observed. Initially, q := false, since nothing has been observed yet.

The steps of the loop:
  1. Pex determines inputs i such that q(i)=false using a constraint solver. By construction, the input i will take an execution path that we have not seen before. (And initially, this means i can by any input since we haven't seen any execution path yet.)
  2. Pex executes the test with the chosen input i, and monitors the execution of the test and the program-under-test takes.
  3. During the execution, the program takes a particular path which is determined by all the conditional branches of the program. The set of all conditions that determine the execution is called the path condition, written as the predicate p: I -> {true, false} over the formal input parameters. Pex computes a representation of this predicate.
  4. Set q := (q or p), i.e. we record that we have now seen the path represented by p.
  5. Go to 1.

Pex' constraint solver can deal with values of all types that may appear in .Net programs:

Pex filters out those inputs which violate stated assumptions.

Besides the immediate inputs (arguments to parameterized unit tests), a test can draw further input values from the PexChoose static class. The choices also determines the behavior of parameterized mocks.
(c) Microsoft Corporation. All rights reserved. pex Wiki Documentation 0.93.50813.0