This research is funded in part by DARPA as part of the MUSE program (contract #FA8750-15-2-0009) and by NSF Award New Frontiers in Constraint-Based Program Analysis.