blob: 284b63bfb38de47f0dcbb9dccb00b44db56ad5b4 (
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
28
29
|
+++
title = "Repeated application of a translation pass in CompCert"
date = "2022-10-04"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3i"]
forwardlinks = []
zettelid = "3c3i1"
+++
Currently it's true that if-conversion is quite tricky to prove, because
the recursive nature of the translation is quite complicated. However,
if one limits the translation to just modifying parts of the code in a
non-recursive way, then the proof becomes simpler. At every point one
only has to reason about two possibilities, either the current point has
been converted, meaning another block that exists in the graph has been
chosen and has been inlined, or the current block has not changed at
all.
Once one has defined a translation like that, one can just repeat it
multiple times with different rewrites to get any kind of
transformations one wants. To prove the correctness of the multiple
applications one should be able to prove that the `match_prog` property
holds for any reflexive and transitive closure. In addition to that, an
instance of the linker type class also needs to be implemented to show
that separate compilation is still supported as well, however that
should also just work because the `match_prog` property is very similar
to other `match_prog` properties.
|
