Knowledge compilation is emerging as an effective tool for scaling exact inference to complex probabilistic programs. The essence of knowledge compilation is to encode a probabilistic program as a compact data structure, such as a binary decision diagram. This inference strategy strongly resembles symbolic execution. In parallel work, we have used this observation to repurpose the symbolic executor Rosette to perform probabilistic inference. Here, we aim to develop the mathematical foundation for this adaptation of Rosette and expand its applications beyond probability and non-determinism. The key insight is that both probabilistic choice and non-deterministic choice are (commutative) affine effects. We show that every affine effect gives rise to a denotational semantics for symbolic execution. This semantics is inspired by models of name generation and the sheaf-theoretic approach to the Giry monad. Our semantics is based on a category of worlds containing symbolic heaps. Types then denote world-dependent sets, and programs denote world-dependent functions. We show that this semantics is sound and complete in the sense of Torlak and Bodik: it captures all and only those outcomes that are reachable by computation using the original affine effect.