Semantic Equivalence Checking for HHVM Bytecode
Nick Benton · 2018
We describe a semantic differencing tool used to compare the byte-codes generated by two different compilers for Hack/PHP at Facebook. The tool is a prover for a simple relational Hoare logic for low-level code and is used in testing, allowing the developers to focus on semantically significant differences between the outputs of the two compilers.