In DSE, some inputs to the program under test are made symbolic while the rest are fixed. Starting with an initial concrete assignment to the symbolic inputs, the DSE engine executes the program both concretely and symbolically and maintains a symbolic state that maps program variables to expressions over the symbolic inputs. Whenever the symbolic execution encounters a conditional opera- tion, the symbolic state’s evaluation of the condition or its negation are added to the path condition , depending on the concrete result of the operation. Once the execution finishes, the path condition uniquely characterizes the executed control flow path. By negating the last constraint of the path condition or of one of its prefixes, the DSE engine generates a constraint for a different path. It then calls a constraint solver to check feasibility of that path and to obtain a satisfying assignment for the symbolic input variables that drives the next execution down that path.
© Blake Loring 2018