source: etc/campbell/dev-notes/2011-09-23-runtime.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: 2.2 KB
1The prototype compiler adds some runtime functions at the Clight level to
2implement operations that the target does not support, e.g. 32 bit arithmetic.
3It also replaces these operations (breaking down some of the expressions into
4multiple statements in the process because function calls are not permitted in
5Clight code).
7The reason for performing this so early in the compiler is that the cost
8labels for these functions must appear in the source so that they are visible
9throughout the compilation chain.  Moreover, the operations are replaced early
10because the trace of costs must be preserved throughout.  This ruins my idea
11of merely performing the substitution at a point that is more convenient
12(e.g., RTL/RTLabs).
14So there are a few possibilities that come to mind:
16 1. follow the prototype, writing a nasty expression splitting function to
17    deal with the substitution,
19 2. extend the Clight semantics to produce extra cost labels for the affected
20    operations and perform the substitution whenever I like, or
22 3. change the Clight semantics to execute the runtime function instead of the
23    operation (nasty - we don't check that the substituted function works
24    properly).
26Some other considerations are:
28 a. We have to prove that the substitution works at some point (unless we use
29    the underhanded option 3).
31 b. Some of the replacements could be candidates for inlining (offhand I can't
32    remember if our labelling semantics works for inlining).
34 c. We somehow have to deal with showing that our labelling is complete.  I
35    don't know how that will work yet, but the substitutions might make that
36    more difficult.
38 d. The 8051 is really crap: it can only do single bit shifts/rotations.
39    Implementing multi-bit shifts is difficult at Clight, because there's no
40    easy way to leave single bit shifts in place without changing the
41    intermediate languages, and no way to spot that a shift is constant by RTL
42    without doing a non-local analysis.
45On an aside, I wasn't sure why the prototype calls the cast simplification
46twice.  It's because the runtime functions are written in C, not Clight, so
47the operands get promoted back to int and have to be simplified down again...
Note: See TracBrowser for help on using the repository browser.