A constraint solver and its application to machine code test generation

© 2012 Dr. Trevor Alexander HansenSoftware defects are a curse, they are so difficult to find that most software is declared finished, only later to have defects discovered. Ideally, software tools would find most, or all of those defects for us. Bit-vector and array reasoning is important to the software testing and verification tools which aim to find those defects. The bulk of this dissertation investigates how to build a faster bit-vector and array solver. The usefulness of a bit-vector and array solver depends chiefly on it being correct and efficient. Our work is practical, mostly we evaluate different simplifications that make problems easier to solve. In particular, we perform a bit-vector simplification phase that we call “theory-level bit-propagation” which propagates information throughout the problem. We describe how we tested parts of this simplification to show it is correct. We compare three approaches to solving array problems. Surprisingly, on the problems we chose, we show that the simplest approach, a reduction from arrays and bit-vectors to arrays, has the best performance. In the second part of this dissertation we study the symbolic execution of compiled software (binaries). We use the solver that we have built to perform symbolic execution of binaries. Symbolic execution is a program analysis technique that builds up expressions that describe all the possible states of a program in terms of its inputs. Symbolic execution suffers from the “path explosion”, where the number of paths through a program grows tremendously large, making analysis impractical. We show an effective approach for addressing this problem