blob: 290781295615b5d6a668a6ed6cfad879802fbdaa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
+++
title = "Adding a new CompCert pass"
date = "2020-12-10"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a4"]
forwardlinks = ["3a4b"]
zettelid = "3a4a"
+++
The main stages that are necessary when adding a compiler pass in
CompCert are the following:
- Specify the operational semantics and syntax of the language.
- Create the specification of the translation algorithm.
- Create the algorithm that corresponds to the specification.
- Prove that the algorithm implements the specification.
- Prove that the specification retains the behaviour of the program
according to the operational semantics of the original language and
the target language.
These steps are all necessary when specifying complex translations,
however, when proving a simple transformation, it may not always be
necessary to provide a specification of the translation algorithm.
Instead, it is simple enough, the algorithm itself can be used for the
proof.
|
