source: etc/campbell/dev-notes/2011-09-06-light-to-minor-tmp.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: 1.4 KB
1I still need to do something about the temporary variable generation in the
2Clight to Cminor pass.  At the moment it is wrong in two ways:
4  1. the identifiers used could already be used in the program, and
5  2. only two "typ"s are covered, technically any appearence of the rest is
6     ill-typed (although the types aren't immediately checked, so it can
7     continue working for a bit).
9Some possible solutions for 1:
11  a. replace all the local variables with fresh identifiers, or
12  b. look at the set of identifiers in the program and pick fresh ones.
14and 2:
16  c. generate an identifier for each typ (there are a finite number of choices),
17  d. generate identifiers as required.
19d is preferable because it only generates variables that are used, and doesn't
20conflate different uses of temporaries.
22a would make identifying the original variable names more difficult when
23looking at the Cminor code, but we never generate errors involving variables
24in the Cminor to RTLabs stage anyway (and have shown this on the branch).  We
25already carry a map from Clight variables to the kind of storage, so could
26easily include a freshly allocated identifier in the map.  For b we could
27create the "universe" record for allocating new identifiers based on the set
28of identifiers in the program.
30[12th:] Fresh name generation could also be useful for adding Clight functions
31for arithmetic operations (i.e., implementing the Matita version of
Note: See TracBrowser for help on using the repository browser.