EVM AOT编译器翻译验证方法、装置及计算机设备

本申请涉及一种EVM AOT编译器翻译验证方法、装置及计算机设备，获取对EVM字节码进行语义保持的前端规范化处理得到的与EVM字节码在可观察语义范围内等价的源程序；获取对EVM字节码编译得到目标机器码作为目标程序；分别将源程序和目标程序在任意满足预设约束的输入状态下的可观察行为，通过符号化建模表示为对齐的逻辑语义表示，得到源侧逻辑语义表示和目标侧逻辑语义表示，并判断二者是否存在可观察行为差异；基于对应的判断结果确定验证结论，验证结论表征EVM字节码与对应的目标机器码在预设约束和可观察语义范围内是否等价，实现程序级语义等价性验证，验证对象覆盖所有符号输入，能够对编译结果给出更可靠的正确性结论。