Symbolic Execution Based Automatic Performance Optimization for MPI Programs