Compilers and Their Role in Software Analysis and Verification
Recall the big picture in Verification as Science. What is the role of the compiler?
Compiler is the closest relative of a program analysis and verification system: they both manipulate programs taking into account the meaning of statement constructs.
- they have same initial phases
Compiler front-end = program analyzer front-end:
- tokenization (lexical analysis)
- parsing (syntax analysis)
- creating abstract syntax trees
- resolving identifiers
- translation to intermediate form
Differences in goals:
- compiler generates executable object code
- analyzer answers questions about the source code
Natural way of integrating them:
- perform front-end operations
- ask analyzer: is program meaningful?
- try to optimize the code, ask analyzer: do conditions that enable optimization hold?
- perform code generation