source: etc/campbell/dev-notes/2012-10-31-clight-to-cminor.txt @ 2472

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

Misc clight->cminor notes.

File size: 2.9 KB
1[There were a few notes in 2012-10-18-front-end-correctness.txt too.]
3Variable mapping
6The stage has a mapping var_types that tells us where each variable should live,
7either as a global (in both Clight and Cminor), at a particular position on the
8stack or as a local variable in the environment (both in Cminor, in Clight they
9are an entry in the environment which gives a memory block for that variable).
11There are some properties of that mapping that should hold:
13- globals are present in the global environment and not the local environment
14  (local variables may shadow globals)
15- positions on the stack should be unique
17We can restrict the valid environments and memories according to this mapping.
18Rereading the CompCert mm paper, remember that values need to be mapped
19according to the memory mapping too (I previous wrote the variable mapping,
20but that doesn't provide the memory block mapping), extend the embedding on
21function calls, and ensure that we only provide mappings for used blocks.
23Object sizes
26I don't think we do any checks for excessively large objects and we *might*
27get into trouble here due to overflow.  I'm not entirely sure about that though,
28because signed and unsigned addition are the same with two's complement.  Even
29with excessively sized arrays I think we end up squashing the offset in the
30Clight pointer arithmetic.
32Fitting this in with the memory model changes might be more difficult (because
33we might wrap to the start of the stack frame rather than the array).  Adding a
34check that the stack size returned by characterise_vars fits in memory might
35suffice.  Note that we'd still end up checking the stack frame size later in the
36compilation chain, though, as the frames become larger due to spilling.
40Variable characterisation (globals not in local env, stack/var are, stack
41│                          allocations disjoint)
43├→ Memory mapping (needs to update mapping on fn entry for new environment,
44│  │               provide equivalent memory on exit; determines value mapping)
45│  │
46├──┼→ Expression correctness
47│  │   │                         temporary variables (Local only; not in memory)
48│  │   ↓                          extends env on the fly - may have to assume   
49└──┴→ Statement correctness    ←  some overapproximation in simulation         
50       │ (need to carry some knowledge about break/continue destinations in
51       │  simulation)
52       │
53       └→ Program correctness
55More stuff:
56- On function entry we store parameters that have stack allocated to them - so
57  calls will have to do several steps to get back to the simulation relation
58- The simulation relation will need to relate the continuations for loops in
59  Clight with a list of facts about where the entry/exit labels in Cminor go,
60  as there is no corresponding information in Cminor continuations/stacks.
Note: See TracBrowser for help on using the repository browser.