source: etc/campbell/dev-notes/2012-05-10-globalenvs-transformations.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 3.0 KB
Line 
1Global environments and program transformations.
2
3The current form of global environments is partially ported from CompCert:  it
4consists of a record of types and operations to provide the abstraction that
5CompCert gets from modules, and an implementation that was a slightly hacky
6but straightforward instantiation of the record.  This is unusual for CerCo
7because we normally don't use much abstraction (Matita isn't very good at it),
8and we don't have any other implementations to worry about.
9
10The lemmas were left out, partly because we didn't want to prove them straight
11away, and partly because Matita choked on the large record definition.
12Moreover, we have since changed the definition of the program record so that
13many of the statements that were ported would need updated.
14
15Now we're starting to prove things about the transformations in the compiler
16we need to show some facts about the resulting global environments.  The
17CompCert code we started from has several generic transformations:
18
19  1. transform_program, which applies a function uniformly to all the source
20     program's function definitions;
21  2. transform_partial_program, which is the same except that the
22     transformation can fail using the error monad;
23  3. transform_partial_program2, which also applies a second function to the
24     program's variables; and
25  3'.the match' predicate, which provides a relational version of
26     transform_partial_program2.
27
28Our code uses:
29
30labelling           - transform_program
31cast simplification - transform_program
32[add runtime        - direct]
33Clight to Cminor    - direct, was transform_partial_program2, try again?
34Cminor init         - direct
35Cminor to RTLabs    - transform_partial_program
36
37Back-end; not sure how final these are.  Worse, there appears to be a separate
38version of the global environments for the back-end.
39RTLabs to RTL       - transform_program
40RTL to ERTL         - transform_program
41ERTL to LTL         - transform_program
42LTL to LIN          - transform_program
43LIN to ASM          - direct
44
45
46The proofs accompanying functions in the Clight to Cminor stage are a bit of a
47problem.  They assert that the universe for temporary generation is fresh for
48the fundef.  [One way to deal with this is to generate the universe for each
49function.  This should be fine because the variables are local to each
50function.  I held off from doing this before because of the prospect of doing
51runtime function generation, but as that should be moving to the middle of the
52compiler it isn't an issue.  Actually, no - it makes proving the lack of
53clashes harder, because while it's fine for the generated Cminor, the property
54we need to show on the characterisation of variables is subtler.]
55
56---
57
58Note that the order of variables and functions in the program matter:
59duplicates will be tolerated, and reorderings will change the pointers
60‘allocated’ to each symbol.
61
62The dependence of the back-end function types on the program variables
63complicates the transformation functions:  the type of the function
64transformation function is specialised to the list of global variables.
Note: See TracBrowser for help on using the repository browser.