Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis