Software systems change on a continuous basis, with each patch prone to introducing new errors and security vulnerabilities. While providing a full functional specification for the program is a notoriously difficult task, writing a \textit{patch specification} that describes the behaviour of the patched version in terms of the unpatched one (e.g.,``the post-patch version is a refactoring of the pre-patch one'') is often easy. To reason about such specifications, program analysers have to concomitantly analyse the pre- and post-patch software versions.

In this paper, we propose $\textrm{P}^\textrm{3}$, a framework for automated reasoning about \textit{p}atches via \textit{p}roduct \textit{p}rograms. While product programs have been used before, particularly in a security context, $\textrm{P}^\textrm{3}$ is the first framework that automatically constructs product programs for a real-world language (namely C), supports diverse and complex patches found in real software, and provides runtime support enabling techniques as varied as greybox fuzzing and symbolic execution to run unmodified.

Our experimental evaluation on a set of complex software patches from the challenging CoREBench suite shows that $\textrm{P}^\textrm{3}$ can successfully handle intricate code, inter-operate with the widely-used analysers AFL++ and KLEE, and enable reasoning over patch specifications.