PReach: A probabilistic reachability analyzer to identify hard to reach program statements

The research artifact we present here is PReach. PReach implements a heuristic for probabilistic reachability analysis to identify hard to reach program statements. Only other existing probabilistic reachability analysis tools that can be used for this purpose are probabilistic symbolic execution and statistical symbolic execution. Limitations of symbolic execution based techniques are: 1) they can not analyze behaviors of arbitrarily large program paths and 2) the cost of analysis increases exponentially with increasing execution depth, and 3) exponential increase in the number of paths combined with increasing sizes of path constraints can lead to double exponential blow up in the cost of analysis. PReach addresses these shortcomings by avoiding path explosion issue and reducing the cost of path constraints solving. \tool can also model behavior of arbitrarily large program paths and the cost of analysis increases polynomially with the size of program, not exponential to the execution depth. PReach approximates the reachability probability of a given program statement using 1) branch selectivity which it computes using model counting, 2) dependency analysis, which it uses to identify input-dependent branch conditions that influence statement reachability, 3) abstract interpretation, which it uses to identify the set of values that reach a branch condition, and 4) a discrete-time Markov chain model, which it constructs to capture the control flow structure of the program together with the selectivity of each branch. PReach can identify hard to reach statements with high precision and accuracy in benchmarks from software verification and testing competitions, Apache Commons Lang, and the DARPA STAC program. PReach achieves comparable precision and accuracy for bounded execution depth and better precision and accuracy when execution depth is unbounded and the number of program paths grows exponentially. Moreover, PReach is more scalable than both probabilistic and statistical symbolic execution