An Architecture Supporting Formal and Compositional Binary Analysis