Compiler validation via program verification

摘要

To overcome the difficulties inherent in traditional compiler validating methods, a new technique is herein provided for validating compiler output via program verification. In one embodiment, this technique is implemented as an automated tool that merges both a source program and the compiler-generated target program into a single (intermediate) program. An automated program verifier is then applied to the merged program. Subsequently, the program verifier compares the source and target programs and determines if the programs are semantically equivalent.

主权项

1. A method for verifying a compiler comprising:
receiving a plurality of programs, the plurality of programs comprising at least a source program and a target program corresponding to the source program; receiving a plurality of compiler-generated hints corresponding to the source program; converting the source program into an intermediate representation of the source program; converting the target program into an intermediate representation of the target program, the converting the source program and the converting the target program including performing a semantic translation and a syntactic translation on the source program and the target program to cause the intermediate representation of the source program and the intermediate representation of the target program to have matching semantics; merging the intermediate representation of the source program and the intermediate representation of the target program into a single merged program by merging one or more procedures in the intermediate representation of the source program with one or more corresponding procedures in the intermediate representation of the target program to form one or more single procedures in the single merged program; and validating the merged program.